Assignment

Write and give output from TESTING for the following:

1. A list reversal function using the snoc list function can be written as follows:
   

   fun snoc a [] = [a]   |    snoc a (h :: t) = h :: snoc a t;  fun rev [] = []                                        |    rev [a] = [a]                               |    rev (h :: t) = snoc h (rev t);

   The complexity of rev is O(n²) for a list of length n because rev invokes snoc n times and snoc recurses approximately n times on a list of n elements. For example: snoc 4 [1,2,3] generates the following recursive calls:
   
   snoc 4 [1,2,3]     returns [1,2,3,4]
   snoc 4 [2,3]        returns [2,3,4]
   snoc 4 [3]           returns [3,4]
   snoc 4 []             returns [4]
   
   Then to reverse a list of 3 elements snoc is invoked on lists of length 3+2+1=6 times, length 4 on lists of 4+3+2+1=10 times, length 5 one lists of 5+4+3+2+1=15 time, length 100 of 5050 times, length 1000 of 500500 total recursions, etc. The number of recursions is then roughly approximated by n²/2 giving the order O(n²).
   
   We can do better. A reverse of O(n) for a list of length n is:

   fun helper (nil, a) = a                      |    helper(h::t, a) = helper(t, h::a);  fun rev L = helper(L, nil);  rev [1,2,3,4]; returns [4,3,2,1]

   The real work is done through the helper function by accumulating and eventually returning the result of h::a. To reverse a list of length n now requires only n recursions on the helper function. Some examples of the intermediate calls to helper: 

   helper ([ ], [3,2,1])         returns [3,2,1] the base case.
   helper ([1], [ ])               returns helper([ ], 1::[ ]) = helper( [ ], [1])
   helper([2,3], [1])            returns helper([3], 2::[1]) = helper( [3], [2,1])
                                                                           = helper( [], 3::[2,1])
                                                                           = helper( [], [3,2,1])
                                                                           = [3,2,1]
   
   
   Assignment 1

   Give a similar reverse function of O(n) for the definition of mylist:

   datatype 'el mylist = NIL | CONS of 'el * 'el mylist;           val c = CONS(1,CONS(2,CONS(3, NIL)));       rev c;            val it = CONS (3, CONS (2, CONS (1, NIL))) : int mylist;

         
2. Propositional Calculus is the foundation of symbolic logic, digital circuit design, and much of formal reasoning in artificial intelligence. It is a language in which we can represent and reason about properties and relationships in the world. The language is defined by:

Propositional Symbols            Truth Symbols            Connectives

P, Q, R, S, ....                                            T, F                            And, Or, Not, Eq, and Impl

Propositional symbols denote propositions or statements about the world that may be either true or false. Sentences in the propositional calculus are formed from these atomic symbols according to the following syntactical rules:

1. Every propositional symbol and truth symbol is a sentence. For example: T, P and Q are sentences.
2. The negation of a sentence is a sentence, for example: Not P and Not T are sentences.
3. The conjunction or And of two sentences is a sentence, for example Q And Not P.
4. The disjunction or Or of two sentences is a sentence, for example Q Or Not P.
5. The implication or Imp for another is a sentence, for example Q Imp P.
6. The equivalence or Eq of two sentences is a sentence, for example Q Eq Not P.

Legal sentences are also called well-formed formulas or WFF's. The symbols ( ) are used to group symbols into subexpressions and to control the order of evaluation. For example, (P Or Q) Eq R  is very different from P Or (Q Eq R).

Propositional Calculus Semantics or meaning of legal sentences. The interpretation or truth value for sentences is defined by the following truth tables:

P Not P T F F T

P  Q P And Q F F F F T F T F F T T T

P  Q P Or Q F F F F T T T F T T T T

P  Q P Eq Q F F T F T F T F F T T T

P  Q P Imp Q F F T F T T T F F T T T

Two sentences are equivalent if they have the same value under all truth value assignments. This equivalence may be demonstrated using truth tables . By demonstrating that they have identical truth tables, we prove that sentences are equivalent. For example, the following is a proof that P Imp Q and Not P Or Q are equivalent.

P  Q P Imp Q Not P Not P Or Q P Imp Q Eq Not P Or Q  F F T  T T T F T T T T T T F F F F T T T T F T T

ML representation of propositional calculus is relatively direct. The following is the definition of the truth symbols T, F and the conjunction or And.

datatype BOOL = T | F;

fun And (T, T) = T
|     And (_, _) = F;

And(T,F);
val it = F : BOOL

Infix operators of a given precedence can be defined in ML for functions. The following defines And as left-associate (greater integer values accord higher precedence). 

infix 4 And;

allowing more natural syntax of:

T And F;
val it = F : BOOL

A truth table for all combinations of true and false to exercise a binary BOOL function is:

fun TT2 f = [
                        f(F,F), 
                        f(F,T), 
                        f(T,F), 
                        f(T,T)  
                     ]; 

Testing - Because And has been defined as an infix function, the (op And) is required to pass in prefix form.

TT2 (op And);
val it = [F, F, F, T] : BOOL list

Familiar sentences such as one of de Morgan's laws can be defined by:

fun DeMorgan(P,Q) = Not(P Or Q) Eq (Not P And Not Q);

And evaluated for all combinations of T and F for P and Q, proving that Not(P Or Q) Eq (Not P And Not Q), notice that function DeMorgan is not defined as an infix operator so that (op DeMorgan) is not required:

TT2 DeMorgan;
val it = [T, T, T, T] : BOOL list

Assignment 2 

1. Complete the definitions for Not, Or, Eq, Imp. Define Or, Eq, Imp as infix operations. Define with the precedence assigned by C++.
2. Prove using truth table evaluation in ML:
   1. Not(Not P) Eq P
   2. Contrapositive Law: (P Imp Q) Eq (Not Q Imp Not P)
   3. The other de Morgan's law, there are two.
   4. Distributive laws, there are two.
3. Give a solution to turn one light on and off from three separate switches. If the light is on, changing the position of any switch turns the light off, if the light is off, changing the position of any switch turns the light on. This is the configuration common in rooms with three entrance doors. Give the ML function definition and truth table verification.

Turn In

1. Cover sheet with your name, date, and Homework 4.
2. Print out for Assignment 1 and Assignment 2 of function definitions.
3. Print out for Assignment 1 and Assignment 2 of interactions containing the evaluation results of all the functions.

Document last modified: