Re: Types, sets, and relations

sowa <sowa@turing.pacss.binghamton.edu>
Date: Tue, 27 Apr 93 08:20:13 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9304271220.AA23587@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU, macgregor@ISI.EDU,
        sowa@turing.pacss.binghamton.edu
Subject: Re: Types, sets, and relations

In reponse to Bob MacGregor's note, I would like to expand a bit
on why I want to distinguish types and sets.  In my Conceptual Structures
book, I made the point that sets were defined purely extensionally by
listing their elements, but that types were defined intensionally by
their "meaning".  The denotation of a type would be a set, but type
equality would require more than just equality of the corresponding sets.

As an example, the type Unicorn would not be a subtype of Cow,
even though the set of all unicorns (being empty) would be a subset
of the set of all cows.  Another example would be Plato's old
example of the equality of the sets of featherless-bipeds,
animals-with-speech, and human-beings.  Those three sets may be
equal by extension, but the terms have very different meanings,
and they might become different if some change occurs in the world.

Diogenes the Cynic (the guy who went around with a lantern looking
for an honest man) once plucked a chicken and threw it into the Academy,
saying "Here is Plato's man."

To formalize the distinction, I would say that a set is defined
by its extension -- listing its elements.  But a type is defined by
stating axioms.  For two sets, S1 is a subset of S2 if every element
of S1 is also an element of S2.  But for types, T1 is only a subtype
of T2 if the axioms for T1 imply the axioms for T2.

In the case of the cows and unicorns, one axiom for unicorn would be
that it has only one horn, but an axiom for cows would be that it has
two horns.  Therefore, neither one could be a subtype of the other.
However, in the world as it is today, there are no unicorns; therefore,
the set of unicorns is a subset of the set of cows.  Similarly, the
axioms for defining the types Featherless-biped and Animal-with-speech
would be very different, even though their sets might be the same.

Some comments on Bob's note:

> ... We and many of our users
> find the distinction between Type and Monadic-Relation useful, but we
> have not discovered a reliable semantic basis for this distinction, and
> I would hazard a guess that we never will.

What I'm asking for is a three-way syntactic distinction, which one
model theory or another might cause to collapse into one or two.
The current KIF semantics causes types, sets, and monadic relations
to collapse into the same constructs in the model theory.  A modal
formulation with multiple situations (I hate to call them possible
worlds after all that discussion two weeks ago) might distinguish
them.  What I want to do is to distinguish them to accommodate
different theories that may exist now or in the future.

> My second reason for disagreement is that John's suggestion places a
> greater burden on the translation process, plus it requires that the
> translator make seemingly arbitrary distinctions. For example, Loom
> provides distinct means for introducing concepts (Types) and properties
> (Monadic-Relations) into a knowledge base, but their use within queries
> is identical. To conform to John's proposal, a Loom statement like

   (forall (?x) (implies (A ?x) ...))

> would have a different translation into KIF depending on whether "A"
> had been introduced as a concept or as a property.

In the current version of KIF, types are not distinguished as a 
semantic category.  Their use in a quantifier list is defined by
a macro expansion to exactly the same form as a monadic relation.
Therefore, you can, if you wish, map LOOM concepts and properties
into exactly the same KIF form -- namely, monadic relations.

Bottom line:  KIF has a purely extensional semantics that eliminates
any distinction between types, sets, and monadic relations.  That
approach simplifies a lot of theoretical issues.  I'm not completely
happy with it, but I'm willing to go along in order to reach agreement
on a version of model theory that is well understood and does not get
into any unresolved research issues.

However, there are other systems that do make such distinctions on
various grounds -- formal, pragmatic, esthetic, or traditional.
Some of those distinctions turn out to be very important when dealing
with modal and intensional issues.  However, I don't believe that we
should hold up the development of KIF and the conceptual schema
standards until all of the theoretical differences are resolved.
But I do want to preserve a syntactic distinction so that if a richer
model theory is later proposed for a future version of KIF, older
knowledge bases can be imported into the richer KIF with a minimum
of revision and rewriting.

It is always easy to ignore a distinction when it is not relevant to
your immediate problem.  But it is much harder to put distinctions into
a knowledge representation when they weren't there from the start.

John