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

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 `IF`s 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 (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

**Problem 135. ** Define

**Problem 136. ** Prove that your

**Problem 137. ** Prove that your

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: