SUO: CL Motivators and the IFF-MT
All,
In a recent message Chris Menzel gave reasons (motivations) for the
elimination in CL of the distinction between predicates and individuals.
I. classification or instantiation
II. functional terms
III. nominalization
The IFF-MT is in accord with this, although of course it handles things
abstractly at the lower metalevel. In terms of the IFF model, the basic
abstract data type of the IFF-MT, these are handled vertically, outside-in,
and horizontally, respectively. An IFF model-theoretic structure (aka model,
or structure or interpretation) can be thought of as a hypergraph of
classifications -- for any model A, in place of nodes there is an entity
classification ent(A) with entity types (sorts of things) and the universe
of discourse as entity instances, and in place of hyperedges there is a
relation classification with relation types and a set of tuples as relation
instances.
I. Instantiation goes right to the classification heart of the IFF-MT, where
classification is the celebrated norm. IFF-MT would prefer to model in terms
of the binary metatheoretic (entity or relation) classification primitive
|=, rendering
(Foo ?x) as ?x |=ent Foo
(Mammal rover) as rover |=ent Mammal
(Class Mammal) as Mammal |=ent Class
(Class Class) as Class |=ent Class
where rover, Mammal and Class are entities in the universe of discourse
(entity instances) and Foo, Mammal, Class are entity types. In short, the
IFF-MT makes no restrictions between the instances and types of a
classification.
II. The IFF-MT handles "function terms" (aka function types) as follows. For
any IFF type language L (this includes the type language underlying an IFF
model):
1. There is a metatheoretic primitive embedding function
func(L) --> rel(L)
from function types to relation types, that preserves arity, signature
and typing. Since terms and expressions form another type language
expr(L) extending L, this includes terms and expressions.
2. There is special subset of functional relations that is the image of
the embedding function.
In short, the IFF-MT maps functions and terms into relations and
expressions.
III. What remains is nominalization.
Nominalization is the process of converting a verb (predicate) into a
abstract noun.
It is a process that is deprecated by the "plain English movement" ;^)
http://www.plainenglish.co.uk/plainenglishguide.html#Anchor-Wha-6089.
Consider the predicate "famous" in the expression
"Martin is famous"
This is represented in the IFF-MT as either an entity type
martin |=ent Famous
or as a unary relation type
(martin) |=rel Famous
In the IFF-MT we allow an overlap between unary relation types and entity
types; perhaps this could be made more explicit with an equivalence
bijection between a distinguished subset of unary relation types and a
distinguished subset of entity types.
Now there seem to be several alternate ways to represent these (depending on
what?):
1. As just another object in the universe of discourse (an entity instance).
The term famous in the expression
"Being famous is the only thing Quentin desires"
that is represented in CL as
(x)(Desires(quentin, x) <-> x = Famous)
must be represented in the IFF-MT as an entity instance, since x varies over
(some part of) the universe of discourse.
So here we would have an entity type or a unary relation type that is also
an entity instance. This is not a problem in a classification, since types
and instances do not need to be distinct. In fact, some classifications have
the same set for both. BTW, if you really need a formal definition for
"individual" in any IFF-MT model A, it would most likely would be the set
difference
indiv(A) ::= univ(A) - typ(ent(A)),
where
univ(A) ::= inst(ent(A)).
2. As a nullary relation type, following Bill Anderson's suggestion of using
a nullary lambda expression definition. .
The term famous in the expression
"Being famous is the only thing Quentin desires"
can be represented in the version of CL beyond the plain vanilla version:
(forall (?x)
(<=>
(desires quentin ?x)
(= ?x (lambda () (famous quentin))))
stating that what Quentin desires is a proposition.
In terms of the IFF-MT, the ?x on the left side of this equivalence must
vary over (some part of) the universe of discourse, whereas the ?x on the
right must be a nullary relation type, since lambda expression definition
are represented as interpretations in the IFF-MT and interpretations map the
relation types of one language to the expressions of a second language.
Currently there are no meta-constraints in the IFF-MT preventing an entity
instance from being a relation type.
As Chris M. mentions, this lambda operator representation still involves a
nominalization -- the lambda operator is precisely the formal analog of the
gerundive and other nominalizing constructions.
* Its use with an empty sequence of variables as in your example is the
representation of sentential nominalization
(i.e., the formation of proposition-denoting nominals from arbitrary
sentences);
* Its use with a nonempty sequence corresponds to general verb phrase
nominalization.
In the IFF-MT nominalization is handled in a two-step process.
1. Convert to span form.
2. Use the nominalization map from relation types to entity types, a map
that converts case links to binary relation types.
The lambda operator above is represented in the IFF-MT as the composition of
IFF interpretation with IFF nominalization.
In summary, the IFF-MT provides mechanisms to handle the three CL motivators
of classification (instantiation), function terms and nominalization.
Robert E. Kent
rekent@ontologos.org