|
|
|---|
|
|
|
|---|
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 app to concatenate two lists. For example
(app '(1 2 3) '(4 5 6)) evaluates to (1 2 3 4 5 6).
Problem 9.
Define rev to reverse a list. For example,
(rev '(1 2 3)) evaluates to (3 2 1).
Problem 10.
Define mapnil to “copy” a list, replacing each element by nil.
Thus, (mapnil '(1 2 3)) evaluates to (nil nil nil).
Problem 11.
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)).
Problem 12.
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.
Problem 13.
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.
Problem 14.
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).
Problem 15.
Define (tip e x) to determine whether e occurs as a tip
of the binary tree x.
Problem 16.
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).
Problem 17.
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.
Next: