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.
Define app to concatenate two lists. For example (app '(1 2 3) '(4 5 6)) evaluates to (1 2 3 4 5 6).
Define rev to reverse a list. For example, (rev '(1 2 3)) evaluates to (3 2 1).
Define mapnil to “copy” a list, replacing each element by nil. Thus, (mapnil '(1 2 3)) evaluates to (nil nil nil).
The result of “swapping” the pair (x . y) is the pair (y . x). Define swap-tree to swap every cons in a binary tree. Thus, (swap-tree '((1 . 2) . (3 . 4))) evaluates to ((4 . 3) . (2 . 1)).
Define mem to take two arguments and determine if the first one occurs as an element of the second. Thus, (mem '2 '(1 2 3)) evaluates to t and (mem '4 '(1 2 3)) evaluates to nil.
Define the list analogue of subset, i.e., (sub x y) returns t or nil according to whether every element of x is an element of y.
Define int to take two lists and to return the list of elements that appear in both. Thus (int '(1 2 3 4) '(2 4 6)) evaluates to (2 4).
Define (tip e x) to determine whether e occurs as a tip of the binary tree x.
Define (flatten x) to make a list containing the tips of the binary tree x. Thus, (flatten '((1 . 2) . (3 . 4))) evaluates to (1 2 3 4).
Define evenlen to recognize lists of even length. Thus, (evenlen '(1 2 3)) evaluates to nil and (evenlen '(1 2 3 4)) evaluates to t.