Lists



next up previous
Next: Sets Up: No Title Previous: Relations on Numbers

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 ... ) 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)))))



next up previous
Next: Sets Up: No Title Previous: Relations on Numbers



Vishal I. Sikka
Wed Dec 7 13:23:42 PST 1994