Types vs. monadic relations

Message-id: <9202032346.AA11346@quark.isi.edu>
Date: Mon, 3 Feb 92 18:43:28 EST
From: sowa@watson.ibm.com
To: macgregor@ISI.EDU
Cc: interlingua@ISI.EDU, srkb@ISI.EDU, cg@cs.umn.edu
Subject: Types vs. monadic relations

In response to your question,

> What do you consider to be the semantic difference between
> a "type" and a "monadic relation"?  Why should we care?

I believe that there are several reasons, some philosophical and
some computational:

 1. Consider the phrase "a red ball".  In an unsorted or untyped
    logic, you could represent that statement by the following

       (Ex)(red(x) & ball(x)).

    This puts the red(x) and ball(x) predicates on exactly the same
    ontological footing.  In a sorted logic, there are four ways to
    express that information, depending on which of the two predicates
    represent types or monadic relations:

    a)   (Ex)(red(x) & ball(x)).

    b)   (Ex:ball)red(x).

    c)   (Ex:red)ball(x).

    d)   (Ex:red)(Ey:ball)x=y.

    Formula (a) asserts that x is of the universal or unrestricted type
    at the top of the type hierarchy and that it has the properties of
    redness and ballness.  Formula (b) asserts that x is an instance
    of an object called a ball, and it has the property of redness.
    Formula (c) asserts that x is a patch of redness that has the
    property of ballness.  Formula (d) asserts that x is a patch of
    redness, y is an object ball, and x and y are the same object.

    In terms of truth values, all four formulas are true or false under
    exactly the same conditions.  Therefore, they are truth-functionally
    equivalent.  But ontologically, they make different assumptions
    about the nature of reality.  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.  However, there may be some philosophical purposes for which
    one might prefer any of the other four statements.

    There are very strong psychological, linguistic, and philosophical
    reasons for saying that there is something "natural" about viewing
    the world in terms of objects with properties.  But I would also
    argue that the system should accommodate any ontology that anyone
    might find useful for any purpose.  Therefore, I believe that the
    logic should distinguish types syntactically, but allow the knowledge
    engineer to decide what the types should be for any particular

 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.  Consider the sentences "Every cat is on a mat" and
    "Some cat is on a mat" in both an unsorted and a sorted logic:

       (Ax:cat)(Ey:mat) on(x,y).

       (Ax)(Ey)(cat(x) -> (mat(y) & on(x,y)).

       (Ex:cat)(Ey:mat) on(x,y).

       (Ex)(Ey)(cat(x) & mat(y) & on(x,y)).

    First note that the statements in sorted logic are shorter and
    simpler than the equivalent statements in unsorted logic.  Second,
    note that both the English sentences and the sorted logic formulas
    have the same syntactic form for the universal and existential cases,
    but that in the unsorted logic, the universal quantifier requires an
    implication and the existential quantifier requires a conjunction.

    As someone who has taught many iterations of logic courses, I can
    assure you that the omission of the implication with universal
    quantifiers is one of the most frequent causes of student errors.
    And not only students make that mistake -- there are textbooks on
    logic by very good logicians and computer scientists that carelessly
    omit the implication with the universal.   If they had been using a
    sorted logic, they would not have made that mistake.

 3. A third reason for sorted logic has philosophical, linguistic, and
    computational support.  Philosophically, when you use an unrestricted
    quantifier, such as (Ax), you allow that quantifier to range over
    everything in the universe, possibly over types that no one has ever
    imagined; but when you restrict it, as in (Ax:cat), you have reduced
    its range of applicability by many orders of magnitude and limit it
    to things that you could reasonably identify as cats.  Linguistically
    quantifiers in natural languages are always used to modify terms
    (usually nouns or noun phrases, but sometimes verbs or adjectives)
    that explicitly limit the range of quantification.  Computationally,
    it is far more efficient to compute the denotation of a formula in
    terms of a model if its quantifiers are limited to small subsets
    of the universe of discourse than if they are free to range over
    anything at all.

 4. Finally, there are very strong computational reasons for using
    sorted logic in theorem proving.  Len Schubert's steamroller
    problem is a famous example of a rather simple problem that can
    be handled far more efficiently in a sorted logic than in an
    unsorted logic.

    For a collection of papers on sorted logics and theorem proving
    techniques using them, see

    K. H. Blaesius, U. Hedstueck, & C-R. Rollinger (1990) _Sorts and
    Types in Artificial Intelligence_, Lecture Notes in Artificial
    Intelligence, vol. 418, Springer Verlag.

Note, by the way, that 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.

> Also, should I assume that the distinction between "role" and
> "binary relation" (whatever it may be) is similar?

That depends on the system.  If you had a system that used both terms
"role" and "binary relation", then that system would presumably make
some sort of distinction between them.  But if you use "role" in one
system for what you might use the term "binary relation" in some other
system, then the only difference would be in the choice of words.

Note that the distinction between types and monadic relations is
maintained in both sorted predicate calculus and in conceptual graphs.
Furthermore, translations back and forth between the two systems
consistently preserve that distinction.

John Sowa