**Mail folder:**SRKB Mail**Next message:**sowa@watson.ibm.com: "Standards"**Previous message:**Gio Wiederhold: "Re: Report on ANSI X3H4 meeting"**Reply:**YOUR NAME HERE: "Re: 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

Bob, 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 formula: (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 application. 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