Chris Pollett>Old Classes>CS440, Fall 1997>Hw2

Homework #2 Due Oct. 1

Read Paulson 60-82 97-107, 123-149, 164-170, 340-356. Submit your code in a single file called:

hw2.sml

Make sure your code is well commented and make sure you leave blank lines between your functions so your code doesn't stress out the eyes of the grader. The pages 164-170 should make your life easier on problems 3 and 4.

1. Write ML for the functions on lists nth front(i, [x0, . . . , xk]) = xi and nthback(i, [x0,. . . , xk]) = xi_k. If i is too big use exceptions to give an error of form "uncaught exception integer argument too large"

2. Write a function string operating as follows. First, it prints "Please input a string to format." Then it receives input from the keyboard terminated by a carriage return. If this input is of the form of quotes followed by some text followed by quotes it just echoes that string, except \" is not considered a pair of end quotes and causes a pair of quotes to be printed in the output. If the string is not of the correct form it outputs a snide remark like "I don't like this string."

3. Write a datatype called prop for propositional formulas in the following way:

(a) Atoms are propositional formulas. By atoms we mean propositional variables which we represent as pairs where X is the first component of the pair and the second component of the pair is of datatype number defined as follows: the letter O is a number, if Y is a number then S(Y) is a number.

(b) If A, B are propositional formulas then so are NOT (A), AND(A, B), and OR(A, B).

4. A cedent is a list of formulas. A sequent is an ordered pair of cedents. Write a structure called Sequent which contains the following:

(a) a datatype s for sequents

(b) A function succedent(A, B) = B.

(c) A function antecedent(A, B) =A.

(d) A function valid([Al,. . . , An], [Bl,. . . Bn]) which returns either true or false depending on whether NOT(AND_i Ai) OR (OR_j Bj) is true under all truth assignments.