Complexity of convertibility in simply typed λ-calculus with sums

Question

For the simply typed λ-calculus with only the function type →, the complexity of deciding βη-equivalence is well-understood: it's TOWER-complete (as mentioned here). I expect the same should be true with product types (and surjective pairing); for the upper bound, the strategy would just be to normalize and then compare β-normal η-long forms. However things are much less clear when one adds sum types and strong η: it is already non-trivial to show that convertibility is decidable in that case. (In fact with both sums and the empty type this was only proved in 2016 by Scherer; the introduction to that paper recapitulates the history for the question with just sums.)

So I wonder: is there anything known about the computational complexity of this problem? (For instance, maybe Scherer's proof of a finite model property leads to effective bounds on the size of the models, which would give a bound for a decision procedure?)

Answer 1

(Gabriel Scherer reporting.) I'm not a complexity person, so my answer will be partial. Here is what I can tell in short amount of thinking:

• You mention that the arrow(,product) case is TOWER-complete, but the answer you reference only points out that it is TOWER-hard I think. I checked the reference of Mairson mentioned, it shows that equivalence is not elementary recursive but does not provide an upper-bound. (Maybe there is an easy way to get an upper-bound from the termination argument, do you have a reference? I would not be surprised for example in the complexity was an exponential tower whose height is the maximal arrow-order of types appearing in the typing derivations of the types to compare.)

• The lower-bound argument by Mairson relies entirely on the complexity of computing the beta-short normal form of both terms, not on the cost of computing the beta-short eta-long normal forms from the beta-short normal forms (trivial in absence of sums, linear in the size of the type) or checking that the two beta-short eta-long normal forms are equal. Already in absence of sums, short terms can describe very long computations, and the size of beta-normal form can be exponential in the amount of computation steps. (The complexity of checking the two normal forms is not obvious, but it is clearly polynomial in their sizes, and in fact linear according to recent work.)

• When you add sums, my intuition is that the worst-case time necessary to compute a beta-normal form does not change much. There is no canonical/consensual notion of "beta-short eta-long normal form" anymore, but all definitions used in equivalence procedures are more costly to compute than in absence of sums, with an exponential blowup when going from beta-short to beta-short eta-long -- but maybe this could be avoided with explicit sharing of duplicated subterms. Finally, comparing those beta-short eta-long normal forms should not be more costly than in absence of sums.

My intuition is that equivalence for just sums (in absence of the empty type) can be decided with notions of normal forms (for example in the rewriting-based works of Ghani and Lindley) that "only" have an exponential blowup in the size of the beta-short normal form. If reduction (computing the beta-normal form) is TOWER-hard in the first place, and if my non-expert understanding of TOWER is correct, this means that we remain TOWER-hard without going to a worse complexity class.

The size of the canonical forms used in my work with the empty type (as one notion of beta-short eta-long forms) does not only depend on the size of the input terms, but also on the size of the types in the typing judgment (context and goal). (It may suffer from a blowup that is an exponential tower whose height is the size of the judgment types.) The size of the finite model is related to the size of the canonical forms, it is probably just linear in the size of the canonical forms. (The model instantiates each atomic type $\alpha$ with the finite type $1 + 1 + \dots$ counting the number of neutral subterms of type $\alpha$ in the canonical forms.) This would give you an upper-bound on the size of the model (to summarize: TOWER upper-bound on the number of reduction steps to a beta-normal form, plus an exponential blowup in term size at each step, followed by a size blowup to put the beta-normal forms in canonical form that is tower-of-exponentials in the size of the judgment types).

(Warning: this paragraph is wrong, see below.) But I don't think that this upper-bound is effective: my intuition is that the worst-case number of distinct neutral subterms in the canonical forms does not depend on the size of the beta-normal forms, only on the types in the typing judgment. I would hope that there is an upper bound on the size of the model that does not depend on the reduction length or size of beta-normal forms, only in the judgment types.

Below: the intuition above is wrong, as pointed out in a comment below. You can indeed create a lambda-term of size n that computes a Church integer of size n-hight-tower-of-exponentials, which will constrain about as many neutral subterms.

Answer 2

A higher-level answer, after thinking a bit more about this problem.

The high-level intuition of the finite-model result in my work is that neutrals subterms correspond to how the terms "observe" their context. Even if an atomic type $\alpha$ may be instantiated by a type with an arbitrary number of inhabitants, to distinguish two specific terms $t, u$ you need at most as many elements in $\alpha$ as they make observations of this type $\alpha$ (so: counting the neutral subterms of type $\alpha$ occurring in either of those terms).

This reasoning relies on having a focused normal form, which is stronger than being a $\beta$-short normal form. Focusing prevents "breaking" a neutral with elimination constructs ((match x with inl () -> n | inr -> lam y. y) v, which "hides" the neutral subterm n v), which you could get with commuting conversion rules. In addition, it forces neutral subterms occurring in non-neutral subterms to be of atomic type. For an example of the latter restriction, you cannot write $x : \alpha \to \beta \vdash x : \alpha \to \beta$, you have to write $x : \alpha \to \beta \vdash \lambda (y : \alpha). x~y$. This corresponds, in the sequent calculus, to restricting the axiom rule to atomic types.

In absence of empty types, my intuition is that you cannot get more than TOWER-many neutral subterms in the normal form of a term. (You provided Church naturals as as an example where we can effectively get this many neutral subterms.) Putting a term in focused form may expand its size, but again, not by more than an exponential factor, so we remain TOWER. So the intuition is that the atomic types are instantiated with TOWER-sized finite types.

Then term-based approaches to decide equivalence use different notions of normal forms, often stronger than focusing (in my work: canonical forms, which are a sort of maximal multi-focusing). They can be thought of as approximating, in the syntax of terms, the extensional representation of inhabitants in the set-theoretic model. (For example: Böhm trees are doing exactly this.) You could consider instead, as a concrete syntax for elements in the set-theoretic model, their representations as finite trees, where trees at atomic types $\alpha$ (instantiated by a finite type) are just a natural number, trees for $A*B$ are pairs of trees, trees of $A+B$ are a pair of a boolean and a tree, and trees of $A \to B$ are one node with $A$-many children that are trees of $B$.

You can compare two such trees in time linear over their size (obviously), and this gives you an equivalence algorithm, an upper bound. The size of those trees is, in the worst case, an exponential tower over the size of the atomic type(s). If I understand this right, this suggests that the size of the tree is an exponential tower over an exponential tower over the initial, non-reduced term, which remains an exponential tower.

Now about the empty type: canonical forms in presence of the empty type are a bit strange, because they need to search for proofs that the context is inconsistent. But if you have this extensional view of the elements of the set-theoretic model, adding the empty type does not increase the size of the trees, on the contrary it makes some sub-trees trivial when it appears on the left of an arrow. So my intuition would be that you get the same upper bound.