**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