Re: Types, sets, and email@example.com
Date: Wed, 28 Apr 1993 13:48:41 +0000
Subject: Re: Types, sets, and relations
> My impression is that the principal
>controversy surrounding the issue of "Type" as a KIF entity is that
>Mike Genesereth doesn't like it. At least, I have yet to hear anyone
>else speak out against inclusion of types in KIF.
OK, try this. There are two problems I can see. The first problem is that
KIF is supposed to be a Standard, so if one includes some sorting
[footnote: I will use 'sort' to refer to somne subset of a first-order
universe, 'type' as in type theory, ie essentially a higher-order
constuct.] mechanism then one wants to get it right. But there are many
possible ones, so which should we use? Heres a quick list:
1. Simple quantifier sorting: domain understood to be partitioned
into disjoint categories over which quantifiers range.
2. As 1., and relation argument-places have assigned sorts (so now
a sort-incoherent expression such as Married(Arthur,New_York) is
3. As 1. except sorts can be nested inside one another, so that the
sorts form a (semi?)lattice structure. This is more expressive, eg now we
can have sorts Man, Woman and Human and quantify over humans.
4. Like 3. except names can be assigned sorts as well. Now
reasoning has to defined more carefully, eg what is the result of unifying
a variable of sort Human with a name of sort Female? Seems like it ought to
be the same name but with its sort restricted to Woman (=Female intersect
Human), but how are these dynamic assignments of sorts to be handled?
5. Like 4., except that argument places of relations have sorts
assigned (ie like 4. and 2.). This is more expressive and certainly better
for translating programming languages into, but is even more complicated in
its reasoning patterns.
6. Like 5. but allowing overloading. Eg Married(x,y) is wellformed
if x is Man and y Woman OR if x is Woman and y Man. This is more natural
still but horrendously complicated in defining validity.
And there are no doubt other possibilities as well. If we allow
lambda-abstraction as well, then the scene becomes even more complicated.
This doesnt argue that any of these are incorrect or not useful, but it
does pose a problem of selection for standards. But the esecond problem I
have with sorting is that I cannot see what it could possibly mean, that
cannot be (easily) defined in an unsorted language. Bob McGregor says that
he (and others) regards 'types and roles' as 'fundamental to a KR system',
but I (and others) have never seen any coherent explanation of WHY they so
regard them. And to say that the systems they feel comfortable with have
them in, is not an adequate explanation. Any beginning of an idea what the
semantics of 'types' is, that makes them other than predicates?
Beckman Institute (217)244 1616 office
405 North Mathews Avenue (217)328 3947 or (415)855 9043 home
Urbana, IL. 61801 (217)244 8371 fax
firstname.lastname@example.org or Phayes@cs.uiuc.edu