'Active' and 'inactive' lambda terms and Church.

138 Views Asked by At

In the historic survey on lambda calculus and combinators 'History of lambda-calculus and combinatory logic' by Cardone and Hindley, we read:

(Church’s name is often associated with the λI-calculus, the version of λ-calculus in which λx.M is only counted as a term when x occurs free in M. But he did not limit himself so strictly to this version as is often thought. In 1932 and ’33 he allowed non-λI-terms λx.M to exist but not to be “active”, i.e. he did not allow a term (λx.M)N to be contracted when x did not occur free in M, see [Church, 1932, pp. 352, 355]. In his 1940 paper on type theory, where consistency would have been less in doubt, although probably not yet actually proved, he was happy for non-λI-terms to be active [Church, 1940, pp. 57, 60]. Only in his 1941 book did he forbid their very existence [Church, 1941, p. 8].)

Can anyone shed light on why such terms being allowed or not, or being considered 'active' or not is an important issue?

1

There are 1 best solutions below

0
On BEST ANSWER

As I mentioned in my comment, the $\lambda I$ calculus is intimately related to relevance logic. As you can see from that Wikipedia page, this was a topic that interested Alonzo Church. However, this connection is less strong in an untyped context.

The second part of my comment is meant to be suggestive of meta-theoretical properties $\lambda I$ has that the normal $\lambda$ calculus does not. Since $\lambda I$ is still Turing-complete (as we'd say nowadays), these simpler meta-logical properties are convenient. This answer briefly discusses some of those meta-theoretic properties referencing a short discussion of $\lambda I$ in Barendregt's "The Lambda Calculus: Its Syntax and Semantics".

If we drop the requirement that $x$ is free in $M$ in $\lambda x.\!M$ but we compensate by making $(\lambda x.\!M)N$ not reducible (if $M$ and $N$ are irreducible), then it becomes a normal form, and we maintain at least some of the meta-theoretical properties while loosening the syntax a bit. In particular, this change keeps the property, discussed in the aforementioned answer, that if a term $T$ has a normal form, then so do all its subterms. Note that this is not true in the $\lambda$ calculus. For example, with the term $(\lambda x.\!\lambda y.\!y)((\lambda w.\!ww)(\lambda w.\!ww))$ which has the normal form $\lambda y.\!y$ though $(\lambda w.\!ww)(\lambda w.\!ww)$ has no normal form. If we disallow the $\beta$-reduction involving $x$, then the term has no normal form.