Recursion and Induction: Still More Problems
The next several problems will lead you to define a tautology checker in ACL2 and to prove that it is sound and complete. This is an excellent exercise if you are interested in theorem proving.
An IF-expression is a cons whose car is IF. A quote is a cons whose car is QUOTE. A variable is anything besides an IF-expression or a quote. An expression is a variable, a quote, or an IF-expression.
Note: By these definitions, any object is an expression. But we typically think of IF-expressions as being of the form (IF a_1 a_2 a_3) and quotes being of the form (QUOTE a). But rather than check that they are of this form we will just use car and cdr to chew into IFs and quotes to access the desired substructure, which we will call “arguments” one, two, and three.
An assignment is a list of pairs, (var . val), where var is a variable and val is an arbitrary object (but is typically a Boolean).
We define the value of an expression under an assignment as follows. The value of a variable is the val associated with that variable, or nil if the variable is not bound. The value of a quote is the first argument of the quote. The value of an IF-expression depends on the value, v, of the first argument. If v is nil, the value of the IF-expression is the value of its third argument; otherwise, it is the value of its second argument.
Define these concepts.
An expression is said to be in IF-normal form if no IF-expression in the expression has an IF-expression in its first argument. Thus, (IF A (IF B C D) D) is in IF-normal form, but (IF (IF A B 'NIL) C D) is not. It is possible to put an expression into IF-normal form while preserving its value, by repeatedly transforming it with the rule:
(IF (IF a b c) x y) = (IF a (IF b x y) (IF c x y))
Define the notion of IF-normal form and admit the function norm that normalizes an expression while preserving its value.
Given an expression in IF-normal form, define the function tautp that explores all feasible branches through the expression and determines that every output is non-nil. We say a branch is infeasible if, in order to traverse it during evaluation under an assignment, the assignment would have to assign some variable both nil and non-nil.
Define tautology-checker to recognize whether an expression has a non-nil value under all possible assignments.
Prove that your tautology-checker is sound: if it says an expression is a tautology, then the value of the expression is non-nil, under any assignment.
Prove that your tautology-checker is complete: if it fails to recognize an expression, then some assignment falsifies the expression.
This concludes Recursion and Induction. Are you interested in learning how to use the ACL2 theorem prover? (Maybe explore <<introduction-to-the-theorem-prover>>?)