29
$\begingroup$

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?

$\endgroup$
36
$\begingroup$

Yes, sure. Many typed lambda calculi accept only strongly normalizing terms, by design, so they cannot express arbitrary computations. But a type system can be anything you like; make it broad enough, and you can express all deterministic computations.

A trivial type system that encompasses a Turing-complete fragment of the lambda calculus is the one that accepts every term as well-typed (with a top type). $$\dfrac{}{\Gamma \vdash M : \top}$$

More practically, statically typed functional programming languages have at their core a typed lambda calculus which allows a fixpoint combinator as well-typed. For example, start with the simply typed lambda calculus (or the ML type system or system F or any other type system of your choice) and add a rule that makes some fixpoint combinator like $\mathbf{Y} = \lambda f. (\lambda x. f (x\,x)) (\lambda x. f (x\,x))$ well-typed. $$ \dfrac{\Gamma \vdash f : T \rightarrow T} {\Gamma \vdash \mathbf{Y}\,f : T} \qquad \dfrac{\Gamma \vdash f : T \rightarrow T} {\Gamma \vdash (\lambda x. f (x\,x)) (\lambda x. f (x\,x)) : T} $$ The rules as presented above are rather clumsy, as they make terms like $\mathbf{Y}\,f$ well-typed even though their constituents are not well-typed — they are not fully compositional. A simple fix is to add a fixpoint combinator as a language constant and provide a delta rule for it; then it is a simple matter to have a type system and reduction semantics with type preservation. You do get away from the pure lambda calculus into the realm of lambda calculus with constants. $$\begin{gather*} \dfrac{}{\Gamma \vdash \textbf{fix} : (T \rightarrow T) \rightarrow T} \\ \textbf{fix}\,f \to f (\textbf{fix}\,f) \\ \end{gather*}$$

Sticking to the pure lambda calculus, an interesting type system is the lambda calculus with intersection types.

$$ \dfrac{\Gamma \vdash M : T_1 \quad \Gamma \vdash M : T_2} {\Gamma \vdash M : T_1 \wedge T_2} (\wedge I) \qquad\qquad \dfrac{} {\Gamma \vdash M : \top} (\top I) $$

Intersection types have interesting properties with respect to normalization:

  • A lambda-term can be typed without using the $\top I$ rule iff it is strongly normalizing.
  • A lambda-term admits a type not containing $\top$ iff it has a normal form.

See Characterization of lambda-terms that have union types for an insight as to why intersection types have such a remarkable scope.

So you have a type system that defines a Turing-complete language (since every term is well-typed), and a simple characterization of terminating computations. Of course, since this type system characterizes normalization, it is not decidable.

A remark on the rule names $(\top I)$ and $(\wedge I)$: they have no formal meaning, but they are chosen deliberately. the $I$ stands for “introduction”, because these are introduction rules — they introduce the symbol ($\wedge$ or $\top$) into the type below the line. Dually, you'll find elimination rules, when a symbol appears above the line but not below. For example, the rule to typecheck a lambda expression in the simply-typed lambda calculus is the introduction rule for $\rightarrow$, and the rule to typecheck an application is the elimination rule for $\rightarrow$.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.