definitions

• Mail folder: Interlingua Mail
• Next message: Robert MacGregor: "Re: Moving the Debate on Definitions Forward "
• Previous message: Rolf Stachowitz: "Interlingua for kr-languages "

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