definitionsDavid A. McAllester <email@example.com>
Date: Wed, 11 Jul 90 10:22 EDT
From: David A. McAllester <firstname.lastname@example.org>
I will be at the AAAI interlingua meeting and decided to would send out
some food for thought.
I am concerned about definitions. Suppose we define descendant-of as
follows (the definition is in Ontic syntax, but it should be
translatable into the interlingua).
(define (a (descendant-of x))
(either (a (child-of x))
(a (descendent-of (a (child-of x))))))
Now suppose I assert
(is (a (child-of (a human)))
(This is equivalent to (forall x (human x) -> forall y (child-of x y) -> (human y))).
Intuitively, I should now be able to prove
(is (a (descendant-of (a human)))
Unfortunately, under the proposed treatment of definitions, this last
statement does NOT follow from the definition and the statement that
every child of a human is a human. More specifically, consider the
two first order formulas
1) forall x y
((descendant-of x y)
<-> ((child-of x y)
or (exists z
(descendent-of x z)
and (child-of z y))))
2) (forall x (human x) -> (forall y (child-of x y) -> (human y)))
There exists a first order model satisying both 1) and 2) such that some
human has a descendent that is not a human. Therefore, it would be
UNSOUND to conclude that every descendent of a human is human.
In general, the obvious first order treatment of recursive definitons is
inadequate. Under Ontic's semantics for recursive definitions it does
follow that every descendent of a human is human. Unfortunately, I am
unable to translate my Ontic definitions into the interlingua (or into
first order logic in general).
I would recommend using the mu-calculus to represent recursive
definitions. The predicate descendant-of can be represented in the
mu-calculus as the following mu-expression (this is a predicate
expression, not a definition).
(R = (lambda (x y) (or (child-of x y)
(exists z (R x z) and (child-of z y))))))
In the traditional syntax for the mu-calculus, the operator
``the-least'' is replaced by ``mu'' which is used as a fixed-point
operator similar to the Y operator in the lambda calculus. However, the
above syntax makes the semantics clearer. The symbol R is a
second-order bound variable of the expression. One can then define
descendant-of as a simple abbreviation for a mu expression
(R = (lambda (x y)
(or (child-of x y)
(exists z (R x z) and (child-of z y)))))))
In general, I think a definition should always be a simple introduction
of a symbol as an abbreviation for an expression. I don't think there
is any problem with allowing lambda predicates, lambda functions,
and mu-expressions in the interlingua.