**Mail folder:**Interlingua Mail**Next message:**John McCarthy: "definitions and analytic truth "**Previous message:**Richard Fikes: "Re: Interlingua Reference Manual"**In-reply-to:**schubert@cs.rochester.edu: "definitions and analytic truth"**Reply:**John McCarthy: "definitions and analytic truth "

Full-Name: Richard Fikes Sender: Richard Fikes <fikes@hpp.stanford.edu> Date: Sun, 5 Jan 1992 23:26:17 PST From: Richard Fikes <fikes@sumex-aim.stanford.edu> Reply-To: fikes@sumex-aim.stanford.edu To: schubert@cs.rochester.edu, macgregor@isi.edu Cc: fikes@hpp.stanford.edu, interlingua@isi.edu, sowa@watson.ibm.com Subject: Re: definitions and analytic truth In-reply-to: Your message of Fri, 3 Jan 92 18:45:04 EST Message-id: <CMM.0.88.694682777.fikes@hpp.Stanford.EDU>

Len and Bob, As I mentioned in my message last evening to Vijay Saraswat, Mike and I are completing a draft of the reference manual for a proposed 3.0 version of the interlingua. Bob's message about the use of lambda's in definitions was particularly timely, because the 3.0 language includes lambda constructs, and I am in the process of revising the definitions chapter of the manual in light of that and other changes in the language. I would like to get your input on the revisions I have in mind for that chapter. In order for you to understand the revisions, I will first describe below the changes in the other parts of the language that I think directly affect definitions. 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. As before, a definition declares the "category" of a constant (i.e., as an object, function, or relation), declares the "arity" of the constant when a relation or function is being defined, and has associated with it a sentence called its "domain assertion". The meaning of a definition is that its domain assertion is true and that its domain assertion is an "analytic truth". Analytic truths are those sentences that are true by definition or that are logically entailed from analytic truths. The "member" relation for sets and the "setof" set constructor operator have been carefully defined in 3.0 so as to avoid paradoxes. Relations and functions are defined to be sets of tuples of elements >From the universe of discourse, and all relations and functions are themselves considered to be part of the universe of discourse. Since function constants and relation constants denote functions and relations and since functions and relations are objects in the universe of discourse, function and relation constants are allowed to appear as arguments in terms and sentences. "lambda" is a function-forming operator defined as follows. The semantic value of the term "(lambda (<indvar>* [<seqvar>]) <term>)" is the set of tuples associated with the function that maps every tuple of objects "matching" the variable list to the value of the term when the variables in the variable list are assigned to the objects in the tuple. That meaning is expressed with the following axiom schema: (= (lambda ($v1 ... $vk [@w]) gamma) (setof (list $v1 ... $vk [@w] value) (= value gamma))) 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)) The syntax for functional terms and relational sentences has been extended to allow lambda and kappa expressions to appear in the place of function or relation constants. So, for example, a relational sentence can have either of the following forms: (<relconst> <term>*) | ((kappa (<indvar>* [<seqvar>]) <sentence>) <term>*) Finally, remember that relations and functions in KIF can take varying numbers of arguments. For example, "+" can take two or more arguments. Thus, the set which is the semantic value of a relation or function can contain tuples of differing lengths. Now, given that base language, what is the appropriate domain assertion for definitions of relations and functions? Function definitions have the following form: (defrelation r ($v1 ... $vk [@w]) s1 ... sn) Previously, we have considered the domain assertion associated with a relation definition of the above form to be the following: (<=> (r $v1 ... $vk [@w]) (and s1 ... sn)) We now have the alternative, as suggested by Bob, of considering the domain assertion to be: (= r (kappa ($v1 ... $vk [@w]) (and s1 ... sn))) Len argued in his last message that those two domain assertions are equivalent, given typical definitions of kappa and relation application. I agree. However, because KIF allows functions and relations to take varying numbers of arguments, they differ, as follows. The first form says that the relation holds for every tuple of objects matching the variable list if and only if the conjunction of sentences are satisfied when the variables in the variable list are assigned to the objects in the tuple. It does not, however, say anything about whether the relation holds for tuples that do not match the variable list. So, for example, if the variable list consists of two variables, the first form does not tell us whether the relation holds for any given tuple consisting of three elements. The second form does not suffer from that problem in that it says that r is precisely the set of tuples which both match the variable list and satisfy the conjunction of sentences. An analogous argument holds for function definitions using defunction. So, it seems that for KIF 3.0, the appropriate domain assertion for defrelation is an equivalence using kappa and for defunction is an equivalence using lambda. If we use equivalences involving kappa and lambda as domain assertions for defunction and defrelation definitions, what is the appropriate domain assertion for defprimrelation definitions? It seems that our previous implication form suffers from the same problem as the forms for defrelation and defunction. However, in the case of defprimrelation, we cannot say that the relation being defined is equivalent to any kappa form (unless we introduce a new relation constant in each case representing the unspecified "residue" of meaning). Instead, I propose the following. Given a definition of the following form: (defprimrelation r ($a1 ... $ak [@t]) s1 ... sn) consider its domain assertion to be: (=> (r @args) ((kappa ($a1 ... $ak [@t]) (and s1 ... sn)) @args)) This domain assertion says that any tuple for which the relation holds must both match the variable list of the kappa expression and satisfy the sentences in the kappa expression. That assertion gives us the semantics we want in that it covers all tuples. What do you think? In particular, I would like to know whether you agree with these new domain assertions and whether you agree with distinguishing definitions from sentences. Regards, Richard