# definitions

David A. McAllester <dam@ai.mit.edu>
```Date: Wed, 11 Jul 90 10:22 EDT
From: David A. McAllester <dam@ai.mit.edu>
Subject: definitions
To: interlingua@vaxa.isi.edu
Cc: pwtc!tc.pw.com!fikes@labrea.stanford.edu
Message-id: <19900711142238.4.DAM@CROCE.AI.MIT.EDU>
```
```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)))
(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)))
(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).

(the-least R
(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

(define descendant-of
(the-least R
(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.

David McAllester

```