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

Question

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)?

Answer 1

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.