

Introduction to Logic

Tools for Thought


A list is a finite sequence of objects. Lists can be flat, e.g. [a, b, c]. Lists can also be nested within other lists, e.g. [a, [b, c], d].
A linked list is a way of representing nested lists of variable length and depth. Each element is represented by a cell containing a value and a pointer to the remainder of the list. Our goal in this example is to formalize linked lists and define some useful relations.

To talk about lists of arbitrary length and depth, we use the binary function constant cons, and we use the object constant nil to refer to the empty list. In particular, a term of the form cons(τ_{1}, τ_{2}) designates a sequence in which τ_{1} denotes the first element and τ_{2} denotes the rest of the list. With this function constant, we can encode the list [a, b, c] as follows.
cons(a, cons(b, cons(c, nil)))

The advantage of this representation is that it allows us to describe functions and relations on lists without regard to length or depth.
As an example, consider the definition of the binary relation member, which holds of an object and a list if the object is a toplevel member of the list. Using the function constant cons, we can characterize the member relation as shown below. Obviously, an object is a member of a list if it is the first element; however, it is also a member if it is member of the rest of the list.
∀x.∀y.member(x, cons(x, y))
∀x.∀y.∀z.(member(x, z) ⇒ member(x, cons(y, z)))


In similar fashion, we can define functions to manipulate lists in different ways. For example, the following axioms define a relation called append. The value of append (its last argument) is a list consisting of the elements in the list supplied as its first argument followed by the elements in the list supplied as its second. For example, we would have append(cons(a,nil), cons(b, cons(c, nil)), cons(a, cons(b, cons(c, nil)))). And, of course, we need negative axioms as well (omitted here).
∀z.append(nil, z, z)
∀x.∀y.∀z.∀w.(append(y, z, w) ⇒ append(cons(x, y), z, cons(x,w)))


We can also define relations that depend on the structure of the elements of a list. For example, the among relation is true of an object and a list if the object is a member of the list, if it is a member of a list that is itself a member of the list, and so on. (And, once again, we need negative axioms.)
∀x.among(x, x)
∀x.∀y.∀z.(among(x, y) ∨ among(x, z) ⇒ among(x, cons(y, z)))


Lists are an extremely versatile representational device, and the reader is encouraged to become as familiar as possible with the techniques of writing definitions for functions and relations on lists. As is true of many tasks, practice is the best approach to gaining skill.

Use the arrow keys to navigate.
Press the escape key to toggle all / one.

