🚀 go-pugleaf

In article  <1992Nov20.210803.5903@tamsun.tamu.edu> 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.  Such a
definition is taken to define the function that satisfies the equation

  f(x) = E

Of course in general there are many such functions, so to get a unique
solution we assume that the above definition defines f as the least
fixed point of the function F defined by

  F(f) := \x.E

In the days of Peano there was no fixed point theory, and even
induction was suspect, so recursion was severely restricted.  And
since the domain (the natural numbers) is totally ordered the result
is that Peano's recursive definitions define unique functions even
without taking the least fixed point (I think).  But restricted forms
of recursion are more properly named with the restriction, as in
"primitive recursion".  As I recall, there are several versions of
Peano arithmetic, each with a slightly different restriction on what
counts as a legal recursive definition.

]Since you say at the beginning of your note what *you* mean by a
]recursive definition, my comment here is essentially a quibble that
]doesn't address the substance of your remarks.  But if you are in fact
]using such a deeply entrenched term in a nonstandard fashion, you
]would seem to be a lot better off calling the notion you've defined
]something else.

I think this just is a difference in cultures (so I'm glad I had a
chance to clarify this).  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.  As you observed
yourself, X can be viewed as a zero-adic function, in which case this
is real functional recursion.

I prefer to generalize in the other direction though, saying that
recursive definitions always define names rather than function
symbols, and that

  f(x) := E

is just a convenient form of the more basic

  f := \x.E

which is just a convenient form of the even more basic

  Def f . f = \x.E
-- 
					David Gudeman
gudeman@cs.arizona.edu