Recursion and Induction: Function Definitions

To define a function, we use the form `(defun` *f* (*v_1* … *v_n*) *β*`)` where *f* is the function symbol being defined, the *v_i* are the
formal variables or simply *formals*, and *β* is the body of the
function.

Operationally, a definition means that to compute `(`*f* *a_1* …
*a_n*`)` one can evaluate the actuals, *a_i*, bind the formals, *v_i* , to those
values, and compute *β* instead. Logically speaking, a definition adds
the axiom that `(`*f* *v_1* … *v_n*`)` is equal to *β*.

Here are the Lisp definitions of the standard propositional logic connectives:

(defun not (p) (if p nil t)) (defun and (p q) (if p q nil)) (defun or (p q) (if p p q)) (defun implies (p q) (if p (if q t nil) t)) (defun iff (p q) (and (implies p q) (implies q p)))

Note that in Lisp, `and` and `or` are not Boolean valued. E.g.,
`(and t 3)` and `(or nil 3)` both return `3`. This is
unimportant if they are only used propositionally, e.g., `(and t 3)`
↔ `(and 3 t)` ↔ `t`, if
“↔” means `iff`. In Lisp, any non-nil value is
propositionally equivalent to `t`.

Here is a recursive definition that copies a `cons`-structure.

(defun tree-copy (x) (if (consp x) (cons (tree-copy (car x)) (tree-copy (cdr x))) x))

For example, the term `(tree-copy '((1 . 2) . 3))` has the value `((1
. 2) . 3)`.

(Maybe explore <<`defun`>>? Be advised, however, that ACL2's
Definitional Principle imposes restrictions that may not make sense just yet.)

In the exercises below you may wish to define auxiliary (“helper”) functions as part of your solutions.

**Problem 8. ** Define

**Problem 9. ** Define

**Problem 10. ** Define

**Problem 11. ** The result of “swapping” the pair

**Problem 12. ** Define

**Problem 13. ** Define the list analogue of subset, i.e.,

**Problem 14. ** Define

**Problem 15. ** Define

**Problem 16. ** Define

**Problem 17. ** Define

Next: