Re: syntax for typed quantification

sowa <sowa@turing.pacss.binghamton.edu>
Date: Wed, 28 Jul 93 21:09:25 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9307290109.AA25669@turing.pacss.binghamton.edu>
To: Gruber@KSL.Stanford.Edu, fikes@KSL.Stanford.Edu, mrg@CS.stanford.edu,
        sowa@turing.pacss.binghamton.edu
Subject: Re:  syntax for typed quantification
Cc: cg@cs.umn.edu, interlingua@isi.edu, interlingua@isi.edui,
        sowa@turing.pacss.binghamton.edu

Tom,

Sets and types are two very different kinds of things.  I would be
happy to represent types with monadic relations.  But we also need
sets for purposes too numerous to bother summarizing here.

Furthermore, every application of sets has frequent need to quantify
over the elements of a set.  In conceptual graphs, I have a systematic
way of quantifying over sets and their elements in a way that maps
very directly to natural language.  I would like to see new kinds of
quantifiers added to KIF to simplify the mapping in both directions.

Example:  One of my standard examples is the sentnece "Every
trailer truck has as part 18 wheels."  Following is the CG form:

   [TRAILER-TRUCK: @every]->(PART)->[WHEEL: {*}@18].

And following is the KIF translation:

   (forall (?x trailer_truck)
           (exists (?s set)
                   (and (count ?s 18)
                        (forall (?w)
                                (=> (member ?w ?s)
                                    (and (wheel ?w) (part ?x ?w)) )))))

The "in" keyword helps to simplify that expression somewhat:

   (forall (?x trailer_truck)
           (exists (?s set)
                   (and (count ?s 18)
                        (forall (?w in ?s)
                                (and (wheel ?w) (part ?x ?w)) ))))

This isn't as compact as I would like it to be, but it is a little
better than the above.  The primary reason for these features is
NOT human readability, but ease of translation both to and from
CGs and other high-level notations.  There is no problem mapping
CGs to KIF -- expanding a high-level notation into a lower level
is easy.  The hard part is to figure out which little constructions
in KIF should be combined to reconstruct the CG form. 

I can always translate the KIF form back into a low-level CG that is
just as ugly as the KIF.  But I want to translate KIF into a
high-level CG from which I can generate the original English
"Every trailer truck has 18 wheels" instead of the sentence
"For every trailer truck x, there is a set s and s has 18 elements
and for all w if w is a member of s then w is a wheel and x has
as part w."  This may use English words, but it is not something
pleasant to read.

The basic purpose of KIF is to serve as an Interlingua between
various KR languages.  Macro expansion is adequate to map from
a high level notation to a low-level notation.  That is a simple,
linear-time process.  But the inverse of macro expansion is in
general undecidable.  Without a good repertoire of high-level
constructions in KIF, it would be impossible to reconstruct a
readable form in conceptual graphs or any other high-level notation
that maps sets to a form that can represent English plurals in
a readable way.

Other kinds of high-level constructions that I would like to
see in KIF are the quantifiers for exactly-one, unique,
exactly-N, etc.  Whitehead and Russell had E! for exactly-one
and E!! for unique.  They occur frequently in mathematics
and program spec's, and they also simplify the mappings to
and from English.

John