Consider a syntactic restriction of the (untyped) $\lambda$-calculus in which an application cannot have another application as an immediate subterm. More precisely, restricted terms ($R,S,...$) and non-application restricted terms ($N,O,...$) are given mutually recursively by the grammar: $$ R, S, ... ::= N \,\mid\, N\,N \\ N, O, ... ::= x \,\mid\, \lambda x.N $$ Equivalently: $$ R, S, ... ::= x \,\mid\, \lambda x. R \,\mid\, x\,y \,\mid\, x\,(\lambda y.R) \,\mid\, (\lambda x.R)\,y \,\mid\, (\lambda x.R)\,(\lambda y.S) $$ It can be checked that restricted terms are closed by $\beta$-reduction under arbitrary contexts.

What is the expressive power of this restricted $\lambda$-calculus (with $\beta$-reduction)? Can it express all computable functions? Remark that this restriction is not strong enough to guarantee termination; e.g. the non-terminating term $\Omega := (\lambda x. x\,x)\,(\lambda x. x\,x)$ is a restricted term.

  • 1
    $\begingroup$ Hi Pablo, the usual route to Turing completeness uses fixpoint combinators. Here, I have a hard time seeing how these may work because the ones I am aware of are all applications, so you can't use them in the restricted framework (if $Y$ is a fixpoint combinator which is an application, when you want to find the fixpoint of an arbitrary term $F$ you'd write $YF$, which is not allowed). So a first question would be whether non-application restricted fixpoint combinators exist... I have no idea, but quite a lot is known about fixpoint combinators, so maybe someone has an answer :-) $\endgroup$ Commented Jan 11, 2022 at 14:17


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.