Problem # 15

Submitted by Alex Simpson
Date: 1995
Statement. Is the equational theory of typed $λ$ -calculus with ﬁnite sums the maximum consistent typically-ambiguous congruence? $\text{[math]}$
Problem Origin. The problem was posed by Alex Simpson and probably others.

Extend the simply-typed $λ$ -calculus with syntax for ﬁnite product and sum types. This has a standard notion of $β$ -equality, $= β$ . By $= βη$ we mean the equational theory induced semantically by interpretations in bicartesian closed categories (cartesian closed categories with ﬁnite coproducts ). It is not hard to axiomatize this equality. Following [Statman, 1983], a typed congruence relation $~$ , is said to be typically ambiguous if it is preserved under type substitutions; that is: $s ~ t: σ$ implies $* * * s ~ t : σ$ , where the $* (⋅)$ transformation performs a substitution of types for atomic types. The main question is:

A (possibly) weaker version of the question is simply: is it the case that the only typically-ambiguous congruence relation properly extending $= βη$ is the inconsistent relation? There are various semantic equivalents to and consequences of a positive answer to this latter question. An equivalent statement is: given any bicartesian-closed category $𝒞$ that is not a preorder, the equational theory induced by all interpretations in $𝒞$ is exactly $=βη$ ; see [Simpson, 1995] for a similar equivalence for the calculus without coproducts. In fact, it is enough to consider only the category of ﬁnite sets; that is, another equivalent is: the equational theory induced by interpretations in the category of ﬁnite sets is exactly $=βη$ . (To show that this implies that $= βη$ is maximal amongst consistent typically-ambiguous congruences, one encodes the category of ﬁnite sets within the type theory using ﬁnite coproducts of the unit type.) The last equivalent above is simply the ﬁnite model property for $= βη$ , a standard consequence of which is decidability. A related result, the decidability of $= βη$ in the case of non-empty coproducts is known from [Ghani, 1995] and [Altenkirch et al., 2001]. Again for non-empty sums only, the completeness of $= βη$ with respect to interpretations in the category of sets was shown by [Dougherty and Subrahmanyam, 2000]; their argument makes essential use of inﬁnite sets. A fragment of completeness relative to ﬁnite sets has been shown by [Altenkirch and Uustalu, 2004], who established completeness and decidability results for the extension of typed $λ$ -calculus with a base type of booleans, but without other atomic types.

References for # 15

[Altenkirch et al., 2001] Altenkirch, T., Dybjer, P., Hofmann, M., and Scott, P. (2001). Normalization by evaluation for typed lambda calculus with coproducts. In Logic in Computer Science, pages 303–310. IEEE Computer Society Press.

[Altenkirch and Uustalu, 2004] Altenkirch, T. and Uustalu, T. (2004). Normalization by evaluation for $λ →2$ . In Functional and Logic Programming, volume 2998 of Lecture Notes in Computer Science, pages 260–275.

[Dezani-Ciancaglini and Plotkin, 1995] Dezani-Ciancaglini, M. and Plotkin, G., editors (1995). Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science. Springer-Verlag.

[Dougherty and Subrahmanyam, 2000] Dougherty, D. and Subrahmanyam, R. (2000). Equality between functionals in the presence of coproducts. Information and Computation, 157:52–83.

[Ghani, 1995] Ghani, N. (1995). Beta-eta equality for coproducts. In [Dezani-Ciancaglini and Plotkin, 1995], pages 171–185.

[Simpson, 1995] Simpson, A. (1995). Categorical completeness results for simply-typed $λ$ -calculus. In [Dezani-Ciancaglini and Plotkin, 1995], pages 414–427.

[Statman, 1983] Statman, R. (1983). $λ$ -deﬁnable functionals and $β η$ conversion. Archiv für Mathematische Logik und Grundlagenforschung, 23:21–26.