At 15:37 +0100 1999/06/03, Peter Hancock wrote:
>By the way, I'm not wild about Hans's term "constant variables". In
>Church's lambda-I calculus, you aren't allowed abstractions where the
>bound variable doesn't occur in the body. It would be better to
>distinguish linear (exactly once), affine (at most once), and general
>abstraction. All 0, 1, * and ^ are affine, but + is not. All 1, *
>and ^ are linear, but 0 is not. Reduction of affine combinators
>needs essentially no new space, I think.
I think Church's restriction that a bound variable must occur in the bound
expression is more technical in nature, but not essential in a practical
application. The thing is that the lambda-calculus does not come with an
interpretation of the symbols. So if one adds (in an interpreation of the
lambda-calculus) a symbol O such that O(f)(x) = x, then
lambda x.O(x)(f)
where f does not contain x is a legal expression in Church's calculus, but
this expresion becomes equivalent to
lambda x.f
when O(x)(f) = f is substituted.
Here O lambda a b . b, as before.
Hans Aberg
* Email: Hans Aberg <mailto:[EMAIL PROTECTED]>
* Home Page: <http://www.matematik.su.se/~haberg/>
* AMS member listing: <http://www.ams.org/cml/>
