;;; -*- Mode:Lisp; Syntax:Common-Lisp; Package:ONTOLINGUA-USER; Base:10 -*-;;; If you load this file (with translation into the "KIF" implementation;;; -- the default ), then the definitions are saved on property lists;;; and can be used for online documentation and in cross-reference reports.(in-package "ONTOLINGUA-USER") ;inherits from the KIF package;all constants defined here are exported;from the KIF package.(define-theoryKIF-LISTS(kif-numbers) "The KIF vocabulary for lists as defined in the KIF 3.0 specification.") (in-theory 'kif-lists) (define-classLIST(?x) "A list is a sequence --- an ordered bag --- of elements. It is KIF primitive.") (define-classNULL(?list) "True of the list with no items." :iff-def (and (list ?list) (= (length ?list) 0))) (define-instanceNIL(null) "The list with no items, of length 0. All null lists are equal to this object, called NIL.") (define-functionLISTOF(@items) :-> ?list "LISTOF is the sequence constructor function for KIF. It takes any finite number of arguments and denotes the list (i.e., sequence, tuple) of those items. LISTOF is an operator in KIF." :def (list ?list)) (define-relationSINGLE(?list) "A list of length 1." :iff-def (and (list ?list) (= (length ?list) 1))) (define-relationDOUBLE(?list) "A list of length 2." :iff-def (and (list ?list) (= (length ?list) 2))) (define-relationTRIPLE(?list) "A list of length 3." :iff-def (and (list ?list) (= (length ?list) 3))) (define-functionFIRST(?list) :def (list ?list) :lambda-body (if (exists @items (= (listof ?x @items) ?list)) ?x)) (define-functionREST(?list) :-> ?rest-list :iff-def (or (and (null ?list) (= ?rest-list ?list)) (exists (?x @items) (and (= ?list (listof ?x @items)) (= ?rest-list (listof @items)))))) (define-functionLAST(?list) :def (list ?list) :lambda-body (cond ((null ?list) bottom) ((null (rest ?list)) (first ?list)) (true (last (rest ?list))))) (define-functionBUTLAST(?list) :lambda-body (cond ((null ?list) bottom) ((null (rest ?list)) nil) (true (cons (first ?list) (butlast (rest ?list)))))) (define-relationITEM(?x ?list) "The sentence {\tt (item $\tau_1$ $\tau_2$)} is true if and only if the object denoted by $\tau_2$ is a non-empty list and the object denoted by $\tau_1$ is either the first item of that list or an item in the rest of the list." :def (and (list ?list) (not (null ?list)) (or (= ?x (first ?list)) (item ?x (rest ?list))))) (define-relationSUBLIST(?l1 ?l2) "The sentence {\tt (sublist $\tau_1$ $\tau_2$)} is true if and only if the object denoted by $\tau_1$ is a final segment of the list denoted by $\tau_2$." :def (and (list ?l1) (list ?l2) (or (= ?l1 ?l2) (sublist ?l1 (rest ?l2))))) (define-functionCONS(?x ?list) :-> ?new-list "The function {\tt cons} adds the object specified as its first argument to the front of the list specified as its second argument." :def (and (list ?list) (list ?new-list)) :lambda-body (if (= ?list (listof @l)) (listof ?x @l))) (define-functionAPPEND(?l1 ?l2) :-> ?new-list "The function {\tt append} adds the items in the list specified as its first argument to the list specified as its second argument. ." :def (and (list ?l1) (list ?l2) (list ?new-list)) :lambda-body (if (null ?l1) (if (list ?l2) ?l2) (cons (first ?l1) (append (rest ?l1) ?l2)))) (define-functionREVAPPEND(?l1 ?l2) :-> ?new-list "The function {\tt revappend} is similar to append, except that it adds the items in reverse order." :def (and (list ?l1) (list ?l2) (list ?new-list)) :lambda-body (if (null ?l1) (if (list ?l2) ?l2) (revappend (rest ?l1) (cons (first ?l1) ?l2)))) (define-functionREVERSE(?list) :-> ?new-list "The function {\tt reverse} produces a list in which the order of items is the reverse of that in the list supplied as its single argument." :def (and (list ?list) (list ?new-list)) :lambda-body (revappend ?list (listof))) (define-functionADJOIN(?x ?list) :-> ?new-list "The functions {\tt adjoin} and {\tt remove} construct lists by adding or removing objects from the lists specified as their arguments." :def (and (list ?list) (list ?new-list)) :lambda-body (if (item ?x ?list) ?list (cons ?x ?list))) (define-functionREMOVE(?x ?list) :-> ?new-list "The functions {\tt adjoin} and {\tt remove} construct lists by adding or removing objects from the lists specified as their arguments." :def (and (list ?list) (list ?new-list)) :lambda-body (cond ((null ?list) nil) ((and (= ?x (first ?list)) (list ?list)) (remove ?x (rest ?list))) ((list ?list) (cons ?x (remove ?x (rest ?list)))))) (define-functionSUBST(?x ?y ?z) "The value of {\tt 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." :lambda-body (cond ((= ?y ?z) ?x) ((null ?z) nil) ((list ?z) (cons (subst ?x ?y (first ?z)) (subst ?x ?y (rest ?z)))) (true ?z))) (define-functionLENGTH(?list) :-> ?n "The function constant {\tt length} gives the number of items in a list." :def (and (list ?list) (nonnegative-integer ?n)) :lambda-body (cond ((null ?list) 0) ((list ?list) (1+ (length (rest ?list)))))) (define-functionNTH(?list ?n) "{\tt nth} returns the item in the list specified as its first argument in the position specified as its second argument." :def (and (list ?list) (natural ?n)) :lambda-body (cond ((= ?n 1) (first ?list)) ((positive ?n) (nth (rest ?list) (1- ?n))))) (define-functionNTHREST(?list ?n) :-> ?new-list "{\tt nthrest} returns the list specified as its first argument minus the first $n$ items, where $n$ is the number specified as its second argument." :def (and (list ?list) (natural ?n) (list ?new-list)) :lambda-body (cond ((= ?n 0) (if (list ?list) ?list)) ((positive ?n) (nthrest (rest ?list) (1- ?n)))))