Re: Eliminable Definitions

• Mail folder: Interlingua Mail
• Next message: Robert MacGregor: "definition-t vs. definition-k"
• Previous message: Richard Fikes: "Agenda, Time, and Place for AAAI Meeting -- RSVP Please"
• In-reply-to: Peter Norvig: "Re: Moving the Debate on Definitions Forward "

Date: Mon, 23 Jul 90 14:39 EDT
From: David A. McAllester <dam@ai.mit.edu>
Subject: Re: Eliminable Definitions
To: norvig@teak.berkeley.edu, interlingua@vaxa.isi.edu
In-reply-to: <2857242106-5537126@spaulding>
Message-id: <19900723183909.9.DAM@CROCE.AI.MIT.EDU>

I would like to propose that definitions be ELIMINABLE in the following sense:

If a given function, formula, or object can be denoted by an expression
involving definitions, then there should exist an expression
not involving definitions that denotes the same function formula or object.

For example, definitions are eliminable in the lambda calculus because
every function that can be named using definitions can also be named by
a lambda expression.

If definitions are eliminable then all definitions can be expressed
as (definition <symbol> <expression>) which states that <symbol>
is semantically an abbreviation for <expression>.  This seems to
be a ``KIF style'' definition (definition-k) in the sense that one could
ask for the definition of a given symbol, or ask if John believes
that the symbol Bachelor is defined to be (lambda (x) (and ...)).
Eliminable definitions require the existence of lambda predicates
and lambda functions.

Intuitively, a definiton should provide a unique meaning for the defined
symbol in terms of ``earlier'' or ``more basic'' symbols.  Eliminable
definitions make this unique meaning explicit.

Recursive definitions are a problem.  Eliminable definitions make this
pre-existing problem more explicit.  Existing proposals for recursive
definitions do not specify a unique meaning for the defined symbol in
terms of more basic symbols.

	David McAllester