5
$\begingroup$

In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126). Later in the book he shows how to construct models of all these types. (I'm pretty new to all of this, but I assume this is a pretty standard system.)

It looks as though it is not possible to extend this system with a 0 type for the following reason:

Let $\sigma$ be $\mu t.t\to 0$. $\mbox{unfold}: \sigma \to \sigma \to 0$ and $\mbox{fold}: (\sigma \to 0)\to \sigma$. Then $W(\mbox{unfold})(\mbox{fold}(W(\mbox{unfold}))): 0$, where $W = \lambda xy.xyy$.

From this you can prove all equations between terms (e.g. from the existence of a closed term $t:0$, $\lambda x.t:A \to 0$ is an isomorphism between any type $A$ and $0$.)

A natural thought would be to work in a linear or affine type theory where the $W$ combinator isn't allowed, and which therefore might allow solutions to type equations like $\sigma = \sigma \to 0$.

My questions is: Is the resulting type theory consistent, and can anyone explain to me how to go about constructing models? (References would also be welcome, but the papers I've looked at so far have generally presupposed more knowledge than I have).

$\endgroup$
8
$\begingroup$
  1. First, note that nothing turns on the presence or absence of the empty type: if you have a nonlinear calculus with function types and unrestricted recursive types, then it is inconsistent. Indeed, your derivation works regardless of the type of the answer -- the very same term you have works for $\mu a.\; a \to X$ for any $X$.

    This is known as Curry's Paradox, and is also known as the Y combinator. There is a nice discussion of this in Greg Restall's paper Curry's Revenge: the costs of non-classical solutions to the paradoxes of self-reference.

  2. Next, your observation that the fixed point combinators rely upon contraction is astute. Curry's paradox depends on all three of contraction, unrestricted recursive types, and a function space, and removing any one of them suffices to block it.

    For example, I asked a very similar question here a few years back, and learned that multiplicative-additive linear logic with recursive types is not Turing-complete. This is called the "Small Normalization Theorem" (Theorem 4.22) in Girard's original paper on linear logic.

  3. You can still construct models of this language (with or without units) using domain theory. The main technical difficulty is the interpretation of recursive types. I don't know a good introduction to how to solve recursive domain equations. I learned it from Plotkin and Smyth's The Category-Theoretic Solution of Recursive Domain Equations, but that was really not a good tutorial for me: I needed a fair amount of help to understand it. The critical intuitions are all there, but it's quite dense. Maybe Abramsky and Jung's handbook chapter might be more accessible? I don't really have any great suggestions.

$\endgroup$
  • $\begingroup$ "I don't know a good introduction to how to solve recursive domain equations." I agree and it's really unacceptable given how old the techniques are at this point. I would recommend Abramsky & Jung but also "Domains and Lambda Calculi" (Curien and Amadio) helped me to understand the constructions. $\endgroup$ – Max New Jun 2 '17 at 20:07
  • 1
    $\begingroup$ Thanks Neel. Regarding 1: I should have been clearer. There are two senses of inconsistency that should be kept apart: it's true that the propositional logic characterized by the inhabited types is inconsistent whether or not you have a 0 type. But in the system Mitchell describes you can't prove all equations between terms. The version with the 0 type does prove all equations: that's what I was worried about. $\endgroup$ – Andrew Bacon Jun 2 '17 at 21:59
  • $\begingroup$ Regarding 3: similarly, the cpo models with the 0 type are presumably going to all be trivial (each type with 1 element). (Because in non-trivial Henkin models, 0 must be interpreted as the empty set. If $\sigma$ is empty, then $\sigma \to 0$ is non-empty, and conversely, so $\sigma = \sigma \to 0$ has no solution.) I will definitely check out those references for my own edification, but they seem to be using CPOs. My hope was to find solutions of $\sigma = \sigma \to 0$ (and other domain equations) in models of linear or affine type theory. $\endgroup$ – Andrew Bacon Jun 2 '17 at 22:11
  • $\begingroup$ Regarding 2: That looks interesting. I'm not very familiar with these things: Is there some connection between Turing completeness and the set of inhabited types being inconsistent? $\endgroup$ – Andrew Bacon Jun 2 '17 at 22:51
  • 1
    $\begingroup$ Personally, I found Bos&Hemerik - "An Introduction to the Category-theoretic Solution of Recursive Domain Equations" very useful, since it really shows the full proof step-by-step. $\endgroup$ – chi Jun 5 '17 at 16:56

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.