Description
This laboratory assignment is intended to familiarize you with a style of programming that will be needed for the upcoming Programming Project 1. It involves using a set of transformations to change one expression into another. Specifically, it asks you to write an OCaml function that takes an expression in propositional logic as its argument, and returns a new expression that is equivalent to the original one, but in which the connective ‘∨’ (or) does not appear.
1. Theory.
Expressions in propositional logic are usually written with the connectives ‘¬’ (not), ‘∧’ (and), ‘∨’ (or), ‘→’ (implies) and ‘↔’ (is equivalent to). However, all these connectives are not really necessary. It is possible to write any expression using only ‘¬’ and ‘∧’, or using only ‘¬’ and ‘∨’. For example, an expression that uses ‘¬’, ‘∧’, and ‘∨’ can be written without ‘∨’ by applying the transformations 1 and 2, shown below. The arrow ‘⇒’ means may be rewritten as.
1 α ∨ β
⇒
¬ (¬ α ∧ ¬ β) 2 ¬ ¬ α
⇒
α
For example, suppose we have the expression ¬ a ∨ ¬ b. We use transformation 1 to rewrite it as a new expression ¬ (¬ ¬ a ∧ ¬ ¬ b). We then use transformation 2 twice, to rewrite the new expression as ¬ (a ∧ b). The final expression is said to be unorified, which is pronounced like un-horrified, but without the h. (This is a fake word invented for this assignment, and used nowhere else.)
2. Implementation.
We can use OCaml’s pattern matching rules to write a function that unorifies expressions in propositional logic. To do that, we must first define an OCaml type proposition to represent these expressions:
type proposition =
False |
True |
Var of string |
And of proposition ∗ proposition |
Or of proposition ∗ proposition |
Not of proposition ;;
The OCaml type proposition represents propositional expressions in the following way, where the squiggly arrow ‘↝’ means is represented as. It is like a similar type to be discussed in the lectures, but simpler.
false
↝
False true
↝
True a, b, c …
↝
Var "a", Var "b", Var "c" … α ∧ β
↝
And (α, β) α ∨ β
↝
Or (α, β) ¬ α
↝
Not α
Only the connectives ‘¬’, ‘∧’, and ‘∨’ are represented. We could have represented the connectives ‘→’ and ‘↔’ too, but they would make this assignment more complicated. For example, the expression ¬ (a ∨ ¬ b) is represented as an instance of the type proposition like this:
Not (Or (Var "a", Not (Var "b")))
For this assignment, you must write an OCaml function called unorify that takes a proposition like this as its only argument. It must return a new proposition that is equivalent to the original one, but in which no Or’s appear. The function unorify must do this by recursively applying transformations 1 and 2 shown in the previous section. Here are some hints.
-
As stated earlier, unorify can use OCaml pattern matching rules to do most of its work. The left side of each rule matches an expression, and breaks it into pieces. The right side of each rule may call unorify on some of the pieces, to make new pieces. Then it puts the pieces back together to return a new, equivalent expression, but without any Or’s.
-
There is probably no way to make unorify completely tail-recursive.
-
One way to write unorify uses seven or eight pattern matching rules. Some of the rules handle expressions involving And, Or, Not, with an extra rule to handle everything else. The other rules will handle expressions that are prefixed by Not’s. (This hint may make more sense after you’ve started writing code.)
-
My definition for unorify is approximately 11 lines of recursive OCaml code. Yours may be longer or shorter, depending on how clever you are, and how you like to indent.
3. Deliverables.
The file tests5.ml contains some tests. It also contains the definition of the type proposition shown above. Insert your code into this file, and then run it with OCaml. Note that unlike previous test files, you must write the tests yourself, translating from propositional logic expressions into instances of the OCaml type proposition. This is to help you become accustomed to OCaml’s constructor notation, which may be unfamiliar.
When you think your code is correct, then submit the test file with your code in it. If you don’t know how and where to submit your work, then ask your lab TA’s. It must be submitted by 11:55 PM on Tuesday, October 19, 2021.
