Re: definitions and analytic truth

• 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