NetNews Usenet Archive 1992 #27/NN_1992_27.iso/spool/sci/logic/2172

Internet Message Format | 1992-11-24 | 2.5 KB

Path: sparky!uunet!spool.mu.edu!sdd.hp.com!usc!cs.utexas.edu!tamsun.tamu.edu!tamsun.tamu.edu!not-for-mail
From: [e-mail] (Chris Menzel)
Newsgroups: sci.logic
Subject: Re: recursive definitions and paradoxes
Date: 23 Nov 1992 23:38:30 -0600
Organization: Texas A&M University, College Station, TX
Lines: 46
Message-ID: <[e-mail]>
References: <[e-mail]>
NNTP-Posting-Host: tamsun.tamu.edu

In article <[e-mail]> [e-mail] (David Gudeman) writes:
>In article  <[e-mail]> Chris Menzel writes:
>]
>]It seems to me, David, that you cause unnecessary confusion by calling
>]these and, as you do later in your post, the definition of the Russell
>]set recursive definitions.  By my lights, the usual understanding is
>]that a recursive definition is one in which a function f is defined on
>]a well-founded relation R such that for each object b in the field of
>]R, f(b) is defined in terms of f(x) for x such that xRb.
>
>This is a limited form of recursion, not the general form that is used
>in the lambda calculus and combinatory calculus.  In general a
>function definition
>
>  f(x) := E
>
>(where ':=' is usually an equals with a triangle, a dot, or another
>bar over it) is recursive if f appears on the right-hand side.

Well I've looked in Fitch's book on Combinatory Logic, Curry's
mathematical logic text, and Barendregt's article in the Handbook of
Mathematical Logic on the untyped lambda calculus and can find no such
definition.  Fitch does refer to the type of definition you refer to
in the section of his book that immediately follows the section on
recursion, but calls them "self-referential" or "impredicative" or
something to that effect (I left the book in my office and can't
recall the exact term at the moment).  At any rate, as far as I could
see, the term 'recursive' is used only for recursive definitions in
the sense I gave above or for recursive functions in the usual sense.
Do you happen to have any references to support your usage?

>My notion of recursion should be quite
>familiar to anyone who knows the modern work in the lambda calculus.
>Within the tradition I am familiar with, I can't imagine what else you
>would call a definition X := E where X occurs in E and the sentence
>is taken to define X as the unique solution to X = E.

How about, say, "impredicative" or "self-referential", for example?

>                    David Gudeman
>[e-mail]

--Chris Menzel
  Philosophy Department
  Texas A&M University