The Yoneda Reduction of Polymorphic Types (Extended Version)

TL;DR

This paper investigates Yoneda-inspired type isomorphisms in System F, enabling quantifier elimination through a process called Yoneda reduction, with applications in counting inhabitants and program equivalence.

Contribution

It introduces Yoneda reduction as a novel type rewriting technique that eliminates quantifiers in polymorphic types, extending the understanding of type isomorphisms in System F.

Findings

Yoneda reduction can eliminate quantifiers from polymorphic types.

Conditions for full quantifier elimination are established.

Applications include counting inhabitants and checking program equivalence.

Abstract

In this paper we explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than beta-eta-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types, that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to compute program equivalence in some fragments of System F.

Equations

$$\forall X.(A\Rightarrow X)\Rightarrow (B\Rightarrow X)\equiv B\Rightarrow A\forall X.(X\Rightarrow A)\Rightarrow (X\Rightarrow B)\equiv A\Rightarrow B$$

$$\forall X.X\Rightarrow X\Rightarrow A$$

$$\forall X.(A\Rightarrow X)\Rightarrow (B\Rightarrow X)\Rightarrow C$$

$$\forall X.(X\Rightarrow A)\Rightarrow (X\Rightarrow B)\Rightarrow D$$

$$\forall X.(A_{0}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\ \equiv\ B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto A_{0}\right\rangle$$

$$\forall X.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow A_{0})\Rightarrow B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\ \equiv\ B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto A_{0}\right\rangle$$

$$\displaystyle\forall X.(A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle$$

$$\displaystyle\forall X.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow A\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle)\Rightarrow C\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle$$

$$\boxed{\begin{matrix}\forall X.\forall\vec{Y}.\Big{\langle}\forall\vec{Z}_{k}.\langle A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\rangle_{j}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Big{\rangle}_{k}\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\quad\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}\quad\forall\vec{Y}.B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\{\mu X.\}\sum_{k}\left(\exists\vec{Z}_{k}.\prod_{j}A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right)\right\rangle\\ \ \\ \forall X.\forall\vec{Y}.\left\langle\forall\vec{Z}_{k}.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow A_{j}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\right\rangle_{k}\Rightarrow B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\quad\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}\quad\forall\vec{Y}.B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto\{\nu X.\}\forall\vec{Z}_{k}.\prod_{j}A_{j}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\right\rangle\end{matrix}}$$

$$\boxed{\begin{array}{c}A\Rightarrow (B\Rightarrow C)\equiv B\Rightarrow (A\Rightarrow C)\\ \\ \forall X.\forall Y.A\equiv \forall Y.\forall X.A\\ \\ A\equiv \forall X.A(X\notin FV(A))A\Rightarrow \forall X.B\equiv \forall X.A\Rightarrow B\end{array}}$$

$$\boxed{\begin{array}{c}A\times 1\equiv A1\Rightarrow A\equiv A\\ \\ A\times (B\times C)\equiv (A\times B)\times CA\times B\equiv B\times A\\ \\ (A\times B)\Rightarrow C\equiv A\Rightarrow (B\Rightarrow C)\forall X.A\times B\equiv \forall X.A\times \forall X.B\\ \\ A+0\equiv AA\times 0\equiv 00\Rightarrow A\equiv 1\\ \\ A+(B+C)\equiv (A+B)+CA+B\equiv B+A\\ \\ A\times (B+C)\equiv (A\times B)+(A\times C)(A+B)\Rightarrow C\equiv (A\Rightarrow C)\times (B\Rightarrow C)\end{array}}$$

$$\boxed{\begin{matrix}\mu X.A\equiv\nu X.A\equiv A\quad(X\notin FV(A))\\ \\ \mu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\equiv A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\mu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right\rangle\qquad\nu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\equiv A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\nu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right\rangle\end{matrix}}$$

$$\begin{array}{rl}t& =\lambda y_1{y}_2.y_1{u}_{11}{u}_{12}\\ t& =\lambda y_1{y}_2.y_2{u}_{21}{u}_{22}\end{array}$$

$${\Phi }_X^X(t)$$

$${\Phi }_Y^X(t)$$

$${\Phi }_{(C\Rightarrow D)}^X(t)$$

$${\Phi }_{(\forall X.C)}^X(t)$$

$$\forall X.\Big{\langle}\forall\vec{Y}_{k}.\big{\langle}A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\big{\rangle}_{j}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Big{\rangle}_{k}\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\qquad\qquad\forall X.\Big{\langle}\forall\vec{Y}_{j}.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow A_{j}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\Big{\rangle}_{j}\Rightarrow B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle$$

$$\begin{array}{rl}{X}^{♯}& =X\\ (A\to B{)}^{♯}& =A^{♯}\to B^{♯}\\ (\forall X.A{)}^{♯}& =\forall X.A^{♯}\\ 1^{♯}& =\forall X.X\to X\\ 0^{♯}& =\forall X.X\end{array}$$

$$\begin{split}(A\times B)^{\sharp}&=\forall X.(A^{\sharp}\to B^{\sharp}\to X)\to X\\ (A+B)^{\sharp}&=\forall X.(A^{\sharp}\to X)\to(B^{\sharp}\to X)\to X\\ (\mu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle)^{\sharp}&=\forall X.(A^{\sharp}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow X)\Rightarrow X\\ (\nu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle)^{\sharp}&=\forall Y.(\forall X.X\Rightarrow(X\Rightarrow A^{\sharp}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle)\Rightarrow Y)\Rightarrow Y\end{split}$$

$$x^{♯}$$

$$(\lambda x.t{)}^{♯}$$

$$(tu{)}^{♯}$$

$$(\Lambda X.t{)}^{♯}$$

$$(tB{)}^{♯}$$

$${\star }^{♯}$$

$$({\xi }_{C}t{)}^{♯}$$

$$⟨t,u{⟩}^{♯}$$

$$({\pi }_i^{C}t{)}^{♯}$$

$$({\iota }_{i}t{)}^{♯}$$

$$({\delta }_C(t,y.u_1,y.u_2{)}^{♯}$$

$$({\mathsf{in}}_{P}t{)}^{♯}$$

$$({\mathsf{fold}}_P(t){)}^{♯}$$

$$({\mathsf{out}}_{P}t{)}^{♯}$$

$$({\mathsf{unfold}}_P(t){)}^{♯}$$

$${\mathtt{c}}_X[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{B\to C}}[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\forall Y.B}}[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{B\times C}}[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{1}}[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{B+C}}[x]$$

$$\displaystyle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{0}}[x]$$

$$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.B}[x]$$

Full text

1. 1 Introduction

2. 1.1 A Type-Rewriting Theory of Polymorphic Types

3. 1.2 Program Equivalence in System F with Finite Characteristic

4. 2 Yoneda Type Isomorphisms

5. 3 Counting Type Inhabitants with Yoneda Type Isomorphisms

6. 4 From Polymorphic Types to Polynomial Trees

7. 4.1 A $\beta\eta$-invariant representation of $\mathsf{\Lambda 2}$-types

8. 4.2 Polynomial Trees

9. 5 Yoneda Reduction and the Characteristic of a Polymorphic Type

10. 5.1 Yoneda Reduction

11. 5.2 The Coherence Condition

12. 5.3 The Characteristic

13. 6 Preliminaries on Theories of Program Equivalences

14. 7 System F with Finite Characteristic

15. 7.1 The Systems $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$

16. 7.2 Embedding $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ into Monomorphic Systems

17. 7.3 The equivalence of $\mathsf{\Lambda 2^{\kappa\leq 0}}/\mathsf{\Lambda 2^{\kappa\leq 1}}$ with $\mathbb{B}/\mu\mathbb{B}$

18. 7.4 Program Equivalence in $\mathsf{\Lambda 2^{\kappa\leq 0}}$ is decidable.

19. 7.5 Program Equivalence in $\mathsf{\Lambda 2^{\kappa\leq 1}}$ is undecidable.

20. 8 Program Equivalence and Predicativity

21. 9 Conclusion

22. A The $\varepsilon$-Theory and the Yoneda Isomorphisms

23. B $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and $\mu\mathbb{B}$ are full subcategories of $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$

1 Introduction

The study of type isomorphisms is a fundamental one both in the theory of programming languages and in logic, through the well-known proofs-as-programs correspondence: type isomorphisms supply programmers with transformations allowing them to obtain simpler and more optimized code, and offer new insights to understand and refine the syntax of type- and proof-systems.

Roughly speaking, two types $A,B$ are isomorphic when one can transform any call by a program to an object of type $A$ into a call to an object of type $B$, without altering the behavior of the program. Thus, type isomorphisms are tightly related to theories of program equivalence, which describe what counts as the observable behavior of a program, so that programs with the same behavior can be considered equivalent.

The connection between type isomorphisms and program equivalence is of special importance for polymorphic type systems like System F (hereafter $\mathsf{\Lambda 2}$). In fact, while standard $\beta\eta$-equivalence for $\mathsf{\Lambda 2}$ and the related isomorphisms are well-understood [12, 14], stronger notions of equivalence (as those based on parametricity or free theorems [43, 22, 1]) are often more useful in practice but are generally intractable or difficult to compute, and little is known about the type isomorphisms holding under such theories.

A cornerstone result of category theory, the Yoneda lemma, is sometimes invoked [7, 19, 9, 41, 20] to justify some type isomorphisms in $\mathsf{\Lambda 2}$ like e.g.

[TABLE]

which do not hold under $\beta\eta$-equivalence, but only under stronger equivalences. Such isomorphisms are usually justified by reference to the interpretation of polymorphic programs as (di)natural transformations [7], a well-known semantics of $\mathsf{\Lambda 2}$ related to both parametricity [32] and free-theorems [42], and yielding a not yet well-understood equational theory over the programs of $\mathsf{\Lambda 2}$ [18, 13, 28], that we call here the $\varepsilon$-theory. Other isomorphisms, like those in Fig. 1, can be justified in a similar way as soon as the language of $\mathsf{\Lambda 2}$ is enriched with other type constructors like $1,0,+,\times,\Rightarrow$ and least/greatest fixpoints $\mu X.A,\nu X.A$.

All such type isomorphisms have the effect of eliminating a quantifier, replacing it with a combination of monomorphic type constructors, and can be used to test if a polymorphic type has a finite number of inhabitants (as illustrated in Fig. 2) or, as suggested in [9], to devise decidable tests for program equivalence.

In this paper we develop a formal study of the elimination of quantifiers from polymorphic types using a class of type isomorphisms, that we will call Yoneda type isomorphisms, which generalize the examples above. Then, we explore the application of such type isomorphisms to establish properties of program equivalence for polymorphic programs.

1.1 A Type-Rewriting Theory of Polymorphic Types

In the first part of the paper (Sections 3-5) we investigate the type-rewriting arising from Yoneda type isomorphisms and its connection with proof-theoretic techniques to count type inhabitants.

Counting type inhabitants with type isomorphisms

Examples like the one in Fig. 2 suggest that, while arising from a categorical reading of polymorphic programs, Yoneda Type Isomorphisms have a proof-theoretic flavor. To demonstrate this, we show that the use of such isomorphisms to count type inhabitants can be compared with some well-known proof-theoretic sufficient conditions for a simple type $A$ to have a unique or finitely many inhabitants [2, 11], namely the balancedness, negatively-non duplicated and positively-non duplicated conditions. We show that whenever an inhabited simple type $A$ satisfies any of the first two conditions (resp. a special case of the third), then its universal closure $\forall\vec{X}.A$ can be converted to 1 by applying Yoneda type isomorphisms and usual $\beta\eta$-isomorphisms, and when $A$ satisfies a special case of the third, then it can be converted to $1+\dots+1$. Furthermore, we suggest that the appearance of the fixpoints in isomorphisms like $(**)$ can be related to a well-known approach to counting type inhabitants by solving systems of polynomial fixpoint equations [44].

Eliminating Quantifiers with Yoneda Reduction

We then turn to investigate in a more systematic way the quantifier-eliminating rewriting over types arising from the left-to-right orientation of Yoneda type isomorphisms. A major obstacle here is that the rewriting must take into account possible applications of $\beta\eta$-isomorphisms, whose axiomatization is well-known to be challenging in presence of the constructors $+,0$ [16, 21] (not to say of $\mu,\nu$). For this reason we introduce a family of rewrite rules, that we call Yoneda reduction, defined not directly over types but over a class of finite trees which represent the types of $\mathsf{\Lambda 2}$ (but crucially not those made with $0,+,\dots$) up to $\beta\eta$-isomorphism.

Using this rewriting we establish some sufficient conditions for eliminating quantifiers, based on elementary graph-theoretic properties of such trees, which in turn provide some new sufficient conditions for the finiteness of type inhabitants of polymorphic types. First, we prove quantifier-elimination for the types satisfying a certain coherence condition which can be seen as an instance of the 2-SAT problem. We then introduce a more refined condition by associating each polymorphic type $A$ with a value $\kappa(A)\in\{0,1,\infty\}$, that we call the characteristic of $A$, so that whenever $\kappa(A)\neq\infty$, $A$ rewrites into a monomorphic type, and when furthermore $\kappa(A)=0$, $A$ converges to a finite type. In the last case our method provides an effective way to count the inhabitants of $A$.

The computation of $\kappa(A)$ is somehow reminiscent of linear logic proof-nets, as it is obtained by inspecting the existence of cyclic paths in a graph obtained by adding some “axiom-links” to the tree-representation of $A$.

1.2 Program Equivalence in System F with Finite Characteristic

In the second part of the paper (Sections 6-8) we direct our attention to programs rather than types, and we exploit our results on type isomorphisms to establish some non-trivial properties of program equivalence for polymorphic programs in some suitable fragments of $\mathsf{\Lambda 2}$.

Computing equivalence with type isomorphisms

Computing program equivalence under the $\varepsilon$-theory can be a challenging task, as this theory involves global permutations of rules which are difficult to detect and apply [13, 28, 40, 31, 42]. Things are even worse at the semantic level, since computing with dinatural transformations can be rather cumbersome, due to the well-known fact that such transformations need not compose [7, 25].

Nevertheless, our approach to quantifier-elimination based on the notion of characteristic provides a way to compute program equivalence without the appeal to $\varepsilon$-rules, free theorems and parametricity, since all polymorphic programs having types of finite characteristic can be embedded inside well-known monomorphic systems. To demonstrate this fact, we introduce two fragments $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ of $\mathsf{\Lambda 2}$ in which types have a fixed finite characteristic, and we prove that these are equivalent, under the $\varepsilon$-theory, respectively, to the simply typed $\lambda$-calculus with finite products and co-products (or, equivalently, to the free bicartesian closed category $\mathbb{B}$), and to its extension with $\mu,\nu$-types (that is, to the free cartesian closed $\mu$-bicomplete category $\mu\mathbb{B}$ [34, 8]). Using well-known facts about $\mathbb{B}$ and $\mu\mathbb{B}$ [36, 8, 27], we finally establish that the $\varepsilon$-theory is decidable in $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and undecidable in $\mathsf{\Lambda 2^{\kappa\leq 1}}$.

Program equivalence and predicativity

We provide an example of how the correspondence between polymorphic types of finite characteristic and $\mu,\nu$-types can be used to prove non-trivial properties of program equivalence. A main source of difficulty with $\mathsf{\Lambda 2}$ is that polymorphic programs are impredicative, that is, a program of universal type $\forall X.A$ can be instantiated at any type $B$, yielding a program of type $A[B/X]$. It is thus useful to be able to predict when a complex type instantiation can be replaced by a one of smaller complexity, without altering the program behavior.

Using the fact that a universal type $\forall X.A$ of finite characteristic in which $A$ is of the form $A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$ is isomorphic to the initial algebra $\mu X.T$ of some appropriate functor $T$, we establish a sufficient condition under which a program containing an instantiation of $\forall X.A$ as $A[B/X]$ can be transformed into one with instantiations of types strictly less complex than $B$.

We finally use this condition to provide a simpler proof of a result from [31], showing that all programs in a certain fragment of $\mathsf{\Lambda 2^{\kappa\leq 0}}$ (the fragment freely generated by the embedding of finite sums and products) can be transformed into predicative programs only containing atomic type instantiations, a result related to some recent investigations on atomic polymorphism [15].

Preliminaries and Notations

We will presuppose familiarity with the syntax of $\mathsf{\Lambda 2}$ (in the version à la Church) and its extensions $\mathsf{\Lambda 2p},\mathsf{\Lambda 2p_{\mu\nu}}$ with sum and product types, as well as $\mu$ and $\nu$-types. We indicate by $\mathsf{\Lambda},\mathsf{\Lambda p},\mathsf{\Lambda p_{\mu\nu}}$ their respective quantifier-free fragments. We recall the syntax of these systems in some more detail in Sec. 6. We let $\mathtt{V}=\{X,Y,Z,\dots\}$ indicate the countable set of type variables.

Let $\mathsf{S}$ indicate any of the type systems above. We let $\Gamma\vdash_{\mathsf{S}}t:A$ indicate that the judgement $\Gamma\vdash t:A$ is derivable in $\mathsf{S}$. We indicate as $t[x]$ a term with a unique free variable $x$, and we let $t[x]:A\vdash_{\mathsf{S}}^{\Gamma}B$ be shorthand for $\Gamma,x:A\vdash_{\mathsf{S}}t:B$.

A theory of $\mathsf{S}$ is a class of equations over well-typed terms satisfying usual congruence rules. Standard theories of $\mathsf{\Lambda 2},\mathsf{\Lambda 2p},\mathsf{\Lambda 2p_{\mu\nu}}$ are those generated by $\beta\eta$-equivalence and by contextual equivalence, recalled in Sec.. 6. We will also consider a less standard theory, the $\varepsilon$-theory, also described in Sec. 6. For all theory $\mathsf{T}$ including $\beta\eta$-equivalence, we let $\mathbb{C}_{\mathsf{T}}({\mathsf{S}})$ be the category whose objects are the types of $\mathsf{S}$ and whose arrows are the $\mathsf{T}$-equivalence classes of terms $t[x]:A\vdash_{\mathsf{S}}B$. $\mathbb{C}_{\mathsf{T}}(\mathsf{S})$ is cartesian closed as soon as $\mathsf{S}$ contains products, meaning in particular that $\mathbb{C}_{\mathsf{T}}(\mathsf{S})(A\times B,C)\simeq\mathbb{C}_{\mathsf{T}}(\mathsf{S})(A,B\Rightarrow C)$.

By a $\mathsf{T}$-isomorphism, indicated as $A\equiv_{\mathsf{T}}B$, we mean a pair of terms $t[x]:A\vdash_{\mathsf{S}}B$, $u[x]:B\vdash_{\mathsf{T}}A$ such that $t[u[x]]\simeq_{\mathsf{T}}x$ and $u[t[x]]\simeq_{\mathsf{T}}x$ (where $t[u[x]]$ is $t[x\mapsto u]$).

2 Yoneda Type Isomorphisms

In this section we introduce an axiomatization for a class of type isomorphisms that we call Yoneda type isomorphisms. For this we will rely on a standard axiomatization of the $\beta\eta$-isomorphisms of $\mathsf{\Lambda 2p_{\mu\nu}}$ (recalled in Fig. 4(a)-4(c) in Sec. 6)111Note that while this axiomatization is complete for the $\beta\eta$-isomorphisms of $\mathsf{\Lambda 2}$ [14], it fails to be complete (already at the propositional level) in presence of sums and the empty type [16, 21]. and on the well-known distinction between positive and negative occurrences of a variable $X$ in a type $A$.

Notation 2.1**.**

Throughout the text we will indicate as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} a positive occurrence of $X$, and as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}} a negative occurrence of $X$. When $B$ occurs within a larger type $A$, we will often note $B$ as B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle to indicate that all occurrences of the variable $X$ in $B$ are positive occurrences in $A$, or as B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle to indicate that all occurrences of the variable $X$ in $B$ are negative occurrences in $A$. So for instance, when $B$ only contains positive occurrences of $X$, we write the type $A=X\Rightarrow B$ as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle (since all positive occurrences of $X$ in $B$ are positive in $A$) and the type $A^{\prime}=B\Rightarrow X$ as B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} (since all positive occurrences of $X$ in $B$ are negative in $A$) .

The focus on positive/negative occurrences highlights a connection with to the so-called functorial semantics of $\mathsf{\Lambda 2}$ [7, 18], in which types are interpreted as functors and typed programs as (di)natural transformations between such functors. More precisely, any positive type A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle gives rise to a functor $\Phi_{A}^{X}:\mathbb{C}_{\mathsf{T}}(\mathsf{S})\to\mathbb{C}_{\mathsf{T}}(\mathsf{S})$, any negative type A\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle gives rise to a functor $\Phi_{A}^{X}:\mathbb{C}_{\mathsf{T}}(\mathsf{S})^{\mathsf{op}}\to\mathbb{C}_{\mathsf{T}}(\mathsf{S})$ and, more generally, any type $A$ gives rise to a functor $\Phi_{A}^{X}:\mathbb{C}_{\mathsf{T}}(\mathsf{S})^{\mathsf{op}}\times\mathbb{C}_{\mathsf{T}}(\mathsf{S})\to\mathbb{C}_{\mathsf{T}}(\mathsf{S})$. In all such cases, the action of the functor on a type $A$ is obtained by replacing positive/negative occurrences of $X$ by $A$, and the action on programs can be defined inductively (we recall this construction in Sec. 6, see also [13, 29]).

With types being interpreted as functors, a polymorphic term $t[x]:A\vdash_{\mathsf{\Lambda 2}}B$ is interpreted as a transformation satisfying an appropriate naturality condition: when $A$ and $B$ have the same variance, $t[x]$ is interpreted as an ordinary natural transformation; instead, if $A$ and $B$ have mixed variances, then $t[x]$ is interpreted as a dinatural transformation.

In the framework of syntactic categories, such (di)naturality conditions are expressed by families of equational rules over typed programs [13, 28], generating, along with the usual $\beta\eta$-equations, a theory of program equivalence that we here call the $\varepsilon$-theory (and which we define formally in Sec. 6). These equational rules are usually interpreted as parametricity conditions [32], or as instances of free theorems [42].

As mentioned in the introduction, our goal in these first sections is not that of investigating the $\varepsilon$-theory directly, but rather to explore a class of type isomorphisms that hold under this theory (that is, of isomorphisms in the syntactic categories $\mathbb{C}_{\varepsilon}(\mathsf{S})$, with $\mathsf{S}=\mathsf{\Lambda 2},\mathsf{\Lambda 2p},\mathsf{\Lambda 2p_{\mu\nu}}$). For example, in functorial semantics a type of the form \forall X.A\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle is interpreted as the set of natural transformations between the functors A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle. Now, if A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle is of the form A_{0}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} (i.e. it is a representable functor), using the $\varepsilon$-theory we can deduce (see App. A) a “Yoneda lemma” in the form of the quantifier-eliminating isomorphism below:

[TABLE]

Similarly, if A\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle,B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle are both negative and A\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle is of the form {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Rightarrow A_{0} (i.e. it is a co-representable functor), we can deduce another quantifier-eliminating isomorphism:

[TABLE]

Observe that both isomorphisms ($\star$ ‣ 1) from the Introduction are instances of (1) or (2).

As we admit more type-constructors in the language, we can use the $\varepsilon$-theory to deduce stronger schemas for eliminating quantifiers. For instance, using least and greatest fixed points \mu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle,\nu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle of positive types, we can deduce the stronger schemas [41] below.

[TABLE]

Note that (1) and (2) can be deduced from (3) and (4) using the isomorphisms $\mu X.A\equiv_{\beta\eta}\nu X.A\equiv_{\beta\eta}A$, when $X$ does not occur in $A$. Moreover, adding sum and product types enables the elimination of the quantifier $\forall X$ also from a type of the form A=\forall X.(A_{11}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow A_{12}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow(A_{21}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow A_{22}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle by using $\beta\eta$-isomorphisms, as follows:

A\equiv_{\beta\eta}\forall X.\left({\left(\sum_{i=1,2}\prod_{j=1,2}A_{ij}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right)}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right)\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\equiv B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\mu X.\left(\sum_{i=1,2}\prod_{j=1,2}A_{ij}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right)\right\rangle

These considerations lead to introduce the following class of isomorphisms.

Notation 2.2**.**

Given a list $L=\langle i_{1},\dots,i_{k}\rangle$, and an $L$-indexed list of types $(A_{i})_{i\in L}$, we will use $\langle A_{i}\rangle_{i\in L}\Rightarrow B$ as a shorthand for $A_{i_{1}}\Rightarrow\dots\Rightarrow A_{i_{k}}\Rightarrow B$.

Definition 2.1**.**

A Yoneda type isomorphism is any instance of the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}, \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} in Fig. 3, where the expressions $\{\mu X.\}$, $\{\nu X.\}$ indicate that the binder $\mu X.$ (resp. $\nu X.$) is applied only if {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} (resp. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}) actually occurs in some of the $A_{jk}$ (resp. $A_{j}$), and $\exists\vec{Y}.A$ is a shorthand for $\forall Y^{\prime}.(\forall\vec{Y}.A\Rightarrow Y^{\prime})\Rightarrow Y^{\prime}$.

For all types $A,B$ of $\mathsf{\Lambda 2p_{\mu\nu}}$, we write $A\equiv_{\mathsf{Y}}B$ when $A$ can be converted to $B$ using \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} and the (partial, see f.n. 1) axiomatization of $\beta\eta$-isomorphisms in Fig. 4(a)-4(c).

In App. A we prove in detail that the two schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} are valid under the $\varepsilon$-theory, and thus that whenever $A\equiv_{\mathsf{Y}}B$, $A$ and $B$ are interpreted as isomorphic objects in all dinatural and parametric models of $\mathsf{\Lambda 2}$.

3 Counting Type Inhabitants with Yoneda Type Isomorphisms

In the previous section we introduced and motivated Yoneda Type Isomorphisms as arising from a categorical reading of polymorphic programs as (di)natural transformations. However, such isomorphisms also have a proof-theoretic flavor since, as we observed in the Introduction, they can be used to check if a closed polymorphic type has a finite number of inhabitants (up to contextual equivalence), by showing that $A$ can be transformed into a closed quantifier-free type $A^{\prime}$, and in this case to effectively count such inhabitants (by reducing $A^{\prime}$ to a finite sum $0+1+\dots+1=\sum_{i=1}^{k}1$).

At least in some simple cases, the way in which a quantifier $\forall X.A$ is eliminated by applying the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} can be related with the structure of the $\beta$-normal $\eta$-long terms of type $A$. For instance, suppose $A$ is the simple type $(C_{11}\Rightarrow C_{12}\Rightarrow X)\Rightarrow(C_{21}\Rightarrow C_{22}\Rightarrow X)\Rightarrow X$ (where none of the $C_{ij}$ contains occurrences of $X$) and $t$ is a $\beta$-normal $\eta$-long term of type $A$. Then $t$ must be of one of the following forms:

[TABLE]

Since $X$ does not occur in the $C_{ij}$ we can suppose that $y_{1},y_{2}$ do not occur in the terms $u_{ij}$, so that $u_{ij}$ is a closed term of type $C_{ij}$. Hence a closed term of $A$ is obtained from closed terms of $C_{11}$ and $C_{12}$, or from closed terms of $C_{21}$ and $C_{22}$, and we deduce that the number of inhabitants of $A$ must be the same as the number of inhabitants of $\sum_{i}\prod_{j}C_{ij}$, which is precisely the type we would obtain by applying \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} to $\forall X.A$.

The situation becomes tricker if we admit the types $C_{ij}$ to have positive occurrences of $X$, so that \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} yields the fixpoint type \mu X.\sum_{i}\prod_{j}C_{ij}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle. In this case all we can say is that the closed terms $\lambda y_{1}y_{2}.u_{ij}$ have type $C^{\prime}_{ij}:=(C_{11}\Rightarrow C_{12}\Rightarrow X)\Rightarrow(C_{21}\Rightarrow C_{22}\Rightarrow X)\Rightarrow C_{ij}$. In the concluding section we suggest that a purely proof-theoretic explanation of \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} could be developed also in this case by considering a technique of counting type-inhabitants of simple types by solving a system of polynomial fixpoint equations [44].

A natural question about counting type inhabitants using type isomorphisms is whether this approach can be compared with existing proof-theoretic criteria for having a finite number of inhabitants. We provide a first answer to this question by comparing the use of Yoneda Type Isomorphism with some well-known criteria for the finiteness/uniqueness of the inhabitants of a simple type.

Let us start with a “warm-up” example.

Example 3.1**.**

In [11] it is proved that the type A=(((({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}})\Rightarrow({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{W}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{W}} has a unique inhabitant. Here’s a quick proof of $\forall XYZW.A\equiv_{\mathsf{Y}}1$:

[TABLE]

The literature on counting simple type inhabitants is vast (e.g. [2, 11, 10, 37]) and includes both complete algorithms and simpler sufficient conditions for a given type to have a unique or finite number of inhabitants. The latter provide then an ideal starting point to test our axiomatic theory of type isomorphisms, as several of these conditions are based on properties like the number of positive/negative occurrences of variables.

We tested Yoneda type isomorphisms on two well-known sufficient conditions for unique inhabitation. A simple type $A$ is balanced when any variable occurring free in $A$ occurs exactly once as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} and exactly once as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}. $A$ is negatively non-duplicated if no variable occurs twice in $A$ as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}. An inhabited simple type which is either balanced or negatively duplicated has exactly one inhabitant [2]. The isomorphisms $\equiv_{\mathsf{Y}}$ subsume these two conditions in the following sense:

Proposition 3.1**.**

*Let $A[X_{1},\dots,X_{n}]$ be an inhabited simple type with free variables $X_{1},\dots,X_{n}$. If $A[X_{1},\dots,X_{n}]$ is either balanced or negatively non-duplicated, then $\forall X_{1}\dots\forall X_{n}.A\equiv_{\mathsf{Y}}1$. *

Proof.

Write $A$ as $\langle A_{k}\rangle_{k\in K}\Rightarrow X_{u}$ and suppose $t=\lambda x_{1}.\dots x_{\sharp K}.x_{v}t_{1}\dots t_{p}$ is a closed term of type $A$ in $\eta$-long $\beta$-normal form. This forces $A_{v}=\langle A_{jv}\rangle_{j\in J_{v}}\Rightarrow X_{u}$, with $\sharp J_{v}=p$, and implies that the terms $t_{j}^{*}=\lambda x_{1}\dots x_{\sharp K}.t_{j}$ have type $\langle A_{k}\rangle_{k\in K}\Rightarrow A_{jv}$.

We argue by induction on the size of $t$.

• •

suppose $A$ is balanced. Since $X_{u}$ occurs positively in the rightmost position of $A$ and negatively in the rightmost position of $A_{v}$, it cannot occur in any other $A_{w}$, for $w\neq v$. We deduce that the variable $x_{v}$ cannot occur in any of the terms $t_{j}$. Then, up to some $\beta\eta$-isomorphisms, we can write $\forall\vec{X}.A$ as \forall\vec{X}_{v\neq u}.\forall X_{v}.\left(\langle A_{jv}\rangle_{j\in J_{v}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}_{u}\right)\Rightarrow\left(\langle A_{w}\rangle_{w\neq v}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right), and by applying isomorphism \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} we obtain the type $\forall\vec{X}_{v\neq u}.\langle A_{w}\rangle_{w\neq v}\Rightarrow\prod_{j\in J_{v}}A_{jv}$.

Since the terms $\lambda x_{1}\dots\hat{x}_{v}\dots x_{\sharp K}.t_{j}$ have the balanced type $A_{j}^{*}=\langle A_{w}\rangle_{w\neq v}\Rightarrow A_{jv}$, by the induction hypothesis we deduce $A_{j}^{*}\equiv_{\mathsf{Y}}1$, and thus we deduce $\forall\vec{X}_{v\neq u}.\langle A_{w}\rangle_{w\neq v}\Rightarrow\prod_{j\in J_{v}}A_{jv}\equiv_{\beta\eta}\forall\vec{X}_{v\neq u}.\prod_{j\in J_{v}}A_{j}^{*}\equiv_{\beta\eta}\prod_{j\in J_{v}}\forall\vec{X}_{v\neq u}A_{j}^{*}\equiv_{\mathsf{Y}}\prod_{j\in J_{v}}1\equiv_{\beta\eta}1$.

• •

Suppose $A$ is negatively non-duplicated; we will exploit the fact that $A$ admits at most one $\eta$-long $\beta$-normal term up to equivalence (see [2]). We argue by induction that $A$ reduces to $1$ using $\beta\eta$-isomorphisms and isomorphisms of the form $\equiv_{X^{c}}$, where the variable $X$ occurs negatively exactly once. Since $X_{u}$ occurs negatively once in rightmost position of $A_{v}$, it can only occur positively in the $A_{jv}$ and negatively in the $A_{w}$ for $w\neq v$.

Moreover, we claim that $x_{v}$ cannot occur in the $t_{j}$. In fact, suppose some $t_{j}$ contains $x_{v}$. Since it is $\eta$-long it contains a subterm of the form $x_{v}w_{1}\dots w_{p}$, where $w_{j}$ cannot be $\beta\eta$-equivalent to $t_{j}$. Then by replacing $w_{j}$ with $t_{j}$ in $t$ we obtain a new term $t_{1}$ of type $A$. It is clear that this process can be repeated yielding infinitely many distinct $\beta$-normal and $\eta$-long terms $t_{2},t_{3},\dots$ of type $A$. This is impossible because $A$ admits only one term up to $\beta\eta$-equivalence.

Hence, up to some $\beta\eta$-isomorphisms, we can write $\forall\vec{X}.A$ as \forall\vec{X}_{w\neq u}.\forall X_{v}.\left(\langle A_{jv}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle\rangle_{j\in J_{v}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}_{u}\right)\Rightarrow\left(\langle A_{w}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle\rangle_{w\neq v}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right), and by applying \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} we obtain the type \forall\vec{X}_{w\neq u}.\langle A_{w}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\mapsto\alpha\right\rangle\rangle_{w\neq v}\Rightarrow\alpha, where \alpha=\mu X_{u}.\prod_{j\in J_{v}}A_{jv}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle, which is $\beta\eta$-isomorphic to \forall\vec{X}_{w\neq u}.\langle A_{w}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\mapsto\alpha\right\rangle\rangle_{w\neq v}\Rightarrow\Pi_{j\in J_{v}}A_{jv}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\alpha\right\rangle, and finally to \prod_{j\in J_{v}}\left(\forall\vec{X}_{w\neq u}.\langle A_{w}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\mapsto\alpha\right\rangle\rangle_{w\neq v}\Rightarrow A_{jv}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\alpha\right\rangle\right).

Since the terms $\lambda x_{1}\dots\hat{x}_{v}\dots x_{\sharp K}.t_{j}$ have the negatively non-duplicated type A_{j}^{*}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle=\langle A_{w}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle\rangle_{w\neq v}\Rightarrow A_{jv}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle, by the induction hypothesis we deduce \forall\vec{X}.A_{j}^{*}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\right\rangle\equiv_{\mathsf{Y}}1 using $\beta\eta$-isomorphisms and isomorphisms of the form $\equiv_{X_{w}^{c}}$, where $w\neq v$, so we deduce that also \forall\vec{X}_{w\neq u}A_{j}^{*}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\mapsto\alpha\right\rangle\equiv_{\mathsf{Y}}1 holds. We can then conclude \forall\vec{X}.A\equiv_{\mathsf{Y}}\prod_{j\in J_{v}}\forall\vec{X}_{v\neq u}A_{j}^{*}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{u}\mapsto\alpha\right\rangle\equiv_{\mathsf{Y}}\prod_{j\in J_{v}}1\equiv_{\beta\eta}1.

∎

Observe that, since the type in Example 3.1 is neither balanced nor negatively non-duplicated, type isomorphisms provide a stronger condition than the two above.

We tested another well-known property, dual to one of the previous ones: a simple type $A$ is positively non-duplicated if no variable occurs twice in $A$ as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}. A positively non-duplicated simple type has a finite number of proofs [11]. We reproved this fact using type isomorphisms, but this time only in a restricted case. Let the depth $d(A)$ of a simple type $A$ be defined by $d(X)=0$, $d(A\Rightarrow B)=\max\{d(A)+1,d(B)\}$.

Proposition 3.2**.**

Let $A[X_{1},\dots,X_{n}]$ be an inhabited simple type with free variables $X_{1},\dots,X_{n}$. If $A$ is positively non-duplicated and $d(A)\leq 2$, then $\forall X_{1}\dots\forall X_{n}.A\equiv_{\mathsf{Y}}0+1+\dots+1$.

We need the following lemma:

Lemma 3.3**.**

Suppose $A=\langle A_{i}\Rightarrow X_{i}\rangle_{i\in L}\Rightarrow U$ has free variables $X_{1},\dots,X_{n}$, where the $A_{i}$ are $\Rightarrow$-free $\mathsf{\Lambda p_{\mu\nu}}$-types and $U$ is a closed type constructed using only 0 and 1. Then $\forall X_{1}\dots\forall X_{n}.A\equiv_{\mathsf{Y}}U$.

Proof.

We argue by induction on the number of variables $X_{1},\dots,X_{n}$ freely occurring in $A$. If $n$ is 0 then the list $L$ is empty, so the claim is obvious. Otherwise, suppose $L$ has a first element $i_{0}$, so that $A$ can be written, up to some $\beta\eta$-isomorphism, as \langle A_{u}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}_{i_{0}}\rangle_{u}\Rightarrow\langle B_{v}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}_{v}\rangle_{v}\Rightarrow U where the A_{u}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle and A_{u}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle are $\Rightarrow$-free types and $Y_{v}\neq X$. Then \forall X_{1}\dots\forall X_{n}.A\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}}\forall X_{1}\dots\widehat{\forall X}_{i_{0}}\dots\forall X_{n}.\langle B_{v}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle\theta\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}_{v}\rangle_{v}\Rightarrow U, where \theta:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\mapsto\mu X_{i_{0}}.\sum_{u}A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{i_{0}}\right\rangle_{u}, so we can conclude by the induction hypothesis. ∎

Proof of Proposition 3.2.

We will establish the following stronger claim. Let a quasi-polynomial be a type of the form $\langle A_{k}\rangle_{k\in K}\Rightarrow\sum_{i=1}^{p}\prod_{j=1}^{p_{i}}u_{ij}$, where $p,p_{i}\geq 1$, the $A_{k}$ are simple types of depth $\leq 1$ (hence of the form $\langle X_{v_{k}}\rangle_{v_{k}}\Rightarrow X_{k}$) and the $u_{ij}$ are either variables or 0,1. We claim that for any quasi-polynomial $P[X_{1},\dots,X_{n}]$, if $P$ is positively non-duplicated, then $\forall X_{1}\dots\forall X_{n}.P\equiv_{\mathsf{Y}}0+1+\dots+1$.

We argue by induction on the number of variables occurring among the $u_{ij}$.

If all $u_{ij}$ are either [math] or $1$, then any $A_{k}=\langle X_{v_{k}}\rangle_{v_{k}}\Rightarrow X_{k}$ is $\beta\eta$-isomorphic to $(\Pi_{v_{k}}X_{v_{k}})\Rightarrow X_{k}$ so we can apply Lemma 3.3 yielding $\forall X_{1}\dots\forall X_{n}.P\equiv_{\mathsf{Y}}\sum_{i=1}^{p}\prod_{j=1}^{p_{i}}u_{ij}\equiv_{\beta\eta}0+1+\dots+1$.

Suppose now $u_{i_{0}j_{0}}=Z$. Since $P$ is positively non-duplicated, we can write $P$, up to some $\beta\eta$-isomorphisms, as \langle\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}_{lm}\rangle_{l}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}}\rangle_{m}\Rightarrow\langle B_{m^{\prime}}\rangle_{m^{\prime}}\Rightarrow\sum_{i=1}^{p}\prod_{j=1}^{p_{i}}u_{ij} where none of $Z_{lm}$ coincides with $Z$ and $Z$ does not occur in any of the $B_{m^{\prime}}$. Then we deduce \forall X_{1}\dots\forall X_{n}.P\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}}\forall X_{1}\dots\widehat{\forall Z}\dots\forall X_{n}.\langle B_{m^{\prime}}\rangle_{m^{\prime}}\Rightarrow\sum_{i=1}^{p}\prod_{j=1}^{p_{i}}u_{ij}\theta, where \theta:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}\mapsto\sum_{m}\prod_{l}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}_{lm}. Observe that the type $\langle B_{m^{\prime}}\rangle_{m^{\prime}}\Rightarrow\sum_{i=1}^{p}\prod_{j=1}^{p_{i}}u_{ij}\theta$ is positively non-duplicated, has one variable less than $P$, and moreover, reduces using $\beta\eta$-isomorphisms to a type of the form $\langle B_{m^{\prime}}\rangle_{m^{\prime}}\Rightarrow\sum_{i=1}^{p^{\prime}}\prod_{j=1}^{p^{\prime}_{i}}v_{ij}$, where the $v_{ij}$ are among $0,1,X_{1},\dots,\widehat{Z},\dots,X_{n}$. We can thus apply the induction hypothesis. ∎

4 From Polymorphic Types to Polynomial Trees

As we already observed, read from left to right, the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} yield rewriting rules over $\mathsf{\Lambda 2p_{\mu\nu}}$-types which eliminate occurrences of polymorphic quantifiers. Yet, a major obstacle to study this rewriting is that the application of \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} might depend on the former application of $\beta\eta$-isomorphisms (as we did for instance in the previous section). Already for the propositional fragment $\mathsf{\Lambda p}$, the $\beta\eta$-isomorphisms are not finitely axiomatizable and it is not yet clear if a decision algorithm exists at all (see [16, 21]). This implies in particular that a complete criterion for the conversion of a $\mathsf{\Lambda 2}$-type to a monomorphic (or even finite) type can hardly be computable.

For this reason, we will restrict our goal to establishing some efficiently recognizable (in fact, polytime) sufficient conditions for quantifier-elimination. Moreover, we will exploit the well-known fact that the constructors $0,1,+,\times,\mu,\nu$ can be encoded inside $\mathsf{\Lambda 2}$ to describe our rewriting entirely within (a suitable representation of) $\mathsf{\Lambda 2}$-types, for which $\beta\eta$-isomorphisms can be finitely axiomatized [14].

Even if one restricts to $\mathsf{\Lambda 2}$-types, recognizing if one of the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} applies to a $\mathsf{\Lambda 2}$-type $\forall X.A$ might still require to first apply some $\beta\eta$-isomorphisms. For example, consider the $\mathsf{\Lambda 2}$-type A=\forall X.(({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}. In order to eliminate the quantifier $\forall X$ using \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}, we first need to apply the $\beta\eta$-isomorphism $A\Rightarrow(B\Rightarrow C)\equiv_{\beta\eta}B\Rightarrow(A\Rightarrow C)$, turning $A$ into \forall X.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow(({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}, which is now of the form \forall X.(B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow C\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, with B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}} and C\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle=(({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}. We can then apply \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}, yielding (({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}.

To obviate this problem, we introduce below a representation of $\mathsf{\Lambda 2}$-types as labeled trees so that $\beta\eta$-isomorphic types are represented by the same tree. In the next section we will reformulate the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} as reduction rules over such trees. This approach drastically simplifies the study of this rewriting, and will allow us to establish conditions for quantifier-elimination based on elementary graph-theoretic properties.

4.1 A $\beta\eta$-invariant representation of $\mathsf{\Lambda 2}$-types

We introduce a representations of $\mathsf{\Lambda 2}$-types as rooted trees whose leaves are labeled by colored variables, with colors being any c\in\mathsf{Colors}=\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{blue}}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{red}}}\}. We indicate such variables as either $X^{c}$ or simply as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}},{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}. Moreover, we indicate as $\mathbin{\overline{c}}$ the unique color different from $c$.

By a rooted tree we indicate a finite connected acyclic graph with a chosen vertex, called its root. If $(\mathscr{G}_{i})_{i\in I}$ is a finite family of rooted trees, we indicate as

\big{\{}\mathscr{G}_{i}\big{\}}_{i\in I}$$u

the tree with root $u$ obtained by adding an edge from any of the roots of the trees $\mathscr{G}_{i}$ to $u$.

Definition 4.1**.**

The sets {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{E}}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathcal{E}}} of positive and negative $\mathsf{\Lambda 2}$-trees are inductively defined by:

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}\quad:=\quad\leavevmode\hbox to63.37pt{\vbox to38pt{\pgfpicture\makeatletter\hbox{\hskip 16.11737pt\lower-29.66751pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.78436pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}{i}\Big{}}{i\in I}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{35.75244pt}{-3.07498pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.64775pt}{-26.3345pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\vec{Y}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{7.4652pt}{-8.533pt}\pgfsys@lineto{13.70021pt}{-15.65706pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{34.05261pt}{-6.60799pt}\pgfsys@lineto{26.13347pt}{-15.65706pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\qquad\qquad\qquad{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}\quad:=\quad\leavevmode\hbox to63.37pt{\vbox to38pt{\pgfpicture\makeatletter\hbox{\hskip 16.11737pt\lower-29.66751pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.78436pt}{-2.5pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}{i}\Big{}}{i\in I}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{35.75244pt}{-3.07498pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{16.64775pt}{-26.3345pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\vec{Y}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{7.4652pt}{-8.533pt}\pgfsys@lineto{13.70021pt}{-15.65706pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{34.05261pt}{-6.60799pt}\pgfsys@lineto{26.13347pt}{-15.65706pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}

---

*where $X$ is a variable, $\vec{Y}$ indicates a finite set of variables, and the edge in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} (resp. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}) with label {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} (resp. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}) is called the head of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} (resp. of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}). The trees *

\{\ \}_{\emptyset}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}$$\emptyset *

and *

\{\ \}_{\emptyset}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}$$\emptyset *

are indicated simply as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}.*

Free and bound variables of a tree $\mathsf{E}=$

\Big{\{}\mathsf{E}_{i}\Big{\}}_{i\in I}$$X$$\vec{Y}

are defined by $\mathsf{f}\mathcal{V}(\mathsf{E})=\bigcup_{i=1}^{n}\mathsf{f}\mathcal{V}(\mathsf{E}_{i})\cup\{X\}-\vec{Y}$ and $\mathsf{b}\mathcal{V}(\mathsf{E})=\bigcup_{i=1}^{n}\mathsf{b}\mathcal{V}(\mathsf{E}_{i})\cup\vec{Y}$.

We can associate a positive and a negative $\mathsf{\Lambda 2}$-tree to any $\mathsf{\Lambda 2}$-type as follows. Let us say that a type $A$ of $\mathsf{\Lambda 2}$ is in normal form (shortly, in NF) if $A=\forall\vec{Y}.A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$ where each of the variables in $\vec{Y}$ occurs in $A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$ at least once, and the types $A_{1},\dots,A_{n}$ are in normal form.

We will show that the tree-representation of $\mathsf{\Lambda 2}$-types captures $\beta\eta$-isomorphism classes, in the sense that $A\equiv_{\beta\eta}B$ iff {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B). For instance, the two $\beta\eta$-isomorphic types \forall XY.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow(\forall Z.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}} and \forall X.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow\forall Y.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow\forall Z.{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}} translate into the same $\mathsf{\Lambda 2}$-tree, shown in Fig. 7(b) (where underlined node labels and dashed edges can be ignored, for now).

The $\beta\eta$-isomorphisms of $\mathsf{\Lambda 2}$ are completely axiomatized as shown in Fig. 4(a). A type $A$ of $\mathsf{\Lambda 2}$ is in normal form (shortly, in NF) if $A=\forall\vec{Y}.A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$ where each variable in $\vec{Y}$ occurs at least once in $A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$, and the types $A_{1},\dots,A_{n}$ are in normal form. Let $\mathsf{NF}(\mathsf{\Lambda 2})$ be the set of $\mathsf{\Lambda 2}$-types in NF.

Given $A,B\in\mathsf{NF}(\mathsf{\Lambda 2})$, with $A=\forall\vec{Y}.A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$ and $B=\forall\vec{Z}.B_{1}\Rightarrow\dots\Rightarrow B_{m}\Rightarrow X^{\prime}$, let $A\sim B$ when $n=m$, $\vec{Y}=\vec{Z}$, $X=X^{\prime}$ and there exists $\sigma\in\mathfrak{S}_{n}$ such that $A_{i}\sim B_{\sigma(i)}$ for $i=1,\dots,n$.

Lemma 4.1**.**

• i.

For all $A\in\mathsf{\Lambda 2}$, there exists a type $\mathsf{NF}(A)\in\mathsf{NF}(\mathsf{\Lambda 2})$ such that $A\equiv_{\beta\eta}\mathsf{NF}(A)$.

• ii.

For all $A,B\in\mathsf{\Lambda 2}$, $A\equiv_{\beta\eta}B$ iff $\mathsf{NF}(A)\sim\mathsf{NF}(B)$.

Proof.

Claim $i.$ is a consequence of applying the isomorphisms $\forall X.A\equiv_{\beta\eta}A$ when $X$ does not occur in $A$ and the isomorphisms $A\Rightarrow\forall X.B\equiv_{\beta\eta}\forall X.A\Rightarrow B$ to push quantifiers in leftmost position. Claim $ii.$ follows then since the only other isomorphism rule is the permutation $A\Rightarrow(B\Rightarrow C)\equiv_{\beta\eta}B\Rightarrow(A\Rightarrow C)$. ∎

The definition of the tree-type {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A) only depends on $\mathsf{NF}(A)$. Moreover, it can be checked by induction on $A$ that $\mathsf{NF}(A)\sim\mathsf{NF}(B)$ holds iff {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B). Hence, we deduce from Lemma 4.1 that $A\equiv_{\beta\eta}B$ iff {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B).

Definition 4.2**.**

For all $A\in\mathsf{\Lambda 2}$, with $\mathsf{NF}(A)=\forall\vec{Y}.A_{1}\Rightarrow\dots\Rightarrow A_{n}\Rightarrow X$, let

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)=\leavevmode\hbox to91.04pt{\vbox to40.98pt{\pgfpicture\makeatletter\hbox{\hskip 26.71696pt\lower-32.51253pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.38396pt}{-2.36401pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{t}}}(A_{i})\Big{}}{i=1,\dots,n}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{52.82428pt}{-3.07498pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.18367pt}{-29.17952pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\vec{Y}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{49.564pt}{-6.60799pt}\pgfsys@lineto{35.25485pt}{-19.4864pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{9.6313pt}{-8.66899pt}\pgfsys@lineto{21.65067pt}{-19.4864pt}\pgfsys@stroke\pgfsys@invoke{ } \par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\qquad\qquad{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{t}}}(A)=\leavevmode\hbox to91.04pt{\vbox to40.98pt{\pgfpicture\makeatletter\hbox{\hskip 26.71696pt\lower-32.51253pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.38396pt}{-2.36401pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A{i})\Big{}}_{i=1,\dots,n}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{52.82428pt}{-3.07498pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{25.18367pt}{-29.17952pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\vec{Y}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{49.564pt}{-6.60799pt}\pgfsys@lineto{35.25485pt}{-19.4864pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{9.6313pt}{-8.66899pt}\pgfsys@lineto{21.65067pt}{-19.4864pt}\pgfsys@stroke\pgfsys@invoke{ } \par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}

---

4.2 Polynomial Trees

To formulate the schemas \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} in the language of rooted trees we exploit an encoding of the types of the form \mu X.\exists\vec{Y}.\sum_{i\in I}\prod_{j\in J_{i}}A_{ij}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and \nu X.\forall\vec{Y}.\prod_{j\in J}A_{j}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle as certain special trees employing two new constants $\bullet$ and $\blacktriangle$. This encoding is easily seen to be a small variant, in the language of finite trees, of the usual second-order encodings.

We first introduce a handy notation for “polynomial” types, i.e. types corresponding to a generalized sum of generalized products. Following [17], any such type $A$ is completely determined by a diagram of finite sets $I\stackrel{{\scriptstyle f}}{{\leftarrow}}J\stackrel{{\scriptstyle g}}{{\to}}K$ and a $I$-indexed family of types $(A_{i})_{i\in I}$, so that $A=\sum_{k\in K}\prod_{j\in J_{k}}A_{f(j)}$, where $J_{k}:=g^{-1}(k)$. In the following, we will call the given of a finite diagram $I\stackrel{{\scriptstyle f}}{{\leftarrow}}J\stackrel{{\scriptstyle g}}{{\to}}K$, and an $I$-indexed family $(a_{i})_{i\in I}$ a polynomial family, and indicate it simply as $(a_{jk})_{k\in K,j\in J_{k}}$.

We now enrich the class of $\mathsf{\Lambda 2}$-trees as follows:

Definition 4.3** (Polynomial trees).**

Let $\bullet,\blacktriangle$ indicate two new constants.

• •

the set {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathcal{P}}} of positive polynomial trees is defined by adding to the clauses defining positive $\mathsf{\Lambda 2}$-trees two new clauses:

\left\{\leavevmode\hbox{\set@color\ignorespaces\minipage{433.62pt} \leavevmode\hbox to74.74pt{\vbox to41.84pt{\pgfpicture\makeatletter\hbox{\hskip 35.01793pt\lower-33.38753pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.68492pt}{-2.38501pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}\right\rangle\Big{}}{j}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{31.89322pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.41148pt}{-28.30452pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\vec{X}_{k}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.1105pt}{-8.648pt}\pgfsys@lineto{9.09233pt}{-17.62708pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{30.45537pt}{-5.533pt}\pgfsys@lineto{22.39128pt}{-17.62708pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\par\par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} \endminipage }\right\}_{k}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}$$\bullet        \Big{\{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{j}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\blacktriangle}}\right\rangle\Big{\}}_{j}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\blacktriangle}}$$\vec{X}

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\blacktriangle}}$$\blacktriangle

** where $X$ is some variable, ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle)_{k,j} (resp. ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{j}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle)_{j}) is a polynomial family (resp. a family) of positive polynomial trees with no occurrence of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, and $(\vec{X}_{k})_{k\in K}$ is a $K$-indexed family of finite sets of variables.*

• •

the set {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathcal{P}}} of negative polynomial trees is defined by adding to the clauses defining negative $\mathsf{\Lambda 2}$-trees two new clauses:

\left\{\leavevmode\hbox{\set@color\ignorespaces\minipage{433.62pt} \leavevmode\hbox to74.74pt{\vbox to41.84pt{\pgfpicture\makeatletter\hbox{\hskip 35.01793pt\lower-33.38753pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.68492pt}{-2.38501pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\Big{{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}{jk}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}\right\rangle\Big{}}{j}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{31.89322pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{12.41148pt}{-28.30452pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\vec{X}_{k}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{0.1105pt}{-8.648pt}\pgfsys@lineto{9.09233pt}{-17.62708pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{ }{}\pgfsys@moveto{30.45537pt}{-5.533pt}\pgfsys@lineto{22.39128pt}{-17.62708pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\par\par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} \endminipage }\right\}_{k}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}$$\bullet        \Big{\{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{j}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\blacktriangle}}\right\rangle\Big{\}}_{j}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\blacktriangle}}$$\vec{X}

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\blacktriangle}}$$\blacktriangle

** where $X$ is some variable, ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{jk}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle)_{k,j} (resp. ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{j}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle)_{j}) is a polynomial family (resp. a family) of negative polynomial trees with no occurrence of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}, and $(\vec{X}_{k})_{k\in K}$ is a $K$-indexed family of finite sets of variables.*

We indicate by $\mathcal{P}$ the set of all polynomial trees, and by $\mathcal{P}_{0}$ the set of all polynomial trees with no bound variables, which are called simple.

Any polynomial tree $\mathsf{E}\in\mathcal{P}$ can be converted into a type $\tau(\mathsf{E})$ of $\mathsf{\Lambda 2p_{\mu\nu}}$ as illustrated in Fig. 5. It is easily checked that, whenever $\mathsf{E}$ is simple, $\tau(\mathsf{E})$ has no quantifier. Moreover, one can check that for all $\mathsf{\Lambda 2}$-type, \tau({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A))=A.

We conclude this section with some basic example of polynomial trees.

Example 4.1**.**

• •

*The constant types [math] and $1$ are represented as positive/negative trees by {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathbf{0}}}=\leavevmode\hbox to11.17pt{\vbox to24.89pt{\pgfpicture\makeatletter\hbox{\hskip 5.58301pt\lower-19.55939pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-16.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\bullet}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-5.533pt}\pgfsys@lineto{0.0pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathbf{0}}}=\leavevmode\hbox to11.17pt{\vbox to24.89pt{\pgfpicture\makeatletter\hbox{\hskip 5.58301pt\lower-19.55939pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-16.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\bullet}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-5.533pt}\pgfsys@lineto{0.0pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathbf{1}}}=\leavevmode\hbox to28.24pt{\vbox to24.89pt{\pgfpicture\makeatletter\hbox{\hskip 14.11891pt\lower-19.55939pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.7859pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.2859pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-16.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\bullet}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{5.21608pt}{-5.533pt}\pgfsys@lineto{3.31932pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-5.21608pt}{-5.533pt}\pgfsys@lineto{-3.31932pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } \par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}, {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathbf{1}}}=\leavevmode\hbox to28.24pt{\vbox to24.89pt{\pgfpicture\makeatletter\hbox{\hskip 14.11891pt\lower-19.55939pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-10.7859pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.2859pt}{-2.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.25pt}{-16.22638pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\small\bullet}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{5.21608pt}{-5.533pt}\pgfsys@lineto{3.31932pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } { {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-5.21608pt}{-5.533pt}\pgfsys@lineto{-3.31932pt}{-8.69337pt}\pgfsys@stroke\pgfsys@invoke{ } \par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}. *

• •

*The diagram $\{1,2\}\stackrel{{\scriptstyle 1,3\mapsto 1;2\mapsto 2}}{{\leftarrow}}\{1,2,3\}\stackrel{{\scriptstyle 1,2\mapsto 1;3\mapsto 2}}{{\to}}\{1,2\}$, along with the family $(X_{i})_{i\in\{1,2\}}$, yields the polynomial family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{jk})_{k,j}, with {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{11}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{32}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{1} and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{21}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{2}, and yields the polynomial tree *

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}$$\emptyset$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\bullet}}$$\emptyset$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}$$\bullet *

• encoding the type $\mu X_{1}.(X_{1}\times X_{2})+X_{1}$.*

• •

*The diagram $\{1,2\}\stackrel{{\scriptstyle id}}{{\leftarrow}}\{1,2\}\to\{1\}$ with the same family as above yields the polynomial tree *

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\blacktriangle}}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\blacktriangle}}$$\emptyset$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}_{2}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\blacktriangle}}$$\emptyset$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\blacktriangle}}$$\blacktriangle *

• encoding the type $\nu X_{1}.X_{1}\times X_{2}$.*

5 Yoneda Reduction and the Characteristic of a Polymorphic Type

In this section we introduce a family of rewriting rules \leadsto_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\leadsto_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} over polynomial trees, that we call Yoneda reduction, which correspond to the left-to-right orientation of the isomorphisms \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}. We will then exploit Yoneda reduction to establish two sufficient conditions to convert a $\mathsf{\Lambda 2}$-type $A$ into a quantifier-free type $A^{\prime}$ such that $A\equiv_{\mathsf{Y}}A^{\prime}$.

5.1 Yoneda Reduction

We will adopt the following conventions:

Notation 5.1**.**

We make the assumption that all bound variables of a polynomial tree $\mathsf{E}$ are distinct. More precisely, for any $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, we suppose there exist unique nodes $\mathsf{r}_{X}$ and $\mathsf{h}_{X}$ such that $\mathsf{r}_{X}:\vec{X}$, for some set of variable $\vec{X}$ such that $X\in\vec{X}$, and $\mathsf{h}_{X}$ is the head of the sub-tree whose root is $\mathsf{r}_{X}$.

We will call two distinct nodes parallel if they are immediate successors of the same node, and we let the distance $d(\alpha,\beta)$ between two nodes in a polynomial tree be the number of edges of the unique path from $\alpha$ to $\beta$.

Using polynomial trees we can identify when a quantifier can be eliminated from a type independently from $\beta\eta$-isomorphisms, by inspecting a simple condition on the tree-representation of the type based on the notion of modular node, introduced below.

Definition 5.1**.**

For all $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, a terminal node $\alpha:X^{c}$ in $\mathsf{E}$ is said modular if $\alpha\neq\mathsf{h}_{X}$, $1\leq d(\alpha,\mathsf{r}_{X})\leq 2$ and $\alpha$ has no parallel node of label $X^{c}$. A pair of nodes of the form (\alpha:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}},\beta:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}) is called a $X$-pair, and a $X$-pair is said modular if one of its nodes is modular.

In the trees in Fig. 7 the modular nodes are underlined and the modular pairs are indicated as dashed edges.

Definition 5.2**.**

A variable $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$ is said eliminable when every $X$-pair of $\mathsf{E}$ is modular. For every color $c$, we furthermore call $X$ $c$-eliminable if every node $\alpha:X^{\mathbin{\overline{c}}}$ is modular.

We let {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} be a shorthand for “{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{blue}}}}-eliminable” and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} be a shorthand for “{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{red}}}}-eliminable”. These notions are related as follows:

Lemma 5.1**.**

$X$* is eliminable iff it is either {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} or {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}}.*

Proof.

If $X$ is neither {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} nor {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}}, then there exist non-modular nodes \alpha:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}},\beta:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, whence the $X$-pair $(\alpha,\beta)$ is not modular. Conversely, suppose $X$ is eliminable but not {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}}. Hence there is a non modular node \alpha:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}. For all node \beta:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, since the $X$-pair $(\alpha,\beta)$ is modular, $\beta$ is modular. We deduce that $X$ is {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}}. ∎

Example 5.1**.**

*The variable $X$ is {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} but not {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} in the tree in Fig. 7(a), and it is both {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} in the tree in Fig. 7(b). *

The proposition below shows that a variable $X$ is {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} (resp. {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}}) in the tree of a $\mathsf{\Lambda 2}$-type $\forall X.A$ exactly when $\forall X.A$ matches, up to $\beta\eta$-isomorphisms, with the left-hand type of the schema \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} (resp. \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}).

Proposition 5.2**.**

• •

$X$* is {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} iff {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} is as in Fig. 6(a) left, for some polynomial family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\rangle)_{k\in K,j\in J_{k}}, family ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\rangle)_{l\in L} and blue variable {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}} (possibly {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} itself).*

• •

$X$* is {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} iff {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} is as in Fig. 6(b) left, for some polynomial family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\rangle)_{k\in K,j\in J_{k}}, family ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{k}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\rangle)_{k\in K}, family ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\rangle)_{l\in L} and blue variable {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}.*

• •

$X$* is {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}} iff {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}} is as in Fig. 6(c) left, for some polynomial family ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{D}}}_{jk}\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\rangle)_{k\in K,j\in J_{k}}, family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{k}\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\rangle)_{k\in K}, family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}_{l}\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\rangle)_{l\in L} and red variable {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\neq{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}.*

• •

$X$* is {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}} iff {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}} is as in Fig. 6(d) left, for some polynomial family ({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{D}}}_{jk}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\rangle)_{k\in K,j\in J_{k}}, family ({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}_{l}\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\rangle)_{l\in L} and red variable {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}} (possibly {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}} itself).*

Proof.

If $X$ is {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{eliminable}}} in a positive tree {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}=

\Big{\{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{i}\Big{\}}_{i\in I}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}$${\vec{Y}}X

, then let us split the negative subtrees {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{i} into those which do not contain terminal nodes with label {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, that we indicate as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, and those which contain a (necessarily unique) modular node of label {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, that we indicate as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{G}}}_{k}. Since {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{G}}}_{k} contains a unique modular node \alpha_{k}:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}} which is no more than two edges far away from the root of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}, then {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{G}}}_{k} is of the form

\Big{\{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Big{\}}_{i\in I}$${\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}$${\vec{Z}_{k}}

, where possibly $I=Z_{k}=\emptyset$, (so that {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{G}}}_{k}={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}).

If $X$ is {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{eliminable}}} in a positive tree {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}=

\Big{\{}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{E}}}_{i}\Big{\}}_{i\in I}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}$$\vec{Y}X

, then, since all nodes \alpha:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} are modular, it must be {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\neq{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}. Let us split the positive subtrees {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{i} into those which do not contain terminal nodes with label {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}, that we indicate as {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle, and those which contain a (necessarily unique) modular node of label {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}, that we indicate as {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}_{k}. Since {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}_{k} contains a unique modular node \alpha_{k}:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\alpha}} which is no more than two edges far away from the root of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}, then {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{G}}_{k} is of the form

{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}$$\Big{\{}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\Big{\}}_{i\in I}$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}_{k}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle$${\vec{{Z}}_{k}}

.

The two cases with a negative tree are described in a dual way (i.e. by switching blue and red everywhere). ∎

For all four cases of Prop. 5.2 we define a rewriting rule which eliminates $X$.

Definition 5.3** (Yoneda reduction).**

Let $\mathsf{F}\in\mathcal{P}$ and $X\in\mathsf{b}\mathcal{V}(\mathsf{F})$ be an eliminable variable. The rules $\mathsf{F}\leadsto_{X^{c}}\mathsf{F}^{\prime}$ consist in replacing the subtree $\mathsf{E}$ of $\mathsf{F}$ rooted in $\mathsf{r}_{X}$ as illustrated in Fig. 6.

Example 5.2**.**

The tree in Fig. 7(b) rewrites as illustrated in Fig. 8.

By inspecting the rules in Fig. 6 one can check that $\mathsf{E}\leadsto_{X^{c}}\mathsf{E}^{\prime}$ implies $\tau(\mathsf{E})\equiv_{\mathsf{Y}}\tau(\mathsf{E}^{\prime})$. From this we can deduce by induction:

Lemma 5.3**.**

For all $\mathsf{\Lambda 2}$-type $A$, if {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)\leadsto^{*}\mathsf{E}\in\mathcal{P}_{0}, then $A\equiv_{\mathsf{Y}}\tau(\mathsf{E})\in\mathsf{\Lambda p_{\mu\nu}}$.

The lemma above suggests to study the elimination of quantifiers from $\mathsf{\Lambda 2}$-types by studying the convergence of $\mathsf{\Lambda 2}$-trees onto simple polynomial trees. This will be our next goal.

5.2 The Coherence Condition

When a reduction is applied to $\mathsf{E}$, several sub-trees of $\mathsf{E}$ can be either erased or copied and moved elsewhere. Hence, the resulting tree $\mathsf{E}^{\prime}$ might well have a greater size and even a larger number of bound variables than $\mathsf{E}$. Nevertheless, sequences of Yoneda reductions always terminate, as one can define a measure which decreases at each step.

Proposition 5.4**.**

There is no infinite sequence of Yoneda reductions.

Proof.

Let $K$ be the number of terminal nodes of $\mathsf{E}$ and, for all bound variable $X_{i}$ of $\mathsf{E}$, let $K_{i}$ be the number of terminal nodes of the subtree $\mathsf{E}_{i}$ of $\mathsf{E}$ with root $\mathsf{r}_{X_{i}}$. Fix some $s>K^{2}$ and let $\mu(\mathsf{E})$ be the sum of all $s^{K_{i}}$, for all bound variable $X_{i}$. If $\mathsf{E}\leadsto_{X_{i}^{c}}\mathsf{E}^{\prime}$, then the elimination of $X_{i}$ comes at the cost of possibly duplicating the bound variables which are at distance at least one from the root of $\mathsf{E}_{i}$. These are no more than $K_{i}$ and can be duplicated for no more than $K_{i}$ times. Since for each such variable $j$, it must be $K_{j}<K_{i}$, we deduce that $\mu(\mathsf{E}^{\prime})$ is obtained by replacing in $\mu(\mathsf{E})$ the summand $s^{K_{i}}$ by a sum of no more than $K_{i}^{2}$ summands which are bounded by $s^{K_{i}-1}$. Hence, if we write $\mu(\mathsf{E})$ as $a+s^{K_{i}}$, then $\mu(\mathsf{E}^{\prime})\leq a+K_{i}^{2}s^{K_{i}-1}<a+s^{K_{i}}=\mu(\mathsf{E})$. We deduce that the measure $\mu(\mathsf{E})$ strictly decreases under reduction, and so, if an infinite sequence of reductions exists, then after a large enough number of step one must obtain a tree $\mathsf{E}^{\prime}$ such that $\mu(\mathsf{E}^{\prime})<0$, which is impossible. ∎

Although sequences of reductions always terminate, they need not terminate on a simple polynomial tree, that is, on the encoding of a monomorphic type. This can be due to several reasons. Firstly, one bound variable might not be eliminable. Secondly, even if all variables are eliminable, this property need not be preserved by reduction. For example, take the type A=\forall X.\forall Y.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow(({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{W}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}: although $X$ and $Y$ are both eliminable (in the associated tree), if we apply a reduction to $X$, then $Y$ ceases to be eliminable, and similarly if we reduce $Y$ first. Such conflicts can be controlled by imposing a suitable coherence relation on variables.

Definition 5.4**.**

Let $\mathsf{E}$ be a polynomial tree, $X,Y\in\mathsf{b}\mathcal{V}(\mathsf{E})$ and $c,d\in\mathsf{Colors}$. $X^{c}$ and $Y^{d}$ are said coherent if there exists no parallel modular nodes of the form $\alpha:X^{\mathbin{\overline{c}}},\beta:Y^{\mathbin{\overline{d}}}$ in $\mathsf{E}$.

Example 5.3**.**

In the tree in Fig. 7(b), {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}} and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}} are coherent, while {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} and {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}} are not.

Definition 5.5** (coherence condition).**

Let $\mathsf{E}$ be a polynomial tree. A valuation of $\mathsf{E}$ is any map $\phi:\mathsf{b}\mathcal{V}(\mathsf{E})\to\mathsf{Colors}$. For all valuation $\phi$ of $\mathsf{E}$, we call $\mathsf{E}$ $\phi$-coherent if for all $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, $X$ is $\phi(X)$-eliminable, and moreover for all $Y\neq X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, $X^{\phi(X)}$ is coherent with $Y^{\phi(Y)}$. We call $\mathsf{E}$ coherent if it is $\phi$-coherent for some valuation $\phi$ of $\mathsf{E}$.

Remark 5.1** (Coherence is an instance of 2-SAT).**

The problem of checking if a polynomial tree $\mathsf{E}$ is coherent can be formulated as an instance of 2-SAT (a well-known polytime problem): consider $n$ Boolean variables $x_{1},\dots,x_{n}$ (one for each bound variable of $\mathsf{E}$), and let $a_{i}^{c}$ be $x_{i}$ if c={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{blue}}} and $\lnot x_{i}$ if c={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{red}}}. Consider then the 2-CNF $A\land B$, where $A$ is the conjunction of all $a_{i}^{c}\vee a_{i}^{c}$ such that $X_{i}$ is not $\mathbin{\overline{c}}$-eliminable in $\mathsf{E}$, and $B$ is the conjunction of all $a_{i}^{c}\lor a_{j}^{d}$, for all incoherent $X_{i}^{\mathbin{\overline{c}}}$ and $X_{j}^{\mathbin{\overline{d}}}$. Then a coherent valuation of $\mathsf{E}$ is the same as a model of $A\land B$.

As observed before, a reduction $\mathsf{E}\leadsto_{X}\mathsf{E}^{\prime}$ might copy or erase some bound variables of $\mathsf{E}$. One can then define a map $g:\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})\to\mathsf{b}\mathcal{V}(\mathsf{E})$ associating any variable in $\mathsf{E}^{\prime}$ with the corresponding variable in $\mathsf{E}$ of which it is a copy. A sequence of reductions $\mathsf{E}_{0}\leadsto_{X_{1}^{c_{1}}}\dots\leadsto_{X_{n}^{c_{n}}}\mathsf{E}_{n}$ induces then, for $1\leq i\leq n$, maps $g_{i}:\mathsf{b}\mathcal{V}(\mathsf{E}_{i})\to\mathsf{b}\mathcal{V}(\mathsf{E}_{i-1})$, and we let $G_{i}:\mathsf{b}\mathcal{V}(\mathsf{E}_{i})\to\mathsf{b}\mathcal{V}(\mathsf{E}_{0})$ be $g_{1}\circ g_{2}\circ\dots\circ g_{i}$.

The rewriting properties of coherent trees are captured by the following notion:

Definition 5.6** (standard reduction).**

A sequence of reductions $\mathsf{E}_{0}\leadsto_{X_{1}^{c_{1}}}\dots\leadsto_{X_{n}^{c_{n}}}\mathsf{E}_{n}$ is said standard if for all $i,j=1,\dots,n$, $G_{i}(X_{i})^{c_{i}}$ is coherent with $G_{j}(X_{j})^{c_{j}}$ in $\mathsf{E}_{0}$. We say that $\mathsf{E}$ strongly converges under standard reduction if all standard reductions starting from $\mathsf{E}$ terminate on a simple polynomial tree.

We indicate a standard reduction as $\mathsf{E}\leadsto_{\mathsf{stand}}^{*}\mathsf{E}^{\prime}$. We will show that standard reduction preserves coherence.

Lemma 5.5**.**

If $\mathsf{E}$ is coherent, and $\mathsf{E}\leadsto_{\mathsf{stand}}^{*}\mathsf{E}^{\prime}$, then $\mathsf{E}^{\prime}$ is coherent.

Proof.

For any node $\alpha$ of $\mathsf{E}^{\prime}$ there exists a unique node, that we indicate as $g(\alpha)$, from which $\alpha$ “comes from” through the reduction step. Moreover, for each bound variable $Y\in\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})$ there exists a unique bound variable $g(Y)\in\mathsf{b}\mathcal{V}(\mathsf{E})$ from which $Y$ “comes from” through the reduction step.

We indicate as $\alpha\preceq\beta$ the tree-order relation on the nodes of $\mathsf{E}$ (so that the root of $\mathsf{E}$ is the minimum node). Suppose $\mathsf{E}$ is $\phi$-coherent and $\mathsf{E}\leadsto_{X^{\phi(X)}}\mathsf{E}^{\prime}$. We will show that $\mathsf{E}^{\prime}$ is $\phi\circ g$-coherent.

Let $\mathsf{F}$ be the sub-tree of $\mathsf{E}$ with root $\mathsf{r}_{X}$, fix a variable $Y$ in $\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})$. We must consider four possible cases, corresponding to the four reduction rules. Each rule requires itself four subcases. We only consider the case of the first rule (hence with $\mathsf{E}$ positive), as the other three cases can be proved in a similar way.

({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}\leadsto_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}^{\prime}}})

We first show that $Y$ is $\phi(g(Y))$-eliminable in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}^{\prime}, by showing that any modular node $\alpha:g(Y)$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}} is transformed into a modular node $\beta:Y$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}^{\prime}. We argue by considering the relative position of $\mathsf{r}_{X}$ and $\mathsf{r}_{Z}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}:

($\mathsf{r}_{X}=\mathsf{r}_{g(Y)}$)

Since {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} and $g(Y)^{\phi(g(Y))}$ are coherent in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}, and all nodes $\alpha:g(Y)^{\mathbin{\overline{\phi(g(Y))}}}$ are modular, each such node $\alpha$ must be a terminal node of some of the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle (see Fig. 6(a)). In fact, if $\alpha$ were a terminal node of some {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, then either {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle=g(Y)^{\mathbin{\overline{\phi(g(Y))}}}, which contradicts the assumption that {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} and $g(Y)^{\phi(g(Y))}$ are coherent, or its distance from $\mathsf{r}_{X}=\mathsf{r}_{g(Y)}$ is greater than 2, against the assumption that $\alpha$ is modular. Now, since all nodes in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle which are not labeled with {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} are not “moved” by the reduction rule (see Fig. 6(a)), and no new node labeled $g(Y)^{\phi(g(Y))}$ is created by $\theta$ (since otherwise it should come from a node with same label in some {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle), all nodes $\alpha:Y^{\mathbin{\overline{\phi(g(Y))}}}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}^{\prime}}} are modular, whence $Y$ is $\phi(g(Y))$-eliminable in $\mathsf{F}^{\prime}$.

($\mathsf{r}_{X}\prec\mathsf{r}_{g(Y)}$)

First, if $\mathsf{r}_{g(Y)}$ occurs within either the {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle or the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, then one can check that, by the transformation from {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}} to {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}^{\prime}}}, the relative positions between the nodes $g(\alpha):g(Y)^{c}$ and $\mathsf{r}_{g(Y)}$ in $\mathsf{E}$ coincide with the relative positions between the nodes $\alpha$ and $\mathsf{r}_{Y}$, and thus all modular nodes $\delta:g(Y)^{\mathbin{\overline{\phi(g(Y))}}}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}} yield modular nodes $\delta^{\prime}:Y^{\mathbin{\overline{\phi(g(Y))}}}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}^{\prime}.

Suppose now $g(Y)$ is among some set $\vec{Z}_{k}$ (see Fig. 6(a)). One can check that for all node $\delta:g(Y)^{\mathbin{\overline{\phi(g(Y))}}}$ occurring in $\mathsf{F}$ within one of the {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{D}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, if, in the transformation of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}} in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}}^{\prime}, $\delta$ is transformed into $\delta^{\prime}$, then $d(\delta,\mathsf{r}_{g(Y)})$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} is the same as $d(\delta^{\prime},\mathsf{r}_{Y})$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime}. Moreover, it is clear that $\delta^{\prime}$ cannot be the head of the sub-tree rooted in $\mathsf{r}_{Y}$, and that if $\delta$ has no parallel node with same label, so does $\delta^{\prime}$. Hence, if $\delta$ is modular, so is $\delta^{\prime}$.

($\mathsf{r}_{g(Y)}\prec\mathsf{r}_{X}$)

If a modular node $\delta:g(Y)^{\mathbin{\overline{\phi(g(Y))}}}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}} is transformed into some node $\delta^{\prime}:Y^{\mathbin{\overline{\phi(Y)}}}$ in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime}, then $\delta^{\prime}$ is modular too. In fact, no such $\delta$ can be actually moved by the reduction rule, since the only possibilities are that either $\delta\prec\mathsf{r}_{X}$ or $\delta$ coincides with one of the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle. Since neither the node $\mathsf{r}_{Y}$ is moved, we deduce that $\delta^{\prime}$ has the same distance from $\mathsf{r}_{g(Y)}$ than $\delta$ has from $\mathsf{r}_{g(Y)}$, that it has no parallel node with same label and cannot be the head of the sub-tree rooted in $\mathsf{r}_{Y}$, whence $\delta^{\prime}$ is modular.

($\mathsf{r}_{g(Y)}\not\preceq\mathsf{r}_{X},\mathsf{r}_{X}\not\preceq\mathsf{r}_{g(Y)}$

We can argue as in the case above, since the transformation from {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}}} to {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{F}^{\prime}}} cannot move any node $\delta:g(Y)^{\mathbin{\overline{\phi(g(Y))}}}$.

We conclude then that, for all $Y\in\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})$, $Y$ is $\phi(g(Y))$-eliminable. It remains to check that for all $Y,Z\in\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})$, $Y^{\phi(g(Y))}$ and $Z^{\phi(g(Y))}$ are coherent. It can be checked that for any parallel nodes $\alpha:Y^{\mathbin{\overline{\phi(g(Y))}}},\beta:Z^{\mathbin{\overline{\phi(g(Z))}}}$ in $\mathsf{E}^{\prime}$, $g(\alpha)$ and $g(\beta)$ are parallel in $\mathsf{E}$. Hence, if $Y^{\phi(g(Y))}$ and $Z^{\phi(g(Y))}$ are not coherent, then $g(Y)^{\phi(Y)}$ and $g(Z)^{\phi(Z)}$ are not coherent, against the assumption.

∎

Let us call a $c$-eliminable variable $X$ $c$-canceling in the following cases:

• •

$\mathsf{r}_{X}$ is the root of a positive tree as in Fig. 6(a) left, where c={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{blue}}}, $Y\neq X$ and no node in any sub-tree {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{F}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle has label {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}};

• •

$\mathsf{r}_{X}$ is the root of a positive tree as in Fig. 6(b) left, c={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{red}}} and no node in any sub-tree {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{F}}_{l}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle has label {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}};

• •

$\mathsf{r}_{X}$ is the root of a negative tree as in Fig. 6(c) left, c={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathrm{blue}}} and no node in any sub-tree {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle has label {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}};

• •

$\mathsf{r}_{X}$ is the root of a negative tree as in Fig. 6(d), c={\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathrm{red}}}, $Y\neq X$ and no node in any sub-tree {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{F}}_{l}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle has label {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}.

In fact, $X$ is $c$-canceling precisely when by applying a $X^{c}$-reduction step, the action of the substitution $\theta$ from Fig. 6 is empty, so that the whole left-hand part of the tree, including some of its bound variables, is erased. Observe that, if $X$ is not $c$-canceling, and $\mathsf{E}\leadsto_{X^{c}}\mathsf{E}^{\prime}$, then the application $Y\mapsto g(Y)$ from a bound variable of $\mathsf{E}^{\prime}$ to a bound variables of $\mathsf{E}$ from which $Y$ “comes from” is a surjective function $g:\mathsf{b}\mathcal{V}(\mathsf{E}^{\prime})\to\mathsf{b}\mathcal{V}(\mathsf{E})-\{X\}$.

Moreover, let us call a standard reduction $\mathsf{E}\leadsto_{\mathsf{stand}}^{*}\mathsf{E}^{\prime}$ least-canceling if for all $c$-canceling variable $X$, a reduction $\leadsto_{X^{c}}$ is performed only after all bound variables $Y$ occurring above the node $\mathsf{r}_{X}$ are eliminated. Let us indicate by $\mathsf{E}\leadsto_{\mathsf{canc}}\mathsf{E}^{\prime}$ that $\mathsf{E}$ reduces to $\mathsf{E}^{\prime}$ by a sequence of least-canceling standard reductions.

Using Lemma 5.5 we can prove:

Theorem 5.6**.**

$\mathsf{E}$* is coherent iff $\mathsf{E}$ strongly converges under standard reduction.*

Proof.

Suppose $\mathsf{E}$ is coherent. From Lemma 5.5 we deduce that if $\mathsf{E}\leadsto_{\mathsf{stand}}^{*}\mathsf{E}^{\prime}$, then either $\mathsf{E}^{\prime}\in\mathcal{P}_{0}$ or $\mathsf{E}^{\prime}\leadsto_{\mathsf{stand}}\mathsf{E}^{\prime\prime}$ for some $\mathsf{E}^{\prime\prime}$. Since sequences of standard reductions terminate, we deduce that $\mathsf{E}$ must in the end converge onto some simple tree.

Conversely, suppose $\mathsf{E}$ strongly converges under $\leadsto_{\mathsf{stand}}$. Since all standard reductions converge, there must be a converging least-canceling standard reduction $\mathsf{E}=\mathsf{E}_{0}\leadsto_{Y_{1}^{c_{1}}}\mathsf{E}_{1}\leadsto_{Y_{2}^{c_{2}}}\dots\leadsto_{Y_{n}^{c_{n}}}\mathsf{E}_{n}\in\mathcal{P}_{0}$. Let $\delta(X)=\min\{i\mid G_{i}(Y_{i})=X\}$ and $\phi(X)=c_{\delta(X)}$. Using the fact that the variables $G_{i}(Y_{i})^{c_{i}}$ are pairwise coherent and include all bound variables of $\mathsf{E}$, one can check that $\delta$ and $\phi$ are well-defined and $\mathsf{E}$ is $\phi$-coherent. ∎

Using Lemma 5.3 we further deduce:

Corollary 5.1**.**

Let $A$ be a type of $\mathsf{\Lambda 2}$. If {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A) is coherent, then there exists a $\mathsf{\Lambda p_{\mu\nu}}$-type $A^{\prime}$ such that $A\equiv_{\mathsf{Y}}A^{\prime}$.

5.3 The Characteristic

We now introduce a refined condition for coherent trees, which can be used to predict whether a type rewrites into a finite type (i.e. one made up from $0,1,+,\times,\Rightarrow$ only) or into one using $\mu,\nu$-constructors.

An intuition from Section 2 is that, for a type of the form \forall X.(A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle (which rewrites into B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\mu X.A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right\rangle) to reduce to one without $\mu,\nu$-types, the variable $X$ must not occur in $A$ at all. However, the property “$X$ does not occur in $A$” need not be preserved under reduction. Instead, we will define a stronger condition that is preserved by standard reduction by inspecting a class of paths in the tree of a type.

Definition 5.7**.**

Let $\mathsf{E}$ be a polynomial $\mathsf{\Lambda 2}$-tree and let $\preceq$ indicate the natural order on the nodes of $\mathsf{E}$ having the root of $\mathsf{E}$ as its minimum. A down-move in $\mathsf{E}$ is a pair $\alpha\vartriangleright\beta$, such that, for some bound variable $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, $(\alpha,\beta)$ is an $X$-pair and $\beta$ is modular. An up-move in $\mathsf{E}$ is a pair $\alpha\vartriangleright\beta$ such that $\alpha\neq\beta$, $\alpha$ is a modular node with immediate predecessor $\gamma$, $\beta:X$ for some $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$, and $\gamma\preceq\beta$. An alternating path in $\mathsf{E}$ is a sequence of nodes $\alpha_{0}\dots\alpha_{2n}$ such that $\alpha_{2i}\vartriangleright\alpha_{2i+1}$ is a down-move and $\alpha_{2i+1}\vartriangleright\alpha_{2i+2}$ is an up-move.

In Fig. 9(b) are illustrated some alternating paths. Observe that whenever {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} occurs in A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, we can construct a cyclic alternate path in the tree of \forall X.(A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow B\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle: down-move from an occurrence of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} in $A$ to the modular node labeled {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}, then up-move back to {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}. We deduce that if no cyclic alternate path exists, then any subtype of the form above must be such that {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} does not occur in $A$. This leads to introduce the following:

Definition 5.8**.**

For any polynomial tree $\mathsf{E}$, the characteristic of $\mathsf{E}$, $\kappa(\mathsf{E})\in\{0,1,\infty\}$ is defined as follows: if $\mathsf{E}$ is coherent, then $\kappa(\mathsf{E})=0$ if it has no cyclic alternating path, and $\kappa(\mathsf{E})=1$ if it has a cyclic alternating path; if $\mathsf{E}$ is not coherent, $\kappa(\mathsf{E})=\infty$.

The characteristic is indeed stable under standard reduction:

Lemma 5.7**.**

For all $\mathsf{E},\mathsf{E}^{\prime}$, if $\mathsf{E}$ reduces to $\mathsf{E}^{\prime}$ by standard reduction, then $\kappa(\mathsf{E}^{\prime})\leq\kappa(\mathsf{E})$.

Proof.

If $\kappa(\mathsf{E})=\infty$ the claim is trivial. If $\kappa(\mathsf{E})=1$, then by Lemma 5.5, $\kappa(\mathsf{E}^{\prime})\leq 1=\kappa(\mathsf{E})$.

Suppose now $\kappa(\mathsf{E})=0$. We must show that there is no cyclic alternate path in $\mathsf{E}^{\prime}$, on the assumption that there is no cyclic path in $\mathsf{E}$. Suppose $\mathsf{E}^{\prime}$ is obtained by a reduction as the one in Fig. 6(a). As in the proof of Lemma 5.5, for any node $\alpha$ of $\mathsf{E}^{\prime}$, let $g(\alpha)$ be the unique node in $\mathsf{E}$ $\alpha$ “comes from”. We will show that any alternating path from $\gamma_{1}$ to $\gamma_{n}$ in $\mathsf{E}^{\prime}$ induces an alternate path from $g(\gamma_{1})$ to $g(\gamma_{n})$ in $\mathsf{E}$. From this fact it immediately follows that $\kappa(\mathsf{E}^{\prime})\leq 0$, since any cyclic path in $\mathsf{E}^{\prime}$ would induce a cyclic path in $\mathsf{E}$, against the assumption that $\kappa(\mathsf{E})=0$.

First observe that if $\delta:Y^{c}$ is a modular node in $\mathsf{E}^{\prime}$, then $g(\delta):g(Y)^{c}$ is a modular node in $\mathsf{E}$. In fact one can check that:

• •

if $g(\delta):g(Y)^{c}$ is the head of the sub-tree of $\mathsf{E}$ rooted in $\mathsf{r}_{g(Y)}$, then also $\delta$ is the head of the sub-tree of $\mathsf{E}^{\prime}$ rooted in $\mathsf{r}_{Y}$ (it suffices to check for the cases $\mathsf{r}_{g(Y)}\preceq\mathsf{r}_{X}$ and $\mathsf{r}_{g(X)}\prec\mathsf{r}_{X}$);

• •

if $d(g(\delta),\mathsf{r}_{g(Y)})>2$, then $d(\delta,\mathsf{r}_{Y})>2$ (again, one has to check the cases $\mathsf{r}_{g(Y)}\preceq\mathsf{r}_{X}$ and $\mathsf{r}_{g(X)}\prec\mathsf{r}_{X}$);

• •

if $g(\delta):g(Y)^{c}$ has a parallel node $\beta:g(Y)^{c}$, then also $\delta:Y^{c}$ has a parallel node $\beta^{\prime}:Y^{c}$ with $g(\beta^{\prime})=\beta$.

From this it follows that if $(\gamma:Y^{c})\vartriangleright(\delta:Y^{\mathbin{\overline{c}}})$ is a down-move in $\mathsf{E}^{\prime}$; then $(g(\gamma):g(Y)^{c})\vartriangleright(g(\delta):g(Y)^{\mathbin{\overline{c}}})$ is a down-move in $\mathsf{E}$. Moreover, if $(\gamma:Y^{c})\vartriangleright(\delta:Z^{d})$ is an up-move in $\mathsf{E}^{\prime}$, then two possibilities arise:

• •

$\gamma:Y^{c}$ is a modular node occurring either in some of the {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}\right\rangle or of the {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\theta\right\rangle, and $\delta:Z^{d}$ is a terminal node in the same sub-tree. Then $g(\gamma)$ is a modular node occurring either in some copy of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle or in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and $g(\delta)$ is a terminal node in the same sub-tree, so we conclude that $g(\gamma)\vartriangleright g(\delta)$ is an up-move in $\mathsf{E}$.

• •

$\gamma:Y^{c}$ is a modular node occurring in some copy of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\theta\right\rangle, and $\delta:Z^{d}$ is a terminal node in the sub-tree {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\bullet}}\right\rangle which is on top of {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\theta\right\rangle. Then $g(\gamma)$ is modular in $\mathsf{E}$ and by construction there exists a terminal node \alpha:{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} in {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{\mathsf{F}}}_{l}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\theta\right\rangle, a modular node \beta:{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}} in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{D}}}_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, so that there is an alternate path $g(\gamma)\vartriangleright\alpha\vartriangleright\beta\vartriangleright g(\delta)$ in $\mathsf{E}$, as illustrated in Fig. 10.

We conclude that if $\alpha_{0}\dots\alpha_{2n}$ is an alternate path in $\mathsf{E}^{\prime}$, then we can find an alternate path $g(\alpha_{0})g(\alpha_{1})\dots g(\alpha_{2})g(\alpha_{3})\dots g(\alpha_{2n-2})g(\alpha_{2n-1})\dots g(\alpha_{2n})$ in $\mathsf{E}$.

A similar argument can be developed for the other tree reduction rules. ∎

Using the observation above and Lemma 5.7 we can easily prove:

Proposition 5.8**.**

Suppose $\kappa(\mathsf{E})\in\{0,1\}$ and $\mathsf{E}$ reduces to $\mathsf{E}^{\prime}\in\mathcal{P}_{0}$ by standard reduction. If $\kappa(\mathsf{E})=0$, then $\tau(\mathsf{E}^{\prime})\in\mathsf{\Lambda p}$, and if $\kappa(\mathsf{E})=1$, then $\tau(\mathsf{E}^{\prime})\in\mathsf{\Lambda p_{\mu\nu}}$.

For a $\mathsf{\Lambda 2}$-type $A$, we can define its characteristic as \kappa(A)=\kappa({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)). From Prop. 5.8 and Lemma 5.3 we deduce then a new criterion for finiteness:

Corollary 5.2**.**

Let $A$ be a closed $\mathsf{\Lambda 2}$-type. If $\kappa(A)=0$, then $A\equiv_{\mathsf{Y}}0+1+\dots+1$.

The criterion based on the characteristic can be used to capture yet more finite $\mathsf{\Lambda 2}$-types. In fact, whenever a type $A$ reduces to a type with characteristic [math], we can deduce that $A\equiv_{\mathsf{Y}}0+1+\dots+1$. Note that such a type $A$ need not even be coherent. For instance, the (tree of) the type A=\forall XY.(\forall Z.(({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}, is not coherent (since the variable $Z$ is not eliminable), but reduces, by eliminating $X$, to (the tree of) \forall Y.{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}, which has characteristic [math], and in fact we have that $A\equiv_{\mathsf{Y}}1$.

As this example shows, a type $A$ can reduce to a finite sum $0+1+\dots+1$ even if some of its subtypes cannot be similarly reduced. In fact, while we can eliminate all quantifiers from the type $A$ above, we cannot do this from its subtype \forall Z.(({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Z}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Z}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}). By contrast, in the next section we show that the characteristic satisfies nice compositionality conditions that will allow us to define suitable fragments of $\mathsf{\Lambda 2}$.

6 Preliminaries on Theories of Program Equivalences

After developing the rewriting theory of Yoneda Type Isomorphisms, our goal in the next section will be to exploit the correspondence it provides between polymorphic and monomorphic types to investigate properties of program equivalence in $\mathsf{\Lambda 2}$. In this section we introduce the fundamental notions of type systems and program equivalence we will be concerned with.

The terms of $\mathsf{\Lambda 2}$ are generated by usual $\lambda$-calculus constructors, i.e. variables $x,y,z,\dots$, application $tu$ and abstraction $\lambda x.t$, plus polymorphic constructors $tA$, for all type $A$ and $\Lambda X.t$ for all $X\in\mathtt{V}$. The terms of $\mathsf{\Lambda 2p_{\mu\nu}}$ (and its $\mu,\nu$-free fragment $\mathsf{\Lambda 2p}$) involve, in addition to the constructors for $\mathsf{\Lambda 2}$, the following constructors: product constructors $\langle t,u\rangle$, $\pi_{i}t$ ($i=0,1$); sum constructors $\iota_{i}t$ ($i=0,1$) and $\delta_{A}(t,y.u_{1},y.u_{2})$ for all type $A$; the $1$ constructor $\star$; the 0 destructors $\xi_{A}t$, for all type $A$; fixpoints constructors $\mathsf{fold}_{A}(t),\mathsf{in}_{A}t,\mathsf{unfold}_{A}(t),\mathsf{out}_{A}t$ for any type $A$.

Notation 6.1**.**

Let $L=\langle i_{1},\dots,i_{k}\rangle$ be a list. If $(t_{k})_{i\in L}$ is a $L$-indexed list of terms, we let for any term $u$, $u\langle t_{k}\rangle_{i\in L}$ be shorthand for $ut_{i_{1}}\dots t_{i_{k}}$; if $\langle x_{i_{1}},\dots,x_{i_{k}}\rangle$ is a $L$-indexed list of variables, we let for any term $u$, $\lambda\langle x_{k}\rangle_{i\in L}.u$ be shorthand for $\lambda x_{i_{1}}\dots\lambda x_{i_{k}}.u$.

The typing rules of $\mathsf{\Lambda 2p}$ and $\mathsf{\Lambda 2p_{\mu\nu}}$ are recalled in Fig. 11(a)-11(b). $\beta$ and $\eta$-rules are recalled in Fig. 11(c)-11(d) and 11(e). We let the $\beta\eta$-theory of $\mathsf{\Lambda 2p_{\mu\nu}}$ (and its fragments) be the smallest congruent theory closed under $\beta$ and $\eta$ rules.

In addition to the $\beta\eta$-theory, in the next sections we will investigate two other theories: the one arising from contextual equivalence and the $\varepsilon$-theory.

Definition 6.1**.**

The contextual equivalence relation for $\mathsf{\Lambda 2p_{\mu\nu}}$ and $\mathsf{\Lambda p}$ is defined by

$\Gamma\vdash t\simeq_{{\mathsf{ctx}}}u:A$* iff for all context $\mathtt{C}:(\Gamma\vdash A)\Rightarrow(\vdash 1+1)$, $\mathtt{C}[t]\simeq_{\beta\eta}\mathtt{C}[u]$*

The contextual equivalence relation for $\mathsf{\Lambda 2}$ is defined by

$\Gamma\vdash t\simeq_{{\mathsf{ctx}}}u:A$* iff for all context $\mathtt{C}:(\Gamma\vdash A)\Rightarrow(\vdash\forall X.X\Rightarrow X\Rightarrow X)$, $\mathtt{C}[t]\simeq_{\beta\eta}\mathtt{C}[u]$*

It is a standard result that contextual equivalence (for either $\mathsf{\Lambda 2p_{\mu\nu}}$ or $\mathsf{\Lambda 2}$) is closed under congruence rules and thus generates an equational theory ${\mathsf{ctx}}$.

An equational theory $\mathsf{T}$ for $\mathsf{\Lambda 2p_{\mu\nu}}$ is consistent when it does not contain the equation $\iota_{1}(\star)\simeq_{\mathsf{T}}\iota_{2}(\star):1+1$. Similarly, an equational theory $\mathsf{T}$ for $\mathsf{\Lambda 2}$ is consistent when it does not contain the equation $\Lambda X.\lambda xy.x\simeq_{\mathsf{T}}\Lambda X.\lambda xy.y:\forall X.X\Rightarrow X\Rightarrow X$. It is well-known that ${\mathsf{ctx}}$ is the maximum consistent theory (both for $\mathsf{\Lambda 2p_{\mu\nu}}$and $\mathsf{\Lambda 2}$).

To introduce the $\varepsilon$-theory we first recall how positive types A\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and negative type B\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle are associated with functors $\Phi_{A}^{X}:\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2})\to\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2})$ and $\Phi_{B}^{X}:\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2})^{\mathsf{op}}\to\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2})$. We let $\Phi_{A}^{X}(C)=A[C/X]$, $\Phi_{B}^{X}(C)=B[C/X]$ and for all $t[x]:C\vdash D$,

[TABLE]

One can check that $\Phi_{A}^{X}(x)\simeq_{\eta}x$ and \Phi_{A}^{X}(t[u[x]])\simeq_{\beta}\Phi_{A}^{X}(t)\Big{[}x\mapsto\Phi_{A}^{X}(u)\Big{]}.

The definition above can be extended to the types defined using all other constructors, yielding functors $\Phi_{A}^{X}:\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2p_{\mu\nu}})\to\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2p_{\mu\nu}})$ and $\Phi_{B}^{X}:\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2p_{\mu\nu}})^{\mathsf{op}}\to\mathbb{C}_{\beta\eta}(\mathsf{\Lambda 2p_{\mu\nu}})$.

For simplicity, we will define the $\varepsilon$-theory for an ad-hoc fragment $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$ of $\mathsf{\Lambda 2p_{\mu\nu}}$, in which types are restricted so that a universal type $\forall X.A$ is always of one of the two forms below:

[TABLE]

As this set of types is stable by substitution, all type rules and equational rules of $\mathsf{\Lambda 2p_{\mu\nu}}$ scale well to $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$. We will meet again this subsystem of $\mathsf{\Lambda 2p_{\mu\nu}}$ in the next section as well as in App. B.

To each universal type $\forall X.A$ of $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$ as in Eq. (10) left we can associate an equational rule, that we call a $\varepsilon$-rule, illustrated in Fig. 12(a); similarly, to each type as in Eq. (10) right we can associate a $\varepsilon$-rule as illustrated in Fig. 12(b).222Observe that $\forall X.C$ might well be of both forms (10) left and right. From the viewpoint of category theory, the two $\varepsilon$-rules for a type $\forall X.A$ correspond to requiring that the transformations induced by a polymorphic programs of type $\forall X.A$ are strongly dinatural [41], or, in other words, that the diagrams illustrated in Fig. 12(c) and Fig. 12(d) commute.

Definition 6.2** ($\varepsilon$-theory).**

The $\varepsilon$-theory of $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$ is the smallest congruent equational theory closed under $\beta$-, $\eta$-equations as well as $\varepsilon$-rules.

For the interested reader, in App. A we check in detail that the isomorphisms \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}},\equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} hold under the $\varepsilon$-theory of $\mathsf{\Lambda 2p_{\mu\nu}}$.

We recall in Fig. 13(a) and 13(b) the usual embedding ♯ of $\mathsf{\Lambda 2p_{\mu\nu}}$ into $\mathsf{\Lambda 2}$. It is well-known that $\beta$-equivalent terms of $\mathsf{\Lambda 2p_{\mu\nu}}$ translate under ♯ into $\beta$-equivalent terms of $\mathsf{\Lambda 2}$, and that $\eta$-equivalent terms of $\mathsf{\Lambda 2p_{\mu\nu}}$ translate under ♯ into terms which are equivalent up to dinaturality (see [32, 19]), that is, into $\varepsilon$-equivalent terms of $\mathsf{\Lambda 2}$. Moreover, for all $\mathsf{\Lambda 2p_{\mu\nu}}$-type $A$ we can define terms \mathsf{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A}}[x]:A\vdash_{\mathsf{\Lambda 2p_{\mu\nu}}}A^{\sharp} and \mathsf{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{A}}[x]:A^{\sharp}\vdash_{\mathsf{\Lambda 2p_{\mu\nu}}}A (as illustrated in Fig. 14). It is a good exercise with $\varepsilon$-rules to check that $\mathtt{c}_{A}[\mathtt{c}_{A}^{-1}[x]]\simeq_{\varepsilon}x:A^{\sharp}$ and $\mathtt{c}_{A}^{-1}[\mathtt{c}_{A}[x]]\simeq_{\varepsilon}x:A$ hold.

Remark 6.1**.**

It is easily checked that for all type $A$ of $\mathsf{\Lambda 2p_{\mu\nu}}$, $A\equiv_{\mathsf{Y}}A^{\sharp}$ holds, the only non immediate case being

[TABLE]

7 System F with Finite Characteristic

In this section we show that Yoneda reduction can be used to characterize the $\varepsilon$-theory in some fragments of $\mathsf{\Lambda 2}$. We introduce two fragments $\mathsf{\Lambda 2^{\kappa\leq 0}},\mathsf{\Lambda 2^{\kappa\leq 1}}$ of $\mathsf{\Lambda 2}$ in which types have a fixed finite characteristic, and we show that the $\varepsilon$-theory for such fragment can be computed by embedding polymorphic programs into well-known monomorphic systems.

We recall that the free bicartesian closed category is the category $\mathbb{B}=\mathbb{C}_{\beta\eta}(\mathsf{\Lambda p})$ and the free cartesian closed $\mu$-bicomplete category $\mu\mathbb{B}$ [34, 8] is the category $\mathbb{C}_{\beta\eta}(\mathsf{\Lambda p_{\mu\nu}})$. We will show that, under the $\varepsilon$-theory, $\mathsf{\Lambda 2^{\kappa\leq 0}}$ is equivalent to $\mathbb{B}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ is equivalent to $\mu\mathbb{B}$. We will then use this embedding to establish that this theory is decidable in the fragment of characteristic 0 (where it also coincides with contextual equivalence) and undecidable in the fragment of characteristic 1.

7.1 The Systems $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$

We first have to check that the types with a fixed finite characteristic do yield well-defined fragments of $\mathsf{\Lambda 2}$. This requires to check two properties. First, the characteristic has to be compositional: a subtype of a type of characteristic $k$ cannot have a higher characteristic, since every subtype of a type of the fragment must be in the fragment itself. Second, since a universally quantified variable can be instantiated with any other type of the fragment, the characteristic must be closed by instantiation: if $\forall X.A$ and $B$ have characteristic $k$, then $A[B/X]$ must have characteristic (at most) $k$.

Lemma 7.1**.**

(compositionality)

If $A$ is a sub-type of $B$, then $\kappa(A)\leq\kappa(B)$.

(closure by instantiation)

$\kappa(A[B/X])\leq\max\{\kappa(\forall X.A),\kappa(B)\}$.

Proof.

If $\phi:\mathsf{b}\mathcal{V}(B)\to\mathsf{Colors}$ and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B) is $\phi$-coherent, then {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A) is $\phi^{\prime}$-coherent, where $\phi^{\prime}$ is the restriction $\phi|_{{\mathsf{b}\mathcal{V}(A)}}$ of $\phi$ to $\mathsf{b}\mathcal{V}(A)$. Moreover, it is clear that any cyclic alternate path in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A) yields a cyclic alternate path in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B).

The set $\mathsf{b}\mathcal{V}(A[B/X])$ can be identified with $V=\mathsf{b}\mathcal{V}(A)\uplus\biguplus_{i=1}^{k}\mathsf{b}\mathcal{V}(B)$, where $\uplus$ indicates disjoint union $k$ is the number of occurrences of $X$ in $A$. Suppose {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(\forall X.A) is $\phi$-coherent and {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B) is $\psi$-coherent, and let $\chi:=\phi|_{\mathsf{b}\mathcal{V}(A)}\uplus\biguplus_{i=1}^{k}\psi$; we claim that {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A[B/X]) is $\chi$-coherent. First, any bound variable $\neq X$ in $A$ is coherent with any bound variable within any of the copies of $B$ in $A[B/X]$. Moreover, one can check that if an alternate path starts somewhere in the tree of $A[B/X]$ and enters the sub-tree corresponding to a copy of $B$, then the path must end within this sub-tree, since in any alternate path starting from (a copy of) $B$ all labels are bound variables of (this copy of) $B$, which are disjoint from all other bound variables. We deduce then that a cyclic alternate path in the tree of $A[B/X]$ can only be a cyclic alternate path in either {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A) or in one copy of {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(B). Since both cases are excluded by assumption, no alternate cyclic path exists. ∎

Thanks to Lemma 7.1 the following fragments can be seen to be well-defined.

Definition 7.1** (Systems $\mathsf{\Lambda 2}^{\kappa\leq k}$).**

For $k=0,1$, let $\mathsf{\Lambda 2}^{\kappa\leq k}$ be the subsystem of $\mathsf{\Lambda 2}$ with same typing rules and types restricted to the types of $\mathsf{\Lambda 2}$ of characteristic $k$.

7.2 Embedding $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ into Monomorphic Systems

The standard embedding ♯ of $\mathsf{\Lambda 2p_{\mu\nu}}$ into $\mathsf{\Lambda 2}$ recalled in the previous section restricts to an embedding of $\mathbb{B}$ and $\mu\mathbb{B}$ in $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$, respectively. As this embedding preserves $\beta$ and $\eta$-rules up to the $\varepsilon$-theory, it yields then a functor ${}^{\sharp}:\mu\mathbb{B}\to\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})$, which restricts to a functor from $\mathbb{B}$ to $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 0}})$.

We will now define a converse embedding from $\mathsf{\Lambda 2^{\kappa\leq 0}}$ (resp. $\mathsf{\Lambda 2^{\kappa\leq 1}}$) into $\mathsf{\Lambda p}$ (resp. $\mathsf{\Lambda p_{\mu\nu}}$), yielding a functor ${}^{\flat}:\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})\to\mu\mathbb{B}$, restricting to a functor from $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 0}})$ to $\mathbb{B}$.

The embedding of types

Recall that from Proposition 5.8 we already know that the types of $\mathsf{\Lambda 2^{\kappa\leq 0}}$ (resp. $\mathsf{\Lambda 2^{\kappa\leq 1}}$) are isomorphic, modulo the $\varepsilon$-theory, to types of $\mathsf{\Lambda p}$ (resp. $\mathsf{\Lambda p_{\mu\nu}}$). In fact, since all isomorphisms $\equiv_{\mathsf{Y}}$ are valid under the $\varepsilon$-theory, we can obtain $A^{\flat}$ from any standard reduction of the tree of $A$, using Prop. 5.8. However, since our goal is to also embed the terms of $\mathsf{\Lambda 2^{\kappa\leq 0}}/\mathsf{\Lambda 2^{\kappa\leq 1}}$ into $\mathsf{\Lambda p}/\mathsf{\Lambda p_{\mu\nu}}$, we cannot define ♭ starting from an arbitrary standard reduction, since we need the map $A\mapsto A^{\flat}$ to satisfy two additional properties. First, it has to commute with substitutions, i.e. $(A[B/X])^{\flat}=A^{\flat}[B^{\flat}/X]$; second, we need the embedding to be compositional, meaning that the translation of a complex type can be reconstructed from the translation of its subtypes.

When $\phi$ is a valuation of $\mathsf{E}$ such that $\mathsf{E}$ is $\phi$-coherent, we call $\phi$ simply a coherent valuation of $\mathsf{E}$. We call a reduction $\mathsf{E}_{0}\leadsto_{X_{1}^{c_{1}}}\dots\leadsto_{X_{n}^{c_{n}}}\mathsf{E}_{n}$ uniform if it is standard and satisfies the following two properties:

• •

for all $1\leq i\leq n$, no bound variable occurs in $\mathsf{E}_{i-1}$ in the scope of the quantified variable $X_{i}$;

• •

if $G_{i}(X_{i})=G_{j}(X_{j})$, then $c_{i}=c_{j}$.

We indicate a uniform reduction as $\mathsf{E}\leadsto_{\mathsf{uni}}\mathsf{E}^{\prime}$. In other words, a uniform reduction only eliminates a quantifier after having eliminating all quantifiers in its scope, and when a quantified variable $X$ is copied by the effect of some other reduction, all copies of $X$ are reduced using the same rule.

Any uniform reduction $\mathsf{E}_{0}\leadsto_{X_{1}^{c_{1}}}\dots\leadsto_{X_{n}^{c_{n}}}\mathsf{E}_{n}\in\mathcal{P}_{0}$ that converges to a simple polynomial trees induces a coherent valuation $\chi$ of $\mathsf{E}$, where $\chi(X)$ is the unique $c$ such that for all $i$ such that $G_{i}(X_{i})=X$, $c_{i}=c$. We call the valuation $\chi$ the skeleton of the reduction. Conversely, given a coherent valuation $\chi$of $\mathsf{E}$ one can construct a uniform reduction of $\mathsf{E}$ of which $\chi$ is the skeleton.

The following lemma states that the normal form of a uniform reduction is completely determined by its skeleton.

Lemma 7.2**.**

If two convergent uniform reductions $r_{1}:\mathsf{E}\leadsto_{\mathsf{uni}}\mathsf{E}_{1}$, and $r_{2}:\mathsf{E}\leadsto_{\mathsf{uni}}\mathsf{E}_{2}$ have the same skeleton $\chi$, then $\mathsf{E}_{1}=\mathsf{E}_{2}$.

Proof.

Let the depth of a variable $X\in\mathsf{b}\mathcal{V}(\mathsf{E})$ be the number of distinct bound variables within its scope. Let us call a uniform reduction hierarchical if any variable of depth $k+1$ is eliminated only after all variables of depth $k$ have already been eliminated. It is not difficult to check by induction on the length of reductions that (1) any uniform reduction can be transformed into a hierarchical uniform reduction converging onto the same polynomial tree, (2) two hierarchical uniform reductions with same skeleton converge onto the same polynomial tree. The claim then follows from (1) and (2). ∎

We indicate the unique result of a converging uniform reduction from $\mathsf{E}$ with skeleton $\chi$ simply as $\chi(\mathsf{E})$.

For all polynomial tree $\mathsf{F}$, let ${\mathbin{\overline{\mathsf{F}}}}$ be the tree obtained by switching colors on all labels. For all polynomial trees $\mathsf{E}$, $\mathsf{F}$ and variable $X\in\mathsf{f}\mathcal{V}(\mathsf{E})$, we let $\mathsf{E}[X\mapsto\mathsf{F}]$ be the result of replacing all terminal nodes of $\mathsf{E}$ labeled {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}} by $\mathsf{F}$ and all terminal nodes of $\mathsf{E}$ labeled {\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}} by ${\mathbin{\overline{\mathsf{F}}}}$.

Lemma 7.3**.**

• i.

If $\mathsf{E}\leadsto_{\mathsf{uni}}\mathsf{E}^{\prime}$ and $\mathsf{F}\in\mathcal{P}_{0}$, then $\mathsf{E}[X\mapsto_{\mathsf{uni}}\mathsf{F}]\leadsto_{{\mathsf{uni}}}\mathsf{E}^{\prime}[X\mapsto\mathsf{F}]$.

• ii.

If $\mathsf{F}\leadsto_{\mathsf{uni}}\mathsf{F}^{\prime}$, then $\mathsf{E}[X\mapsto\mathsf{F}]\leadsto_{\mathsf{uni}}\mathsf{E}[X\mapsto\mathsf{F}^{\prime}]$.

Let $\mathsf{E}$ be a coherent polynomial tree. We define a coherent valuation $\phi_{\mathsf{E}}:\mathsf{b}\mathcal{V}(\mathsf{E})\to\mathsf{Colors}$ using the well-known strongly connected components algorithm for 2-SAT [3] (see Remark 5.1). We recall that a direct graph $G=(V,E)$ is skew symmetric if there exists an involution ${}^{*}:V\to V$ such that for all $v,w\in V$, $v\to w\in E$ iff $w^{*}\to v^{*}\in E$.

Let $G=(|G|,\|G\|)$ be the directed skew-symmetric graph with vertices the colored variables $X_{i}^{c}$, for all $X_{i}\in\mathsf{b}\mathcal{V}(\mathsf{E})$ and $c\in\mathsf{Colors}$, symmetry $(X_{i}^{c})^{*}=X_{i}^{\mathbin{\overline{c}}}$, and with edges $X_{i}^{\mathbin{\overline{c}}}\to X_{i}^{c}$ if $X_{i}$ is not $\mathbin{\overline{c}}$-eliminable and $X_{i}^{c}\to Y_{j}^{d}$, $Y_{j}^{\mathbin{\overline{d}}}\to X_{i}^{\mathbin{\overline{c}}}$ if $X_{i}^{c}$ is incoherent with $Y_{i}^{\mathbin{\overline{d}}}$. Let $X_{i}^{c}\sim Y_{j}^{d}$ if there is a directed path in $G$ from $X_{i}^{c}$ to $Y_{j}^{d}$ and a directed path from $Y_{j}^{d}$ to $X_{i}^{c}$. The equivalence classes of $\sim$ are usually called strong connected components of $G$. Observe that a strong connected component cannot contain both $X_{i}^{c}$ and $X_{i}^{\mathbin{\overline{c}}}$ (otherwise $\mathsf{E}$ would not be coherent). Let $G/\sim=(|G/\sim|,\|G/\sim\|)$ be the directed graph with vertices the strong connected components of $G$ and an edge $a\to b$ if there is $X_{i}^{c}\in a$ and $Y_{j}^{d}\in b$ and an edge $X_{i}^{c}\to Y_{j}^{d}$ in $G$. $G/\sim$ is then a directed acyclic graph, inducing thus an order relation $\prec$ on $|G/\sim|$. We now define a map $\chi:\mathsf{b}\mathcal{V}(\mathsf{E})\to C$ as follows: let us split $|G/\sim|$ in its connected components $G_{1},\dots,G_{n}$; for each component $G_{i}$, choose a linear ordering $a_{1}\prec_{i}\dots\prec_{i}a_{k_{i}}$ of its vertices, compatible with the order $\prec$. We define a partial function $\phi_{i}:\mathsf{b}\mathcal{V}(\mathsf{E})\rightharpoonup\mathsf{Colors}$ by induction on $\succ_{i}$:

• •

for all $X_{j}^{c}\in a_{k_{i}}$, set $\phi_{i}(X_{j})=c$;

• •

for all $X_{j}^{c}\in a_{k_{i}-l}$, if $\phi_{i}(X_{j})$ is not yet defined, set $\phi_{i}(X_{j})=c$.

Finally let $\phi_{\mathsf{E}}=\bigcup_{i=1}^{n}\phi_{i}$. One can check then that $\phi_{\mathsf{E}}$ is a coherent valuation of $\mathsf{E}$.

Lemma 7.4**.**

If $\mathsf{E}$ and $\mathsf{F}$ are coherent and $X\in\mathsf{f}\mathcal{V}(\mathsf{E})$, then $\mathsf{E}[X\mapsto\mathsf{F}]$ is coherent and $\phi_{\mathsf{E}[X\mapsto\mathsf{F}]}(\mathsf{E}[X\mapsto\mathsf{F}])=\phi_{\mathsf{E}}(\mathsf{E})[X\mapsto\phi_{\mathsf{F}}(\mathsf{F})]$.

Proof.

We have that $\mathsf{b}\mathcal{V}(\mathsf{E}[X\mapsto\mathsf{F}])=\mathsf{b}\mathcal{V}(\mathsf{E})\uplus\biguplus_{i=1}^{k}\mathsf{b}\mathcal{V}(\mathsf{F})$, where $X$ occurs $k$ times in $\mathsf{E}$. Observe that in $\mathsf{E}[X\mapsto\mathsf{F}]$ any bound variable coming from a copy of $\mathsf{F}$ is coherent with any bound variables coming from $\mathsf{E}$. Hence, if we construct the graph $G/\sim$ of the strongly connected components, the variables from $\mathsf{E}$ and those from the copies of $\mathsf{F}$ belong to different connected components of $G/\sim$. Thus, since by construction the value $\phi_{\mathsf{E}[X\mapsto\mathsf{F}]}(Y)$ only depends on the connected component of $Y$ in $G/\sim$, we deduce that $\phi_{\mathsf{E}[X\mapsto\mathsf{F}]}=\phi_{\mathsf{E}}\uplus\biguplus_{i=1}^{k}\phi_{\mathsf{F}}$.

Using this fact along with Lemma 7.3 we deduce the existence of two uniform reductions $\mathsf{E}[X\mapsto\mathsf{F}]\leadsto_{{\mathsf{uni}}}\mathsf{E}[X\mapsto\phi_{\mathsf{F}}(\mathsf{F})]\leadsto_{{\mathsf{uni}}}\phi_{\mathsf{E}}(\mathsf{E})[X\mapsto\phi_{\mathsf{F}}(\mathsf{F})]$ and $\mathsf{E}[X\mapsto\mathsf{F}]\leadsto_{{\mathsf{uni}}}\phi_{\mathsf{E}[X\mapsto\mathsf{F}]}(\mathsf{E}[X\mapsto\mathsf{F}])$ with the same skeleton, so using Lemma 7.2 we deduce our claim. ∎

We can now define $A^{\flat}$ as follows:

Definition 7.2**.**

For all $A\in\mathsf{\Lambda 2^{\kappa\leq 1}}$, we let A^{\flat}:=\tau(\phi_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A))).

From Lemma 7.4 we immediately deduce that $(A[B/X])^{\flat}=A^{\flat}[B^{\flat}/X]$. Moreover, we can check that if $A=B\Rightarrow C$, then $A^{\flat}=B^{\flat}\Rightarrow C^{\flat}$ and that, if $A=\forall X.C$, then since $A^{\flat}$ is obtained by uniform reduction, we can suppose that {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{t}}}(A)\leadsto_{\mathsf{\mathsf{uni}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime}\leadsto_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime\prime}, where \tau({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime\prime})=A^{\flat} and \tau({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime})=\forall X.C^{\flat}, and since $X$ is eliminable in {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{E}}}^{\prime}, $C^{\flat}$ must have one of forms below

[TABLE]

for given types $A_{jk},A_{j},B$ which are strictly less complex than $A$.

The Embedding of Terms

Using the properties of the embedding of type just defined as well as the terms for the Yoneda type isomorphisms from App. A, we can define the embedding of terms from $\mathsf{\Lambda 2^{\kappa\leq 1}}$ to $\mathsf{\Lambda p_{\mu\nu}}$.

Given $\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 1}}}t:A$ (resp. $\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}t:A$), we define a term $t^{\flat}$ such that $\Gamma^{\flat}\vdash_{\mathsf{\Lambda p_{\mu\nu}}}t^{\flat}:A^{\flat}$ (resp. $\Gamma^{\flat}\vdash_{\mathsf{\Lambda p}}t^{\flat}:A^{\flat}$) holds by induction on $t$. If $t=x$, we let $t^{\flat}=x$, if $t=\lambda x.u$, we let $(t)^{\flat}=\lambda x.t^{\flat}$ and if $t=uv$, we let $(t)^{\flat}=u^{\flat}v^{\flat}$. The case of $t=\Lambda X.u$ and $t=uD$ are less obvious:

• •

if $t=\Lambda X.u$, then $A=\forall X.C$ and by the induction hypothesis $\Gamma^{\flat}\vdash u^{\flat}:C^{\flat}$. Moreover, we can suppose that $C^{\flat}$ is of one of the forms of Eq. (11). Hence we must consider two cases:

• a.

A^{\flat}=B^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\mu X.\sum_{k}\prod_{j}A_{jk}^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right\rangle. Then we let t^{\flat}=\mathtt{s}_{{A_{jk}^{\flat}},{B^{\flat}}}\Big{[}u^{\flat}[X\mapsto\mu X.\sum_{k}\prod_{j}A_{jk}^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle]\Big{]}.

• b.

A^{\flat}=B^{\flat}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto\nu X.\prod_{j}A_{j}^{\flat}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\right\rangle. Then we let t^{\flat}=\mathtt{u}_{{A_{j}^{\flat}},{B^{\flat}}}\Big{[}u^{\flat}[X\mapsto\nu X.\prod_{j}A_{j}^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle]\Big{]}.

where for the terms $\mathsf{s}_{A_{jk}^{\flat},B^{\flat}}$ and $\mathsf{u}_{A_{j}^{\flat},B^{\flat}}$ see App. A.

• •

if $t=uD$, then $A=C[D/X]$ and by the induction hypothesis we have $\Gamma^{\flat}\vdash_{\mathsf{\Lambda 2^{\kappa\leq 1}}}u:(\forall X.C)^{\flat}$. Moreover we have $A^{\flat}=C^{\flat}[D^{\flat}/X]$ and as above we can suppose that $C^{\flat}$ is in one of the forms in Eq. (11), so we consider again two cases:

• a.

If (\forall X.C)^{\flat}=B^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\mu X.\sum_{i}\prod_{j}A_{jk}^{\flat}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\right\rangle, then we let $t^{\flat}=\mathsf{t}_{A_{jk}^{\flat},B^{\flat}}[u^{\flat},D^{\flat}]$.

• b.

If (\forall X.C)^{\flat}=B^{\flat}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto\nu X.\prod_{j}A_{j}^{\flat}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\right\rangle\right\rangle, then we let $t^{\flat}=\mathtt{v}_{A_{j}^{\flat},B^{\flat}}[u^{\flat},D^{\flat}]$.

where for the terms $\mathtt{t}_{A_{jk}^{\flat},B^{\flat}}$ and $\mathsf{v}_{A_{j}^{\flat},B^{\flat}}$ see App. A.

Using the constructions above it is a simple exercise to define explicit isomorphisms ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{d}}_{A}[x],\mathtt{d}_{A}^{-1}[x]):A\vdash A^{\flat} for all type $A$ of $\mathsf{\Lambda 2^{\kappa\leq 1}}$.

7.3 The equivalence of $\mathsf{\Lambda 2^{\kappa\leq 0}}/\mathsf{\Lambda 2^{\kappa\leq 1}}$ with $\mathbb{B}/\mu\mathbb{B}$

The two functors ♯ and ♭ preserve all the relevant structure (products, coproducts, exponentials, initial algebras, final coalgebras), but they are not strictly inverse: $(A^{\flat})^{\sharp}$ is not equal to $A$, but only $\varepsilon$-isomorphic to it (e.g. for A=\forall X.((\forall Y.{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{Y}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}})\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}, we have $A^{\flat}=1$ and (A^{\flat})^{\sharp}=\forall X.{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}). Nevertheless, we will establish that the following equivalences hold:

Theorem 7.5**.**

1. i.

$\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 0}})\cong\mathbb{B}$. 2. ii.

$\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})\cong\mu\mathbb{B}$.

The proof of Theorem 7.5 is done by checking (by way of $\beta$-, $\eta$- and $\varepsilon$-rules) that both $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and $\mathsf{\Lambda p_{\mu\nu}}$ embed fully in $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$, using the lemma below (with $\mathbb{C}=\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})$, $\mathbb{D}=\mu\mathbb{B}$, $\mathbb{E}=\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$ and $f(A)=A^{\flat}$).

Lemma 7.6**.**

Let $\mathbb{C},\mathbb{D}$ be full subcategories of a category $\mathbb{E}$. Let $f:\mathsf{Ob}(\mathbb{C})\to\mathsf{Ob}(\mathbb{D})$ be surjective and suppose there is a map $u$ associating each object $a$ of $\mathbb{C}$ with an isomorphism $u_{a}:a\to f(a)$ in $\mathbb{E}$. Then $f$ extends to an equivalence of categories $F:\mathbb{C}\to\mathbb{D}$.

Proof.

Let $F(a)=f(a)$ and $F(g:a\to b)=u_{b}\circ g\circ u_{a}^{-1}\in\mathbb{E}(f(a),f(b))=\mathbb{D}(f(a),f(b))$. $F$ is clearly faithful and surjective. It is also full since for any $h\in\mathbb{D}(F(a),F(b))$ there exists $k=u^{-1}_{b}\circ h\circ u_{a}\in\mathbb{\mathsf{missing}}E(a,b)=\mathbb{C}(a,b)$ such that $h=F(k)$.∎

Let $\mathbb{C}=\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})$, $\mathbb{D}=\mu\mathbb{B}$ and let $\mathbb{E}=\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2p_{\mu,\nu}^{*}})$. We know that there is a surjective map ${}^{\flat}:\mathsf{Ob}(\mathbb{C})\to\mathsf{Ob}(\mathbb{D})$ as well as isomorphisms $(\mathtt{d}_{A}[x],\mathtt{d}_{A}^{-1}[x]):A\to A^{\flat}$ in $\mathbb{E}$. Thus, to apply Lemma 7.6 it remains to check that $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2^{\kappa\leq 1}})$ and $\mu\mathbb{B}$ are full subcategories of $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2p_{\mu\nu}})$. Concretely, this means checking that:

• •

for any term $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$ in which $\Gamma,A$ are $\mathsf{\Lambda 2^{\kappa\leq 1}}$-types we can find a term $u\simeq_{\varepsilon}t$ such that $\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 1}}}u:A$ holds;

• •

for any term $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$ in which $\Gamma,A$ are types of $\mu\mathbb{B}$ we can find a term $u\simeq_{\varepsilon}t$ such that $\Gamma\vdash_{\mathsf{\Lambda p_{\mu\nu}}}u:A$ holds.

This is where we will actually use our embeddings, since we take $u=t^{\sharp}$ in the first case and $u=t^{\flat}$ in the second case. The verification of $t\simeq_{\varepsilon}u$ involves both $\varepsilon$- and $\beta\eta$-equations and is postponed to App. B.

7.4 Program Equivalence in $\mathsf{\Lambda 2^{\kappa\leq 0}}$ is decidable.

Theorem 7.5 can be used to deduce properties of program equivalence in $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ from well-known properties of program equivalence for $\mathbb{B}$ and $\mu\mathbb{B}$. In fact, it is known that $\beta\eta$-equivalence in $\mathsf{\Lambda p}$ (i.e. arrow equivalence in $\mathbb{B}$) is decidable and coincides with contextual equivalence [36], while contextual equivalence for $\mu\mathbb{B}$ is undecidable [8]. Using Theorem 7.5 we obtain similar facts for $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$:

Theorem 7.7**.**

The $\varepsilon$-theory for $\mathsf{\Lambda 2^{\kappa\leq 0}}$ is decidable and coincides with contextual equivalence.

The first claim of Theorem 7.7 is proved by defining a new embedding $t\mapsto t^{\natural}$ of $\mathsf{\Lambda 2^{\kappa\leq 0}}$ into $\mathsf{\Lambda p}$, exploiting the well-known fact that for the terms of the system $\mathsf{\Lambda 2p}$ one can obtain a normal form under $\beta$-reduction and commutative conversions [39]333Actually, [39] does not consider commuting conversions for [math], but these can be added without altering the existence of normal forms.. Using the isomorphisms $\mathtt{d}_{A}[x],\mathtt{d}_{A}^{-1}[x]$ between $A$ and $A^{\flat}$, a term $t$ such that $\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}t:A$ holds is first translated into $u=\mathtt{d}_{A}[t[x_{i}\mapsto\mathtt{d}_{A_{i}}^{-1}[x_{i}]]]$ (where $\Gamma=x_{1}:A_{1},\dots,x_{n}:A_{n}$), and then $t^{\natural}$ is defined as the normal form of $u$. From the fact that $\Gamma^{\flat}\vdash_{\mathsf{\Lambda 2p}}t^{\natural}:A^{\flat}$ and that $t^{\natural}$ is in normal form, we can deduce that $\Gamma^{\flat}\vdash_{\mathsf{\Lambda p}}t^{\natural}:A^{\flat}$ holds, so the embedding is well-defined.

Using the embedding $t\mapsto t^{\natural}$ we prove the proposition below, from which the claim of Theorem 7.7 descends (using the fact that $\simeq_{\beta\eta}$ and $\simeq_{{\mathsf{ctx}}}$ coincide and are decidable in $\mathsf{\Lambda p}$).

Proposition 7.8**.**

The following are equivalent:

• i.

$\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}t\simeq_{\varepsilon}u:A$*; *

• ii.

$\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}t\simeq_{{\mathsf{ctx}}}u:A$.

• iii.

$\Gamma^{\flat}\vdash_{\mathsf{\Lambda p}}t^{\natural}\simeq_{\beta\eta}u^{\natural}:A^{\flat}$.

Proof.

(i.$\Rightarrow$ ii.)

Since $\simeq_{{\mathsf{ctx}}}$ is the maximal consistent theory, it is clear that $\simeq_{\varepsilon}\subseteq\simeq_{{\mathsf{ctx}}}$.

(ii.$\Rightarrow$ iii.)

Suppose $\Gamma^{\flat}\vdash_{\mathsf{\Lambda p}}t^{\natural}\not\simeq_{\beta\eta}u^{\natural}:A^{\natural}$. Since $\simeq_{\beta\eta}$ and $\simeq_{{\mathsf{ctx}}}$ coincide in $\mathsf{\Lambda p}$, there exists a context $\mathtt{C}:(\Gamma^{\flat}\vdash A^{\flat})\Rightarrow(\vdash 1+1)$ such that $\mathtt{C}[t^{\natural}]\not\simeq_{\beta\eta}\mathtt{C}[u^{\natural}]$. Observe that this also implies $\mathtt{d}_{B}^{-1}[\mathtt{C}[t^{\natural}]]\not\simeq_{\beta\eta}\mathtt{d}_{B}^{-1}[\mathtt{C}[u^{\natural}]]$, where $B=\forall X.X\Rightarrow X\Rightarrow X$.

Let $\mathtt{F}:(\Gamma\vdash A)\to(\Gamma^{\flat}\vdash A^{\flat})$ be $(\lambda x_{1}.\dots.\lambda x_{k}.\mathtt{d}_{B}[x])\mathtt{d}_{A_{1}}^{-1}[x_{1}]\dots\mathtt{d}_{A_{k}}^{-1}[x_{k}]$, where $\Gamma=\{x_{1}:A_{1},\dots,x_{k}:A_{k}\}$. Then $\mathtt{F}[t]\simeq_{\beta\eta}t^{\natural}$ and $\mathtt{F}[u]\simeq_{\beta\eta}u^{\natural}$.

Let now $\mathtt{E}:(\Gamma\vdash_{\mathsf{\Lambda 2p}}A)\to(\vdash_{\mathsf{\Lambda 2p}}\forall X.X\Rightarrow X\Rightarrow X)$ be the context $\mathtt{d}_{B}^{-1}\circ\mathtt{C}\circ\mathtt{F}$, so that $\mathtt{E}^{\sharp}:(\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}A)\to(\vdash_{\mathsf{\Lambda 2^{\kappa\leq 0}}}\forall X.X\Rightarrow X\Rightarrow X)$. We also have $\mathtt{E}\simeq_{\varepsilon}\mathtt{E}^{\sharp}$ by Th. B.2 in App. B. We now have $\mathtt{E}^{\sharp}[t]\simeq_{\varepsilon}\mathtt{E}[t]\simeq_{\beta\eta}\mathtt{d}_{B}^{-1}[\mathtt{C}[t^{\natural}]]\not\simeq_{\beta\eta}\mathtt{d}_{B}^{-1}[\mathtt{C}[u^{\natural}]]\simeq_{\beta\eta}\mathtt{E}[u]\simeq_{\varepsilon}\mathtt{E}^{\sharp}[t]$, so we can conclude that $t\not\simeq_{{\mathsf{ctx}}}u$.

(iii.$\Rightarrow$ i.)

This immediately follows from the fact $t^{\natural},u^{\natural}$ are obtained from $t,u$ by applying isomorphisms relative to $\varepsilon$-equivalence.

∎

7.5 Program Equivalence in $\mathsf{\Lambda 2^{\kappa\leq 1}}$ is undecidable.

It is well-known that contextual equivalence is undecidable in $\mu\mathbb{B}$ [8]. From this fact we can easily deduce, using the encoding ♯, that contextual equivalence is also undecidable in $\mathsf{\Lambda 2^{\kappa\leq 1}}$.

We do not know if the $\varepsilon$-theory and contextual equivalence coincide in $\mathsf{\Lambda 2^{\kappa\leq 1}}$, as it is not clear whether the embedding $t\mapsto t^{\natural}$ scales to $\mathsf{\Lambda 2^{\kappa\leq 1}}$: this depends on the existence of normal forms for commutative conversions, which are not known to hold in presence of $\mu,\nu$-types (although this is conjectured in [24]).

For this reason, we think it’s worth to provide a direct argument for the undecidability of the $\varepsilon$-theory in $\mathsf{\Lambda 2^{\kappa\leq 1}}$. The correspondence between universal types in $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and $\mu,\nu$-types provides a way to compute $\varepsilon$-equivalence in an indirect way. In fact, the $\varepsilon$-rule for a type $\forall X.A$ of $\mathsf{\Lambda 2^{\kappa\leq 1}}$ can be interpreted as a principle expressing the uniqueness of a function defined by an inductive/co-inductive principle. For example, in the case of the type \mathtt{int}=\forall X.({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow({\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}), from the isomorphism \mathtt{int}\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}\mu X(X+1) we deduce the validity of the $\varepsilon$-rule in Fig. 15(a). Let $C=\mathtt{int}$, $u=\mathsf{s}$, $D$ (the successor function) and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}} be given by some function $f:\mathtt{int}\Rightarrow A$. Then the $\varepsilon$-rule yields the uniqueness rule in Fig. 15(b), which expresses the uniqueness of functions defined by iterations.

We will exploit this correspondence to establish the undecidability of the equivalence generated by $\varepsilon$-rules from the result below.

Theorem 7.9** (Okada, Scott).**

Let $\mathsf{S}$ be a system containing the type $\mathtt{int}$ of integers (with terms $\mathsf{0}:\mathtt{int}$ and $\mathsf{s}:\mathtt{int}\Rightarrow\mathtt{int}$), closed by arrow types and having, for all type $A,B$ a recursor $\mathsf{rec}_{A,B}:(\mathtt{int}\Rightarrow A\Rightarrow B\Rightarrow B)\Rightarrow(A\Rightarrow B)\Rightarrow(A\Rightarrow\mathtt{int}\Rightarrow B)$ satisfying

[TABLE]

Let $\simeq_{\gamma}$ be an equivalence over $\mathsf{S}$ containing $\simeq_{\beta},\simeq_{\eta}$ and closed by the following rule:

[TABLE]

for all $f:A\Rightarrow\mathtt{int}\Rightarrow B$ and $h:\mathtt{int}\Rightarrow A\Rightarrow B\Rightarrow B$. Then $\simeq_{\gamma}$ is undecidable.

Let us first show that we can restrict to a weaker rule:

Lemma 7.10**.**

The rule (U) is deducible from the rule

[TABLE]

Proof.

Let $Q=\mathsf{rec}_{A,B}h(\lambda x.fx\mathsf{0})$. Since $Qa(\mathsf{S}y)\simeq hya(Qay)$ and $Qa\mathsf{0}\simeq fa\mathsf{0}$, by (wU) we deduce $Qay\simeq\mathsf{rec}_{A,B}h(\lambda x.Qa0)ay\simeq\mathsf{rec}_{A,B}h(\lambda x.fa\mathsf{0})ay$.

Now, if $fx(\mathsf{S}y)\simeq hxy(fxy)$ holds, by (wU) we deduce $fay\simeq\mathsf{rec}_{A,B}h(\lambda x.fa0)ay$ and by composing this with the equivalence above we finally get $fay\simeq\mathsf{rec}_{A,B}h(\lambda x.fx0)ay$. ∎

We now establish some preliminary properties of $\varepsilon$-equivalence over the type $\mathtt{int}$. For simplicity, we will work in an extension of $\mathsf{\Lambda 2^{\kappa\leq 1}}$ with product types. We let $\mathsf{0}=\Lambda X.\lambda fx.x$ and $\mathsf{s}=\lambda y.\Lambda X.\lambda fx.f(yXfx)$, $\mathsf{P}=\lambda x.\pi_{2}\left(x(\mathtt{int}\times\mathtt{int})\lambda y.\langle\mathsf{s}(\pi_{1}y),\pi_{1}y\rangle\langle\mathsf{0},\mathsf{0}\rangle\right)$.

Lemma 7.11**.**

• •

$x:\mathtt{int}\vdash x\simeq_{\varepsilon}x(\mathtt{int})(\mathsf{s})\mathsf{0}$.

• •

$\mathsf{P}(\mathsf{s}x)\simeq_{\varepsilon}x$.

Proof.

We prove both results as a consequence of unicity of iteration. If $Fx=x$, then $F\mathsf{0}\simeq_{\beta}\mathsf{0}(\mathtt{int})(\mathsf{s})\mathsf{0}$ and $F(\mathsf{s}x)=\mathsf{s}x=\mathsf{s}(Fx)$, whence by unicity $x=Fx\simeq_{\varepsilon}x(\mathtt{int})(\mathsf{s})\mathsf{0}$.

Let {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}[x]:=x(\mathtt{int}\times\mathtt{int})\lambda y.\langle\mathsf{s}(\pi_{1}y),\pi_{1}y\rangle\langle\mathsf{0},\mathsf{0}\rangle. We have $\mathsf{P}(\mathsf{s}\mathsf{0})=\mathsf{0}$ and, since \mathsf{P}(\mathsf{s}x)\simeq_{\beta}\pi_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}[x], and \pi_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}[\mathsf{s}x]\simeq_{\beta}\mathsf{s}(\pi_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}[x]), we have \mathsf{P}(\mathsf{s}(\mathsf{s}x))\simeq_{\beta}\mathsf{s}(\pi_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}[x])\simeq_{\beta}\mathsf{s}(\mathsf{P}(\mathsf{s}x)), so by unicity we conclude $\mathsf{P}(\mathsf{s}x)\simeq_{\varepsilon}x(\mathtt{int})(\mathsf{s})\mathsf{0}\simeq_{\varepsilon}x$. ∎

To apply Theorem 7.9 we will exploit the type $\mathsf{Rec}_{Y}=\forall X.(\mathtt{int}\Rightarrow Y\Rightarrow X\Rightarrow X)\Rightarrow(Y\Rightarrow X)\Rightarrow Y\Rightarrow\mathtt{int}\Rightarrow X$. Observe that $\mathsf{Rec}_{Y}$ is isomorphic to the non-polymorphic type $(\mu X.(\mathtt{int}\times Y\times X)+Y)\times\mathtt{int}\times Y$. Using Lemma 7.11, it can be checked by induction that the term $\mathsf{rec}:\forall Y.\mathsf{Rec}_{Y}$ given by $\mathsf{rec}(X)(Y)hxay=y(X)(\lambda z.h(\mathsf{P}y)az)(xa)$ yields, for all types $A,B$ of $\mathsf{\Lambda 2^{\kappa\leq 1}}$, a recursor $\mathsf{rec}(A)(B)$ in $\mathsf{\Lambda 2}_{\kappa\leq 3}$ under $\simeq_{\varepsilon}$.

Proposition 7.12**.**

The rule (U) holds in $\mathsf{\Lambda 2^{\kappa\leq 1}}$ under $\simeq_{\varepsilon}$ with $\mathsf{rec}$ as recursor.

Proof.

Let $\mathsf{Z}:\mathtt{int}\Rightarrow A\Rightarrow\mathtt{int}\Rightarrow\mathtt{int}$ be the term $\mathsf{Z}xyz=\mathsf{s}z$. We claim that $\mathsf{rec}(A)(\mathtt{int})(\mathsf{Z})(\lambda x.0)ay\simeq_{\varepsilon}y$. In fact $\mathsf{rec}(A)(\mathtt{int})(\mathsf{Z})(\lambda x.0)ay\simeq_{\beta}y(\mathtt{int})(\lambda z.\mathsf{Z}(\mathsf{P}y)az)\mathsf{0}\simeq_{\beta\eta}y(\mathtt{int})(\mathsf{s})\mathsf{0}\simeq_{\varepsilon}y$, by Lemma 7.11. Let now $f:A\Rightarrow\mathtt{int}\Rightarrow B$. If $fa(\mathsf{Z}xay)\simeq_{\varepsilon}hxa(fax)$, we deduce, by the $\varepsilon$-rule in Fig. 16 with $t[x]=fax:\mathtt{int}\vdash B$, that $fa(\mathsf{rec}(A)(\mathtt{int})(\mathsf{Z})(\lambda x.0)ay)\simeq_{\varepsilon}\mathsf{rec}(A)(B)(h)(\lambda x.fa0)\ ay$. By what we just proved this implication corresponds to the rule (wU), so we can conclude by Lemma 7.10. ∎

We can thus finally conclude:

Theorem 7.13**.**

Both the $\varepsilon$-theory and contextual equivalence for $\mathsf{\Lambda 2^{\kappa\leq 1}}$ are undecidable.

8 Program Equivalence and Predicativity

In this section we sketch an example of how the correspondence between the polymorphic system $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and the monomorphic system $\mu\mathbb{B}$ can be used to prove non-trivial properties of program equivalence in $\mathsf{\Lambda 2}$.

A main source of difficulty to compute program equivalence of polymorphic programs is that, while these can be instantiated at any type, programs with different type instantiations can behave in the same way. This is made evident by the $\varepsilon$-rules from Fig. 12(a) and Fig. 12(b), which allow one to permute an instantiation on a type $A$ into one on any type $B$, provided there is a suitable term {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}t}[x]:A\vdash^{\Gamma}B.

A natural question is thus whether one can use such rules to turn a program into one with instantiations of lower complexity. This cannot be possible in all cases since the so-called predicative fragments of $\mathsf{\Lambda 2}$, that is the subsystems of $\mathsf{\Lambda 2}$ in which type instantiations must satisfy some complexity bound, are known to be strictly less expressive than $\mathsf{\Lambda 2}$ (see for instance [23]). However, using the correspondence between universal types in $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and initial algebras, we will deduce a useful sufficient condition under which this simplifications can be put forward in $\mathsf{\Lambda 2^{\kappa\leq 1}}$.

After presenting this condition, we will use it to provide a quick proof based on type isomorphisms of a result that was established in [31] by the same authors by computing $\varepsilon$-rules directly: any polymorphic program in a certain fragment of $\mathsf{\Lambda 2}$ (in fact, a fragment of $\mathsf{\Lambda 2^{\kappa\leq 0}}$) arising from the encoding of finite sum and product types, can be transformed into one containing only atomic instantiations.

We first illustrate our idea with an example.

Example 8.1** (pointwise induction).**

Suppose we recursively define a function $t:\mathtt{int}\Rightarrow(A\Rightarrow B)$ by “$\mathtt{int}$-induction on $A\Rightarrow B$”: we let $t(0)$ be some fixed function $u:A\Rightarrow B$ and we let $t({n+1})$ be the function $x\mapsto h((t(n)(x))$, for some $h:B\Rightarrow B$. In fact, since the variable $x:A$ is used as a parameter, we could equivalently define $t$ by “$\mathtt{int}$-induction on $B$”: we let $t_{x}(0)$ be some fixed $c=u(x)$, and $t_{x}(n+1)$ be $h(t_{x}(n))$, so that $t(n)(x)=t_{x}(n)$.

A bit more formally, the argument from Example 8.1 shows the equivalence of the two contexts {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}_{1}}=[\ ](A\Rightarrow B)(\lambda fx.h(fx))(u) and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}_{2}}=\lambda x.[\ ](B)(h)(ux) of type $\mathtt{int}\vdash A\Rightarrow B$. Observe that these two contexts are not $\beta\eta$-equivalence and, in particular, that they differ for the fact that the second contains a type instantiation which is strictly less complex than the one of the first.

We can formalize the notion of being “less complex” as follows: given a type $A$ of $\mathsf{\Lambda 2}$, we let the set $\mathtt{RS}(A)$ of right simplifications of $A$ be inductively as follows:

[TABLE]

Moreover, for all type $A$, we let $\mathsf{at}(A)\in\mathtt{RS}(A)$ indicate the rightmost variable of $A$.

The reasoning from Example 8.1 can be justified at a more abstract level by exploiting the isomorphism \mathtt{int}\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}\mu X.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}+1, which shows that $\mathtt{int}$ is isomorphic to the initial $X+1$-algebra. In fact, by appealing to initial algebras we can justify similar arguments for a large class of inductive types like $\mathtt{int}$, that we define as follows (essentially following a terminology from [31]): let us call a type $P[X]$ polynomial when it is of the form

[TABLE]

and let us call $P[X]$ constant if $X$ does not occur in any of the $A_{jk}$. This terminology is justified by the isomorphism

[TABLE]

showing that the universal type $\forall X.P[X]$ coincides (under the $\varepsilon$-theory) with the initial \sum_{k}\prod_{j}A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle-algebra. Note that the fixpoint binder $\mu X.$ occurs precisely when $P[X]$ is non-constant.

Let a $P[X]$-algebra be a triple $(\Gamma,C,\langle u_{k}\rangle_{k})$ made of a context $\Gamma$, a type $C$ and terms u_{k}:\langle x_{j}:A_{jk}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto C\right\rangle\rangle_{j}\vdash^{\Gamma}C, and a $P[X]$-algebra morphism from $(\Gamma,C,\langle u_{k}\rangle_{k})$ to $(\Delta,D,\langle v_{k}\rangle_{k})$ be an inclusion $\Gamma\subseteq\Delta$444We consider here context inclusions for simplicity but one might rather consider a context morphism. and a term $w[x]:C\vdash^{\Delta}D$ such that

[TABLE]

The pair $(\forall X.P,\langle\mathsf{t}^{P}_{k}\rangle_{k})$, where $\mathsf{t}^{P}_{k}[\langle x_{j}\rangle_{j}]$ is the term

[TABLE]

is the initial $P[X]$-algebra, that is, the initial object in the category of $P[X]$-algebras and $P[X]$-algebra morphisms. This means in particular, that for all $P[X]$-algebra $(C,\langle u_{k}\rangle_{k})$, one can define a context

[TABLE]

called $P[X]$-induction on $C$, which is a $P[X]$-algebra morphism which satisfies the following universal property: for all $P[X]$-algebra morphism $v[x]$ from the initial $P[X]$-algebra to $(C,\langle u_{k}\rangle_{k})$, $v[x]\simeq_{\varepsilon}\mathtt{Ind}_{C}^{P}(\langle u_{k}\rangle_{k})[x]$.

In Example 8.1 first observe that the type $\mathtt{int}$ is of the form $\forall X.\mathtt{int}[X]$, where $\mathtt{int}[X]=(X\Rightarrow X)\Rightarrow(X\Rightarrow X)$ is a polynomial type. The two ways of defining our function correspond to two $\mathtt{int}[X]$-algebras $(\emptyset,A\Rightarrow B,\langle x\mapsto\lambda y.h(xy),u\rangle)$ and $(\{y:A\},B,\langle x\mapsto hx,uy\rangle)$. These are related by the $\mathtt{int}[X]$-algebra morphism $v[x]=xy$; moreover, the two contexts {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}_{1} and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}_{2} correspond to the associated $\mathtt{int}[X]$-induction morphisms (respectively on $A\Rightarrow B$ and $B$). We can then deduce the equivalence {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}}_{1}\simeq_{\varepsilon}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{C}_{2}} from the fact that $\mathtt{int}$ is the initial $\mathtt{int}[X]$-algebra.

The moral of this argument is that one can simplify the type of a $P[X]$-induction whenever one has a $P[X]$-algebra morphism which is an elimination context.

Definition 8.1** (elimination and introduction contexts).**

Elimination contexts* and introduction contexts for $\mathsf{\Lambda 2}$ are defined by the grammars*

[TABLE]

A pair of dual contexts (noted ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}})_{A\vdash B}) is a pair made by an elimination context {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}:A\vdash B and an introduction context {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{I}}:B\vdash A such that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{I}}\circ{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{E}}\simeq_{\eta}[\ ].

For any type $A$ and right simplification $B\in\mathtt{RS}(A)$, we can always construct a pair of dual contexts ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}})_{A\vdash B} by letting {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}} be $[\ ]$ followed by type and term variable applications and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}} be made of abstractions on the same variables. For example, if $A=\forall X.Y\Rightarrow\forall Z.(X\Rightarrow Y)\Rightarrow Z$ and $B=(X\Rightarrow Y)\Rightarrow Z$, then we can let {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}}=[\ ]XyZ and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}}=\Lambda X.\lambda y.\Lambda Z.[\ ].

The lemma below generalizes to an arbitrary polynomial type $P[X]$ the reasoning of Example 8.1, allowing to turn a $P[X]$ induction on $A$ into a $P[X]$-induction on $B$, for $B\in\mathtt{RS}(A)$:

Lemma 8.1** (simplification lemma).**

Let $P[X]$ be a polynomial type, $A$ be a $\mathsf{\Lambda 2}$-type, $B\in\mathtt{RS}(A)$, and ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}})_{A\vdash B} be a pair of dual contexts. If {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}} is a morphism between two $\Phi_{P}^{X}$-algebras $(\Gamma,A,\langle u_{k}^{A}\rangle_{k})$ and $(\Delta,B,\langle u_{k}^{B}\rangle)$, then

[TABLE]

Proof.

Since {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}}\big{[}[\ ](A)\langle\lambda\langle x_{j}\rangle_{j}.u_{k}^{A}[\langle x_{j}\rangle_{j}]\rangle_{k}\big{]} and $[\ ](B)\langle\lambda\langle x_{j}\rangle_{j}.u_{k}^{B}[\langle x_{j}\rangle_{j}]\rangle_{k}$ are both $P[X]$-algebra morphisms from the initial $P[X]$-algebra to $(B,\langle u_{k}^{B}\rangle)$, initiality implies that they are $\varepsilon$-equivalent. The claim then follows by applying $\eta$-equivalences. ∎

When $P[X]$ is a constant polynomial type, from Lemma 8.1 we can deduce a rather striking fact: any type instantiation of the initial algebra $\forall X.P[X]$ on a type $A$ can be atomized, i.e. transformed into a term using a type instantiation on the variable $\mathsf{at}(A)$.

Let us fix, for all type $A$, a pair of dual contexts ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}}_{A},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{In}}_{A})_{A\vdash\mathsf{at}(A)}.

Lemma 8.2** (atomization lemma).**

For all constant polynomial type $P[X]$ and type $B$ of $\mathsf{\Lambda 2}$,

[TABLE]

Proof.

Since $P[X]$ is constant, for any choice of $k,j$, A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto B\right\rangle=A_{jk} and $\Phi^{X}_{A_{jk}}(t)=x$. This implies that, given the context \Gamma=\{\big{\langle}y_{k}:\langle{A_{jk}}\rangle_{j}\Rightarrow B\big{\rangle}_{k}\}, {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}}_{B} is trivially a $P[X]$-algebra morphism from $(\Gamma,B,\langle y_{k}\langle x_{j}\rangle_{j}\rangle_{k})$ to (\Gamma,\mathsf{at}(B),\langle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{El}}_{B}[y_{k}\langle x_{j}\rangle_{j}\rangle_{k}]). We then have

[TABLE]

[TABLE]

where the last term is the desired one. ∎

While the lemma above is rather technical, it has a rather intuitive explanation: it permits to transform any instantiations of a type of the form $\forall X.P[X]$, where $P[X]$ is a constant polynomial type, into an atomic instantiation, preserving the contextual behavior of the program. This property can be restated as the existence of an embedding between the fragment $\mathsf{\Lambda 2^{Poly}}$ (see [31]) of $\mathsf{\Lambda 2}$ (in fact, of $\mathsf{\Lambda 2^{\kappa\leq 0}}$) in which all universal types are of the form $\forall X.P[X]$, for some polynomial type $P[X]$, and the predicative fragment $\mathsf{\Lambda 2_{at}}$ of $\mathsf{\Lambda 2}$ (see [15]), in which all type instantiations are atomic.

Theorem 8.3** (atomizing embedding).**

If $\Gamma\vdash_{\mathsf{\Lambda 2^{Poly}}}t:A$, then there exists a term ${t^{\downarrow}}$ such that $\Gamma\vdash_{\mathsf{\Lambda 2_{at}}}{t^{\downarrow}}:A$ and $t\simeq_{\varepsilon}{t^{\downarrow}}$.

Proof.

$t^{\downarrow}$ is obtained by replacing in $t$ any subterm of the form $tB$, with $B$ non-atomic, as in Eq. (14).

∎

Remark 8.1** (Comparing predicative and impredicative embeddings of $\mathsf{\Lambda p}$).**

The result above is discussed in [31] in connection with some results from [15], which describes a variant FF of the standard embedding ♯ of $\mathsf{\Lambda p}$ into $\mathsf{\Lambda 2}$ whose target is the predicative systems $\mathsf{\Lambda 2_{at}}$. In fact, by composing ♯ with atomization $t\mapsto(t^{\sharp})^{\downarrow}$ one obtains an embedding of $\mathsf{\Lambda p}$ into $\mathsf{\Lambda 2_{at}}$ which is $\beta$-equivalent to FF. From this fact we deduce that the standard embedding and the predicative variant from [15] are indeed $\varepsilon$-equivalent.

9 Conclusion

Related Work

The connection between parametricity, dinaturality and the Yoneda isomorphism is well-known [7, 32, 19]. The extension of this correspondence to initial algebras comes from [41]. [9] exploits this connection to define a schema to test the equivalence of two programs $t,u$ of type \forall X.(F\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow(G\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle\Rightarrow X^{\prime})\Rightarrow H\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle by first instantiating $X$ as \alpha=\mu X.F\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and then applying $t,u$ to the canonical morphism F\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\alpha\right\rangle\Rightarrow\alpha (in fact, this is exactly how one side of the isomorphisms \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} are constructed). The possibility of expressing program equivalence through naturality conditions has recently attracted new attention due to [4], where these are investigated using ideas from homotopy type theory. Type isomorphisms in $\mathsf{\Lambda 2}$ with the Yoneda lemma are also discussed in [20]. In [30] a similar restriction based on the Yoneda isomorphism is used by the first author to describe a fragment of second order multiplicative linear logic with a decidable program equivalence.

Future Work

The definition of the characteristic employs an acyclicity condition which is reminiscent of linear logic proof-nets. In particular, we would like to investigate whether the alternating paths can be related to the cyclic proofs for linear logic systems with $\mu,\nu$-types [6]. Moreover, the notion of characteristic seems likely to scale to second order multiplicative-exponential linear logic, an extension which might lead to better expose the intrinsic duality in the tree-shapes in Fig. 6.

The connection between Yoneda type isomorphisms and proof-search techniques suggests to look for canonical proof-search algorithms for $\mathsf{\Lambda 2^{\kappa\leq 0}}$ and $\mathsf{\Lambda 2^{\kappa\leq 1}}$ (for instance using focusing as suggested in [35]). Moreover, the appeal to least/greatest fixpoints suggests a connection with the technique to count inhabitants by computing fixpoints of polynomial equations [44]. For example, given A=({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{1}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{2}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}, one can show by proof-theoretic reasoning that the number $|A|$ of inhabitants of $A$ is a solution of the fixpoint equation $|A|=|A_{Y_{1}}|+(|A|\times|A_{Y_{2}}|)$, where A_{Y_{i}}=({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{1}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{2}\Rightarrow{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}})\Rightarrow{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{i}, which implies $|A|=0$, since $|A_{Y_{i}}|=0$. On the other hand, Yoneda type isomorphisms yield the strikingly similar computation \forall\vec{Y}X.A\equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}\forall\vec{Y}.\mu X.{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{1}+({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\times{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}_{2})\equiv_{\vec{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{Y}}}}\mu X.0+({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\times 0)\equiv 0.

Finally, we would like to explore an apparent correspondence between Yoneda type isomorphisms of the form

[TABLE]

and the so-called inversion principles discussed in the proof-theoretic literature (see [26]), which relate introduction and elimination rules for generalized connectives [33, 38, 5] (for example, the isomorphism

[TABLE]

encodes the symmetry between rules for a ternary connective ${\dagger}$ as shown in Fig. 17).

Appendix A The $\varepsilon$-Theory and the Yoneda Isomorphisms

We prove that the isomorphisms \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} and \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} hold under the $\varepsilon$-theory. Let us start from \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}, recalled below:

[TABLE]

In the case of Eq. (15) we can construct terms

[TABLE]

where T\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle=\sum_{k}\exists\vec{Y}_{k}.\prod_{j}A_{jk}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and \alpha=\mu X.T\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, $\mathtt{in}_{k}^{\sharp I}:X_{k}\Rightarrow\sum_{k}^{\sharp I}X_{k}$ and $\mathtt{prod}_{j}:\langle X_{j}\rangle_{j}\Rightarrow\prod_{j}^{\sharp J_{k}}X_{j}$ are defined composing usual sum and product constructors, and $\mathsf{pack}$ is defined as follows:

[TABLE]

With such terms we can then construct a term

[TABLE]

Moreover, using sum and product destructors we can construct terms

[TABLE]

where \Delta=\{\langle f_{k}:\forall\vec{Y}_{k}.\langle A_{jk}\left\langle{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}\mapsto Z\right\rangle\rangle_{j}\Rightarrow Z\rangle_{k}\} and

[TABLE]

where $\pi^{j}_{i}$ and $\delta^{\sharp K}(t,\langle z.u_{k}\rangle_{k})$ indicate suitable generalized product and sum destructors which can be defined inductively using product and sum destructors, and the term $\mathsf{unpack}$ is defined as follows:

[TABLE]

One can check that \mathtt{b}[x,{\alpha}]\big{[}\langle f_{k}\mapsto\hat{\mathtt{a}}_{k}\rangle_{k}\big{]}:T\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\mapsto\alpha\right\rangle\vdash\alpha is $\beta\eta$-equivalent to $\mathsf{in}_{T}x$, from which we deduce

[TABLE]

In this way the isomorphism \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}} are realized in $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2p_{\mu,\nu}^{*}})$ by the two terms below:555We are here supposing that $X$ does occur in at least some of the $A_{jk}$ (so that $\mu X.$ actually occurs in the left-hand type of \equiv_{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}}). If this is not the case, the construction can be done in a similar (and simpler) way.

[TABLE]

We can compute then

[TABLE]

and

[TABLE]

[TABLE]

where the central $\varepsilon$-equivalence is justified using the $\varepsilon$-rule in Fig. 12(a) with $E=\alpha$, $F=X$, $e_{k}=\hat{\mathtt{a}}_{k}$ and $\mathtt{v}[x]=\mathsf{fold}_{T}(\lambda x.\mathtt{b}[x,{X}])x$, with the last premise given by the computation below:

[TABLE]

[TABLE]

[TABLE]

where the last $\beta$-equation can be checked by unrolling the definition of $\Phi^{X}_{T}$:

[TABLE]

Let us now consider the isomorphism \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}, recalled below:

[TABLE]

We can define terms666We are here supposing that $X$ does occur in at least some of the $A_{j}$ (so that $\nu X.$ actually occurs in the left-hand type of \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}}). If this is not the case, the construction can be done in a similar (and simpler) way.

[TABLE]

where U\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle=\forall\vec{Y}_{j}.\prod_{j}A_{j}\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle and \beta=\nu X.U\left\langle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{X}}\right\rangle, and a term

[TABLE]

Moreover, using product constructors we can construct a term

[TABLE]

with $\mathtt{d}[\langle f_{j}\rangle_{j},Z]=\lambda z.\Lambda\vec{Y}_{j}.\mathsf{prod}^{\sharp J}(\langle f_{j}\vec{Y}_{j}z\rangle_{j})$ and a term

[TABLE]

where \mathtt{v}_{A_{j},B}[x,Z]=\lambda\langle f_{j}\rangle_{j}.\Phi_{B}^{X}\big{(}\mathsf{unfold}_{U}(\mathtt{d}[\langle f_{j}\rangle_{j},Z])x\big{)}.

In this way the isomorphism \equiv_{{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}{X}}} are realized in $\mathbb{C}_{\varepsilon}(\mathsf{\Lambda 2p_{\mu,\nu}^{*}})$ by the two terms below:

[TABLE]

We leave it the reader to check that $\mathtt{u}[\mathtt{v}[x]]\simeq_{\varepsilon}x$ and $\mathtt{v}[\mathtt{u}[x]]\simeq_{\varepsilon}x$, using an argument similar to the one for $\mathtt{s}$ and $\mathtt{t}$ and using the $\varepsilon$-rule in Fig. 12(b).

Appendix B $\mathsf{\Lambda 2^{\kappa\leq 1}}$ and $\mu\mathbb{B}$ are full subcategories of $\mathsf{\Lambda 2p_{\mu,\nu}^{*}}$

Given a term $t$ with $n$ free variables $x_{1},\dots,x_{n}$ and $n$ terms \vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u}_{i}}[x], we let t\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u}} be shorthand for t[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u}_{1}[x_{1}]/x_{1},\dots,{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}u}_{n}[x_{n}]/x_{n}].

In this section we prove the following commutations:

Proposition B.1**.**

If $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$, then \Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A}[t]}\simeq_{\varepsilon}{t^{\sharp}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma}}:A^{\sharp}. 2. 2.

If $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$, then \Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{d}}_{A}[t]}\simeq_{\varepsilon}{t^{\flat}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{d}}}_{\Gamma}}:A^{\flat}.

In fact, from Proposition B.1 we immediately deduce our fullness claims:

Theorem B.2**.**

If $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$ and $\Gamma,A$ are $\mathsf{\Lambda 2^{\kappa\leq 1}}$-types, then there exists $u$ such that $\Gamma\vdash_{\mathsf{\Lambda 2^{\kappa\leq 1}}}u:A$ and $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}{t}\simeq_{\varepsilon}{u}:A$. 2. 2.

If $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}t:A$ and $\Gamma,A$ are $\mathsf{\Lambda p_{\mu\nu}}$-types, then there exists $u$ such that $\Gamma\vdash_{\mathsf{\Lambda p_{\mu\nu}}}u:A$ and $\Gamma\vdash_{\mathsf{\Lambda 2p_{\mu,\nu}^{*}}}{t}\simeq_{\varepsilon}{u}:A$.

Proof.

In the first case let $u=t^{\sharp}$, and in the second case let $u=t^{\flat}$. ∎

We limit ourselves to check the first statement of Prop. B.1, as the other one is established by computing $\varepsilon$-equivalences in a similar way. We need the following two technical lemmas.

Lemma B.3**.**

For all $t:\forall X.A$ as in (15) and type $C$,

[TABLE]

Proof.

From {xC\vec{Y}\ (\Phi_{A_{1}}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})[z_{1}])\dots(\Phi_{A_{k}}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})[z_{k}])}\simeq_{\varepsilon}^{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C}}{\Phi_{P}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})\big{[}xC^{\sharp}\vec{Y}z_{1}\dots z_{k}\big{]}} we deduce t\simeq_{\varepsilon}{\Lambda\vec{Y}.\lambda\vec{z}.\Phi_{P}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C})\circ\Phi_{P}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})\big{[}xC^{\sharp}\vec{Y}\ z_{1}\dots z_{k}\big{]}}\simeq_{\varepsilon}{\Lambda\vec{Y}.\lambda\vec{z}.xC^{\sharp}\vec{Y}z_{1}\dots z_{k}}\simeq_{\eta}{xC^{\sharp}}, where $t$ is the lefthand term in Equation 17. ∎

Lemma B.4**.**

Let $A$ be as in Lemma B.3. Then for all type $C$, {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\forall X.A}C^{\sharp}}\simeq_{\varepsilon}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A[C/X]}}.

Proof.

By a simple calculation we can deduce {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\forall X.A}C^{\sharp}}\simeq_{\beta}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A}[xC^{\sharp}]} and

{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A[C/X]}}\simeq_{\beta}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{A}\Big{[}\Lambda\vec{Y}.\lambda\vec{z}.\Phi_{F}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C})\big{[}xC\vec{Y}\ (\Phi_{A_{f(i_{1})}}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})[z_{1}])\dots(\Phi_{A_{f(i_{k})}}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}^{-1}_{C})[z_{k}])\big{]}\Big{]}}, so we can conclude by Lemma B.3. ∎

Proof of Proposition B.1.

By induction on $t$, we only consider some interesting cases:

• •

if $t={uC}$, then $A=B[C/Y]$, ${t^{\sharp}}={u^{\sharp}C^{\sharp}}$ and by the induction hypothesis {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\forall Y.B}[u]}\simeq_{\varepsilon}{u^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}}. By Lemma B.4 and the induction hypothesis we have {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{B[C/Y]}[u]}\simeq_{\varepsilon}{({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\forall Y.B}[u])C^{\sharp}}\simeq_{\varepsilon}{(u^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma})C^{\sharp}}={t^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}} (as $Y\notin FV(\Gamma)$).

• •

if $t={\delta_{C}(u,x.v_{1},x.v_{2})}$, then ${t^{\sharp}}={u^{\sharp}C^{\sharp}\ \lambda x.v_{1}^{\sharp}\ \lambda x.v_{2}^{\sharp}}$ and by the induction hypothesis we have {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{B_{1}+B_{2}}[u]}\simeq_{\varepsilon}{u^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}} and {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C}[v_{i}]}\simeq_{\varepsilon}{v_{i}^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma,{x}:B_{i}}}. We can compute then

[TABLE]

• •

if $t={\xi_{C}u}$, then ${t^{\sharp}}={u^{\sharp}C}$ and by the induction hypothesis {{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{0}[u]}\simeq_{\varepsilon}{u^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}} so we have {t^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}}={(u^{\sharp}\circ_{\mathsf{m}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma})C}\simeq_{\varepsilon}{({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C}[u])C}\simeq_{\varepsilon}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C}[uC]} where the last step is an application of Lemma B.4.

• •

if $t=\mathsf{in}_{P}u$, then $t^{\sharp}[x]=\Lambda X.\lambda f.f(\Phi_{(P^{\sharp})}^{X}(xXf)[u^{\sharp}])$ and by the induction hypothesis {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P[\mu X.P]}[u]\simeq_{\varepsilon}u^{\sharp}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\Gamma}}. Moreover we have that $A=\mu X.P$ and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P}[t]=\mathsf{fold}_{P}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{f}}\circ{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P}[\beta/X]) where $\beta=\forall X.(P^{\sharp}[X]\Rightarrow X)\Rightarrow X$ and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{f}}[x]=\Lambda X.\lambda f.f(\Phi_{P^{\sharp}}^{X}(xXf)). The equivalence (t^{\sharp}\circ\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma})Xf\simeq_{\varepsilon}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P}[t]Xf is then seen from the diagram in Fig. 18(a), where $(*)$ commutes by the induction hypothesis, $(**)$ commutes since {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P[\mu X.P/X]}\simeq_{\beta\eta}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P}[\beta/X]\circ\Phi_{P}^{X}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P}), and $(***)$ commutes by an instance of a $\varepsilon$-rule.

• •

if $t=\mathsf{fold}_{P}(u)v$, then $t^{\sharp}=v^{\sharp}C^{\sharp}u^{\sharp}$ and by the induction hypothesis we know that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P}[v]\simeq_{\varepsilon}v^{\sharp}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma} and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P(C)\Rightarrow C}[u]\simeq u^{\sharp}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma}. The equivalence between {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C}[\mathsf{fold}_{P}(u)v] and t^{\sharp}\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma}=(v^{\sharp}C^{\sharp}u^{\sharp})\circ_{\mathsf{m}}\vec{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}}_{\Gamma} can be seen from the diagram in Fig. 18(b), where $(*)$ and $(**)$ commute by the induction hypothesis and the commutation of $(***)$ follows from {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{C}[\mathsf{fold}_{P}(u)]\simeq_{\varepsilon}\mathsf{fold}_{P}(u^{\sharp}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P}[C^{\sharp}]) and \mathsf{fold}_{P}(u^{\sharp}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{P})\simeq_{\varepsilon}C^{\sharp}u^{\sharp}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P}, where the latter holds since {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\mathtt{c}}_{\mu X.P} is an isomorphism of initial algebras.

∎