Types vs. monadic relations

sowa@watson.ibm.com
Message-id: <9202041724.AA29471@cs.umn.edu>
Reply-To: cg@cs.umn.edu
Date: Tue, 4 Feb 92 12:24:14 EST
From: sowa@watson.ibm.com
To: macgregor@isi.edu, hayes@cs.stanford.edu
Cc: interlingua@isi.edu, srkb@isi.edu, cg@cs.umn.edu
Subject: Types vs. monadic relations
Bob and Pat,

I'm glad that you agree in principle with the idea of having a typed
KIF, even if you only accept 2 or 3 of my 4 arguments.  But I think
that the discussion is bringing out some interesting points.

First, Bob made the following comment on my response to his question:

>>> What do you consider to be the semantic difference between
>>> a "type" and a "monadic relation"?  Why should we care?
>>
>>     a)   (Ex)(red(x) & ball(x)).
>>     b)   (Ex:ball)red(x).
>>     c)   (Ex:red)ball(x).
>>     d)   (Ex:red)(Ey:ball)x=y.
>>     ....  But ontologically, [the above statements] they make
>>     different assumptions
>>     about the nature of reality.
>
> You state that there is a difference, but you haven't yet said *what*
> it is.  I'd like a rule of inference or something similar to
> motivate the difference.  For example, suppose an end-user comes up
> to me and asks what difference it will make to his application
> whether they define Male-Person as a type or as a unary predicate.
> I'd like to have a good answer for them.  If the answer is that
> doing it one way makes the system run faster, then the distinction
> shouldn't necessarily even be considered declarative knowledge!

I must confess that the representation I recommended in my earlier note,
namely

   (Ex:ball) red(x),

is not the one I usually use.  For the English phrase "a red ball",
I would normally use the following conceptual graph,

   [BALL]->(ATTR)->[RED],

which has the translation

   (Ex:ball)(Ey:red) attr(x,y),

which means "There exists a ball x, there exists a patch of red y,
and x has attribute y."  When I want to treat "red" as a value of
type COLOR, I would also write,

   [BALL]->(CHRC)->[COLOR: red],

which corresponds to the English phrase "a ball of color red".
The CHRC relation (characteristic) is defined in terms of ATTR
and KIND:

   CHRC = (lambda x,y)[ENTITY: *x]->(ATTR)->[&top]->(KIND)->[TYPE: *y],

where &top is the undefined type at the top of the type hierarchy,
TYPE is a second-order type whose instances are names of first-order
types, and KIND is a relation that links something to its type.

I treat COLOR as a subtype of TYPE (a second-order type), and
RED as a subtype of COLORED (a first-order type).  But this is an
issue in ontology rather than logic.

To get back to Bob's point, I agree that there should be clear-cut
guidelines for deciding which representation to use.  My basic rule
is that the content words in English (nouns, verbs, adjectives, and
adverbs) map into concept types.  If the English phrase varies, you
get different representations, as in the examples "a red ball" vs.
"a ball of color red".  But the definitions allow you to transform
one representation into the other, e.g. CHRC -> ATTR + KIND.

Bob also asked about MALE-PERSON.  When represented as two words,
"a male person", I would write

   [PERSON]->(ATTR)->[MALE],

as for "a read ball".  But I might also define MALE-PERSON as a type,

   MALE-PERSON = (lambda x)[PERSON: *x]->(ATTR)->[MALE].

I could also define a monadic relation MALE that applies to persons,
but I don't normally do so, since it doesn't have as systematic a
mapping to natural language.  In Appendix B of _Conceptual Structures_,
I gave a list of 37 conceptual relations that I used in the book, and
only 4 of them were monadic:  NEG for negation, NECS for necessary,
PSBL for possible, and PAST for past tense.  The first three of these
relations apply to propositions, and PAST applies to situations.  But
PAST isn't a primitive, since it is defined in terms of the speech time
and the time of the situation.

Pat made a related point,

>>1. ... In a sorted logic, there are four ways to
>>    express that information, ...:
>
> But this is hardly an advantage.  The language is highly redundant, it seems:
> one can say the same thing in four different ways.  Why do you consider this a
> good thing?  It is a problem both computationally and for human use. If these
> differences have consequence, then four users can say what they thought was
> the same thing but the system understands them differently, and presumably
> will fail to make some inferences that it should make.  If the differences
> have no consequence, this is just like offering the user a variety of fonts.

As I said above, those four representations are not ones that I normally
use with conceptual graphs.  The conceptual graphs do offer different
representations, but each one has a different mapping to natural language
as in the example of "a red ball" vs. "a ball of color red".  Furthermore
the system has formal rules for converting one representation into the
other.  Besides accommodating different expressions in English, the
different representations also allow you to restructure a knowledge base
when you decide to change representations; for example, one system might
represent "red" by a predicate red(x) and another might say color(x,red).
You need some method for allowing either representation to be transformed
into the other.

Bob continued with the following comment:

> Your previous message next listed three arguments in favor of a
> sorted/typed logic.  I agree with all three, and I think KIF ought
> to be typed, but that is a different question.  Suppose I decide to
> make every unary predicate in my KB a type.  Then there is no
> distinction between the two, but I can still use a typed logic.
> You haven't yet presented a concrete (i.e., non-philosophical)
> reason for making the distinction.

I'm glad that you agree with the principle, whether or not you agree
with my first argument.  Pat makes a similar point:

> The difference between a sorted logic and an unsorted one is essentially a
> computational difference, not an assertional one. While I agree that sorted
> languages are an excellent idea, essentially for computational reasons, I
> think we need not get too involved with philosophical intuitions that have
> no semantic basis.  And not all the reasons you give are very convincing.

Whether a philosophical difference is semantic depends on your definition
of semantics.  I agree that it makes no truth-functional difference, but
it does make a difference in your mapping to and from natural language
and in what you consider the principal categories of your ontology.

I like Quine's dictum as a basic guideline for what goes into the
ontology:  "To be is to be the value of a quantified variable."
I would define a type for any category that I would want to quantify
over or refer back to with a variable (or a coreference link in the
graphic form).  I would define a relation for anything that I would
never (or almost never) want to quantify over or refer to -- instances
of negation, possibility, necessity, or past-tenseness, for example.

For that reason, I prefer to make verbs into quantifiable types,
since you can say things like "A cat chased a mouse.  The chase
lasted 14 seconds," where you refer to an action by a verb in one
sentence and refer back to it with a noun in another sentence.
Since you can never be sure when someone is going to reify one of
your verbs, I like to reify them all by default.  But if you have
a knowledge representation that treats verbs as relations, you can
use the lambda expressions to map back and forth.

>> Therefore, they are truth-functionally
>>    equivalent.  But ontologically, they make different assumptions
>>    about the nature of reality.
>
> But then it must be that the way in which they differ in meaning is not
> accessible to the inference system.  So it is merely philosophical decoration.

I agree that they are truth-functionally equivalent, but there is still
an ontological difference:  In one case, you are quantifying over balls
and saying that the one you picked is red.  In the other case, you are
quantifying over patches of redness and saying that the one you picked
is a ball.  According to Quine's dictum, that makes a difference in
what categories you admit into your ontology.

>>I would say that formula (b) comes
>>    closest to the implicit ontology in ordinary language, since most
>>    languages express balls as nouns and colors as words that modify
>>    nouns.
>
> I think this illustrates your error here: a representation language is not a
> natural language.  But we should argue about this offline...

I agree that a representation language is not a natural language.
But in designing conceptual graphs, I have been looking for logical
structures that have a simple and direct mapping to natural languages.
That is certainly not a guideline that motivated Russell & Whitehead,
but I believe that it can lead you to logical forms that are just as
sound, just as computable, and a lot easier to map to and from NL.

>> But I would also
>>    argue that the system should accommodate any ontology that anyone
>>    might find useful for any purpose.
>
> I agree, and that is why I suggested allowing people to assert arbitrary
> properties of predicates. Why do you suppose that being a type is going to be
> the only property that someone might wish to assert of a predicate? At the
> very least one should allow the user to assert the kind of types they require:
> as I am sure you know, languages can be typed in all sorts of ways.

I certainly agree that people should be allowed to assert attributes
of relations, such as transitive, reflexive, used-only-in-SQL, etc.
But when I say in second-order form "This lambda-expression is being
used to define a type," I then want to put it into the type field in
my first-order assertions.  In other words, I want the second-order
distinction to show up syntactically in my first-order statements.
That leads to the second argument:

>>2. A second reason for a sorted or typed logic is that it makes the
>>    formulas much shorter, more readable, and less error-prone for
>>    humans.
>>...note that both the English sentences and the sorted logic formulas
>>    have the same syntactic form for the...
>
> I think this is largely irrelevant. As I understand it, the point of the
> representational standard is not to be especially perspicuous to human readers;
> but in any case a tiny bit of syntactic icing will make an untyped language
> with type information in it look just like a typed language ( in fact, BE such
> a language). Again, I think you are confusing the language of human interface
> with the language of representation.

I agree that readability by humans is not a primary design goal for KIF,
but it is essential for the languages that map to and from KIF.  And the
distinction is much more than a "tiny bit of syntactic icing".  Whether
you write a type as a predicate or a label on a variable is indeed a
minor point, but the major problem is with those implications that you
get for universal quantifiers.  If you have two typed languages A and B,
and you try to map A -> KIF -> B, it can be very difficult to determine
which implications in KIF came from universal quantifiers in A and should
go back into universal quantifiers in B.  In my example, it was hard
enough for "Every cat is on a mat" but just look what happens when you
try to represent "Every chicken coop has a chicken that is pecked by
every other chicken in the coop."

And while we are talking about quantifiers, I would like to see the
Kleene E!x for exactly one and the Whitehead & Russell E!!x for unique.
W & R introduced them in 1910 in order to simplify set expressions, and
if you try to map complex assertions about sets and plurals into a
language without those quantifiers, the result is not pretty.

>>As someone who has taught many iterations of logic courses...
>
> Yes, I have taught logic to undergraduates too.  In my experience the best way
> to get their minds clear is to teach them simple model theory and have them
> learn to interpret what the axioms mean, rather than try to intuitively map
> from English sentences as most of the textbooks do.  But in any case, the
> kinds of errors that philosophy undergraduates make is hardly relevant to the
> use of a system by educated professionals.

Yes, model theory is an excellent exercise for clearing the mind -- it's
sort of like horseradish for the sinuses.  But there are textbooks
written by "educated professionals" that make exactly the same mistakes.
Of course they know better, but unsorted predicate calculus is a very
error-prone language for professionals as well as novices.  And since
I work for a so-called profit-making institution, I end up talking with
a lot more novices than professionals.

>>3....Philosophically, when you use an unrestricted
>>    quantifier...you allow that quantifier to range over
>>    everything in the universe...but when you restrict it... you have reduced
>>    its range of applicability by many orders of magnitude...
>
> This seems confused. Typically the domains might well be infinite anyway,

Nothing that can be computed or stored on a computer is ever infinite.

> talk of 'orders of magnitude' seems wrong: but in any case, surely you arent
> proposing that we handle quantifiers by somehow running through their domains?

A database system certainly does run through the domains in every query.
If you have indexes on the domains, you can often do the search for some
quantifiers in logarithmic rather than linear time.  But then again, you
would need to have typed quantifiers in order to know what the domains
happened to be.

> If so, how would you suggest handling an assertion like 'The native tribes of
> Africa have always respected their elders" ?

That depends on what you want to do with that information.  If you had
a database of native tribes with a complete history of all their members
and the respect each member had for every other member, you could write
a DB query to see if it was true.  Most likely, however, you would just
store that piece of information and wait until African tribes came up
in a conversation.   At that point, you could use it as background
knowledge when thinking of a clever riposte.

>>4. Finally, there are very strong computational reasons for using
>     sorted logic in theorem proving....
>
> Right, I agree.

That's fine.  If we can agree on what the language should look like,
I don't really care how we reached the agreement.

>> Pat Hayes's suggestion of using a second-order
>> assertion such as relation(red) or type(ball) is not sufficient.  It
>> might allow you to preserve the distinction in mapping CGs to and
>> from KIF, but it would do nothing to make KIF more efficient in
>> theorem proving or less error-prone for humans.
>
> But thats not what the KIF is supposed to be. The KIF is for communication
> between systems, a reference language for knowledge. Human perspicuity has
> different requirements, and theorem-proving efficiency is very much a local
> matter in each system. While it makes sense that one system might be able to
> tell another that it treats some predicates in a certain way - so this
> information should be expressible - there is no reason why the KIF reference
> language itself must be optimised for either of these properties.

I agree that efficiency in theorem proving is not essential for KIF.
And for that matter, translating between any two languages can usually
be done in linear time, whereas theorem proving may take polynomial time
at best, exponential time in general, and infinite time in the worst
case.  So if you want to prove a theorem, it's usually best to translate
the formulas into the language for which you have the fastest theorem
prover.

But as I said earlier, a sorted logic simplifies the formulas and can
make KIF a better intermediate language, especially for translations
to and from other sorted or typed languages.

John Sowa