Types, sets, and relations

• Mail folder: Interlingua Mail
• Next message: mineau: "register"
• Previous message: sowa: "Practical effects of all this discussion"
• Reply: macgregor@ISI.EDU: "Re: Types, sets, and relations"

Date: Sat, 24 Apr 93 11:24:52 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9304241524.AA20852@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: Types, sets, and relations
Cc: sowa@turing.pacss.binghamton.edu

I spoke with Mike Genesereth by phone to discuss some of the
issues about mapping CGs <--> KIF.  In particular, he said that
the form (?x in ?s) was being considered in the variable list
following a quantifier; e.g., one could write

   (exists (?s set)
           (forall (?x in ?s) (P ?x)) )

instead of

   (exists (?s set)
           (forall (?x) (=> (member ?x ?s) (P ?x))) )

I am happy with this approach.  But there was one other issue
that bothers me.  Mike said that they were thinking of eliminating
the distinction between types, sets, and monadic relations.
Therefore, one would just write (?x ?s) instead of (?x in ?s),
since the underlying model theory would not make any distinction
between a type ?s and a set ?s.

Mike's argument was an application of Occam's razor:  If a syntactic
difference doesn't have any semantic consequences, then it should be
eliminated.  But I would dispute the point whether "semantics" is
limited to the current model for KIF or to any possible model that
might be introduced in the future.

In our report on the January 18th meeting concerning KIF, CGs, and SUMM,
we agreed to adopt the current KIF semantics, since it was the simplest
and most completely defined.  But both Jim Fulton and I had features in
our languages that were not recognized by the KIF semantics:

 1. Types:  Both CGs and SUMM mark types syntactically and distinguish
    them from monadic relations.  When we map CGs or SUMM to KIF, we
    collapse types to monadic relations for the KIF semantics, but we
    want to preserve the distinction syntactically so that a richer
    semantic model could distinguish them.

 2. Roles:  Both CGs and SUMM have ways of ensuring that certain types
    have obligatory roles associated with them.  Those roles map into
    dyadic relations in KIF, and the obligatory associations are lost.
    It is not necessary to mark those roles syntactically in KIF, since
    their obligatory nature could be enforced by additional axioms when
    they are mapped into KIF.

 3. Collections:  Both CGs and SUMM use braces like {Tom, Dick, Harry}
    to mark collections.  Fulton calls them sets.  I used to call them
    sets, but I'm now calling them collections to leave open the question
    of whether they should be modeled by set theory or mereology.  For
    the mapping to KIF, I can map the collections to sets, but I avoid
    defining any operations on the CG collections that could not be
    supported by either a set theoretic model or a mereological model.

The point of this discussion is that I want to make a clear distinction
between the phrases "is modeled as" and "is identified with".  There are
many research questions in both natural language semantics and
nonmonotonic reasoning where distinctions between types and sets
or roles and dyadic relations are significant.  I agree that we should
not hold up development of KIF and the ANSI and ISO conceptual schemas
until these research issues are settled.  But I also want to ensure
that we don't collapse any distinctions today that would preclude
future extensions that would make an important difference.

Recommendation:  Concetpual graphs, SUMM, English, and a number of
other knowledge representation systems make a distinction between
types, sets, and monadic relations.  In order to simplify the model
theory for the current version of KIF, I would be willing to have
all three of them mapped to the same constructions in the KIF models.

But in order to preserve the option of developing a richer model
theory in the future, I would like to distinguish them syntactically.
Mapping CG types to the quantifier list does mark that distinction,
but if sets are also specified in the same way as types, the other
distinction is lost.  Therefore, I would like to keep the keyword "in"
as a separator between the quantified variable and the set.

Summary:  If T is a type, S is a set, and R is a monadic relation,
I would prefer to use the following notation:

   (forall (?x T) (...))

   (forall (?x in S) (...))

   (forall (?x) (=> (R ?x) (...))

In the current model theory for KIF, all three of these constructions
may have the same denotation, but a future model theory might treat
them differently.

John Sowa