# Expressive power of lambda-calculus with restricted application

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.

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