3
$\begingroup$

Church numerals in lambda calculi are terms of the form $\lambda f x . f(f(\cdots f(x) \cdots ))$. In the simply typed lambda calculus, these numerals must have types of the form $(A\to A) \to A \to A$. Does the converse hold? Must any term of type of the form $(A\to A) \to A \to A$ be a Church numeral? Similarly for Church booleans?

I can't think of any counterexamples and I can't quite see how to set up the induction if true.

$\endgroup$
  • $\begingroup$ I think you might need to exploit how simply typed lambda calculus terms all have a canonical normalize form. $\endgroup$ – DanielV Nov 16 '17 at 5:43
4
$\begingroup$

It depends on what you mean by "of the form". Trivially, I can write $\lambda fx.(\lambda y.y)f x$ say. Of course, this beta-reduces to $\lambda fx.fx$. So, as DanielV points out, you need to consider only normal forms or lambda terms up to $\beta\eta$-equivalence or something similar.

The next issue is whether $A$ is arbitrary. For example, if $A$ happens to be $B\to B$ say, then $\lambda fx.(\lambda y.y)$ is a well-typed lambda term, but not of the form of any Church numeral. However, if $A$ is an arbitrary, unknown type then there is no way to produce a term of type $A$ (indeed there may not be any) except by using $x$ and $f$. In this case, the only normal form terms of the type are Church numerals. This can be formalized by considering the polymorphic lambda calculus (aka System F), and asking about the normal form terms of $\forall A.(A\to A)\to A\to A$. It is a well known but not trivial fact that any strictly positive algebraic data type can be systematically encoded into System F preserving the expected properties. This encoding is called the Böhm-Berarducci encoding. This article by Oleg Kiselyov may serve as a more accessible introduction.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.