## Knowledge Interchange Format Specification

## Chapter 5: Lists

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 `**t1** ... **tk**) to denote
the list of objects denoted by **t1**, ..., **tk**. 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 `**t1** **t2**) is true if and only if
the object denoted by **t2** is a non-empty list and the object
denoted by **t1** 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 `**t1** **t2**) is true if and only if
the object denoted by **t1** is a final segment of the list denoted by
**t2**.

(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) :=
(cond ((null ?l1) (if (list ?l2) ?l2))
((list ?l1) (cons (first ?l1) (append (rest ?l1) ?l2)))))
(deffunction revappend (?l1 ?l2) :=
(cond ((null ?l1) (if (list ?l2) ?l2))
((list ?l1) (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)) (list ?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 **n** items, where
**n** 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))
((and (list ?l) (positive ?n)) (nth (rest ?l) (1- ?n)))))
(deffunction nthrest (?l ?n) :=
(cond ((= ?n 0) (if (list ?l) ?l))
((and (list ?l) (positive ?n)) (nthrest (rest ?l) (1- ?n)))))

Michael R. Genesereth