Types vs. monadic email@example.com
Date: Mon, 3 Feb 92 18:43:28 EST
Cc: interlingua@ISI.EDU, srkb@ISI.EDU, firstname.lastname@example.org
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
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)).
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)(Ey)(cat(x) -> (mat(y) & 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
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.