A2, cse3322, 2006

• Functional programming -- based on λ-calculus, emphasises high-order functions, and recursion, bans side-effects (state, assignment, changeable variables).
• High-order functions -- functions that accept functions as parameters and/or return functions as results.
• Polymorphic types.
• Pattern matching -- functions defined over datatypes "by cases".
• Recursion.
• Trees, lists and other recursive data types.

Background

A well-formed formula [WFF] in propositional logic may consist of:

p, q, fred, etc.   --propositions

not   --logical negation, binds most tightly

and   --binds more tightly than or

or   --binds more tightly than =>

=>   --implication

(...)   --sub-WFF

nothing else, except that you may optionally implement <= (left implication, here), and <=> if you wish.

E.g., (p=>q) => (not p=>not q)

 

Every WFF is [either]

a tautology (true for every assignment of true/false to the propositions), or

a contradiction (false for every ... ), or

satisfiable (neither of the above).

The Problem

In SML,

1. Create a suitable type or types to represent WFFs.

2. Write a function

trav : (string->'t) -> (Uopr->'t->'t) -> ('t->Bopr->'t->'t) -> WFF -> 't

where trav's first parameter acts on a proposition, the second paramater acts on a unary operator (not) and the result of processing (`trav'-ing) its sub-WFF, and the third parameter acts on a binary operator (=>, and, or) and the results of processing its two sub-WFFs.

3. Use `trav' to create an unparser,

show : WFF -> string,   to display a WFF. (It is acceptable to include redundant ( ).)

4. Use `trav' to create a function to evaluate a WFF to true/false,

eval : string list -> WFF -> bool

given a list of propositions that have the value true; propositions not in the list have the value false.

5. Create a parser : string -> WFF. (See [hints] below.)

6. Implement Gentzen's proof system, system-G, for WFFs [click] (rules 1-7), to decide if a given WFF is a tautology, a contradiction, or satisfiable. The steps of the proof must be printed in some simple but easy to follow format.

7. Include a function, demo(), which demonstrates your code on three interesting (but not very slow running) cases.

[max: 10]

Due:

4pm Friday 25 Aug, by 'submit'. Assessment is 'a2'. File name is 'a2.sml'. Window opens Mon. 21 Aug.

NB. Read [assessment(click)].

Late submission: assessment is 'a2late', window opens Sat. 26 Aug. and closes 4pm Fri. 1 Sept. If you have submitted "on-time" we will not mark any late submission. The assignment will be assessed on elegance, generality, efficiency and mastery of the functional programming paradigm.

Hints and feedback

NB. Propositional logic, not predicate logic (predicates can have parameters).

 

There is an example of a recursive-descent parser for expressions including (+, -, *, /, =, <>, <=, <, >=, >, and, or, not) here: [click]. If you want, you may modify it to form the basis of your parser for WFFs (it was created for other reasons, and the operator priority is not quite as you need it).

 

Do not worry about both `=>' and `->' appearing in some WFFs at the demo. There is a subtle difference between them in logic but it does not affect a1. Either stick with => for implication or allow both in input and treat => and -> as synonyms. And yes, -> is also used in SML function types; that is natural because there is a close relationship between type-checking and logic [see]!

If you want to add p<=>q, it is equivalent to (p=>q)and(q=>p).

 

For `a1' we were lenient on uncurried v. curried functions, but for `a2' we shall be quite picky about the type of `trav' etc. being as specified.

 

General tactic to convert abstract syntax in SML types

	abstract syntax	SML
e.g. expressions	Exp ::= identifier | numeral | Uopr Exp | Exp Bopr Exp Uopr ::= - | not Bopr ::= + | - | * | / | = | <> | <= | >= | < > | and | or	datatype Exp = identifier | numeral | unexp of Uopr * Exp | binexp of Exp * Bopr * Exp Choose appropriate names for value constructors and maybe add extra components, e.g. the string of an identifier; e.g., see [here].
WFFs	WFF ::= proposition | Uopr WFF | WFF Bopr WFF Uopr ::= not Bopr ::= and | or | =>	a2, #1

 

Make sure that you have done or can do parts 1 to 5 before you try 6.

• p or ~p   -- the simplest tautology
• p and ~p   -- the simplest contradiction
• p   -- the simplest satisfiable WFF.

Each one of rule 1 to 6 of system G removes a non-`and' from the LHS or a non-`or' from the RHS; if that is impossible we have the base-case, rule 7:

• a and p and b and ... => q or p or r or ...

it is a tautology if some proposition, such as `p', appears on both sides.

 

E.g., rule 1

(p or q)&rest => R

iff (i) p&rest => R

and (ii) q&rest => R

If there is an `or' on the LHS, make two new ones, {LHS' = p & rest}, and also {LHS'' = q & rest}, and then prove two (simpler) things, {LHS' & rest => R}, and also {LHS'' & rest => R}.

Note that p, q, rest and R can be sub-WFFs (trees); they are not necessarily propositions.

 

The standard built-in, datatype 'a option = NONE | SOME of 'a, is useful for a function parameter or result which can be absent (optional).