# Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule:

<identifier> : <type> = <abstraction>


Where <identifier> is the name of the function, <type> is the function type and <abstraction> is the abstraction to be assigned to the identifier.

Then I add a typing rule that says that when you see an assignment such as the above, you use a temporary type context, in which the declared type (the one in <identifier> : <type>) is associated with the identifier, to type check <abstraction> and then make sure the declared type equals the abstraction's type.

And finally I add another rule that would let me have a list of assignments on top of a lambda term which is the one I'd evaluate, such that all these assignments would be added to the global scope before the term is evaluated.

Seems to me that this alone would make it Turing complete since I'd be able to do stuff like:

stackoverflow: NUM -> NUM = λn:NUM.(stackoverflow n)
(stackoverflow 0)


And at the same time, everything I can define in this language would be "well typed" in the sense that it wouldn't be able to define infinite types (I wouldn't be able to define the Y combinator).

So my questions are, is this really Turing complete? And, am I missing something when I say everything would be "well typed" (like for instance, I could define the Y combinator in a way I haven't yet realized or is there any gotcha in this type system)?

If all you have this definition rule (which doesn't perform any computation), it won't help you. You also need a way to use this definition, like you did in your code example: you implicitly used another language construct, where a definition is available in the next line.

To make things precise, I'll consider a construct which combines a definition with a way to use that definition — a “let … in …” construct (a recursive one, since the function is available while you're defining it).

$$\frac{ \Gamma, f \colon T \vdash M : T \qquad \Gamma, f \colon T \vdash N : T' \qquad }{ \Gamma \vdash (\mathtt{let\:} f \colon T = M \mathtt{\:in\:} N) : T' }$$

From a typing perspective, it doesn't matter whether $T$ is a function type or whether $M$ is an abstraction. These restrictions would ensure that you can find a nice execution semantics (the general rule like phrased above allows recursive definitions like let x : int = x + 1 in x which cannot be usefully evaluated, but you can always define such cases as looping forever).

With this language construct, you do have a Turing-complete language, and you can define a fixpoint combinator (even with the abstraction restriction).

let Y : (int→int)→(int→int)  = λg. g (Y g) in …


$Y$ is a fixpoint combinator over the integers. You can make a similar definition at any type.

You can't make a polymorphic fixpoint combinator. This restriction comes with the simply typed lambda calculus. If you added polymorphism (which in itself does not allow recursive functions, for example System F is normalizing), you could get a polymorphic fixpoint combinator with a suitably generalized recursive let construct.

• Note I said there is also a rule that would let you have a list of assignments on top of the lambda term that would be added to the term's scope (I meant value scope not just type scope, such that they can be evaluated). Isn't this just another way to describe your 'let'?. Also, isn't your typing rule a generalized version of mine that can take any term after the = sign, instead of just abstractions, but limiting it to abstractions would still make it Turing complete? I do like the let idea better for being more general though.
– Juan
Commented Dec 22, 2013 at 17:51
• @JuanLuisSoldi You can define separate rules, I combined them just to make the presentation simpler, but the end result is equivalent. As I wrote in my answer, the restriction to abstractions is sufficient to define a fixpoint combinator (for functions, but that's all you need). Commented Dec 22, 2013 at 17:59