3
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 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$
    – Damiano Mazza
    Jan 11, 2022 at 14:17

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.