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$ Jan 11 at 14:17


Your Answer

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

Browse other questions tagged or ask your own question.