I just finished the proof of a property of the simply-typed lambda-calculus that hopefully can serve as a termination argument to decide whether a type has a unique inhabitant.

http://gallium.inria.fr/~scherer/drafts/2-or-more-approximation.pdf

The 10-pages note containing the proof is available, and all comments are warmly welcome – in particular about an already-existing proof of this result, I don’t know about any. The rest of this post is (a HeVeA rendering of) the introduction, motivating the problem and presenting the fact to be proved – or disproved. Feel free to ask yourself whether it is true or false before looking at the full note. The answer is at the last sentence of the introduction (only in the note).

It is interesting that we don’t have much intuition about whether the result is true or false – I changed my mind several times about it, and people asked about it guessed different way. The proof, however, is relatively simple and not particularly technically involved – but I spent a few days simplifying the concepts and the notations.

The correspondence between natural-deduction proofs of propositional intuitionistic logic, usually written as (logic) derivations for judgments of the form Γ ⊢ A, and well-typed terms in the simply-typed lambda-calculus, with (typing) derivations for the judgment Γ ⊢ t : A, is not one-to-one. In typing judgments Γ ⊢ t : A, the context Γ is a mapping from free variables to their type. In logic derivations, the context Γ is a set of hypotheses; there is no notion of variable, and at most one hypothesis of each type in the set. This means, for example, that the following logic derivation

  
 
A ⊢ A
A ⊢ A → A
∅ ⊢ A → A → A

corresponds to two distinct programs, namely λ (x) λ (y) x and λ (x) λ (y) y. We say that those programs have the same shape, in the sense that the erasure of their typing derivation gives the same logic derivation – and they are the only programs of this shape.

Despite, or because, not being one-to-one, this correspondence is very helpful to answer questions about type systems. For example, the question of whether, in a given typing environment Γ, the type A is inhabited, can be answered by looking instead for a valid logic derivation of ⌊Γ⌋ ⊢ A, where ⌊Γ⌋ denotes the erasure of the mapping Γ into a set of hypotheses. If we can independently prove that only a finite number of different types need to be considered to find a valid proof (this is the case for propositional logic because of the subformula property), then there are finitely many set-of-hypothesis Δ, and the search space of sequents Δ ⊢ B to consider during proof search is finite. This property is key to the termination of most search algorithms for the simply-typed lambda-calculus. Note that it would not work if we searched typing derivations Γ ⊢ t : A directly: even if there are finitely many types of interest, the set of mappings from variables to such types is infinite.

In our current brand of work, we are interested in a different problem. Instead of knowing whether there exists a term t such that Γ ⊢ t : A, we want to know whether this term is unique – modulo a given notion of program equivalence. Intuitively, this can be formulated as a search problem where search does not stop to the first candidate, but tries to find whether a second one (that is nonequivalent as a program) exists. In this setting, the technique of searching for logic derivations ⌊Γ⌋ ⊢ A instead is not enough, because a unique logic derivation may correspond to several distinct programs of this shape: summarizing typing environments as set-of-hypotheses loses information about (non)-unicity.

To better preserve this information, one could keep track of the number of times an hypothesis has been added to the context, representing contexts as multisets of hypotheses; given a logic derivation annotated with such counts in the context, we can precisely compute the number of programs of this shape. However, even for a finite number of types/formulas, the space of such multisets is infinite; this breaks termination arguments. A natural idea is then to approximate multisets by labeling hypotheses with 0 (not available in the context), 1 (added exactly once), or 2 (available two times or more); this two-or-more approximation has three possible states, and there are thus finitely many contexts annotated in this way.

The question we answer in this note is the following: is the two-or-more approximation correct? By correct, we mean that if the precise number of times a given hypothesis is available varies, but remains in the same approximation class, then the total number of programs of this shape may vary, but will itself remain in the same annotation class. A possible counter-example would be a logic derivation Δ ⊢ B such that, if a given hypothesis A ∈ Δ is present exactly twice in the context (or has two free variables of this type), there is one possible program of this shape, but having three copies of this hypothesis would lead to several distinct programs.

Is this approximation correct? We found it surprisingly difficult to have an intuition on this question (guessing what the answer should be), and discussions with colleagues indicate that there is no obvious guess – people have contradictory intuitions on this.