Description
Propositional logic is a branch of mathematics that deals with the Boolean constants true and false, with variables that have Boolean values, and with the Boolean operators ¬ (not), ∧ (and), ∨ (or), → (implication), and ↔ (equivalence). An expression constructed from these constants, variables, and operators has a value that depends on the values of its variables. For example, the expression a ∨ (b ∧ c) is true if a is true, or if both b and c are true; it is false otherwise. An expression is a tautology if it is true for all possible values of its variables. For example, the expression ¬ (p ∧ q) → (¬ p ∨ ¬ q) is a tautology, because it is true for all Boolean values of its variables p and q.
We can prove that an expression is a tautology by using rules about Boolean operators. Unfortunately, there are many such rules: a text used in the Discrete Mathematics course here at the University (CSCI 2011) shows about 34 of them. Using these rules requires creativity and luck. It’s possible to write a program that uses them to prove an expression is a tautology, but it’s difficult.
However, it’s easy to write such a program if we use only one operator, called IF, because IF has only five rules. In this programming project, you will write an OCaml program that tests if a Boolean expression is a tautology, using rules about IF’s.
Before we proceed, here’s a warning. In the past few lectures, we’ve discussed writing a tautology checker for propositional logic in OCaml. However, THE PROGRAM YOU WILL WRITE FOR THIS PROJECT USES AN ALGORITHM THAT IS COMPLETELY DIFFERENT FROM THE ONE IN THE LECTURES!
1. Theory.
An IF term is written as (IF π α β), where each of π, α, and β is either true, false, a variable, or another IF term. It acts much like an if–then–else expression in OCaml. If π is true, then (IF π α β) is α. If π is false, then (IF π α β) is β.
We can express the familiar operators of propositional logic using IF’s. Rules 1 through 5 show how to do that. In each rule, the expression on the left side of the arrow ‘⇒’ is replaced by the expression on the right side. (It may help to remember that α → β acts like ¬ α ∨ β, and α ↔ β acts like α = β).
1 ¬ α
⇒
(IF α false true) 2 α ∧ β
⇒
(IF α β false) 3 α ∨ β
⇒
(IF α true β) 4 α → β
⇒
(IF α β true) 5 α ↔ β
⇒
(IF α β (IF β false true))
The first argument of an IF is called its test. The problem with rules 1 through 5 is that they can create IF’s whose tests are other IF’s. These IF’s are hard to work with. As a result, we use rule 6 to rewrite an IF so its test is always a Boolean constant or a variable. After rule 6 has been used as many times as possible on an IF, so all its tests are Boolean constants or variables, we say that the IF is in normal form, or that it has been normalized.
6 (IF (IF π α1 β1) α2 β2) ⇒ (IF π (IF α1 α2 β2) (IF β1 α2 β2))
Now, rules 7 through 11 can simplify normalized IF’s easily—these are the five rules that we mentioned in the introduction. In rule 11, φ{π ⇒ γ} is an expression like φ, except that each appearance of the variable π within it is replaced by γ.
7 (IF true α β)
⇒
α 8 (IF false α β)
⇒
β 9 (IF π true false)
⇒
π 10 (IF π α α)
⇒
α 11 (IF π α β)
⇒
(IF π α{π ⇒ true} β{π ⇒ false})
These rules work just as we would expect them to, if we know how IF’s work. Rules 7 and 8 just choose α or β. Rule 9 says that if we return true when π is true, and false when π is false, then we don’t need an IF. Rule 10 says that if we choose between two identical alternatives, then we also don’t need an IF. And rule 11 says that we know π is true if we choose α, and that π is false if we choose β.
We’ve now built enough mathematical machinery to design an algorithm that tests if an expression from propositional logic is a tautology. Here’s how it works. First, we use rules 1 through 5 to turn the expression into a nested IF. Then we use rule 6 to normalize the IF. Finally, we use rules 7 through 11 to simplify the normalized IF as much as possible. If if simplifies to true, then the expression is a tautology. If it simplifies to false, or to an IF that cannot be simplified any further, then it is not a tautology.
2. Example.
Here’s an example of the algorithm in action. Suppose we want to know if the following expression from propositional logic is a tautology. This could be a question from a CSCI 2011 assignment—if so, then students taking that course could use the algorithm to cheat.
¬ (p ∧ q) → (¬ p ∨ ¬ q)
We now use rules 1 through 5 to write this expression using nothing but IF’s. (In the program you will write, the OCaml function ifify will do this.) When the rules have done their work, we end up with a nested IF that looks like this.
(IF
(IF
(IF p q false)
false
true)
(IF
(IF p false true)
true
(IF q false true))
true)
This expression has tests that are IF’s. Before we can simplify it, we must normalize it by using rule 6 a few times. (In the program you will write, the OCaml function normalize will do this.) We end up with the following normalized, nested IF.
(IF p
(IF q
(IF false
(IF p
(IF false true (IF q false true))
(IF true true (IF q false true)))
true)
(IF true
(IF p
(IF false true (IF q false true))
(IF true true (IF q false true)))
true))
(IF false
(IF false
(IF p
(IF false true (IF q false true))
(IF true true (IF q false true)))
true)
(IF true
(IF p
(IF false true (IF q false true))
(IF true true (IF q false true)))
true)))
Don’t be scared by the length and complexity of this nested IF! You don’t need to know how it works, or what it does: that’s the job of the program you’re writing for this project. For now, you only need to know that there are many obvious ways in which it could be simplified.
Using rules 7 through 11, this nested IF can be simplified all the way down to true. (In the program you will write, the OCaml function simplify will do this.) That means the original expression was a tautology. You might have known that it was, even without using rules, if you remember De Morgan’s laws.
3. Implementation.
The rules in previous sections can be applied mechanically, without having to understand them, so they can be the basis for an automatic tautology testing program. For this project, you must write such a program in OCaml. Your program must use this Ocaml type to represent expressions from propositional logic.
type proposition =
False |
True |
Var of string |
And of proposition ∗ proposition |
Or of proposition ∗ proposition |
Not of proposition |
Imply of proposition ∗ proposition |
Equiv of proposition ∗ proposition |
If of proposition ∗ proposition ∗ proposition ;;
Constructors from the type proposition represent expressions in the following way, where the squiggly arrow ‘↝’ means is represented as. Lower case letters a, b, c, etc., are propositional variables.
false
↝
False true
↝
True a, b, c, etc.
↝
Var "a", Var "b", Var "c", etc. ¬ α
↝
Not α α ∧ β
↝
And (α,β) α ∨ β
↝
Or (α,β) α → β
↝
Imply (α,β) α ↔ β
↝
Equiv (α,β) (IF π α β)
↝
If (π,α,β)
Your program must also have at least the following major functions. To simplify grading, you must use the same function names that are shown here, but you need not use the same parameter names. In the function descriptions, a propositional expression is represented as an instance of the type proposition, using any operators. An IF-expression is also represented as an instance of the type proposition, but its only operators are IF’s.
- ifify p
(10 points.) Here p is a propositional expression. Using rules 1 through 5, translate p to an equivalent IF-expression, and return it. The resulting IF-expression is not normalized.
- normalize c
(10 points.) Here c is an IF-expression as returned from ifify. Translate c to an equivalent normalized IF-expression, and return it.
- simplify c
(10 points.) Here c is a normalized IF-expression, as returned from normalize. Simplify c using rules 7 through 11, and return the resulting IF-expression.
- substitute c v b
(5 points.) This is a helper function for simplify. Here c is a normalized IF-expression. Also, v is a variable name, and b is a Boolean value, represented as instances of the OCaml type proposition. Return c{v ⇒ b}. In other words, return a new IF-expression that is like c, but in which each appearance of v is replaced by b.
- tautology p
(5 points.) Here p is a propositional expression represented as an instance of the OCaml type proposition. Return true if p is a tautology, and return false otherwise. This function must use ifify, normalize, and simplify as its helpers.
Here are some hints. All of these functions, except tautology, will be recursive. Each recursive case will implement one or more rules. Base cases will occur when no more rules can be applied. The recursions make sure that the rules are applied as many times as needed. There is probably no way to make these functions completely tail recursive.
In the part of simplify that handles rule 10, you may use the OCaml operator ‘=’ to test if the two parts of the IF-expression are equal. However, then your program may not be able to prove that certain expressions are tautologies. For example, (IF a b false) and (IF b a false) should be equal, because they have the same Boolean values for all a and b, but they will not be considered equal by ‘=’. For those who like to think about such things, there is a way to test two IF-expressions for equality, using only the functions described here. You won’t get more points for implementing that test, however—sorry.
Of course you may define additional helper functions if you need them. Code for the OCaml type proposition is available on the file tautyTypes.ml .
4. Deliverables.
Unlike the lab assignments, YOU ARE NOT ALLOWED TO WORK WITH A PARTNER ON THIS PROJECT. Although you may discuss the project with others in a general way, IT MUST BE WRITTEN ENTIRELY BY YOURSELF. The project will be due in two weeks, at 11:55 PM on November 1, 2021. You must submit only one file to Canvas, containing your OCaml code. Any output, resulting from running test cases, must appear in comments at the end of your file. If you do not know how or where to turn in your work, then please ask your lab TA.
