**Mail folder:**Interlingua Mail**Next message:**Robert MacGregor: "KIF variable syntax"**Previous message:**sowa@watson.ibm.com: "Definitions and analytic truth"

Message-id: <9201061807.AA20180@quark.isi.edu> To: fikes@sumex-aim.stanford.edu Cc: schubert@cs.rochester.edu, macgregor@isi.edu, fikes@hpp.stanford.edu, interlingua@isi.edu, sowa@watson.ibm.com Reply-To: macgregor@isi.edu Subject: Comments on Richard's proposal for definitions Date: Mon, 06 Jan 92 10:07:07 PST From: Robert MacGregor <macgreg@isi.edu>

Richard, > First of all, we are proposing to distinguish definitions (and > inference rules) from sentences, so that a knowledge base will consist > of a collection of definitions, rules, and sentences. Definitions > (and inference rules) therefore do not have a truth value, cannot be > embedded inside of sentences, cannot appear as arguments to operators, > cannot be derived, etc. I think this is a very positive step forward. > Analogously, "kappa" is a relation-forming operator defined as > follows. The semantic value of the term "(kappa (<indvar>* > [<seqvar>]) <sentence>)" is the set of tuples associated with the > relation that holds for every tuple of objects "matching" the variable > list for which the sentence is satisfied when the variables in the > variable list are assigned to the objects in the tuple. That meaning > is expressed with the following axiom schema: > > (= (kappa ($v1 ... $vk [@w]) phi) > (setof (list $v1 ... $vk [@w]) phi)) > > We now have the alternative, as suggested by Bob, of considering the > domain assertion to be: > > (= r (kappa ($v1 ... $vk [@w]) (and s1 ... sn))) I think mathematical logic rather than Lisp should be the guide for choosing the KIF meaning for the term "lambda". Hence, I agree with the spirit of what your "lambda" and "kappa" operators are doing, but not with your choice of operators. Further, I think of "lambda" as something that is a primitive logical operator -- defining it in terms of a set constructor seems to be a backwards way of doing things (perhaps "setof" should be defined using "lambda"). Regarding the sequence variables -- I think KIF would be a lot cleaner and more palatable if sequence variables were eliminated, so I have no opinion on subtleties that depend on that particular aspect of the language. The recent discussions on definitions do seem to be moving in what I feel is right direction. However, regarding analytic truths and whatnot, I think that efforts to combine everything that a definition represents into a *single* statement are off the mark. For example, suppose I have: (defrelation R (?x) (and (A ?x) (B ?x))) (defrelation S (?x) (and (B ?x) (A ?x)))) Are the definitions of R and S the same? Answer: No. Are the definitions of R and S equivalent? Answer: Yes. What do I mean by equivalent? The following lambda expressions (my usage, not Richard's) (lambda (?x) (and (A ?x) (B ?x))) and (lambda (?x) (and (B ?x) (A ?x))) denote exactly the same predicate. Thus, I would call the definitions of two symbols R and S equivalent if they denote the same thing. However, the SOURCE of the definitions is not the same thing as their denotation, and that distinction has been lost in the sentence (= R (lambda (?x) (and (A ?x) (B ?x)))). I propose inventing a binary relation DEFINITION that maps symbols to the expressions that they define. For example, my interpretation of the declaration (defrelation R (?x) (and (A ?x) (B ?x))) would be the two statements (definition 'R '(lambda (?x) (and (A ?x) (B ?x)))). (= R (lambda (?x) (and (A ?x) (B ?x)))). with some kind of wrapper around the second statement indicating that this is an analytic-truth, law, or whatever we want to call it. Note: when one considers systems that support revision of definitions, (e.g., LOOM) it is mandatory that something equivalent to the source of a definition be available to the reasoner -- lambda expressions lose important information. What about primitive definitions? I propose first reaching agreement on non-primitive definitions, and then tackling primitiveness. - Bob