|
|
|---|
|
|
|
|---|
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.
Problem 132.
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.
Problem 133.
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.
Problem 134.
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.
Problem 135.
Define tautology-checker to recognize whether an expression has
a non-nil value under all possible assignments.
Problem 136.
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.
Problem 137.
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>>?)
Next: