A *list* is a finite sequence of objects. The objects in a
list need not be KIF expressions, though they may be.
In other words, it is just as acceptable to talk about a list of
two people as it is to talk about a list of two symbols.

In KIF, we use the term `(listof ... )` to denote the
list of objects denoted by , ..., . For example, the
following expression denotes the list of an object named `mary`, a list of
objects named `tom`, `dick`, and `harry`, and an object named
`sally`.

`(listof mary (listof tom dick harry) sally)`

The relation `list` is the type predicate for lists. An object is a list
if and only if there is a corresponding expression involving the `listof`
operator.

`(defrelation list (?x) :=`

` (exists (@l) (= ?x (listof @l)))`

The object constant `nil` denotes the empty list. `null` tests whether
or not an object is the empty list. The relation constants `single`,
`double`, and `triple` allow us to assert the length of lists
containing one, two, and three elements, respectively.

`(defobject nil := (listof))`

`(defrelation null (?l) := (= ?l (listof)))`

`(defrelation single (?l) := (exists ?x (= ?l (listof ?x))))`

`(defrelation double (?l) :=`

` (exists (?x ?y) (= ?l (listof ?x ?y))))`

`(defrelation triple (?l) :=`

` (exists (?x ?y ?z) (= ?l (listof ?x ?y ?z))))`

The functions `first`, `rest`, `last`, and `butlast` each
take a single list as argument and select individual items or sublists from
those lists.

`(deffunction first (?l) := (if (= (listof ?x @items) ?l) ?x)`

`(deffunction rest (?l) :=`

` (cond ((null ?l) ?l)`

` ((= ?l (listof ?x @items)) (listof @items))))`

`(deffunction last (?l) :=`

` (cond ((null ?l) bottom)`

` ((null (rest ?l)) (first ?l))`

` (true (last (rest ?l)))))`

`(deffunction butlast (?l) :=`

` (cond ((null ?l) bottom)`

` ((null (rest ?l)) nil)`

` (true (cons (first ?l) (butlast (rest ?l))))))`

The sentence `(item )` is true if and only if
the object denoted by is a non-empty list and the object
denoted by is either the first item of that list or an item in
the rest of the list.

`(defrelation item (?x ?l) :=`

` (and (list ?l)`

` (not (null ?l))`

` (or (= ?x (first ?l)) (item ?x (rest ?l)))))`

The sentence `(sublist )` is true if and only if
the object denoted by is a final segment of the list denoted by
.

`(defrelation sublist (?l1 ?l2) :=`

` (and (list ?l1)`

` (list ?l2)`

` (or (= ?l1 ?l2)`

` (sublist ?l1 (rest ?l2)))))`

The function `cons` adds the object specified as its first
argument to the front of the list specified as its second argument.

`(deffunction cons (?x ?l) :=`

` (if (= ?l (listof @l)) (listof ?x @l)))`

The function `append` adds the items in the list specified as its first
argument to the list specified as its second argument. The function `revappend` is simiar, except that it adds the items in reverse order.

`(deffunction append (?l1 ?l2) :=`

` (if (null ?l1) (if (list ?l2) ?l2)`

` (cons (first ?l1) (append (rest ?l1) ?l2))))`

`(deffunction revappend (?l1 ?l2) :=`

` (if (null ?l1) (if (list ?l2) ?l2)`

` (revappend (rest ?l1) (cons (first ?l1) ?l2))))`

The function `reverse` produces a list in which the order of items is the
reverse of that in the list supplied as its single argument.

`(deffunction reverse (?l) := (revappend ?l (listof)))`

The functions `adjoin` and `remove` construct lists by adding or
removing objects from the lists specified as their arguments.

`(deffunction adjoin (?x ?l) := (if (item ?x ?l) ?l (cons ?x ?l)))`

`(deffunction remove (?x ?l) :=`

` (cond ((null ?l) nil)`

` ((and (= ?x (first ?l)) (listp ?l))`

` (remove ?x (rest ?l)))`

` ((list ?l) (cons ?x (remove ?x (rest ?l))))))`

The value of `subst` is the object or list obtained by substituting the
object supplied as first argument for all occurrences of the object
supplied as second argument in the object or list supplied as third argument.

`(deffunction subst (?x ?y ?z) :=`

` (cond ((= ?y ?z) ?x)`

` ((null ?z) nil)`

` ((list ?z) (cons (subst ?x ?y (first ?z))`

` (subst ?x ?y (rest ?z))))`

` (true ?z)))`

The function constant `length` gives the number of items in a list. `nth` returns the item in the list specified as its first argument in the
position specified as its second argument. `nthrest` returns the list
specified as its first argument minus the first items, where is
the number specified as its second argument.

`(deffunction length (?l) :=`

` (cond ((null ?l) 0)`

` ((list ?l) (1+ (length (rest ?l))))))`

`(deffunction nth (?l ?n) :=`

` (cond ((= ?n 1) (first ?l))`

` ((positive ?n) (nth (rest ?l) (1- ?n)))))`

`(deffunction nthrest (?l ?n) :=`

` (cond ((= ?n 0) (if (listp ?l) ?l))`

` ((positive ?n)) (nthrest (rest ?l) (1- ?n)))))`

Wed Dec 7 13:23:42 PST 1994