Efficient Type Checking for Path Polymorphism

TL;DR

This paper introduces a type-checking algorithm for a complex type system supporting path polymorphism, combining recursive, union, and application types, with a focus on efficiency and correctness.

Contribution

It presents two algorithms for type equivalence and subtyping, including a polynomial-time automata-based method, improving the practicality of type checking for path polymorphism.

Findings

Automata-based algorithm achieves polynomial-time complexity.

Coinductive characterizations underpin the type equivalence and subtyping algorithms.

Syntax-directed presentation proven equivalent to original system.

Abstract

A type system combining type application, constants as types, union types (associative, commutative and idempotent) and recursive types has recently been proposed for statically typing path polymorphism, the ability to define functions that can operate uniformly over recursively specified applicative data structures. A typical pattern such functions resort to is $x\,y$ which decomposes a compound, in other words any applicative tree structure, into its parts. We study type-checking for this type system in two stages. First we propose algorithms for checking type equivalence and subtyping based on coinductive characterizations of those relations. We then formulate a syntax-directed presentation and prove its equivalence with the original one. This yields a type-checking algorithm which unfortunately has exponential time complexity in the worst case. A second algorithm is then proposed, based on automata techniques, which yields a polynomial-time type-checking algorithm.

Equations

$$\begin{array}[]{c}{{\mathtt{cons}}\,{({\mathtt{vl}}\,{1})}}\,{({{\mathtt{cons}}\,{({\mathtt{vl}}\,{2})}}\,{\mathtt{nil}})}\\ {{{\mathtt{node}}\,{({\mathtt{vl}}\,{3})}}\,{({{{\mathtt{node}}\,{({\mathtt{vl}}\,{4})}}\,{\mathtt{nil}}}\,{\mathtt{nil}})}}\,{({{{\mathtt{node}}\,{({\mathtt{vl}}\,{5})}}\,{\mathtt{nil}}}\,{\mathtt{nil}})}\end{array}$$

$$\mathsf{upd}={{f}}\shortrightarrow{\begin{array}[t]{clll}(&{\mathtt{vl}}\,{{z}}&\shortrightarrow&{\mathtt{vl}}\,{({f}\,{z})}\\ \mathrel{|}&{{x}}\,{{y}}&\shortrightarrow&{({{\mathsf{upd}}\,{f}}\,{x})}\,{({{\mathsf{upd}}\,{f}}\,{y})}\\ \mathrel{|}&{w}&\shortrightarrow&w)\end{array}}$$

$$(\mathtt{nil}\text{shortrightarrow}0)\mathtt{cons}(\mathtt{vl}x{\text{shortrightarrow}}_{\left\{x:\mathrm{Nature}\right\}}x+1)(\mathtt{vl}\mathtt{true})$$

$$\mu \alpha .(vl@A)\oplus (\alpha @\alpha )\oplus (cons\oplus node\oplus nil)$$

$$((\mathtt{vl}x{\text{shortrightarrow}}_{\left\{x:\mathsf{Bool}\right\}}\text{if }x\text{ then }1\text{ else }0)|(\mathtt{vl}y{\text{shortrightarrow}}_{\left\{y:\mathrm{Nature}\right\}}y+1))(\mathtt{vl}4)$$

$$\begin{array}[]{l@{\qquad}l}\begin{array}[t]{rlll}p&::=&{x}&\text{(matchable)}\\ &|&\mathtt{c}&\text{(constant)}\\ &|&{p}\,{p}&\text{(compound)}\\ \end{array}&\begin{array}[t]{rlll}t&::=&x&\text{(variable)}\\ \hphantom{m}&|&\mathtt{c}&\text{(constant)}\\ &|&{t}\,{t}&\text{(application)}\\ &|&{p}\shortrightarrow_{\theta}{t}\mathrel{|}\dots\mathrel{|}{p}\shortrightarrow_{\theta}{t}&\text{(abstraction)}\end{array}\\ \\ \begin{array}[t]{rlll}d&::=&\mathtt{c}&\text{(constant)}\\ &|&{d}\,{t}&\text{(compound)}\end{array}&\begin{array}[t]{rlll}m&::=&d&\text{(data structure)}\\ &|&{p}\shortrightarrow_{\theta}{t}\mathrel{|}\dots\mathrel{|}{p}\shortrightarrow_{\theta}{t}&\text{(abstraction)}\end{array}\end{array}$$

$$\begin{array}[]{c}\begin{array}[]{rll}\mathtt{fail}\uplus o&\triangleq&\mathtt{fail}\\ o\uplus\mathtt{fail}&\triangleq&\mathtt{fail}\\ \sigma_{1}\uplus\sigma_{2}&\triangleq&\sigma\end{array}\hskip 14.22636pt\begin{array}[]{rll}\mathtt{wait}\uplus\sigma&\triangleq&\mathtt{wait}\\ \sigma\uplus\mathtt{wait}&\triangleq&\mathtt{wait}\\ \mathtt{wait}\uplus\mathtt{wait}&\triangleq&\mathtt{wait}\end{array}\end{array}$$

$$\begin{array}[]{llll}\{\!\!\{{u}/{{x}}\}\!\!\}&\triangleq&\left\{{u}/{x}\right\}\\ \{\!\!\{{\mathtt{c}}/{\mathtt{c}}\}\!\!\}&\triangleq&\left\{{}\right\}\\ \{\!\!\{{{u}\,{v}}/{{p}\,{q}}\}\!\!\}&\triangleq&\{\!\!\{{u}/{p}\}\!\!\}\uplus\{\!\!\{{v}/{q}\}\!\!\}&\quad\text{if ${u}\,{v}$ is a \emph{matchable form}}\\ \{\!\!\{{u}/{p}\}\!\!\}&\triangleq&\mathtt{fail}&\quad\text{if $u$ is a \emph{matchable form}}\\ \{\!\!\{{u}/{p}\}\!\!\}&\triangleq&\mathtt{wait}\end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\{\!\!\{{u}/{p_{i}}\}\!\!\}=\mathtt{fail}\text{ for all }i<j\quad\{\!\!\{{u}/{p_{j}}\}\!\!\}=\sigma_{j}\quad j\in 1..n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=222.7092pt\hbox{\kern 3.00003pt${\textsc{({$\beta$})}}$}}}\hbox{\kern 72.04306pt\hbox{$\displaystyle{{({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}}\,{u}\rightarrow\sigma_{j}s_{j}}$}}}}\end{array}$$

$$\mathsf{head}=((\mathtt{nil}{\text{shortrightarrow}}_{\left\{\right\}}\mathtt{nothing})|(\mathtt{cons}xxs{\text{shortrightarrow}}_{\left\{x:\mathrm{Nature},xs:\mu \alpha .nil\oplus cons@\mathrm{Nature}@\alpha \right\}}\mathtt{just}x))$$

$$\begin{array}[]{l@{\qquad}l}\begin{array}[]{rlll}D&::=&\alpha&\quad\text{(datatype variable)}\\ &|&\mathbb{c}&\quad\text{(atom)}\\ &|&{D}\mathrel{@}{A}&\quad\text{(compound)}\\ &|&{D}\oplus{D}&\quad\text{(union)}\\ &|&\mu{\alpha}.{D}&\quad\text{(recursion)}\end{array}&\begin{array}[]{rlll}A&::=&X&\quad\text{(type variable)}\\ &|&D&\quad\text{(datatype)}\\ &|&{A}\supset{A}&\quad\text{(type abstraction)}\\ &|&{A}\oplus{A}&\quad\text{(union)}\\ &|&\mu{X}.{A}&\quad\text{(recursion)}\end{array}\end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 18.90932pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=37.81863pt\hbox{\kern 3.00003pt${\textsc{({e-refl})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{A\simeq_{\mu}A}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}B}\quad{}\vdash{B\simeq_{\mu}C}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=89.95105pt\hbox{\kern 3.00003pt${\textsc{({e-trans})}}$}}}\hbox{\kern 25.88498pt\hbox{$\displaystyle{{}\vdash{A\simeq_{\mu}C}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}B}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=38.40543pt\hbox{\kern 3.00003pt${\textsc{({e-symm})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{B\simeq_{\mu}A}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{D\simeq_{\mu}D^{\prime}}\quad{}\vdash{A\simeq_{\mu}A^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=93.60884pt\hbox{\kern 3.00003pt${\textsc{({e-comp})}}$}}}\hbox{\kern 12.79807pt\hbox{$\displaystyle{{}\vdash{{D}\mathrel{@}{A}\simeq_{\mu}{D^{\prime}}\mathrel{@}{A^{\prime}}}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}A^{\prime}}\quad{}\vdash{B\simeq_{\mu}B^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=89.89085pt\hbox{\kern 3.00003pt${\textsc{({e-func})}}$}}}\hbox{\kern 11.40921pt\hbox{$\displaystyle{{}\vdash{{A}\supset{B}\simeq_{\mu}{A^{\prime}}\supset{B^{\prime}}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 23.77051pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=47.54102pt\hbox{\kern 3.00003pt${\textsc{({e-union-idem})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{{A}\oplus{A}\simeq_{\mu}A}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 31.99622pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=63.99243pt\hbox{\kern 3.00003pt${\textsc{({e-union-comm})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{{A}\oplus{B}\simeq_{\mu}{B}\oplus{A}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 59.85864pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=119.71729pt\hbox{\kern 3.00003pt${\textsc{({e-union-assoc})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{{A}\oplus{({B}\oplus{C})}\simeq_{\mu}{({A}\oplus{B})}\oplus{C}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}A^{\prime}}\quad{}\vdash{B\simeq_{\mu}B^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=92.66856pt\hbox{\kern 3.00003pt${\textsc{({e-union})}}$}}}\hbox{\kern 12.79807pt\hbox{$\displaystyle{{}\vdash{{A}\oplus{B}\simeq_{\mu}{A^{\prime}}\oplus{B^{\prime}}}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 15.46997pt\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}B}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=69.34537pt\hbox{\kern 3.00003pt${\textsc{({e-rec})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{\mu{V}.{A}\simeq_{\mu}\mu{V}.{B}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 49.65707pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=99.31415pt\hbox{\kern 3.00003pt${\textsc{({e-fold})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{}\vdash{\mu{V}.{A}\simeq_{\mu}\left\{{\mu{V}.{A}}/{V}\right\}{A}}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}\left\{{A}/{V}\right\}{B}}\quad\mu{V}.{B}\text{ contractive}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=155.3234pt\hbox{\kern 3.00003pt${\textsc{({e-contr})}}$}}}\hbox{\kern 50.02957pt\hbox{$\displaystyle{{}\vdash{A\simeq_{\mu}\mu{V}.{B}}}$}}}}\end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 23.90929pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=47.81857pt\hbox{\kern 3.00003pt${\textsc{({s-refl})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Sigma}\vdash{A\preceq_{\mu}A}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 44.48526pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=88.97052pt\hbox{\kern 3.00003pt${\textsc{({s-hyp})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Sigma,V\preceq_{\mu}W}\vdash{V\preceq_{\mu}W}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.99997pt\hbox{$\displaystyle\penalty 1{{}\vdash{A\simeq_{\mu}B}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=48.40536pt\hbox{\kern 3.00003pt${\textsc{({s-eq})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Sigma}\vdash{A\preceq_{\mu}B}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{A\preceq_{\mu}B}\quad{\Sigma}\vdash{B\preceq_{\mu}C}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=107.17322pt\hbox{\kern 3.00003pt${\textsc{({s-trans})}}$}}}\hbox{\kern 29.4961pt\hbox{$\displaystyle{{\Sigma}\vdash{A\preceq_{\mu}C}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{D\preceq_{\mu}D^{\prime}}\quad{\Sigma}\vdash{A\preceq_{\mu}A^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=110.83101pt\hbox{\kern 3.00003pt${\textsc{({s-comp})}}$}}}\hbox{\kern 16.40918pt\hbox{$\displaystyle{{\Sigma}\vdash{{D}\mathrel{@}{A}\preceq_{\mu}{D^{\prime}}\mathrel{@}{A^{\prime}}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{A\preceq_{\mu}A^{\prime}}\quad{\Sigma}\vdash{B\preceq_{\mu}B^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=109.89073pt\hbox{\kern 3.00003pt${\textsc{({s-func})}}$}}}\hbox{\kern 16.40918pt\hbox{$\displaystyle{{\Sigma}\vdash{{A^{\prime}}\supset{B}\preceq_{\mu}{A}\supset{B^{\prime}}}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{A\preceq_{\mu}C}\quad{\Sigma}\vdash{B\preceq_{\mu}C}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=106.9489pt\hbox{\kern 3.00003pt${\textsc{({s-union-l})}}$}}}\hbox{\kern 24.22932pt\hbox{$\displaystyle{{\Sigma}\vdash{{A}\oplus{B}\preceq_{\mu}C}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 7.82014pt\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{A\preceq_{\mu}B}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=64.04565pt\hbox{\kern 3.00003pt${\textsc{({s-union-r1})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Sigma}\vdash{A\preceq_{\mu}{B}\oplus{C}}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 7.93231pt\hbox{$\displaystyle\penalty 1{{\Sigma}\vdash{A\preceq_{\mu}C}}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=64.04567pt\hbox{\kern 3.00003pt${\textsc{({s-union-r2})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Sigma}\vdash{A\preceq_{\mu}{B}\oplus{C}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Sigma,V\preceq_{\mu}W}\vdash{A\preceq_{\mu}B}\quad W\notin\mathsf{fv}\!\left({A}\right)\quad V\notin\mathsf{fv}\!\left({B}\right)}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=189.58873pt\hbox{\kern 3.00003pt${\textsc{({s-rec})}}$}}}\hbox{\kern 55.12167pt\hbox{$\displaystyle{{\Sigma}\vdash{\mu{V}.{A}\preceq_{\mu}\mu{W}.{B}}}$}}}}\end{array}$$

$$\begin{array}[]{c}\lx@intercol\textbf{Patterns}\hfil\lx@intercol\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\theta(x)=A}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=39.02075pt\hbox{\kern 3.00003pt${\textsc{({p-match})}}$}}}\hbox{\kern 1.7778pt\hbox{$\displaystyle{{\theta}\vdash_{\mathsf{p}}{{x}:A}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 15.7083pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=31.4166pt\hbox{\kern 3.00003pt${\textsc{({p-const})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\theta}\vdash_{\mathsf{p}}{\mathtt{c}:\mathbb{c}}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\theta}\vdash_{\mathsf{p}}{p:D}\quad{\theta}\vdash_{\mathsf{p}}{q:A}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=85.96631pt\hbox{\kern 3.00003pt${\textsc{({p-comp})}}$}}}\hbox{\kern 15.5693pt\hbox{$\displaystyle{{\theta}\vdash_{\mathsf{p}}{{p}\,{q}:{D}\mathrel{@}{A}}}$}}}}\\ \\ \lx@intercol\textbf{Terms}\hfil\lx@intercol\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\Gamma(x)=A}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=40.57632pt\hbox{\kern 3.00003pt${\textsc{({t-var})}}$}}}\hbox{\kern 1.9445pt\hbox{$\displaystyle{{\Gamma}\vdash{x:A}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 14.93053pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=29.86105pt\hbox{\kern 3.00003pt${\textsc{({t-const})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{{\Gamma}\vdash{\mathtt{c}:\mathbb{c}}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Gamma}\vdash{r:D}\quad{\Gamma}\vdash{u:A}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=89.07043pt\hbox{\kern 3.00003pt${\textsc{({t-comp})}}$}}}\hbox{\kern 17.56924pt\hbox{$\displaystyle{{\Gamma}\vdash{{r}\,{u}:{D}\mathrel{@}{A}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\begin{array}[]{c}\left[{p_{i}:A_{i}}\right]_{i\in 1..n}\text{ compatible}\vspace{.1cm}\\ ({\theta_{i}}\vdash_{\mathsf{p}}{p_{i}:A_{i}})_{i\in 1..n}\quad(\mathsf{dom}\left({\theta_{i}}\right)=\mathsf{fm}\!\left({p_{i}}\right))_{i\in 1..n}\quad({\Gamma,\theta_{i}}\vdash{s_{i}:B})_{i\in 1..n}\end{array}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=237.14719pt\hbox{\kern 3.00003pt${\textsc{({t-abs})}}$}}}\hbox{\kern 54.7805pt\hbox{$\displaystyle{{\Gamma}\vdash{({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}:{({{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}})}\supset{B}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Gamma}\vdash{r:{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{B}}\quad{\Gamma}\vdash{u:A_{k}}\quad k\in 1..n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=181.7764pt\hbox{\kern 3.00003pt${\textsc{({t-app})}}$}}}\hbox{\kern 70.40735pt\hbox{$\displaystyle{{\Gamma}\vdash{{r}\,{u}:B}}$}}}}\quad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{{\Gamma}\vdash{s:A}\quad{}\vdash{A\preceq_{\mu}A^{\prime}}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=90.57362pt\hbox{\kern 3.00003pt${\textsc{({t-subs})}}$}}}\hbox{\kern 25.29817pt\hbox{$\displaystyle{{\Gamma}\vdash{s:A^{\prime}}}$}}}}\end{array}$$

$$\begin{array}[]{c}\begin{array}[]{r@{\quad\eqdef\quad}l@{\quad}l}{a}\|_{\epsilon}\quad\triangleq&\left\{{a}\right\}\\ {(A_{1}\star A_{2})}\|_{\epsilon}\quad\triangleq&\left\{{\star}\right\},&\star\in\left\{{\supset,\mathrel{@}}\right\}\\ {(A_{1}\star A_{2})}\|_{i\pi}\quad\triangleq&{A_{i}}\|_{\pi},&\star\in\left\{{\supset,\mathrel{@}}\right\},i\in\left\{{1,2}\right\}\\ {({A_{1}}\oplus{A_{2}})}\|_{\pi}\quad\triangleq&{A_{1}}\|_{\pi}\cup{A_{2}}\|_{\pi}\\ {(\mu{V}.{A^{\prime}})}\|_{\pi}\quad\triangleq&{(\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}})}\|_{\pi}\end{array}\end{array}$$

$$\mathsf{maxpos}\left(P\right)\triangleq \left\{\pi \in P|\nexists {\pi }^{\prime }\ne ϵ.\pi {\pi }^{\prime }\in P\right\}$$

$$\mathsf{mmpos}\left(p,q\right)\triangleq \left\{\pi |\pi \in \mathsf{maxpos}\left(\mathsf{pos}\left(p\right)\cap \mathsf{pos}\left(q\right)\right)\wedge \text{and}p\pi \text{centernot}⊲\text{and}q\pi \right\}$$

$${\mathcal{P}}_{\mathsf{comp}}\left(p:A,q:B\right)\triangleq \forall \pi \in \mathsf{mmpos}\left(p,q\right).A{\Vert }_{\pi }\cap B{\Vert }_{\pi }\ne \varnothing$$

$${\mathcal{P}}_{\mathsf{comp}}\left(p:A,q:B\right)⟹B{⪯}_{\mu }A$$

$$nil{\Vert }_{ϵ}=\left\{nil\right\}(cons@\mathrm{Nature}@(\mu \alpha .nil\oplus cons@\mathrm{Nature}@\alpha )){\Vert }_{ϵ}=\left\{@\right\}$$

$$\begin{array}[]{r@{\quad\eqdef\quad}l@{\quad}l}{\mathscr{A}}|_{{0}}\quad\triangleq&\circ\\ {a}|_{{k+1}}\quad\triangleq&a&\text{for $a\in\mathcal{V}\cup\mathcal{C}$}\\ {(\mathscr{A}_{1}\star\mathscr{A}_{2})}|_{{k+1}}\quad\triangleq&{\mathscr{A}_{1}}|_{{k}}\star{\mathscr{A}_{2}}|_{{k}}&\text{for $\star\in\left\{{\mathrel{@},\supset}\right\}$}\\ {({\mathscr{A}_{1}}\oplus{\mathscr{A}_{2}})}|_{{k+1}}\quad\triangleq&{{\mathscr{A}_{1}}|_{{k+1}}}\oplus{{\mathscr{A}_{2}}|_{{k+1}}}\end{array}$$

$$\begin{array}[]{r@{\quad\eqdef\quad}l@{\quad}l}\llbracket{a}\rrbracket^{\mathfrak{T}}(\epsilon)\quad\triangleq&a\\ \llbracket{A_{1}\star A_{2}}\rrbracket^{\mathfrak{T}}(\epsilon)\quad\triangleq&\star&\text{for $\star\in\left\{{\mathrel{@},\supset,\oplus}\right\}$}\\ \llbracket{A_{1}\star A_{2}}\rrbracket^{\mathfrak{T}}(i\pi)\quad\triangleq&\llbracket{A_{i}}\rrbracket^{\mathfrak{T}}(\pi)&\text{for $\star\in\left\{{\mathrel{@},\supset,\oplus}\right\}$}\\ \llbracket{\mu{V}.{A}}\rrbracket^{\mathfrak{T}}(\pi)\quad\triangleq&\llbracket{\left\{{\mu{V}.{A}}/{V}\right\}{A}}\rrbracket^{\mathfrak{T}}(\pi)\\ \end{array}$$

$$A_1\oplus \dots A_{i-1}\oplus \square \oplus A_{i+1}\oplus \dots \oplus A_n$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 13.17892pt\hbox{$\displaystyle\penalty 1{}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to26.35785pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-refl-al})}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle{a\simeq_{\vec{\mu}}a}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{D\simeq_{\vec{\mu}}D^{\prime}\quad A\simeq_{\vec{\mu}}A^{\prime}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to76.76607pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-comp-al})}}$}}}\hbox{\kern 5.11523pt\hbox{$\displaystyle{{D}\mathrel{@}{A}\simeq_{\vec{\mu}}{D^{\prime}}\mathrel{@}{A^{\prime}}}$}}}}\qquad{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{A\simeq_{\vec{\mu}}A^{\prime}\quad B\simeq_{\vec{\mu}}B^{\prime}}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to75.82579pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-func-al})}}$}}}\hbox{\kern 0.94867pt\hbox{$\displaystyle{{A}\supset{B}\simeq_{\vec{\mu}}{A^{\prime}}\supset{B^{\prime}}}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\mathscr{C}[\left\{{\mu{V}.{A}}/{V}\right\}{A}]\simeq_{\vec{\mu}}B\quad}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to101.56511pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-rec-l-al})}}$}}}\hbox{\kern 20.27782pt\hbox{$\displaystyle{\mathscr{C}[\mu{V}.{A}]\simeq_{\vec{\mu}}B}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{A\simeq_{\vec{\mu}}\mathscr{D}[\left\{{\mu{W}.{B}}/{W}\right\}{B}]\quad A\neq\mathscr{C}[\mu{V}.{C}]}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to163.40094pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-rec-r-al})}}$}}}\hbox{\kern 49.59851pt\hbox{$\displaystyle{A\simeq_{\vec{\mu}}\mathscr{D}[\mu{W}.{B}]}$}}}}\\ \\ {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1{\begin{array}[]{ll}A_{i}\simeq_{\vec{\mu}}B_{f(i)}&\quad f:1..n\to 1..m\\ A_{g(j)}\simeq_{\vec{\mu}}B_{j}&\quad g:1..m\to 1..n\end{array}\quad A_{i},B_{j}\neq\mu,\oplus\quad n+m>2}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\hbox to257.50314pt{$\mathord{=}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu=\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{=}$}\hbox{\kern 3.00003pt${\textsc{({e-union-al})}}$}}}\hbox{\kern 79.7168pt\hbox{$\displaystyle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}\simeq_{\vec{\mu}}{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}}$}}}}\end{array}$$

$$\mathcal{A}::=\square |\mu V.\mathcal{A}|\mathcal{A}\oplus \mathcal{A}$$

$$\begin{array}[]{r@{\quad\eqdef\quad}l@{\quad}l}{\Box[A]}^{\epsilon}\quad\triangleq&A\\ {(\mu{V}.{\mathcal{A}[\vec{A}]})}^{1\pi}\quad\triangleq&{\left\{{\mu{V}.{\mathcal{A}[\vec{A}]}}/{V}\right\}{\mathcal{A}[\vec{A}]}}^{\pi}\\ {({\mathcal{A}_{1}[\vec{A_{1}}]}\oplus{\mathcal{A}_{2}[\vec{A_{2}}]})}^{i\pi}\quad\triangleq&{\mathcal{A}_{i}[\vec{A_{i}}]}^{\pi}&i=1,2\end{array}$$

$$\begin{array}[]{r@{\quad\eqdef\quad}l}{\Box}^{\setminus\mu}\quad\triangleq&\Box\\ {(\mu{V}.{\mathcal{A}})}^{\setminus\mu}\quad\triangleq&{\mathcal{A}}^{\setminus\mu}\\ {({\mathcal{A}_{1}}\oplus{\mathcal{A}_{n}})}^{\setminus\mu}\quad\triangleq&{{\mathcal{A}_{1}}^{\setminus\mu}}\oplus{{\mathcal{A}_{n}}^{\setminus\mu}}\end{array}$$

$$[[\mathcal{A}[\vec{A}]{]]}^{\mathfrak{T}}={\mathcal{A}}^{\setminus \mu }[[[{\mathcal{A}[\vec{A}]}^{{\pi }_1}{]]}^{\mathfrak{T}},\dots ,[[{\mathcal{A}[\vec{A}]}^{{\pi }_n}{]]}^{\mathfrak{T}}]$$

$$[[\mathcal{A}[A]{]]}^{\mathfrak{T}}=[[\square [A]{]]}^{\mathfrak{T}}=[[A{]]}^{\mathfrak{T}}=\square [[[A{]]}^{\mathfrak{T}}]={\square }^{\setminus \mu }[[[{\square [A]}^{ϵ}{]]}^{\mathfrak{T}}]={\mathcal{A}}^{\setminus \mu }[[[{\mathcal{A}[A]}^{ϵ}{]]}^{\mathfrak{T}}]$$

$$\begin{array}[]{rcl@{\quad}l}\llbracket{\mathcal{A}[\vec{A}]}\rrbracket^{\mathfrak{T}}&=&\llbracket{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}\rrbracket^{\mathfrak{T}}\\ &=&\llbracket{\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{\mathcal{A}^{\prime}[\vec{A}]}}\rrbracket^{\mathfrak{T}}&\text{Def.\leavevmode\nobreak\ \ref{def:toBTree}}\\ &=&\llbracket{(\mathcal{A}^{\prime}[\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{\vec{A}}])}\rrbracket^{\mathfrak{T}}\\ &=&{\mathcal{A}^{\prime}}^{\setminus\mu}[\llbracket{{\mathcal{A}^{\prime}[\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{\vec{A}}]}^{\pi_{1}}}\rrbracket^{\mathfrak{T}},\ldots,\\ &&\hphantom{{\mathcal{A}^{\prime}}^{\setminus\mu}[}\llbracket{{\mathcal{A}^{\prime}[\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{\vec{A}}]}^{\pi_{n}}}\rrbracket^{\mathfrak{T}}]&\text{inductive hypothesis}\\ &=&{\mathcal{A}^{\prime}}^{\setminus\mu}[\llbracket{\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{{\mathcal{A}^{\prime}[\vec{A}]}^{\pi_{1}}}}\rrbracket^{\mathfrak{T}},\ldots,\\ &&\hphantom{{\mathcal{A}^{\prime}}^{\setminus\mu}[}\llbracket{\left\{{\mu{V}.{\mathcal{A}^{\prime}}[\vec{A}]}/{V}\right\}{{\mathcal{A}^{\prime}[\vec{A}]}^{\pi_{n}}}}\rrbracket^{\mathfrak{T}}]\\ &=&{\mathcal{A}}^{\setminus\mu}[\llbracket{{\mathcal{A}[\vec{A}]}^{1\pi_{1}}}\rrbracket^{\mathfrak{T}},\ldots,\llbracket{{\mathcal{A}[\vec{A}]}^{1\pi_{n}}}\rrbracket^{\mathfrak{T}}]&\text{Def.\leavevmode\nobreak\ \ref{def:projection} and ${\mathcal{A}}^{\setminus\mu}$}\end{array}$$

Full text

1. Introduction

The lambda-calculus plays an important role in the study of programming languages (PLs). Programs are represented as syntactic terms and execution by repeated simplification of these terms using a reduction rule called $\beta$-reduction. The study of the lambda-calculus has produced deep results in both the theory and the implementation of PLs. Many variants of the lambda-calculus have been introduced with the purpose of studying specific PL features. One such feature of interest is pattern-matching. Pattern-matching is used extensively in PLs as a means for writing more succinct and, at the same time, elegant programs. This is particularly so in the functional programming community, but by no means restricted to that community.

In the standard lambda-calculus, functions are represented as expressions of the form $\lambda x.t$, $x$ being the formal parameter and $t$ the body. Such a function may be applied to any term, regardless of its form. This is expressed by the above mentioned $\beta$-reduction rule: $(\lambda x.t)\,s\rightarrow_{\beta}\left\{{s}/{x}\right\}{t}$, where $\left\{{s}/{x}\right\}{t}$ stands for the result of replacing all free occurrences of $x$ in $t$ with $s$. Note that, in this rule, no requirement on the form of $s$ is placed. Pattern calculi are generalizations of the $\beta$-reduction rule in which abstractions $\lambda x.t$ are replaced by $\lambda p.t$ where $p$ is called a pattern. An example is $\lambda\langle{x},{y}\rangle.x$ for projecting the first component of a pair, the pattern $p$ being $\langle{x},{y}\rangle$. An expression such as ${(\lambda\langle{x},{y}\rangle.x)}\,{s}$ will only be able to reduce if $s$ indeed is of the form $\langle{s_{1}},{s_{2}}\rangle$; it will otherwise be blocked.

Patterns may be catalogued in at least two dimensions. One is their structure and another their time of creation. The structure of patterns may be very general. Such is the case of variables: any term can match a variable, as in the standard lambda-calculus. The structure of a pattern may also be very specific. Such is the case when arbitrary terms are allowed to be patterns [18, 14]. Regarding the time of creation, patterns may either be static or dynamic. Static patterns are those that are created at compile time, such as the pattern $\langle{x},{y}\rangle$ mentioned above. Dynamic patterns are those that may be generated at run-time [12, 11]. For example, consider the term $\lambda x.(\lambda({x}\,{y}).y)$; note that it has an occurrence of a pattern $x\,y$ with a free variable, namely the $x$ in ${x}\,{y}$, that is bound to the outermost lambda. If this term is applied to a constant $\mathtt{c}$, then one obtains $\lambda{\mathtt{c}}\,{y}.y$. However, if we apply it to the constant $\mathtt{d}$, then we obtain $\lambda{\mathtt{d}}\,{y}.y$. Both patterns ${\mathtt{c}}\,{y}$ and ${\mathtt{d}}\,{y}$ are created during execution. Note that one could also replace the $x$ in the pattern ${x}\,{y}$ with an abstraction. This leads to computations that evaluate to patterns.

Expressive pattern features may easily break desired properties, such as confluence, and are not easy to endow with type systems. This work is an attempt at devising type systems for such expressive pattern calculi. We originally set out to type-check the Pure Pattern Calculus (PPC) [12, 11]. PPC is a lambda-calculus that embodies the essence of dynamic patterns by stripping away everything inessential to the reduction and matching process of dynamic patterns. It admits terms such as $\lambda x.(\lambda({x}\,{y}).y)$. We soon realized that typing PPC was too challenging and noticed that the static fragment of PPC, which we dub Calculus of Applicative Patterns (CAP), was already challenging in itself. CAP also admits patterns such as ${{x}}\,{{y}}$ however all variables in this pattern are considered bound. Thus, in a term such as $\lambda({x}\,{y}).s$ both occurrences of $x$ and $y$ are bound in $s$, disallowing reduction inside patterns. Such patterns, however, allow arguments that are applications to be decomposed, as long as these applications encode data structures. They are therefore useful for writing functions that operate on semi-structured data.

The main obstacle for typing CAP is dealing in the type system with a form of polymorphism called path polymorphism [12, 11], that arises from these kinds of patterns. We next briefly describe path polymorphism and the requirements it places on typing considerations.

Path Polymorphism. In CAP data structures are trees. These trees are built using application and variable arity constants or constructors. Examples of two such trees follow, where the first one represents a list and the second a binary tree:

[TABLE]

The constructor $\mathtt{vl}$ is used to tag values ($1$ and $2$ in the first case, and $3$, $4$ and $5$ in the second). A “map” function for updating the values of any of these two structures by applying some user-supplied function $f$ follows, where type annotations are omitted for clarity:

[TABLE]

The expression ${\mathsf{upd}}\,{(+1)}$ may thus be applied to any of the two data structures illustrated above. For example, we can evaluate ${{\mathsf{upd}}\,{(+1)}}\,{{{\mathtt{cons}}\,{({\mathtt{vl}}\,{1})}}\,{({{\mathtt{cons}}\,{({\mathtt{vl}}\,{2})}}\,{\mathtt{nil}})}}$ and also ${{\mathsf{upd}}\,{(+1)}}\,{{{{\mathtt{node}}\,{({\mathtt{vl}}\,{3})}}\,{({{{\mathtt{node}}\,{({\mathtt{vl}}\,{4})}}\,{\mathtt{nil}}}\,{\mathtt{nil}})}}\,{({{{\mathtt{node}}\,{({\mathtt{vl}}\,{5})}}\,{\mathtt{nil}}}\,{\mathtt{nil}})}}$. The expression to the right of “=” is called an abstraction (or case) and consists of a unique branch; this branch in turn is formed from a pattern (${f}$), and a body (in this case the body is itself another abstraction that consists of three branches). An argument to an abstraction is matched against the patterns, in the order in which they are written, and the appropriate body is selected.

Notice the pattern ${{x}}\,{{y}}$. During evaluation of ${{\mathsf{upd}}\,{(+1)}}\,{{{\mathtt{cons}}\,{({\mathtt{vl}}\,{1})}}\,{({{\mathtt{cons}}\,{({\mathtt{vl}}\,{2})}}\,{\mathtt{nil}})}}$ the variables ${x}$ and ${y}$ may be instantiated with different applicative terms in each recursive call to $\mathsf{upd}$. For example:

[TABLE]

The type assigned to ${x}$ and ${y}$ should encompass all terms in its respective column.

Singleton Types and Type Application. A further consideration in typing CAP is that terms such as the ones depicted below should clearly not be typable.

[TABLE]

In the first case, $\mathtt{cons}$ will never match $\mathtt{nil}$. The type system will resort to singleton types in order to determine this: $\mathtt{cons}$ will be assigned a type of the form $\mathbb{cons}$ which will fail to match $\mathbb{nil}$. The second expression in (2) breaks Subject Reduction (SR): reduction will produce $\mathtt{true}+1$. Applicative types of the form ${\mathbb{vl}}\mathrel{@}{\mathbb{true}}$ will allow us to check for these situations, ${}\mathrel{@}{}$ being a new type constructor that applies datatypes to arbitrary types. Also, note the use of typing environments (the expression $\left\{{x:{\rm Nature}}\right\}$) to declare the types of the variables of patterns in branches. These are supplied by the programmer.

Union and Recursive Types. On the assumption that the programmer has provided an exhaustive coverage, the type assigned by CAP to the variable ${x}$ in the pattern $x\,y$ in $\mathsf{upd}$ is:

[TABLE]

Here $\mu$ is the recursive type constructor and $\oplus$ the union type constructor. $\mathbb{vl}$ is the singleton type used for typing the constant $\mathtt{vl}$ and $\mathrel{@}$ denotes type application, as mentioned above. The union type constructor is used to collect the types of all the branches. The variable $y$ in the pattern ${x}\,{y}$ will also be assigned the same type as $x$. Thus variables in applicative patterns are assigned union types. $\mathsf{upd}$ itself is assigned type ${({A}\supset{B})}\supset{({F_{A}}\supset{F_{B}})}$, where $F_{X}$ is $\mu{\alpha}.{{{({\mathbb{vl}}\mathrel{@}{X})}\oplus{({\alpha}\mathrel{@}{\alpha})}}\oplus{({\mathbb{cons}}\oplus{{\mathbb{node}}\oplus{\mathbb{nil}}})}}$.

Type-Checking for CAP. Based on these, and other similar considerations, we proposed typed CAP [19], referred to simply as CAP in the sequel. The system consists of typing rules that combine singleton types, type application, union types, recursive types and subtyping. Also it enjoys several properties, the salient one being safety (subject reduction and progress). Safety relies on a notion of typed pattern compatibility based on subtyping that guarantees that examples such as (2–right) and the following one do not break safety:

[TABLE]

Assumptions on associativity and commutativity of typing operators in [19], make it non-trivial to deduce a type-checking algorithm from the typing rules. The proposed type system is, moreover, not syntax-directed. Also, it relies on coinductive notions of type equivalence and subtyping which in the presence of recursive subtypes are not obviously decidable. A practical implementation of CAP is instrumental since a robust theoretical analysis without such an implementation is of little use.

Goal and Summary of Contributions. This paper addresses this implementation. It does so in two stages:

• •

The first stage presents a naïve but correct, high-level description of a type-checking algorithm, the principal aim being clarity. We propose an invertible presentation of the coinductive notions of type-equivalence and subtyping of [19] and also a syntax-directed variant of the presentation in [19]. This leads to algorithms for checking subtyping membership and equivalence modulo associative, commutative and idempotent (ACI) unions, both based on an invertible presentation of the functional generating the associated coinductive notions.

• •

The second stage builds on ideas from the first algorithm with the aim of improving efficiency. $\mu$-types are interpreted as infinite $n$-ary trees and represented using automata, avoiding having to explicitly handle unfoldings of recursive types, and leading to a significant improvement in the complexity of the key steps of the type-checking process, namely equality and subtype checking.

**Related work. ** For literature on (typed) pattern calculi the reader is referred to [19]. The algorithms for checking equality of recursive types or subtyping of recursive types have been studied in the 1990s by Amadio and Cardelli [1]; Kozen, Palsberg, and Schwartzbach [15]; Brandt and Henglein [4]; Jim and Palsberg [13] among others. Additionally, Zhao and Palsberg [16] studied the possibilities of incorporating associative and commutative (AC) products to the equality check, on an automata-based approach that the authors themselves claimed was not extensible to subtyping [21]. Later on Di Cosmo, Pottier, and Rémy [7] presented another automata-based algorithm for subtyping that properly handles AC products with a complexity cost of ${\mathcal{O}}(n^{2}n^{\prime 2}d^{5/2})$, where $n$ and $n^{\prime}$ are the sizes of the analyzed types, and $d$ is a bound on the arity of the involved products.

Structure of the paper. Sec. 2 reviews the syntax and operational semantics of CAP, its type system and the main properties. Further details may be consulted in [19]. Sec. 3 proposes invertible generating functions for coinductive notions of type-equivalence and subtyping that lead to inefficient but elegant algorithms for checking these relations. Sec. 4 proposes a syntax-directed type system for CAP. Sec. 5 studies a more efficient type-checking algorithm based on automaton. Finally, we conclude in Sec. 6. An implementation of the algorithms described here is available online [10].

2. Review of CAP

2.1. Syntax and Operational Semantics

We assume given an infinite set of term variables ${\mathbb{V}}$ and constants ${\mathbb{C}}$. CAP has four syntactic categories, namely patterns ($p,q,\ldots$), terms ($s,t,\ldots$), data structures ($d,e,\ldots$) and matchable forms ($m,n,\ldots$):

[TABLE]

The set of patterns, terms, data structures and matchable forms are denoted ${\mathbb{P}}$, ${\mathbb{T}}$, ${\mathbb{D}}$ and ${\mathbb{M}}$, resp. Variables occurring in patterns are called matchables. We often abbreviate ${p_{1}}\shortrightarrow_{\theta_{1}}{s_{1}}\mathrel{|}\ldots\mathrel{|}{p_{n}}\shortrightarrow_{\theta_{n}}{s_{n}}$ with $({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}$. The $\theta_{i}$ are typing contexts annotating the type assignments for the variables in $p_{i}$ (*cf. *Sec. 2.3). The free variables of a term $t$ (notation $\mathsf{fv}\!\left({t}\right)$) are defined as expected; in a pattern $p$ we call them free matchables ($\mathsf{fm}\!\left({p}\right)$). All free matchables in each $p_{i}$ are assumed to be bound in their respective bodies $s_{i}$. Positions in patterns and terms are defined as expected and denoted $\pi,\pi^{\prime},\ldots$ ($\epsilon$ denotes the root position). We write $\mathsf{pos}\!\left({s}\right)$ for the set of positions of $s$ and $\and{s}{\pi}$ for the subterm of $s$ occurring at position $\pi$.

A substitution ($\sigma,\sigma_{i},\ldots$) is a partial function from term variables to terms. If it assigns $u_{i}$ to $x_{i}$, $i\in 1..n$, then we write $\{u_{1}/x_{1},\ldots,u_{n}/x_{n}\}$. Its domain ($\mathsf{dom}\left({\sigma}\right)$) is $\left\{{x_{1},\ldots,x_{n}}\right\}$. Also, $\left\{{}\right\}$ is the identity substitution. We write $\sigma s$ for the result of applying $\sigma$ to term $s$. We say a pattern $p$ subsumes a pattern $q$, written ${p}\mathbin{\vartriangleleft}{q}$ if there exists $\sigma$ such that $\sigma p=q$. Matchable forms are required for defining the matching operation, described next.

Given a pattern $p$ and a term $s$, the matching operation $\{\!\!\{{s}/{p}\}\!\!\}$ determines whether $s$ matches $p$. It may have one of three outcomes: success, fail (in which case it returns the special symbol $\mathtt{fail}$) or undetermined (in which case it returns the special symbol $\mathtt{wait}$). We say $\{\!\!\{{s}/{p}\}\!\!\}$ is decided if it is either successful or it fails. In the former it yields a substitution $\sigma$; in this case we write $\{\!\!\{{s}/{p}\}\!\!\}=\sigma$. The disjoint union of matching outcomes is given as follows (“$\triangleq$” is used for definitional equality):

[TABLE]

where $o$ denotes any possible output and $\sigma_{1}\uplus\sigma_{2}\triangleq\sigma$ if the domains of $\sigma_{1}$ and $\sigma_{2}$ are disjoint. This always holds given that patterns are assumed to be linear (at most one occurrence of any matchable). The matching operation is defined as follows, where the defining clauses below are evaluated from top to bottom111This is simplification to the static patterns case of the matching operation introduced in [12].:

[TABLE]

For example: $\{\!\!\{{{{x}}\shortrightarrow{s}}/{\mathtt{c}}\}\!\!\}=\mathtt{fail}$; $\{\!\!\{{\mathtt{d}}/{\mathtt{c}}\}\!\!\}=\mathtt{fail}$; $\{\!\!\{{x}/{\mathtt{c}}\}\!\!\}=\mathtt{wait}$ and $\{\!\!\{{{x}\,{\mathtt{d}}}/{{\mathtt{c}}\,{\mathtt{c}}}\}\!\!\}=\mathtt{fail}$. We now turn to the only reduction axiom of CAP:

[TABLE]

It may be applied under any context and states that if the argument $u$ to an abstraction $({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}$ fails to match all patterns $p_{i}$ with $i<j$ and successfully matches pattern $p_{j}$ (producing a substitution $\sigma_{j}$), then the term ${({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}}\,{u}$ reduces to $\sigma_{j}s_{j}$.

For instance, consider the function

[TABLE]

Then, ${\mathsf{head}}\,{\mathtt{nil}}\rightarrow\mathtt{nothing}$ with $\{\!\!\{{\mathtt{nil}}/{\mathtt{nil}}\}\!\!\}=\left\{{}\right\}$, while ${\mathsf{head}}\,{({{\mathtt{cons}}\,{4}}\,{\mathtt{nil}})}\rightarrow{\mathtt{just}}\,{4}$ since $\{\!\!\{{{{\mathtt{cons}}\,{x}}\,{\mathtt{nil}}}/{\mathtt{nil}}\}\!\!\}=\mathtt{fail}$ and $\{\!\!\{{{{\mathtt{cons}}\,{4}}\,{\mathtt{nil}}}/{{{\mathtt{cons}}\,{x}}\,{\mathit{xs}}}\}\!\!\}=\{4/x,\mathtt{nil}/\mathit{xs}\}$.

Proposition \thetheorem.

Reduction in CAP is confluent [19].

2.2. Types

In order to ensure that patterns such as ${{x}}\,{{y}}$ decompose only data structures rather than arbitrary terms, we shall introduce two sorts of typing expressions: types and datatypes, the latter being strictly included in the former. We assume given countably infinite sets $\mathcal{V}_{D}$ of datatype variables ($\alpha,\beta,\ldots$), $\mathcal{V}_{A}$ of type variables $(X,Y,\ldots$) and $\mathcal{C}$ of type constants $(\mathbb{c},\mathbb{d},\ldots)$. We define $\mathcal{V}\triangleq\mathcal{V}_{A}\cup\mathcal{V}_{D}$ and use meta-variables $V,W,\ldots$ to denote an arbitrary element in it. Likewise, we write $a,b,\ldots$ for elements in $\mathcal{V}\cup\mathcal{C}$. The sets $\mathcal{T}_{D}$ of $\mu$-datatypes and $\mathcal{T}$ of $\mu$-types, resp., are inductively defined as follows:

[TABLE]

Remark 2.1**.**

A type of the form $\mu{\alpha}.{A}$ is not valid in general since it may produce invalid unfoldings. For example, $\mu{\alpha}.{{\alpha}\supset{\alpha}}={(\mu{\alpha}.{{\alpha}\supset{\alpha}})}\supset{(\mu{\alpha}.{{\alpha}\supset{\alpha}})}$, which fails to preserve sorting. On the other hand, types of the form $\mu{X}.{D}$ are not necessary since they denote the solution to the equation $X=D$, hence $X$ is a variable representing a datatype, a role already fulfilled by $\alpha$.

We consider $\oplus$ to bind tighter than $\supset$, while $\mathrel{@}$ binds tighter than $\oplus$. E.g. ${{{D}\mathrel{@}{A}}\oplus{A^{\prime}}}\supset{B}$ means ${({({D}\mathrel{@}{A})}\oplus{A^{\prime}})}\supset{B}$. We write $A\neq\oplus$ to mean that the root symbol of $A$ is different from $\oplus$; and similarly with the other type constructors. Expressions such as ${{A_{1}}\oplus{\ldots}}\oplus{A_{n}}$ will be abbreviated ${{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}$; this is sound since $\mu$-types will be considered modulo associativity of $\oplus$. A type of the form ${{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}$ where each $A_{i}\neq\oplus$, $i\in 1..n$, is called a maximal union. We often write $\mu{V}.{A}$ to mean either $\mu{\alpha}.{D}$ or $\mu{X}.{A}$. A non-union $\mu$-type $A$ is a $\mu$-type of one of the following forms: $\alpha$, $\mathbb{c}$, ${D}\mathrel{@}{A^{\prime}}$, $X$, ${A^{\prime}}\supset{A^{\prime\prime}}$ or $\mu{V}.{B}$ with $B$ a non-union $\mu$-type. We assume $\mu$-types are contractive: $\mu{V}.{A}$ is contractive if $V$ occurs in $A$ only under a type constructor $\supset$ or $\mathrel{@}$, if at all. For instance, $\mu{X}.{{X}\supset{\mathbb{c}}}$, $\mu{X}.{{X}\supset{X}}$ and $\mu{X}.{{\mathbb{c}}\mathrel{@}{{X}\oplus{X}}}$ are contractive while $\mu{X}.{X}$ and $\mu{X}.{{X}\oplus{X}}$ are not. We henceforth redefine $\mathcal{T}$ to be the set of contractive $\mu$-types.

$\mu$-types come equipped with a notion of type equivalence $\simeq_{\mu}$ (Fig. 1) and subtyping $\preceq_{\mu}$ (Fig. 2). In Fig. 2 a subtyping context $\Sigma$ is a set of assumptions over type variables of the form $V\preceq_{\mu}W$ with $V,W\in\mathcal{V}$. (e-rec) actually encodes two rules, one for datatypes ($\mu{\alpha}.{D}$) and one for arbitrary types ($\mu{X}.{A}$). Likewise for (e-fold) and (e-contr). Regarding the subtyping rules, we adopt those for union of [20]. It should be noted that the naïve variant of (s-rec) in which ${\Sigma}\vdash{\mu{V}.{A}\preceq_{\mu}\mu{V}.{B}}$ is deduced from ${\Sigma}\vdash{A\preceq_{\mu}B}$, is known to be unsound [1]. We often abbreviate ${}\vdash{A\preceq_{\mu}B}$ as $A\preceq_{\mu}B$.

2.3. Typing and Safety

A typing context $\Gamma$ (or $\theta$) is a partial function from term variables to $\mu$-types; $\Gamma(x)=A$ means that $\Gamma$ maps $x$ to $A$. We have two typing judgments, one for patterns ${\theta}\vdash_{\mathsf{p}}{p:A}$ and one for terms ${\Gamma}\vdash{s:A}$. Accordingly, we have two sets of typing rules: Fig. 3, top and bottom. We write $\mathrel{\rhd}{\theta}\vdash_{\mathsf{p}}{p:A}$ to indicate that the typing judgment ${\theta}\vdash_{\mathsf{p}}{p:A}$ is derivable (likewise for $\mathrel{\rhd}{\Gamma}\vdash_{\mathsf{p}}{s:A}$). The typing schemes speak for themselves except for two of them which we now comment. The first is (t-app). Note that we do not impose any additional restrictions on $A_{i}$, in particular it may be a union-type itself. This implies that the argument $u$ can have a union type too. Regarding (t-abs) it requests a number of conditions. First of all, each of the patterns $p_{i}$ must be typable under the typing context $\theta_{i}$, $i\in 1..n$. Also, the set of free matchables in each $p_{i}$ must be exactly the domain of $\theta_{i}$. Another condition, indicated by $({\Gamma,\theta_{i}}\vdash{s_{i}:B})_{i\in 1..n}$, is that the bodies of each of the branches $s_{i}$, $i\in 1..n$, must be typable under the context extended with the corresponding $\theta_{i}$. More noteworthy is the condition that the list $\left[{p_{i}:A_{i}}\right]_{i\in 1..n}$ be compatible.

Compatibility is a condition that ensures that Subject Reduction is not violated. We briefly recall it; see [19] for further details and examples. As already mentioned in example (3) of the introduction, if $p_{i}$ subsumes $p_{j}$ (i.e. ${p_{i}}\mathbin{\vartriangleleft}{p_{j}}$) with $i<j$, then the branch ${p_{j}}\shortrightarrow_{\theta_{j}}{s_{j}}$ will never be evaluated since the argument will already match $p_{i}$. Thus, in this case, in order to ensure SR we demand that $A_{j}\preceq_{\mu}A_{i}$. If $p_{i}$ does not subsume $p_{j}$ (i.e. ${p_{i}}\mathbin{\centernot\vartriangleleft}{p_{j}}$) with $i<j$ we analyze the cause of failure of subsumption in order to determine whether requirements on $A_{i}$ and $A_{j}$ must be put forward, focusing on those cases where $\pi\in\mathsf{pos}\!\left({p_{i}}\right)\cap\mathsf{pos}\!\left({p_{j}}\right)$ is an offending position in both patterns. The following table exhaustively lists them:

[TABLE]

In cases (b), (c) and (e), no extra condition on the types of $p_{i}$ and $p_{j}$ is necessary, since their respective sets of possible arguments are disjoint. The cases where $A_{i}$ and $A_{j}$ must be related are (a) and (d): for those we require $A_{j}\preceq_{\mu}A_{i}$. In summary, the cases requiring conditions on their types are: 1) ${p_{i}}\mathbin{\vartriangleleft}{p_{j}}$; and 2) ${p_{i}}\mathbin{\centernot\vartriangleleft}{p_{j}}$ and ${p_{j}}\mathbin{\vartriangleleft}{p_{i}}$.

Definition 2.2**.**

Given a pattern ${\theta}\vdash_{\mathsf{p}}{p:A}$ and $\pi\in\mathsf{pos}\!\left({p}\right)$, we say $A$ admits a symbol $\odot$ (with $\odot\in\mathcal{V}\cup\mathcal{C}\cup\left\{{\supset,\mathrel{@}}\right\}$) at position $\pi$ iff $\odot\in{A}\|_{\pi}$, where:

[TABLE]

Note that $\mathrel{\rhd}{\theta}\vdash_{\mathsf{p}}{p:A}$ and contractiveness of $A$ imply ${A}\|_{\pi}$ is well-defined for $\pi\in\mathsf{pos}\!\left({p}\right)$.

Definition 2.3**.**

The maximal positions in a set of positions $P$ are:

[TABLE]

The mismatching positions between two patterns are defined below where, recall from the introduction, $\and{p}{\pi}$ stands for the sub-pattern at position $\pi$ of $p$:

[TABLE]

For instance, given patterns $\mathtt{nil}$ and ${{\mathtt{cons}}\,{x}}\,{\mathit{xs}}$ with set of positions $\left\{{\epsilon}\right\}$ and $\left\{{\epsilon,1,2,11,12}\right\}$ respectively, we have $\mathsf{maxpos}\!\left({\mathtt{nil}}\right)=\left\{{\epsilon}\right\}$ and $\mathsf{maxpos}\!\left({{{\mathtt{cons}}\,{x}}\,{\mathit{xs}}}\right)=\left\{{11,12}\right\}$, while the only mismatching position among them is the root, i.e. $\mathsf{mmpos}\!\left({\mathtt{nil}},{{{\mathtt{cons}}\,{x}}\,{\mathit{xs}}}\right)=\left\{{\epsilon}\right\}$.

Definition 2.4**.**

Define the compatibility predicate as

[TABLE]

We say $p:A$ is compatible with $q:B$, notation ${p:A}\lll{q:B}$, iff

[TABLE]

A list of patterns $\left[{p_{i}:A_{i}}\right]_{i\in 1..n}$ is compatible if $\forall i,j\in 1..n.i<j\implies{p_{i}:A_{i}}\lll{p_{j}:A_{j}}$.

Following the example above, consider types $\mathbb{nil}$ and ${{\mathbb{cons}}\mathrel{@}{{\rm Nature}}}\mathrel{@}{(\mu{\alpha}.{{\mathbb{nil}}\oplus{{{\mathbb{cons}}\mathrel{@}{{\rm Nature}}}\mathrel{@}{\alpha}}})}$ for patterns $\mathtt{nil}$ and ${{\mathtt{cons}}\,{x}}\,{xs}$ respectively. Compatibility requires no further restriction in this case since $\mathsf{mmpos}\!\left({\mathtt{nil}},{{{\mathtt{cons}}\,{x}}\,{xs}}\right)=\left\{{\epsilon}\right\}$ and

[TABLE]

hence ${\cal P}_{\mathsf{comp}}$ is false and the property gets validated trivially.

On the contrary, recall motivating example (3) on Sec. 1. ${{\mathtt{vl}}\,{{x}}:{\mathbb{vl}}\mathrel{@}{\mathsf{Bool}}}\lll{{\mathtt{vl}}\,{{y}}:{\mathbb{vl}}\mathrel{@}{{\rm Nature}}}$ requires ${\mathbb{vl}}\mathrel{@}{{\rm Nature}}\preceq_{\mu}{\mathbb{vl}}\mathrel{@}{\mathsf{Bool}}$ since $\mathsf{mmpos}\!\left({{\mathtt{vl}}\,{{x}}},{{\mathtt{vl}}\,{{y}}}\right)=\varnothing$ (i.e. ${\cal P}_{\mathsf{comp}}$ is trivially true). This actually fails because ${\rm Nature}\not\preceq_{\mu}\mathsf{Bool}$. Thus, this pattern combination is rejected by rule (t-abs).

Types are preserved along reduction. The proof relies crucially on compatibility.

Proposition 2.5** (Subject Reduction).**

If $\mathrel{\rhd}{\Gamma}\vdash_{\mathsf{p}}{s:A}$ and $s\rightarrow s^{\prime}$, then $\mathrel{\rhd}{\Gamma}\vdash_{\mathsf{p}}{s^{\prime}:A}$.

Let the set of values be defined as $v::={x}\,{v_{1}\ldots v_{n}}\mathrel{|}{\mathtt{c}}\,{v_{1}\ldots v_{n}}\mathrel{|}({p_{i}}\shortrightarrow_{\theta_{i}}{s_{i}})_{i\in 1..n}$. The following property guarantees that no functional application gets stuck. Essentially this means that, in a well-typed closed term, a function which is applied to an argument has at least one branch that is capable of handling it.

Proposition 2.6** (Progress).**

If $\mathrel{\rhd}{}\vdash_{\mathsf{p}}{s:A}$ and $s$ is not a value, then $\exists s^{\prime}$ such that $s\rightarrow s^{\prime}$.

3. Checking Equivalence and Subtyping

As mentioned in the related work, there are roughly two approaches to implementing equivalence and subtype checking in the presence of recursive types, one based on automata theory and another based on coinductive characterizations of the associated relations. The former leads to efficient algorithms [16] while the latter is more abstract in nature and hence closer to the formalism itself although they may not be as efficient. In the particular case of subtyping for recursive types in the presence of ACI operators, the automata approach of [16] is known not to be applicable [21] while the coinductive approach, developed in this section, yields a correct algorithm. In Sec. 5 we explore an alternative approach for subtyping based on automata inspired from [7]. We next further describe the reasoning behind the coinductive approach.

3.1. Preliminaries

Consider type constructors $\mathrel{@}$ and $\supset$ together with type connector $\oplus$ and the ranked alphabet $\mathfrak{L}\triangleq\left\{{a^{0}\mathrel{|}a\in\mathcal{V}\cup\mathcal{C}}\right\}\cup\left\{{\mathrel{@}^{2},\supset^{2},\oplus^{2}}\right\}$. We write $\mathfrak{T}$ for the set of (possibly) infinite types with symbols in $\mathfrak{L}$. This is a standard construction [3, 8] given by the metric completion based on a simple depth function measuring the distance from the root to the minimum conflicting node in two trees. Perhaps worth mentioning is that the type connector $\oplus$ does not contribute to the depth (hence the reason for calling it a connector rather than a constructor) excluding types consisting of infinite branches of $\oplus$, such as ${({\ldots}\oplus{\ldots})}\oplus{({\ldots}\oplus{\ldots})}$, from $\mathfrak{T}$. A tree is regular if the set of all its subtrees is finite. We shall always work with regular trees and also denote them $\mathfrak{T}$.

Definition 3.1**.**

The truncation of a tree $\mathscr{A}$ at depth $k\in\mathbb{N}$ (notation ${\mathscr{A}}|_{{k}}$) is defined inductively222This definition is well-founded [19]. as follows:

[TABLE]

where $\circ\in\mathcal{C}$ is a distinguished type constant used to identify the nodes where the tree was truncated.

Definition 3.2**.**

The function $\llbracket{\bullet}\rrbracket^{\mathfrak{T}}:\mathcal{T}\to\mathfrak{T}$, mapping $\mu$-types to types, is defined inductively as follows:

[TABLE]

Coinductive characterizations of subsets of $\mathcal{T}\times\mathcal{T}$ whose generating function $\Phi$ is invertible admit a simple (although not necessarily efficient) algorithm for subtype membership checking and consists in “running $\Phi$ backwards” [17, Sec. 21.5]. This strategy is supported by the fact that contractiveness of $\mu$-types guarantees a finite state space to explore (*i.e. *unfolding these types results in regular trees); invertibility further guarantees that there is at most one way in which a member of $\nu\Phi$, the greatest fixed-point of $\Phi$, can be generated. Invertibility of $\Phi:\wp\left({\mathcal{T}\times\mathcal{T}}\right)\to\wp\left({\mathcal{T}\times\mathcal{T}}\right)$ means that for any $\langle{A},{B}\rangle\in\mathcal{T}$, the set $\left\{{{\cal X}\in\wp\left({\mathcal{T}\times\mathcal{T}}\right)\mathrel{|}\langle{A},{B}\rangle\in\Phi({\cal X})}\right\}$ is either empty or contains a unique member.

3.2. Equivalence Checking

Fig. 4 presents a coinductive definition of type equality over $\mu$-types. This relation $\simeq_{\vec{\mu}}$ is defined by means of rules that are interpreted coinductively (indicated by the double lines). The rule (e-union-al) makes use of functions $f$ and $g$ to encode the ACI nature of $\oplus$. Letters $\mathscr{C},\mathscr{D}$, used in rules (e-rec-l-al) and (e-rec-r-al), denote contexts of the form:

[TABLE]

where $\Box$ denotes the hole of the context, $A_{j}\neq\oplus$ for all $j\in 1..n\setminus i$ and $A_{l}\neq\mu$ for all $l\in 1..i-1$. Note that, in particular, $\mathscr{C}$ may take the form $\Box$. These contexts help identify the first occurrence of a $\mu$ constructor within a maximal union. In turn, this allows us to guarantee the invertibility of the generating function associated to these rules.

Proposition 3.3**.**

The generating function associated with the rules of Fig. 4 is invertible.

Moreover, $\simeq_{\vec{\mu}}$ coincides with $\simeq_{\mu}$:

Proposition 3.4**.**

$A\simeq_{\vec{\mu}}B$* iff $A\simeq_{\mu}B$.*

This will allow us to check $A\simeq_{\mu}B$ by using the invertibility of the generating function (implicit in the rules of Fig. 4) for $\simeq_{\vec{\mu}}$. The proof of Prop. 3.4 relies on an intermediate relation $\simeq_{\mathfrak{T}}$ over the possibly infinite trees resulting from the complete unfolding of $\mu$-types. This relation is defined using the same rules as in Fig. 4 except for two important differences: 1) the relation is defined over regular trees in $\mathfrak{T}$, and 2) rules (e-rec-l-al) and (e-rec-r-al) are dropped.

The proof is structured as follows. First we characterize equality of $\mu$-types in terms of equality of their infinite unfoldings [19]:

Proposition 3.5**.**

$A\simeq_{\mu}B$* iff $\llbracket{A}\rrbracket^{\mathfrak{T}}\simeq_{\mathfrak{T}}\llbracket{B}\rrbracket^{\mathfrak{T}}$.*

The proof of Prop. 3.4 thus reduces to showing that $A\simeq_{\vec{\mu}}B$ coincides with $\llbracket{A}\rrbracket^{\mathfrak{T}}\simeq_{\mathfrak{T}}\llbracket{B}\rrbracket^{\mathfrak{T}}$. In order to do so, we appeal to the following result that states that inspecting all finite truncations suffices to determine whether $\llbracket{A}\rrbracket^{\mathfrak{T}}\simeq_{\mathfrak{T}}\llbracket{B}\rrbracket^{\mathfrak{T}}$ holds:

Lemma 3.6**.**

$\forall k\in\mathbb{N}.{\mathscr{A}}|_{{k}}\simeq_{\mathfrak{T}}{\mathscr{B}}|_{{k}}$* iff $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$.*

Proof 3.7**.**

This is proved by showing that the relations ${\cal S}\triangleq\left\{{\langle{\mathscr{A}},{\mathscr{B}}\rangle\mathrel{|}\forall k\in\mathbb{N}.{\mathscr{A}}|_{{k}}\simeq_{\mathfrak{T}}{\mathscr{B}}|_{{k}}}\right\}$ and ${\cal R}\triangleq\left\{{\langle{{\mathscr{A}}|_{{k}}},{{\mathscr{B}}|_{{k}}}\rangle\mathrel{|}\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B},k\in\mathbb{N}}\right\}$ are $\Phi_{\simeq_{\mathfrak{T}}}$-dense. Then we conclude by the coinductive principle. For full details refer to [19].

The proofs of Lem. 3.13 and 3.20 rely on some key lemmas which we now state, preceded by some preliminary notions. Let $\mathcal{A},\mathcal{B},\ldots$ refer to (multi-hole) $\mu\oplus$-contexts:

[TABLE]

When $\mathcal{A}$ consists solely of $\mu$ type constructors, then we say that it is a $\mu$-context. As for types, we use notation ${{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathcal{A}_{i}}$ when referring to a context irrespective of how unions are associated within it. Any $A\in\mathcal{T}$, can be uniquely written as a maximal $\mu\oplus$-context $A=\mathcal{A}[A_{1},\ldots,A_{n}]$, where each $A_{i}\neq\mu,\oplus$, $i\in 1..n$. The $\mu\oplus$-depth of $A$ is the depth of $\mathcal{A}$.

Definition 3.8**.**

The projection of a hole’s position $\pi$ in $\mathcal{A}$, notation ${\mathcal{A}[\vec{A}]}^{\pi}$, is defined by induction on $\mathcal{A}$ as follows:

[TABLE]

We write ${\mathcal{A}}^{\setminus\mu}$ for the $\mu\oplus$-context resulting from dropping all the $\mu$ type constructors from $\mathcal{A}$:

[TABLE]

Lemma 3.9**.**

Let $\mathcal{A}$ be a $\mu\oplus$-context. Then,

[TABLE]

where $\pi_{i}$ is the position of the $i$-th hole (in the left-to-right order) in $\mathcal{A}$.

Proof 3.10**.**

Induction on the context $\mathcal{A}$.

• •

$\mathcal{A}=\Box$:

[TABLE]

• •

$\mathcal{A}=\mu{V}.{\mathcal{A}^{\prime}}$:

[TABLE]

• •

$\mathcal{A}={\mathcal{A}_{1}}\oplus{\mathcal{A}_{2}}$:

[TABLE]

where $\left[{\pi_{1},\ldots,\pi_{n}}\right]=\left[{1\pi^{\prime}_{1},\ldots,1\pi^{\prime}_{n_{1}},2\pi^{\prime\prime}_{1},\ldots,2\pi^{\prime\prime}_{n_{2}}}\right]$.

We also need to deduce the form of a type $A$ whose associated tree is a maximal union type.

Lemma 3.11**.**

Let $A\in\mathcal{T}$, $\mathscr{A}_{i}\in\mathfrak{T}$ for $i\in 1..n$ such that $\llbracket{A}\rrbracket^{\mathfrak{T}}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}$ and $\mathscr{A}_{i}\neq\oplus$. Then, there exists $n^{\prime}\leq n$, $\mathcal{A},\mathcal{A}_{1},\ldots,\mathcal{A}_{n^{\prime}}$ maximal $\oplus$-contexts, $A_{1},\ldots,A_{n^{\prime}}\neq\oplus$ and functions $s,t:1..n^{\prime}\to 1..n$ such that

[TABLE]

for every $l\in 1..n^{\prime}$.

Proof 3.12**.**

As noted before, every $A\in\mathcal{T}$ can be uniquely written as a maximal $\mu\oplus$-context $\mathcal{A}^{\prime}$ and types $A^{\prime}_{1},\ldots,A^{\prime}_{m}$ such that $A^{\prime}_{j}\neq\mu,\oplus$ for all $j\in 1..m$, i.e. $A=\mathcal{A}^{\prime}[\vec{A^{\prime}}]$. It is immediate to see, by Def. 3.2 and 3.8, that $m=n$ and

[TABLE]

for every $i\in 1..n$.

Then, we can decompose $\mathcal{A}^{\prime}$ into two parts, namely a maximal $\oplus$-context $\mathcal{A}$ with $n^{\prime}\leq n$ holes, and multiple $\mu\oplus$-contexts $\mathcal{A}^{\prime}_{1},\ldots,\mathcal{A}^{\prime}_{n^{\prime}}$ such that $\mathcal{A}^{\prime}=\mathcal{A}[\vec{\mathcal{A}^{\prime}}]$ and each $\mathcal{A}^{\prime}_{l}$ is either $\Box$ or starts with $\mu$ for every $l\in 1..n^{\prime}$. Thus, there exists types $A_{1},\ldots,A_{n^{\prime}}$ and functions $s,t:1..n^{\prime}\to 1..n$ such that

[TABLE]

Note that $A_{l}\neq\oplus$ since $\mathcal{A}^{\prime}_{l}=\Box,\mu$ for every $l\in 1..n^{\prime}$.

Finally, let $\rho_{1},\ldots,\rho_{n_{l}}$ be the positions of the holes in $\mathcal{A}^{\prime}_{l}$, we have

[TABLE]

for every $l\in 1..n^{\prime}$. Then, it is enough to take $\mathcal{A}_{l}={\mathcal{A}^{\prime}_{l}}^{\setminus\mu}$.

Finally, we show that $A\simeq_{\vec{\mu}}B$ can be determined by checking all finite truncations of its associated regular trees:

Lemma 3.13**.**

$A\simeq_{\vec{\mu}}B$* iff $\forall k\in\mathbb{N}.{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}\simeq_{\mathfrak{T}}{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}$.*

Proof 3.14**.**

For this proof we use notation $\#_{\mu}\!\left({A}\right)$ for the number of occurrences of the $\mu$ type constructor in the maximal $\mu\oplus$-context $\mathcal{A}$ defining $A=\mathcal{A}[\vec{A}]$.

$\Rightarrow)$* Given $A\simeq_{\vec{\mu}}B$, there exists ${\cal S}\in\wp\left({\mathcal{T}\times\mathcal{T}}\right)$ such that ${\cal S}\subseteq\Phi_{\simeq_{\vec{\mu}}}({\cal S})$ and $\langle{A},{B}\rangle\in{\cal S}$. Define:*

[TABLE]

We show that ${\cal R}({\cal S})\subseteq\Phi_{\simeq_{\mathfrak{T}}}({\cal R}({\cal S}))$.

Define ${\cal S}_{c}\triangleq\left\{{\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal S}\mathrel{|}c=\#_{\mu}\!\left({A}\right)+\#_{\mu}\!\left({B}\right)}\right\}$. For each $c\in\mathbb{N}$, we prove:

[TABLE]

Note that if $k=0$, the result follows directly from (e-refl-t) since $\langle{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{\circ},{\circ}\rangle\in\Phi_{\simeq_{\mathfrak{T}}}({\cal R}({\cal S}))$ trivially. So we in fact prove

[TABLE]

We proceed by induction on $c$.

• •

$c=0$. Since $\langle{A},{B}\rangle\in{\cal S}_{0}$ implies $\langle{A},{B}\rangle\in{\cal S}\subseteq\Phi_{\simeq_{\vec{\mu}}}({\cal S})$, one of the following cases must hold:

• –

$\langle{A},{B}\rangle=\langle{a},{a}\rangle$. Then $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{a},{a}\rangle$ for every $k>0$ and we conclude by (e-refl-t), $\Phi_{\simeq_{\mathfrak{T}}}({\cal R}({\cal S}))$.

• –

$\langle{A},{B}\rangle=\langle{{A^{\prime}}\supset{B^{\prime}}},{{A^{\prime\prime}}\supset{B^{\prime\prime}}}\rangle$* with $\langle{A^{\prime}},{A^{\prime\prime}}\rangle\in{\cal S}$ and $\langle{B^{\prime}},{B^{\prime\prime}}\rangle\in{\cal S}$. Then, by definition of ${\cal R}$ we have both $\langle{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{A^{\prime\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle,\langle{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{B^{\prime\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle\in{\cal R}({\cal S})$ for every $k>0$. Finally, by (e-func-t) and Def. 3.1,*

[TABLE]

for every $k>0$.

• –

$\langle{A},{B}\rangle=\langle{{D}\mathrel{@}{A^{\prime}}},{{D^{\prime}}\mathrel{@}{B^{\prime}}}\rangle$* with $\langle{D},{D^{\prime}}\rangle\in{\cal S}$ and $\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal S}$. Similarly to the previous case, we get $\langle{{\llbracket{D}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{D^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle,\langle{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle\in{\cal R}({\cal S})$ for any $k>0$ from Def. 3.2, and conclude by applying (e-comp-t) with Def. 3.1.*

• –

$\langle{A},{B}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}}\rangle$* with $n+m>2$, $A_{i},B_{j}\neq\mu,\oplus$ and there exists functions $f:1..n\to 1..m,g:1..m\to 1..n$ s.t. $\langle{A_{i}},{B_{f(i)}}\rangle\in{\cal S}$ and $\langle{A_{g(j)}},{B_{j}}\rangle\in{\cal S}$ for every $i\in 1..n,j\in 1..m$.*

Once again, we have $\langle{{\llbracket{A_{i}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B_{f(i)}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle,\langle{{\llbracket{A_{g(j)}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B_{j}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle\in{\cal R}({\cal S})$ for every $i\in 1..n,j\in 1..m,k>0$ by Def. 3.2 and ${\cal R}$.

Moreover, since $A_{i},B_{j}\neq\mu,\oplus$ we can assure $\llbracket{A_{i}}\rrbracket^{\mathfrak{T}},\llbracket{B_{j}}\rrbracket^{\mathfrak{T}}\neq\oplus$ too. Thus, we are able to apply (e-union-t) with $f$ and $g$ to conclude,

[TABLE]

for every $k>0$.

• •

$c>1$. Then:

• –

$\langle{A},{B}\rangle=\langle{\mathscr{C}[\mu{V}.{A^{\prime}}]},{B}\rangle$* with $\langle{\mathscr{C}[\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}]},{B}\rangle\in{\cal S}$. By contractiveness of $\mu$-types, we have $\#_{\mu}\!\left({\mathscr{C}[\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}]}\right)<\#_{\mu}\!\left({\mathscr{C}[\mu{V}.{A^{\prime}}]}\right)$. Hence we can apply the inductive hypothesis to get*

[TABLE]

for every $k>0$. Moreover, since $\llbracket{\mathscr{C}[\mu{V}.{A^{\prime}}]}\rrbracket^{\mathfrak{T}}=\llbracket{\mathscr{C}[\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}]}\rrbracket^{\mathfrak{T}}$ by Def. 3.2, we can safely conclude.

• –

$\langle{A},{B}\rangle=\langle{A},{\mathscr{D}[\mu{W}.{B^{\prime}}]}\rangle$* with $\langle{A},{\mathscr{D}[\left\{{\mu{W}.{B^{\prime}}}/{W}\right\}{B^{\prime}}]}\rangle\in{\cal S}$ and $A\neq\mathscr{C}[\mu{V}.{C}]$. As before, we conclude directly from the inductive hypothesis by resorting to contractiveness of $\mu$-types. Thus,*

[TABLE]

for every $k>0$.

$\Leftarrow)$* We show that ${\cal R}\triangleq\left\{{\langle{A^{\prime}},{B^{\prime}}\rangle\mathrel{|}A^{\prime},B^{\prime}\in\mathcal{T},\forall k\in\mathbb{N}.{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}\simeq_{\mathfrak{T}}{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\right\}$ is $\Phi_{\simeq_{\vec{\mu}}}$-dense.*

Let $\langle{A},{B}\rangle\in{\cal R}$. We proceed by induction on $c=\#_{\mu}\!\left({A}\right)+\#_{\mu}\!\left({B}\right)$. From now on we consider $k>0$ to avoid the border case $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{0}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{0}}}\rangle=\langle{\circ},{\circ}\rangle$.

• •

$c=0$. Since $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle\in\mathbin{\simeq_{\mathfrak{T}}}$ and $\mathbin{\simeq_{\mathfrak{T}}}=\Phi_{\simeq_{\mathfrak{T}}}(\simeq_{\mathfrak{T}})$, one of the following cases must hold:

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{a},{a}\rangle$. Then, since $c=0$ it must be the case $A=a=B$. Thus, by (e-refl-al), $\langle{A},{B}\rangle\in\Phi_{\simeq_{\vec{\mu}}}({\cal R})$.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\mathscr{A}^{\prime}}|_{{k-1}}}\supset{{\mathscr{A}^{\prime\prime}}|_{{k-1}}}},{{{\mathscr{B}^{\prime}}|_{{k-1}}}\supset{{\mathscr{B}^{\prime\prime}}|_{{k-1}}}}\rangle$* with*

[TABLE]

Once again, since the outermost constructor of both $A$ and $B$ is not $\mu$, there exists $A^{\prime},A^{\prime\prime},B^{\prime},B^{\prime\prime}\in\mathcal{T}$ such that $A={A^{\prime}}\supset{A^{\prime\prime}}$ and $B={B^{\prime}}\supset{B^{\prime\prime}}$ with $\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{A}^{\prime}$, $\llbracket{A^{\prime\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{A}^{\prime\prime}$, $\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{B}^{\prime}$ and $\llbracket{B^{\prime\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{B}^{\prime\prime}$. Moreover, from (6) and the definition of ${\cal R}$ we get $\langle{A^{\prime}},{B^{\prime}}\rangle,\langle{A^{\prime\prime}},{B^{\prime\prime}}\rangle\in{\cal R}$. We conclude with (e-func-al), $\langle{A},{B}\rangle\in\Phi_{\simeq_{\vec{\mu}}}({\cal R})$.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\mathscr{A}^{\prime}}|_{{k-1}}}\mathrel{@}{{\mathscr{A}^{\prime\prime}}|_{{k-1}}}},{{{\mathscr{B}^{\prime}}|_{{k-1}}}\mathrel{@}{{\mathscr{B}^{\prime\prime}}|_{{k-1}}}}\rangle$* with*

[TABLE]

As in the previous case, we know there exists $D,D^{\prime},A^{\prime},B^{\prime}\in\mathcal{T}$ such that $A={D}\mathrel{@}{A^{\prime}}$, $B={D^{\prime}}\mathrel{@}{B^{\prime}}$ and $\langle{D},{D^{\prime}}\rangle,\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal R}$. Here we use (e-comp-al) to conclude.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{{\mathscr{A}_{i}}|_{{k}}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{{\mathscr{B}_{j}}|_{{k}}}}\rangle$* with $n+m>2$, ${\mathscr{A}_{i}}|_{{k}},{\mathscr{B}_{j}}|_{{k}}\neq\oplus$ and there exists functions $f:1..n\to 1..m,g:1..m\to 1..n$ such that*

[TABLE]

for every $i\in 1..n,j\in 1..m$.

By Lem. 3.11 on $A$, there exists $n^{\prime}\leq n$, maximal $\oplus$-contexts $\mathcal{A},\mathcal{A}_{1},\ldots,\mathcal{A}_{n^{\prime}}$, types $A_{1},\ldots,A_{n^{\prime}}\neq\oplus$ and functions $s,t:1..n^{\prime}\to 1..n$ such that

[TABLE]

for every $l\in 1..n^{\prime}$. Moreover, since $\#_{\mu}\!\left({A}\right)=0$ and $\mathcal{A}$ is maximal, it can only be the case that $n^{\prime}=n$ and $\mathcal{A}_{l}=\Box$ for every $l\in 1..n^{\prime}$. Thus, $s=t=id$ and

[TABLE]

for every $i\in 1..n$.

With a similar analysis we have $B=\mathcal{B}[\vec{B}]$ with $\mathcal{B}$ a maximal $\oplus$-context, and

[TABLE]

for every $j\in 1..m$. Then, from (7), (8)-left and (9)-left we get

[TABLE]

for every $i\in 1..n,j\in 1..m$. Finally, we apply (e-union-al) with $f$, $g$, (8)-right and (9)-right to conclude $\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}}\rangle\in\Phi_{\simeq_{\vec{\mu}}}({\cal R})$.

• •

$c>0$. Then we need to distinguish two cases:

• –

$\#_{\mu}\!\left({A}\right)=0$. Then, it is necessarily the case $\#_{\mu}\!\left({B}\right)>0$. Thus, $B=\mathscr{D}[\mu{W}.{B^{\prime}}]$ and, by Def. 3.2, we have

[TABLE]

for every $k\in\mathbb{N}$. Moreover, by contractiveness of $\mu$-types we know that

[TABLE]

and we can apply the inductive hypothesis to get $\langle{A},{\mathscr{D}[\left\{{\mu{W}.{B^{\prime}}}/{W}\right\}{B^{\prime}}]}\rangle\in{\cal R}$.

Note that $\#_{\mu}\!\left({A}\right)=0$ implies $A\neq\mathscr{C}[\mu{V}.{A^{\prime}}]$. Then, we are under the hypothesis of rule (e-rec-r-al), and we conclude $\langle{A},{\mathscr{D}[\mu{W}.{B^{\prime}}]}\rangle\in\Phi_{\simeq_{\vec{\mu}}}({\cal R})$.

• –

$\#_{\mu}\!\left({A}\right)>0$. Then, $A=\mathscr{C}[\mu{V}.{A^{\prime}}]$. Similarly to the previous case, by Def. 3.2 we have

[TABLE]

for every $k\in\mathbb{N}$. By contractiveness of $\mu$-types we can safely apply the inductive hypothesis to get $\langle{\mathscr{C}[\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}]},{B}\rangle\in{\cal R}$, and finally conclude with rule (e-rec-l-al), $\langle{\mathscr{C}[\mu{V}.{A^{\prime}}]},{B}\rangle\in\Phi_{\simeq_{\vec{\mu}}}({\cal R})$.

Thus we can resort to invertibility of the generating function to check for $\simeq_{\vec{\mu}}$. Fig. 5 presents the algorithm. It uses $\mathrel{\mathtt{seq}}e_{1}\ldots e_{n}$ which sequentially evaluates each of its arguments, returning the value of the first of these that does not fail. Evaluation of $\mathsf{eqtype}({\emptyset},{A},{B})$ can have one of two outcomes: $\mathtt{fail}$, meaning that $A\not\simeq_{\vec{\mu}}B$, or a set $S\in\wp\left({\mathcal{T}\times\mathcal{T}}\right)$ that is $\Phi$-dense with $(A,B)\in S$, proving that $A\simeq_{\vec{\mu}}B$.

3.3. Subtype Checking

The approach to subtype checking is similar to that of type equivalence. First consider the relation $\preceq_{\vec{\mu}}$ over $\mu$-types defined in Fig. 6. It captures $\preceq_{\mu}$:

Proposition 3.15**.**

$A\preceq_{\vec{\mu}}B$* iff $A\preceq_{\mu}B$.*

The proof strategy is similar to that of Prop. 3.4. In this case we resort to a proper subtyping relation for infinite trees that essentially results from dropping rules (s-rec-l-al) and (s-rec-r-al) in Fig. 6.

In this case we resort to Prop. 3.16 and Lem. 3.17 to establish a relation with $\preceq_{\mu}$ via the infinite trees semantics and its finite truncations [19].

Proposition 3.16**.**

$A\preceq_{\mu}B$* iff $\llbracket{A}\rrbracket^{\mathfrak{T}}\preceq_{\mathfrak{T}}\llbracket{B}\rrbracket^{\mathfrak{T}}$.*

Lemma 3.17**.**

$\forall k\in\mathbb{N}.{\mathscr{A}}|_{{k}}\preceq_{\mathfrak{T}}{\mathscr{B}}|_{{k}}$* iff $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$.*

The following lemma allows us to relate the different non-union projections of two maximal union types that belong to a $\Phi_{\preceq_{\vec{\mu}}}$-dense relation.

Lemma 3.18**.**

Let $A,B\in\mathcal{T}$. Suppose $\langle{A},{B}\rangle\in{\cal S}$ and ${\cal S}\subseteq\Phi_{\preceq_{\vec{\mu}}}({\cal S})$. Let $\mathcal{A}$ be the maximal $\mu\oplus$-context such that $A=\mathcal{A}[A_{1},\ldots,A_{n}]$, for some $A_{i}$, $i\in 1..n$, and $\mathcal{B}$ the maximal $\mu\oplus$-context such that $B=\mathcal{B}[B_{1},\ldots,B_{m}]$. Then, there exists $f:1..n\to 1..m$ such that for each $i\in 1..n$, $\langle{{\mathcal{A}[\vec{A}]}^{\pi_{i}}},{{\mathcal{B}[\vec{B}]}^{\rho_{f(i)}}}\rangle\in{\cal S}$.

Proof 3.19**.**

Induction on the sum of the $\mu\oplus$-depths.

• •

If the sum is 0, then $\mathcal{A}=\Box=\mathcal{B}$ and the result is immediate.

• •

If it is greater than 0, we analyze the shape of $\mathcal{A}$:

• –

$\mathcal{A}=\Box$. Then $n=1$ and $A_{n}=A\neq\mu,\oplus$ and we have two possibilities for $\mathcal{B}$:

1. (1)

$\mathcal{B}=\mu{W}.{\mathcal{B}^{\prime}}$. Then the only rule that applies is (s-rec-r-al). By hypothesis of the rule, $\langle{A},{\left\{{\mu{W}.{\mathcal{B}^{\prime}[\vec{B}]}}/{W}\right\}{\mathcal{B}^{\prime}[\vec{B}]}}\rangle\in{\cal S}$. Moreover, since

[TABLE]

and $\mu$-types are contractive (hence none of the $\vec{B}$ can be variables), we can assure $\mathcal{B}^{\prime}$ is a maximal $\mu\oplus$-context too. Then, by inductive hypothesis, there exists $f:1..n\to 1..m$ such that

[TABLE]

for each $i\in 1..n$. Finally, we conclude by Def. 3.8, $\langle{{\mathcal{A}[\vec{A}]}^{\pi_{i}}},{{(\mu{W}.{\mathcal{B}^{\prime}[\vec{B}]})}^{1\rho_{f(i)}}}\rangle\in{\cal S}$. 2. (2)

$\mathcal{B}={\mathcal{B}_{1}}\oplus{\mathcal{B}_{2}}$. From $B=\mathcal{B}[\vec{B}]$, with a similar analysis to the one made for the proof of Lem. 3.11, we can decompose $\mathcal{B}$ into a maximal $\oplus$-context $\mathcal{B}^{\prime}$ and multiple $\mu\oplus$-contexts $\mathcal{B}^{\prime}_{1},\ldots,\mathcal{B}^{\prime}_{m^{\prime}}$ with $m^{\prime}\leq m$. Then, there exists types $B^{\prime}_{1},\ldots,B^{\prime}_{m^{\prime}}$ and functions $s,t:1..m^{\prime}\to 1..m$ such that

[TABLE]

for every $l\in 1..m^{\prime}$. Moreover, since $\mathcal{B}={\mathcal{B}_{1}}\oplus{\mathcal{B}_{2}}$ and $\mathcal{B}^{\prime}$ is maximal, we have $m^{\prime}>1$ and $B^{\prime}_{l}\neq\oplus$ for every $l\in 1..m^{\prime}$.

*Then, we can assure that the only rule that applies for $\langle{A},{B}\rangle\in{\cal S}$ is (s-union-r-al). By hypothesis of it, $\langle{A},{B^{\prime}_{k}}\rangle\in{\cal S}$ for some $k\in 1..m^{\prime}$. Let $m_{k}=t(k)-s(k)$ (*i.e. the number of holes in $\mathcal{B}^{\prime}_{k}$). By inductive hypothesis and (10)-right with $l=k$, there exists $f:1..n\to 1..m_{k}$ such that

[TABLE]

where $\tau^{k}_{h}$ is the position of the $(h-s(k))$-th hole in $\mathcal{B}^{\prime}_{k}$. Let $\rho^{\prime}_{k}$ be the position of the $k$-th hole in $\mathcal{B}^{\prime}$ and take $\rho_{h}=\rho^{\prime}_{k}\tau^{k}_{h}$. Then, by Def. 3.8

[TABLE]

Finally, since $\mathcal{B}^{\prime}[\vec{B^{\prime}}]=B=\mathcal{B}[\vec{B}]$, we resort to the hypothesis and (10)-left to conclude $\langle{{\mathcal{A}[\vec{A}]}^{\pi_{i}}},{{\mathcal{B}[\vec{B}]}^{\rho_{f(i)}}}\rangle\in{\cal S}$.

• –

$\mathcal{A}=\mu{V}.{\mathcal{A}^{\prime}}$. Then the only rule that applies is (s-rec-l-al) and we have

[TABLE]

As before, by contractiveness of $\mu$-types, we get $\langle{\mathcal{A}^{\prime}[\left\{{\mu{V}.{\mathcal{A}^{\prime}[\vec{A}]}}/{V}\right\}{\vec{A}}]},{\mathcal{B}[\vec{B}]}\rangle\in{\cal S}$ with $\mathcal{A}^{\prime}$ still a maximal $\mu\oplus$-context. Then, by inductive hypothesis, there exists $f:1..n\to 1..m$ such that

[TABLE]

for each $i\in 1..n$. Once again we conclude by Def. 3.8, $\langle{{(\mu{V}.{\mathcal{A}^{\prime}[\vec{A}]})}^{1\pi_{i}}},{{\mathcal{B}[\vec{B}]}^{\rho_{f(i)}}}\rangle\in{\cal S}$.

• –

$\mathcal{A}={\mathcal{A}_{1}}\oplus{\mathcal{A}_{2}}$. Here we have two possibilities for $B$:

1. (1)

$B=\mu$* (i.e. $\mathcal{B}=\mu{W}.{\mathcal{B}^{\prime}}$). Then, it can only be the case of (s-rec-r-al) and analysis here is analogous to the one presented before.* 2. (2)

$B\neq\mu$. This case is similar to the one for $\mathcal{B}={\mathcal{B}_{1}}\oplus{\mathcal{B}_{2}}$ presented above. Here we have $A=\mathcal{A}[\vec{A}]$ and we can decompose $\mathcal{A}$ into a maximal $\oplus$-context $\mathcal{A}^{\prime}$ and multiple $\mu\oplus$-contexts $\mathcal{A}^{\prime}_{1},\ldots,\mathcal{A}^{\prime}_{n^{\prime}}$ with $n^{\prime}\leq n$. Then, there exists types $A^{\prime}_{1},\ldots,A^{\prime}_{n^{\prime}}$ and functions $s,t:1..n^{\prime}\to 1..n$ such that

[TABLE]

*for every $l\in 1..n^{\prime}$. Again we get $A^{\prime}_{l}\neq\oplus$ and $n^{\prime}>1$, thus we can only apply (s-union-l-al) for $\langle{A},{B}\rangle\in{\cal S}$. By hypothesis of the rule we know $\langle{A^{\prime}_{l}},{B}\rangle\in{\cal S}$ for every $l\in 1..n^{\prime}$. Now we take $n_{l}=t(l)-s(l)$ (*i.e. the number of holes in $\mathcal{A}^{\prime}_{l}$) and we apply the inductive hypothesis on each assumption of the rule. Thus, there exists $f_{l}:1..n_{l}\to 1..m$ such that

[TABLE]

for every $l\in 1..n^{\prime}$. Then, let $\pi^{\prime}_{l}$ be the position of the $l$-th hole in $\mathcal{A}^{\prime}$ and $\pi_{i}=\pi^{\prime}_{l}\tau^{l}_{i}$ to get

[TABLE]

Finally, we combine all functions $f_{l}$ into one $f:1..n\to 1..m$, and resort to (11)-left (i.e. $\mathcal{A}^{\prime}[\vec{A^{\prime}}]=A=\mathcal{A}[\vec{A}]$) to conclude with $\langle{{\mathcal{A}[\vec{A}]}^{\pi_{i}}},{{\mathcal{B}[\vec{B}]}^{\rho_{f(i)}}}\rangle\in{\cal S}$.

Finally, we prove:

Lemma 3.20**.**

$A\preceq_{\vec{\mu}}B$* iff $\forall k\in\mathbb{N}.{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}\preceq_{\mathfrak{T}}{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}$.*

Proof 3.21**.**

In the following proof we denote with $\#_{\mu}\!\left({A}\right)$ the number $\mu$ type constructors at the head of type $A$:

[TABLE]

$\Rightarrow)$* Given $A\preceq_{\vec{\mu}}B$, there exists ${\cal S}\in\wp\left({\mathcal{T}\times\mathcal{T}}\right)$ such that ${\cal S}\subseteq\Phi_{\preceq_{\vec{\mu}}}({\cal S})$ and $\langle{A},{B}\rangle\in{\cal S}$. Define:*

[TABLE]

We show that ${\cal R}({\cal S})\subseteq\Phi_{\preceq_{\mathfrak{T}}}({\cal R}({\cal S}))$.

Define ${\cal S}_{c}\triangleq\left\{{\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal S}\mathrel{|}c=\#_{\mu}\!\left({A^{\prime}}\right)+\#_{\mu}\!\left({B^{\prime}}\right)}\right\}$. For each $c\in\mathbb{N}$, we prove:

[TABLE]

Note that if $k=0$, the result follows directly from (s-refl-t) since $\langle{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{\circ},{\circ}\rangle\in\Phi_{\preceq_{\mathfrak{T}}}({\cal R}({\cal S}))$ trivially. So we in fact prove

[TABLE]

We proceed by induction on $c$.

• •

$c=0$. Since $\langle{A},{B}\rangle\in{\cal S}$ and ${\cal S}$ is $\Phi_{\preceq_{\vec{\mu}}}$-dense one of the following cases must occur:

• –

$\langle{A},{B}\rangle=\langle{a},{a}\rangle$. Then for any $k>0$, $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{a},{a}\rangle\in\Phi_{\preceq_{\mathfrak{T}}}({\cal R}({\cal S}))$ by (s-refl-t).

• –

$\langle{A},{B}\rangle=\langle{{A^{\prime}}\supset{B^{\prime}}},{{A^{\prime\prime}}\supset{B^{\prime\prime}}}\rangle$* and $\langle{A^{\prime\prime}},{A^{\prime}}\rangle\in{\cal S}$ and $\langle{B^{\prime}},{B^{\prime\prime}}\rangle\in{\cal S}$. From $\langle{A^{\prime\prime}},{A^{\prime}}\rangle\in{\cal S}$ we have $\langle{{\llbracket{A^{\prime\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle\in{\cal R}({\cal S})$, for any $k>0$, as follows from Def. 3.2. Similarly, $\langle{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{B^{\prime\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle\in{\cal R}({\cal S})$. Then by (s-func-t) and Def. 3.1,*

[TABLE]

for any $k>0$.

• –

$\langle{A},{B}\rangle=\langle{{D}\mathrel{@}{A^{\prime}}},{{D^{\prime}}\mathrel{@}{B^{\prime}}}\rangle$* and $\langle{D},{D^{\prime}}\rangle\in{\cal S}$ and $\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal S}$. As before, we get $\langle{{\llbracket{D}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{D^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle,\langle{{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}},{{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k-1}}}\rangle\in{\cal R}({\cal S})$ for any $k>0$ from the definition of $T$, and conclude by applying (s-comp-t) with Def. 3.1.*

• –

$\langle{A},{B}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}},{B}\rangle$* with $n>1$, $B\neq\mu$, $A_{i}\neq\oplus$ and $\langle{A_{i}},{B}\rangle\in{\cal S}$ for all $i\in 1..n$. $A$ can alternately be written as $\mathcal{A}[\vec{A}]$ where $\mathcal{A}$ is a maximal $\oplus$-context.*

Let $\mathcal{A}^{\prime}$ be the $\mu\oplus$-context such that $A=\mathcal{A}^{\prime}[\vec{A^{\prime}}]$ with $A^{\prime}_{i}\neq\mu,\oplus$ for all $i\in 1..n^{\prime}$ (note that $n^{\prime}\geq n$). Similarly, let $\mathcal{B}$ the $\mu\oplus$-context such that $B=\mathcal{B}[\vec{B}]$ with $B_{j}\neq\mu,\oplus$ for all $j\in 1..m$. Note that, since $A=\mathcal{A}[\vec{A}]$, there exist $s,t:1..n\to 1..n^{\prime}$ and $\mu\oplus$-contexts $\mathcal{A}_{1},\ldots,\mathcal{A}_{n}$ such that

[TABLE]

From $\langle{A},{B}\rangle\in{\cal S}$ and Lem. 3.18, there exists $f:1..n^{\prime}\to 1..m$ such that

[TABLE]

where $\pi_{i}$ is the position of the $i$-th hole in $\mathcal{A}^{\prime}$ and $\rho_{f(i)}$ is the position of the $f(i)$-th hole in $\mathcal{B}$. Now we reason as follows:

[TABLE]

Note that since $A^{\prime}_{i}\neq\mu,\oplus$ for all $i\in 1..n^{\prime}$, then ${\mathcal{A}^{\prime}[\vec{A^{\prime}}]}^{\pi_{i}}\neq\mu,\oplus$ too. Then, we can assure that $\llbracket{{\mathcal{A}^{\prime}[\vec{A^{\prime}}]}^{\pi_{i}}}\rrbracket^{\mathfrak{T}}\neq\oplus$ for every $i\in 1..n^{\prime}$. Similarly, $\llbracket{{\mathcal{B}[\vec{B}]}^{\rho_{j}}}\rrbracket^{\mathfrak{T}}\neq\oplus$ for every $j\in 1..m$. Thus, (s-union-t) can be applied safely.

• –

$\langle{A},{B}\rangle=\langle{A},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{l}}}\rangle$* with $\langle{A},{B_{l}}\rangle\in{\cal S}$ for some $l\in 1..m$, $m>1$, $A\neq\mu,\oplus$ and $B_{j}\neq\oplus$ for all $j\in 1..m$. We call $\mathcal{B}$ the maximal $\oplus$-context defining $B$ (i.e. $B=\mathcal{B}[\vec{B}]$ with $B_{j}\neq\oplus$ for every $j\in 1..m$).*

Let $\mathcal{B}^{\prime}$ be the $\mu\oplus$-context such that $B=\mathcal{B}^{\prime}[\vec{B^{\prime}}]$ with $B^{\prime}_{j}\neq\mu,\oplus$ for all $l\in 1..m^{\prime}$ (here $m^{\prime}\geq m$). Similarly, $A=\mathcal{A}[\vec{A}]$ but we know that $\mathcal{A}=\Box$ since $A\neq\mu,\oplus$ by hypothesis. As in the previous case, from $B=\mathcal{B}[\vec{B}]$, there exists $s,t:1..m\to 1..m^{\prime}$ and $\mu\oplus$-contexts $\mathcal{B}_{1},\ldots,\mathcal{B}_{m}$ such that

[TABLE]

Take $\vec{B^{\prime}_{j}}=B^{\prime}_{s(j)},\ldots,B^{\prime}_{t(j)}$ for every $j\in 1..m$. Then, from $\langle{A},{B_{l}}\rangle\in{\cal S}$ and Lem.3.18, there exists $f:1..n\to 1..m^{\prime}$ such that

[TABLE]

Now, from $B^{\prime}_{j}\neq\mu,\oplus$ we can assure ${\mathcal{B}^{\prime}[\vec{B^{\prime}}]}^{\rho^{\prime}_{j}}\neq\mu,\oplus$ for every $j\in 1..m^{\prime}$. Thus, ${\mathcal{B}^{\prime}[\vec{B^{\prime}}]}^{\rho^{\prime}_{f(1)}}\neq\mu,\oplus$ taking $\rho^{\prime}_{f(1)}=\rho_{l}\tau_{f(1)}$ where $\rho_{l}$ is the position of the $l$-th hole in $\mathcal{B}$. Finally, we can assure both $\llbracket{A}\rrbracket^{\mathfrak{T}}$ and $\llbracket{{\mathcal{B}^{\prime}[\vec{B^{\prime}}]}^{\rho^{\prime}_{f(1)}}}\rrbracket^{\mathfrak{T}}$ are non-union. We conclude as follows (recall $n=1$ and $\mathcal{A}=\Box$, thus ${\mathcal{A}[\vec{A}]}^{\pi_{1}}=A$):

[TABLE]

• •

$c>0$. Then:

• –

$\langle{A},{B}\rangle=\langle{\mu{V}.{A^{\prime}}},{B}\rangle$* and $\langle{\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}},{B}\rangle\in{\cal S}$. By inductive hypothesis,*

[TABLE]

Since $\langle{{\llbracket{\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{\llbracket{\mu{V}.{A^{\prime}}}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle$ by Def. 3.2, we conclude.

• –

$\langle{A},{B}\rangle=\langle{A},{\mu{W}.{B^{\prime}}}\rangle$* and $\langle{A},{\left\{{\mu{W}.{B^{\prime}}}/{W}\right\}{B^{\prime}}}\rangle\in{\cal S}$ and $A\neq\mu$. As before, from the inductive hypothesis we get*

[TABLE]

and we conclude by Def. 3.2.

$\Leftarrow)$* We show that ${\cal R}\triangleq\left\{{\langle{A^{\prime}},{B^{\prime}}\rangle\mathrel{|}A^{\prime},B^{\prime}\in\mathcal{T},\forall k\in\mathbb{N}.{\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}\preceq_{\mathfrak{T}}{\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}}|_{{k}}}\right\}$ is $\Phi_{\preceq_{\vec{\mu}}}$-dense.*

Let $\langle{A},{B}\rangle\in{\cal R}$. We proceed by induction on $c=\#_{\mu}\!\left({A}\right)+\#_{\mu}\!\left({B}\right)$. From now on we consider $k>0$ to avoid the border case $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{0}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{0}}}\rangle=\langle{\circ},{\circ}\rangle$.

• •

$c=0$. Since $\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle\in\mathbin{\preceq_{\mathfrak{T}}}$ and $\mathbin{\preceq_{\mathfrak{T}}}=\Phi_{\preceq_{\mathfrak{T}}}(\preceq_{\mathfrak{T}})$, one of the following cases must hold:

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{a},{a}\rangle$. Then, since $c=0$ it must be the case $A=a=B$. Thus, by (s-refl-al), $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\mathscr{A}^{\prime}}|_{{k-1}}}\supset{{\mathscr{A}^{\prime\prime}}|_{{k-1}}}},{{{\mathscr{B}^{\prime}}|_{{k-1}}}\supset{{\mathscr{B}^{\prime\prime}}|_{{k-1}}}}\rangle$* with*

[TABLE]

Once again, since the outermost constructor of both $A$ and $B$ is not $\mu$, there exists $A^{\prime},A^{\prime\prime},B^{\prime},B^{\prime\prime}\in\mathcal{T}$ such that $A={A^{\prime}}\supset{A^{\prime\prime}}$ and $B={B^{\prime}}\supset{B^{\prime\prime}}$ with $\llbracket{A^{\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{A}^{\prime}$, $\llbracket{A^{\prime\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{A}^{\prime\prime}$, $\llbracket{B^{\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{B}^{\prime}$ and $\llbracket{B^{\prime\prime}}\rrbracket^{\mathfrak{T}}=\mathscr{B}^{\prime\prime}$. Moreover, from (12) we get $\langle{B^{\prime}},{A^{\prime}}\rangle,\langle{A^{\prime\prime}},{B^{\prime\prime}}\rangle\in{\cal R}$. We conclude with (s-func-al), $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\mathscr{A}^{\prime}}|_{{k-1}}}\mathrel{@}{{\mathscr{A}^{\prime\prime}}|_{{k-1}}}},{{{\mathscr{B}^{\prime}}|_{{k-1}}}\mathrel{@}{{\mathscr{B}^{\prime\prime}}|_{{k-1}}}}\rangle$* with*

[TABLE]

As in the previous case, we know there exists $D,D^{\prime},A^{\prime},B^{\prime}\in\mathcal{T}$ such that $A={D}\mathrel{@}{A^{\prime}}$, $B={D^{\prime}}\mathrel{@}{B^{\prime}}$ and $\langle{D},{D^{\prime}}\rangle,\langle{A^{\prime}},{B^{\prime}}\rangle\in{\cal R}$. Here we use (s-comp-al) to conclude.

• –

$\langle{{\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}},{{\llbracket{B}\rrbracket^{\mathfrak{T}}}|_{{k}}}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{{\mathscr{A}_{i}}|_{{k}}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{{\mathscr{B}_{j}}|_{{k}}}}\rangle$* such that $n+m>2$, ${\mathscr{A}_{i}}|_{{k}},{\mathscr{B}_{j}}|_{{k}}\neq\oplus$ and there exists $f:1..n\to 1..m$ s.t. ${\mathscr{A}_{i}}|_{{k}}\preceq_{\mathfrak{T}}{\mathscr{B}_{f(i)}}|_{{k}}$.*

We distinguish two cases:

1. (1)

$n=1$. Then ${\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}={\mathscr{A}_{1}}|_{{k}}\neq\mu,\oplus$ and $m>1$. Moreover, by Lem. 3.11 on $B$, there exists $m^{\prime}\leq m$, $\mathcal{B},\mathcal{B}_{1},\ldots,\mathcal{B}_{m^{\prime}}$ maximal $\oplus$-contexts, $B_{1},\ldots,B_{m^{\prime}}\neq\oplus$ and functions $s,t:1..m^{\prime}\to 1..m$ such that

[TABLE]

for every $l\in 1..m^{\prime}$.

Let $h\in 1..m^{\prime}$ such that $f(1)\in s(h)..t(h)$. From

[TABLE]

and (13)-right, we get

[TABLE]

by (s-union-t). Thus, $\langle{A},{B_{h}}\rangle\in{\cal R}$.

Finally, we have $A\neq\mu,\oplus$, $B_{l}\neq\oplus$ and, since $\#_{\mu}\!\left({B}\right)=0$, $m\geq m^{\prime}>1$. We take $f^{\prime}:1..1\to 1..m^{\prime}$ such that $f^{\prime}(1)=h$ and conclude with (13)-left, by (s-union-r-al), $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$. 2. (2)

$n>1$. By Lem. 3.11 on $A$, there exists $n^{\prime}\leq n$, $\mathcal{A},\mathcal{A}_{1},\ldots,\mathcal{A}_{n^{\prime}}$ maximal $\oplus$-contexts, $A_{1},\ldots,A_{n^{\prime}}\neq\oplus$ and functions $s,t:1..n^{\prime}\to 1..n$ such that

[TABLE]

for every $l\in 1..n^{\prime}$.

From (14)-right, by (s-union-t) using function $f$ from the hypothesis, we get

[TABLE]

and thus, $\langle{A_{l}},{B}\rangle\in{\cal R}$ for every $l\in 1..n^{\prime}$.

Then, we conclude by (s-union-l-al) resorting to (14)-left and the fact that $A,B\neq\mu$ by hypothesis (hence $n\geq n^{\prime}>1$) and $A_{l}\neq\oplus$, $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$.

• •

$c>0$. Then we must analyze two cases:

1. (1)

$A=\mu{V}.{A^{\prime}}$. Then ${\llbracket{A}\rrbracket^{\mathfrak{T}}}|_{{k}}={\llbracket{\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}}\rrbracket^{\mathfrak{T}}}|_{{k}}$ by Def. 3.2. Thus, $\langle{\left\{{\mu{V}.{A^{\prime}}}/{V}\right\}{A^{\prime}}},{B}\rangle\in{\cal R}$ too. We conclude by (s-rec-l-al), $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$. 2. (2)

$A\neq\mu$* and $B=\mu{W}.{B^{\prime}}$. Again, $\langle{A},{B}\rangle\in{\cal R}$ implies $\langle{A},{\left\{{\mu{W}.{B^{\prime}}}/{W}\right\}{B^{\prime}}}\rangle\in{\cal R}$. This time we conclude by (s-rec-r-al), $\langle{A},{B}\rangle\in\Phi_{\preceq_{\vec{\mu}}}({\cal R})$.*

Unfortunately, the generating function determined by the rules in Fig. 6, let us call it $\Phi_{\preceq_{\vec{\mu}}}$, is not invertible. Notice that (s-union-r-al) overlaps with itself. For example, $\mathbb{c}\preceq_{\vec{\mu}}{({\mathbb{c}}\oplus{\mathbb{d}})}\oplus{({\mathbb{e}}\oplus{\mathbb{c}})}$ belongs to two $\Phi_{\preceq_{\vec{\mu}}}$-saturated sets (*i.e. *sets ${\cal X}$ such that ${\cal X}\subseteq\Phi_{\preceq_{\vec{\mu}}}({\cal X})$):

\begin{array}[]{rcl}{\cal X}_{1}&=&\left\{{\langle{\mathbb{c}},{(\mathbb{c}\oplus\mathbb{d})\oplus(\mathbb{e}\oplus\mathbb{c})}\rangle,\langle{\mathbb{c}},{(\mathbb{c}\oplus\mathbb{d})}\rangle,\langle{\mathbb{c}},{\mathbb{c}}\rangle}\right\}\\ {\cal X}_{2}&=&\left\{{\langle{\mathbb{c}},{(\mathbb{c}\oplus\mathbb{d})\oplus(\mathbb{e}\oplus\mathbb{c})}\rangle,\langle{\mathbb{c}},{(\mathbb{e}\oplus\mathbb{c})}\rangle,\langle{\mathbb{c}},{\mathbb{c}}\rangle}\right\}\end{array}

However, since this is the only source of non-invertibility we easily derive a subtype membership checking function $\mathsf{subtype}({\bullet},{\bullet},{\bullet})$ that, in the case of (s-union-r-al), simply checks all cases (Fig. 7).

4. Type Checking

A syntax-directed presentation for typing in CAP, inferring judgments of the form ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to7.09pt{\vbox to5.2pt{\pgfpicture\makeatletter\hbox{\hskip 1.19998pt\lower-2.59999pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{{ {\pgfsys@beginscope\pgfsys@setlinewidth{0.32pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{} \pgfsys@moveto{-1.19998pt}{1.59998pt}\pgfsys@curveto{-1.09998pt}{0.99998pt}{0.0pt}{0.09999pt}{0.29999pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.09999pt}{-1.09998pt}{-0.99998pt}{-1.19998pt}{-1.59998pt}\pgfsys@stroke\pgfsys@endscope}} }{}{}{{}}{{ {\pgfsys@beginscope\pgfsys@setdash{}{0.0pt}\pgfsys@rectcap{} {} \pgfsys@moveto{0.09999pt}{-2.59999pt}\pgfsys@lineto{0.09999pt}{2.59999pt}\pgfsys@stroke\pgfsys@endscope}} }{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A}$, may be obtained from the rules of Fig. 3 by dropping subsumption. This requires “hard-wiring” it back in into (t-app). Unfortunately, the naïve syntax-directed variant:

{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{{\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r:({{\oplus}}{\begin{subarray}{c}i\in 1..n\end{subarray}}{A{i}})\supset B}\quad{\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{u:A^{\prime}}\quad A^{\prime}\preceq_{\mu}A_{k},\mbox{ for some }k\in 1..n}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=267.9871pt\hbox{\kern 3.00003pt{\textsc{({t-app-al})}^{\prime}}}}}\hbox{\kern 113.12381pt\hbox{\displaystyle{{\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r,u:B}}}}}}

fails to capture all the required terms. In other words, there are $\Gamma,s$ and $A$ such that ${\Gamma}\vdash{s:A}$ but no $A^{\prime}\preceq_{\mu}A$ such that ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A^{\prime}}$. For example, take $\Gamma(x)\triangleq{({{\mathbb{c}}\oplus{\mathbb{e}}}\supset{\mathbb{d}})}\oplus{({{\mathbb{c}}\oplus{\mathbb{f}}}\supset{\mathbb{d}})}$, $s\triangleq{x}\,{\mathtt{c}}$ and $A\triangleq\mathbb{d}$. More generally, from ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r:A}$ and $A\preceq_{\mu}{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}\supset B$ we cannot infer that $A$ is a functional type due to the presence of union types. A complete (Prop. 4.1) syntax directed presentation is obtained by dropping (t-subs) from Fig. 3 and replacing (t-abs) and (t-app) by (t-abs-al) and (t-app-al), resp., of Fig. 8.

Proposition 4.1**.**

1. (1)

If ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A}$, then ${\Gamma}\vdash{s:A}$. 2. (2)

If ${\Gamma}\vdash{s:A}$, then $\exists A^{\prime}$ such that $A^{\prime}\preceq_{\mu}A$ and ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A^{\prime}}$.

Proof 4.2**.**

1. (1)

By induction on ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A}$ analyzing the last rule applied.

• •

(t-var-al), (t-const-al) and (t-comp-al) are immediate.

• •

(t-abs-al): then $A={{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}$ and, by hypothesis of the rule, we have $\left[{p_{i}:A_{i}}\right]_{i\in 1..n}$ compatible, ${\theta_{i}}\vdash_{\mathsf{p}}{p_{i}:A_{i}}$, $\mathsf{dom}\left({\theta_{i}}\right)=\mathsf{fm}\!\left({p_{i}}\right)$ and ${\Gamma,\theta_{i}}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s_{i}:B_{i}}$ for every $i\in 1..n$. Then, by inductive hypothesis, ${\Gamma,\theta_{i}}\vdash{s_{i}:B_{i}}$ and, by (t-subs), ${\Gamma,\theta_{i}}\vdash{s_{i}:{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}$ for each $i\in 1..n$. Finally we conclude with (t-abs).

• •

(t-app-al): then $A={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}$ and we have ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r:A^{\prime}}$ and ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{u:C}$ with $A^{\prime}\simeq_{\mu}{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{({A_{i}}\supset{B_{i}})}$, $A_{i}\neq\oplus$ and $C\preceq_{\mu}A_{i}$ for every $i\in i..n$. From ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r:A^{\prime}}$, by inductive hypothesis, we have ${\Gamma}\vdash{r:A^{\prime}}$. Moreover, from $A^{\prime}\simeq_{\mu}{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{({A_{i}}\supset{B_{i}})}$ with (s-eq) and (t-subs), we get ${\Gamma}\vdash{r:{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{({A_{i}}\supset{B_{i}})}}$. By (t-subs) once again, we deduce

[TABLE]

Now, from $C\preceq_{\mu}A_{i}$ we get ${A_{i}}\supset{{{\oplus}}_{\begin{subarray}{c}j\in 1..n\end{subarray}}{B_{j}}}\preceq_{\mu}{C}\supset{{{\oplus}}_{\begin{subarray}{c}j\in 1..n\end{subarray}}{B_{j}}}$ for every $i\in 1..n$, and therefore

[TABLE]

From this and (15) we deduce ${\Gamma}\vdash{r:{C}\supset{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}}$ using (t-subs). Finally, from ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{u:C}$ and the inductive hypothesis we have ${\Gamma}\vdash{u:C}$, thus we conclude by applying (t-app), ${\Gamma}\vdash{{r}\,{u}:{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}$. 2. (2)

By induction on ${\Gamma}\vdash{s:A}$ analyzing the last rule applied.

• •

(t-var), (t-const) and (t-comp) are immediate.

• •

(t-abs): then $A={{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{B}$ and, by hypothesis of the rule, we have $\left[{p_{i}:A_{i}}\right]_{i\in 1..n}$ compatible, ${\theta_{i}}\vdash_{\mathsf{p}}{p_{i}:A_{i}}$, $\mathsf{dom}\left({\theta_{i}}\right)=\mathsf{fm}\!\left({p_{i}}\right)$, ${\Gamma,\theta_{i}}\vdash{s_{i}:B}$ for every $i\in 1..n$. Then, by inductive hypothesis, $\exists B_{i}$ such that $B_{i}\preceq_{\mu}B$ and ${\Gamma,\theta_{i}}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s_{i}:B_{i}}$ for each $i\in 1..n$. Finally we conclude by applying (t-abs-al), assigning $s$ the type ${{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}$. Note that ${{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}\preceq_{\mu}B$ and thus we have ${{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{B_{i}}}\preceq_{\mu}{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{B}=A$.

• •

(t-app): then ${\Gamma}\vdash{r:{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{A}}$ and ${\Gamma}\vdash{u:A_{k}}$ for some $k\in 1..n$. By inductive hypothesis we have ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{r:B}$ with $B\preceq_{\mu}{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{A}$. Without loss of generality we can assume $B={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}$ with $B_{j}\neq\oplus$. Moreover, by contractiveness, we can further assume that $B\simeq_{\mu}{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}$ and $B_{j}\neq\mu,\oplus$ for every $j\in 1..m$.

By Prop. 3.15, from (s-union-l-al) we get $B_{j}\preceq_{\mu}{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}}\supset{A}$ for every $j\in 1..m$. Moreover, since $B_{j}\neq\mu,\oplus$ it can only be the case of (s-func-al) thus, by Prop. 3.15 once again, we have $B_{j}={B^{\prime}_{j}}\supset{B^{\prime\prime}_{j}}$ with

[TABLE]

for every $j\in 1..m$. Once again, by contractiveness we can assume $B^{\prime}_{j}\neq\mu$. Resorting to the maximal union type notation once again, we can assume w.l.o.g that ${{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A_{i}}={{\oplus}}_{\begin{subarray}{c}i\in 1..n^{\prime}\end{subarray}}{A^{\prime}_{i}}$ such that $A_{k}={{\oplus}}_{\begin{subarray}{c}i\in I_{k}\end{subarray}}{A^{\prime}_{i}}$ with $I_{k}\subseteq 1..n^{\prime}$ and $A^{\prime}_{i}\neq\oplus$ for every $i\in 1..n^{\prime}$. Then, by Prop. 3.15 and (s-union-l-al), from (16-left) we get $A^{\prime}_{i}\preceq_{\mu}B^{\prime}_{j}$ for every $i\in 1..n^{\prime}$. Hence, from $I_{k}\subseteq 1..n^{\prime}$ we deduce

[TABLE]

for every $j\in 1..m$. By inductive hypothesis from ${\Gamma}\vdash{u:A_{k}}$ we get $\exists C$ such that $C\preceq_{\mu}A_{k}$ and ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{u:C}$. Then, from (17) we deduce $C\preceq_{\mu}B^{\prime}_{j}$ for every $j\in 1..m$ by transitivity of subtyping. Finally, from (16-right) we get ${{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B^{\prime\prime}_{j}}\preceq_{\mu}A$ and we conclude with (t-app-al) since $B\simeq_{\mu}{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{B_{j}}={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{({B^{\prime}_{j}}\supset{B^{\prime\prime}_{j}})}$.

• •

(t-subs): here we have ${\Gamma}\vdash{s:B}$ with $B\preceq_{\mu}A$. By inductive hypothesis we get ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A^{\prime}}$ with $A^{\prime}\preceq B$ and we conclude by transitivity of subtyping.

From this we may obtain a simple type-checking function $\mathsf{tc}({\Gamma},{s})$ (Fig. 9-top) such that $\mathsf{tc}({\Gamma},{s})=A$ iff ${\Gamma}\mathrel{\leavevmode\resizebox{6.88889pt}{3.44444pt}{ \leavevmode\hbox to6.09pt{\vbox to0.4pt{\pgfpicture\makeatletter\hbox{\hskip 0.2pt\lower-0.2pt\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\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{}{{}}{} {}{}{}{}{}{}{{}}{}{}{}{{}}\pgfsys@moveto{0.29999pt}{0.0pt}\pgfsys@lineto{5.23047pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{0.29999pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.23047pt}{0.0pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} } \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}}{s:A^{\prime}}$, for some $A^{\prime}\simeq_{\mu}A$. The interesting clause is that of application, where the decision of whether (t-comp-al) or (t-app-al) may be applied depends on the result of the recursive call. If the term $r$ is assigned a datatype, then a new compound datatype is built; if its type can be rewritten as a union of functional types, then a proper type is constructed with each of the codomains of the latter, as established in rule (t-app-al).

Compatibility between branches is verified by checking if ${\cal P}_{\mathsf{comp}}\!\left({{p:A}},{{q:B}}\right)$ holds:

\begin{array}[]{rcl}\mathsf{compatible}({{p:A}},{{q:B}})&\triangleq&(\mathtt{not}\ \mathsf{pcomp}({{p:A}},{{q:B}}))\mathbin{\mathtt{or}}\mathsf{subtype}({\varnothing},{B},{A})\end{array}

In $\mathsf{pcomp}$ we may assume that it has already been checked that $p$ has type $A$ and $q$ has type $B$. Therefore, if these are compound patterns they can only be assigned application types, and union types may only appear at leaf positions of a pattern. We use this correspondence to traverse both pattern and type simultaneously in linear time, which means the worst-case execution time of the compatibility check is governed by the complexity of subtyping.

[TABLE]

The expression $\mathsf{unfold}({A})$, in the clause defining $\mathsf{tc}({\Gamma},{{r}\,{u}})$, is the result of unfolding type $A$ using rules (e-rec-l-al) and (e-rec-r-al) until the result is an equivalent type $A^{\prime}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{A^{\prime}_{i}}$ with $A^{\prime}_{i}\neq\mu,\oplus$, and then simply verifying that $A^{\prime}_{i}=\mathbin{\supset}$ for all $i\in 1..n$.

[TABLE]

Termination is guaranteed by contractiveness of $\mu$-types. In the worst case it requires exponential time due to the need to unfold types until the desired equivalent form is obtained (e.g. $\mu{X_{1}}.{\ldots\mu{X_{n}}.{{X_{1}}\supset{\ldots{X_{n}}\supset{\mathbb{c}}}}}$).

5. Towards Efficient Type-Checking

The algorithms presented so far are clear but inefficient. The number of recursive calls in $\mathsf{eqtype}$ and $\mathsf{subtype}$ is not bounded (it depends on the size of the type) and unfolding recursive types may increment their size exponentially. This section draws from ideas in [13, 16, 7] and adopts a dag-representation of recursive types which are encoded as term automata (described below). Associativity is handled by resorting to $n$-ary unions, commutativity and idempotence of $\oplus$ is handled by how types are decomposed in their automaton representation (cf. $\mathsf{check}$ in Fig. 13). The algorithm itself is $\mathsf{tc}$ of Fig. 9 except that:

1. (1)

The representation of $\mu$-types are now term automata. This renders $\mathsf{unfold}$ linear. 2. (2)

The subtyping algorithm is optimized, based on the new representation and following ideas from [16, 7].

The end product is an algorithm with complexity ${\mathcal{O}}(n^{7}d)$ where $n$ is the size of the input (*i.e. *that of $\Gamma$ plus $t$) and $d$ is the maximum arity of the $n$-unions occurring in $\Gamma$ and $t$. Note that all the information needed to type $t$ is either in the context or annotated within the term itself. Thus, a linear relation can be established between the size of the input and the size of the resulting type; and we can think of $n$ as the size of the latter.

5.1. Term Automata

$\mu$-types may be understood as finite dags since their infinite unfolding produce a regular (infinite) trees. We further simplify the types whose dags we consider by flattening the union type constructor and switching to an alphabet where unions are $n$-ary: $\mathfrak{L^{n}}\triangleq\left\{{a^{0}\mathrel{|}a\in\mathcal{V}\cup\mathcal{C}}\right\}\cup\left\{{\mathrel{@}^{2},\supset^{2}}\right\}\cup\left\{{\oplus^{n}\mathrel{|}n>1}\right\}$ and we let $\mathfrak{T}^{\mathfrak{n}}$ stand for possibly infinite trees whose nodes are symbols in $\mathfrak{L^{n}}$. $\mu$-types may be interpreted in $\mathfrak{T}^{\mathfrak{n}}$ simply by unfolding and then considering maximal union types as their underlying $n$-ary union types. We do so by resorting to our previous interpretation of $\mu$-types over $\mathfrak{T}$ and the following translation.

Definition 5.1**.**

The function $\llbracket{\bullet}\rrbracket^{\mathfrak{n}}:\mathfrak{T}\to\mathfrak{T}^{\mathfrak{n}}$ is defined inductively as follows:

[TABLE]

Types in $\mathfrak{T}^{\mathfrak{n}}$ may be represented as term automata [1].

Definition 5.2**.**

A term automaton is a tuple ${\cal M}=\langle Q,\Sigma,q_{0},\delta,l\rangle$ where:

1. (1)

$Q$* is a finite set of states.* 2. (2)

$\Sigma$* is an alphabet where each symbol has an associated arity.* 3. (3)

$q_{0}$* is the initial state.* 4. (4)

$\delta:Q\times\mathbb{N}\to Q$* is a partial transition function between states, defined over $1..k$, where $k$ is the arity of the symbol associated by $\ell$ to the origin state.* 5. (5)

$\ell:Q\to\Sigma$* is a total function that associates a symbol in $\Sigma$ to each state.*

We write ${\cal M}_{A}$ for the automaton associated to type $A$. ${\cal M}_{A}$ recognizes all paths from the root of $A$ to any of its sub-expressions. Fig. 10 illustrates an example type, namely $\mathsf{List}_{A}=\mu{\alpha}.{{\mathbb{nil}}\oplus{({{\mathbb{cons}}\mathrel{@}{A}}\mathrel{@}{\alpha})}}$, represented as an infinite tree and as a term automaton ${\cal M}_{\mathsf{List}_{A}}$. If $q_{0}$ is the initial state of ${\cal M}_{\mathsf{List}_{A}}$ and $\widehat{\delta}$ denotes the natural extension of $\delta$ to sequences of symbols, then $\ell(\widehat{\delta}(q_{0},211))=\mathbb{cons}$. As mentioned, the regular structure of trees arising from types yields automata with a finite number of states.

5.2. Subtyping and Subtype Checking

We next present a coinductive notion of subtyping over $\mathfrak{T}^{\mathfrak{n}}$. It is a binary relation $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{{\cal R}}$ up-to a set of hypothesis ${\cal R}$ (Fig. 11). For ${\cal R}=\varnothing$, $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{{\cal R}}$ coincides with $\preceq_{\mu}$, modulo the proper translation.

Proposition 5.3**.**

$A\preceq_{\mu}B$* iff $\llbracket{\llbracket{A}\rrbracket^{\mathfrak{T}}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\llbracket{B}\rrbracket^{\mathfrak{T}}}\rrbracket^{\mathfrak{n}}$.*

So we can use $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}$ to determine whether types are related via $\preceq_{\mu}$: take two types, construct their automaton representation and check whether these are related via $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}$. Moreover, our formulation of $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{{\cal R}}$ will prove convenient for proving correctness of our subtyping algorithm.

The proof of Prop. 5.3 resorts to Prop. 3.16 and 5.4 below.

Proposition 5.4**.**

$\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$* iff $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$.*

Proof 5.5**.**

$\Rightarrow)$* We prove this part by showing that ${\cal R}\triangleq\left\{{\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\mathrel{|}\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}}\right\}$ is $\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$-dense. We proceed by analyzing the shape of any possible element of ${\cal R}$.*

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{a},{a}\rangle$. Then $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\in\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}({\cal R})$.

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\mathscr{T}^{\prime}}\mathrel{@}{\mathscr{T}^{\prime\prime}}},{{\mathscr{S}^{\prime}}\mathrel{@}{\mathscr{S}^{\prime\prime}}}\rangle$. Note that the translation of a type in $\mathfrak{T}$ can only have symbol $\mathrel{@}$ at the root if the original type already does. Then, we know that $\mathscr{A}$ must be of the form ${\mathscr{D}}\mathrel{@}{\mathscr{A}^{\prime}}$, where $\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime}$ and $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime\prime}$. Similarly, we have $\mathscr{B}={\mathscr{D}^{\prime}}\mathrel{@}{\mathscr{B}^{\prime}}$ with $\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime}$ and $\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime\prime}$.

By definition of ${\cal R}$ we have $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$, and by rule (s-comp-t) both $\mathscr{D}\preceq_{\mathfrak{T}}\mathscr{D}^{\prime}$ and $\mathscr{A}^{\prime}\preceq_{\mathfrak{T}}\mathscr{B}^{\prime}$ hold. Then $\langle{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle,\langle{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$. Thus, $\langle{{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}}\rangle\in\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}({\cal R})$. Finally, by Def. 5.1, we have

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\mathscr{T}^{\prime}}\supset{\mathscr{T}^{\prime\prime}}},{{\mathscr{S}^{\prime}}\supset{\mathscr{S}^{\prime\prime}}}\rangle$. Similarly to the previous case, by Def. 5.1, we have $\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{A}^{\prime}}\supset{\mathscr{A}^{\prime\prime}}},{{\mathscr{B}^{\prime}}\supset{\mathscr{B}^{\prime\prime}}}\rangle$ with $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime}$, $\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime\prime}$, $\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime}$ and $\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime\prime}$. Then, from $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$ we get $\langle{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle,\langle{\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ and thus

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{{\oplus}}^{n}_{i}{\mathscr{T}_{i}}},{\mathscr{S}}\rangle$* with $\mathscr{S}\neq\oplus$. A tree of the form ${{\oplus}}^{n}_{i}{\mathscr{T}_{i}}$ can only result from translating a maximal union of $n>1$ elements, thus $\mathscr{A}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}$ where $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}=\mathscr{T}_{i}$. On the other hand, $\mathscr{S}\neq\oplus$ implies $\mathscr{B}\neq\oplus$. From $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$, by (s-union-t), we know $\mathscr{A}_{i}\preceq_{\mathfrak{T}}\mathscr{B}$ for every $i\in 1..n$. Thus, $\langle{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ for every $i\in 1..n$ and we conclude*

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{\mathscr{T}},{{{\oplus}}^{m}_{j}{\mathscr{S}_{j}}}\rangle$* with $\mathscr{T}\neq\oplus$. This case is similar to the previous one. We have $\mathscr{A}\neq\oplus$ and $\mathscr{B}={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}$ with $m>1$ and $\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}=\mathscr{S}_{j}$. From $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$ we know there exists $k\in 1..m$ such that $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}_{k}$ by rule (s-union-t). Thus, $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ and we conclude*

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{{\oplus}}^{n}_{i}{\mathscr{T}_{i}}},{{{\oplus}}^{m}_{j}{\mathscr{S}_{j}}}\rangle$. With a similar argument to the two previous cases we have maximal union types $\mathscr{A}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}$ and $\mathscr{B}={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}$ with $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}=\mathscr{T}_{i}$ and $\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}=\mathscr{S}_{j}$. By (s-union-t) once again, from $\mathscr{A}\preceq_{\mathfrak{T}}\mathscr{B}$ we know that there exists a function $f:1..n\to 1..m$ such that $\mathscr{A}_{i}\preceq_{\mathfrak{T}}\mathscr{B}_{f(i)}$ for every $i\in 1..n$. Thus, $\langle{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}_{f(i)}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ and we resort to $\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$ and Def. 5.1 to conclude

[TABLE]

$\Leftarrow)$* Similarly, we define ${\cal R}\triangleq\left\{{\langle{\mathscr{A}},{\mathscr{B}}\rangle\mathrel{|}\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\right\}$ and show that it is $\Phi_{\preceq_{\mathfrak{T}}}$-dense. We proceed my analyzing the shape of $\langle{\mathscr{A}},{\mathscr{B}}\rangle\in R$:*

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{a},{a}\rangle$. Then $\langle{\mathscr{A}},{\mathscr{B}}\rangle\in\Phi_{\preceq_{\mathfrak{T}}}({\cal R})$ trivially.

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{D}}\mathrel{@}{\mathscr{A}^{\prime}}},{{\mathscr{D}^{\prime}}\mathrel{@}{\mathscr{B}^{\prime}}}\rangle$. By Def. 5.1, $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}}\rangle$. Moreover, since $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$, we have $\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}$ and $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}$. Then, $\langle{\mathscr{D}},{\mathscr{D}^{\prime}}\rangle,\langle{\mathscr{A}^{\prime}},{\mathscr{B}^{\prime}}\rangle\in{\cal R}$ and

[TABLE]

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{A}^{\prime}}\supset{\mathscr{A}^{\prime\prime}}},{{\mathscr{B}^{\prime}}\supset{\mathscr{B}^{\prime\prime}}}\rangle$. As in the previous case we resort to Def. 5.1 to get $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}\supset{\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}\supset{\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}}\rangle$. Then, from $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ we get $\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}$ and $\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}$ by (s-func-up). Thus, $\langle{\mathscr{B}^{\prime}},{\mathscr{A}^{\prime}}\rangle,\langle{\mathscr{A}^{\prime\prime}},{\mathscr{B}^{\prime\prime}}\rangle\in{\cal R}$ and

[TABLE]

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}}\rangle$* with $n+m>2$ and $\mathscr{A}_{i},\mathscr{B}_{i}\neq\oplus$. Then we need to distinguish three cases:*

• –

If $m=1$, then $n>1$ and $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{n}_{i}{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}}$. From $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ we have $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ for every $i\in 1..n$, by (s-union-l-up). Then, $\langle{\mathscr{A}_{i}},{\mathscr{B}}\rangle\in{\cal R}$ and by definition of $\Phi_{\preceq_{\mathfrak{T}}}$ we get

[TABLE]

• –

If $n=1$, then $m>1$ and $\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{m}_{j}{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}$. Here, by (s-union-r-up), we have $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}_{k}}\rrbracket^{\mathfrak{n}}$ for some $k\in 1..m$, and thus $\langle{\mathscr{A}},{\mathscr{B}_{k}}\rangle\in{\cal R}$. Finally we conclude

[TABLE]

• –

If $n>1$ and $m>1$, then both $\mathscr{A}$ and $\mathscr{B}$ are maximal union types with at least two elements each. Here it applies (s-union-up) and we have $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{n}_{i}{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}}$, $\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{m}_{j}{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}$, and there exists $f:1..n\to 1..m$ such that $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}_{f(i)}}\rrbracket^{\mathfrak{n}}$. Then, $\langle{\mathscr{A}_{i}},{\mathscr{B}_{f(i)}}\rangle\in{\cal R}$ and we conclude

[TABLE]

5.2.1. Algorithm Description

The algorithm that checks whether types are related by the new subtyping relation builds on ideas from [7]. Our presentation is more general than required for subtyping; this general scheme will also be applicable to type equivalence, as we shall later see. Call $p\in\mathfrak{T}^{\mathfrak{n}}\times\mathfrak{T}^{\mathfrak{n}}$ valid if $p\in\mathbin{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$. The algorithm consists of two phases. The aim of the first one is to construct a set $U\subseteq\mathfrak{T}^{\mathfrak{n}}\times\mathfrak{T}^{\mathfrak{n}}$ that delimits the universe of pairs of types that will later be refined to obtain a set of only valid pairs. It starts off with an initial pair (*cf. *Fig. 12, $\mathsf{buildUniverse}$) and then explores pairs of sub-terms of both types in this pair by decomposing the type constructors (*cf. *Fig. 12, $\mathsf{children}$). Note that, given $p$, the algorithm may add invalid pairs in order to prove the validity of $p$. The second phase shall be in charge of eliminating these invalid pairs. Note that the first phase can easily be adapted to other relations by simply redefining function $\mathsf{children}$.

$U$ may be interpreted as a directed graph where an edge from pair $p$ to $q$ means that $q$ might belong to the support set of $p$ in the final relation $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}$. In this case we say that $p$ is a parent of $q$. Since types could have cycles, a pair may be added to $U$ more than once and hence have more than one parent. Set $u(p)$ to be the incoming degree of $p$, *i.e. *the number of parents.

During the second phase (Fig. 13, $\mathsf{gfp}$) the following sets are maintained, all of which conform a partition of $U$:

• •

$W$: pairs whose validity has yet to be determined

• •

$S$: pairs considered conditionally valid

• •

$F$: invalid pairs

The algorithm repeatedly takes elements in $W$ and, in each iteration, transfers to $S$ the selected pair $p$ if its validity can be proved assuming valid only those pairs which have not been discarded up until now (*i.e. *those in $W\cup S$). Otherwise, $p$ is transferred to $F$ and all of its parents in $S$ need to be reconsidered (their validity up-to $W$ may have changed). Thus these parents are moved back to $W$ (*cf. *Fig. 13, $\mathsf{invalidate}$). Intuitively, $S$ contains elements in $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W}$. The process ends when $W$ is empty. The only aspect of this second phase specific to $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W}$ is function $\mathsf{check}$, which may be redefined to be other suitable up-to relations.

5.2.2. Correctness

It is based on the fact that $S$ may be considered a set of valid pairs assuming the validity of those in $W$. More generally, the following holds:

Proposition 5.6**.**

The algorithm preserves the following invariant:

• •

$\langle{W},{S},{F}\rangle$* is a partition of $U$*

• •

$F$* is composed solely of invalid pairs*

• •

$S\subseteq\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W}}(S)$**

Proof 5.7**.**

The tree conditions clearly hold at the beginning of the second phase, where $W=U$, and both $S$ and $F$ are empty. Moreover, during the process, pairs are transferred between the three sets preserving the first condition.

Notice that, in each iteration, the decision of whether to invalidate a pair $p$ or move it to $S$ is made analyzing if there are enough elements in $S\cup W$ to prove its validity (cf. Fig. 13, $\mathsf{check}$). We show this by analyzing the structure of $p$:

• •

$p=\langle{a},{a}\rangle$*. As we can see in (s-refl-up), the validity of $p$ does not depend on any other pair (i.e. * its support set is empty). As expected, the algorithm transfers $p$ to $S$ directly, without further checks.

• •

$p=\langle{{\mathscr{D}}\mathrel{@}{\mathscr{A}}},{{\mathscr{D}^{\prime}}\mathrel{@}{\mathscr{A}^{\prime}}}\rangle$. By (s-comp-up), $p$ is only valid if $\langle{\mathscr{D}},{\mathscr{D}^{\prime}}\rangle$ and $\langle{\mathscr{A}},{\mathscr{A}^{\prime}}\rangle$ also are. Those are exactly the pairs that are evaluated to decide whether to invalidate $p$ or not.

• •

$p=\langle{{\mathscr{A}}\supset{\mathscr{B}}},{{\mathscr{A}^{\prime}}\supset{\mathscr{B}^{\prime}}}\rangle$. This case corresponds to (s-func-up), $p$ will be moved to $S$ only if $\langle{\mathscr{A}^{\prime}},{\mathscr{A}}\rangle$ and $\langle{\mathscr{B}},{\mathscr{B}^{\prime}}\rangle$ has not been discarded yet.

• •

$p=\langle{{{\oplus}}^{n}_{i}{\mathscr{A}_{i}}},{{{\oplus}}^{m}_{j}{\mathscr{B}_{j}}}\rangle$. Here the algorithm checks if for each $\mathscr{A}_{i}$ there exists $\mathscr{B}_{j}$ not yet invalidated, to continue considering $p$ a valid pair. This is exactly the hypothesis of rule (s-union-up).

• •

$p=\langle{{{\oplus}}^{n}_{i}{\mathscr{A}_{i}}},{\mathscr{B}}\rangle$. Similarly, as indicated in (s-union-l-up), the process checks that no pair $\langle{\mathscr{A}_{i}},{\mathscr{B}}\rangle$ was already invalidated.

• •

$p=\langle{\mathscr{A}},{{{\oplus}}^{m}_{j}{\mathscr{B}_{j}}}\rangle$. Here, by rule (s-union-r-up), it is enough to find a non-invalid pair $\langle{\mathscr{A}},{\mathscr{B}_{j}}\rangle$ to keep $p$ in the set of conditionally valid pairs.

If there is not enough elements in $S\cup W$ to consider $p$ a valid pair, then it is considered invalid and moved to $F$, preserving the second condition of the invariant.

We now check the last condition. We use indexes 0 and 1 to distinguish between the state of the sets at the beginning and end of each iteration respectively. We consider two cases depending on the decision made on $p$:

• •

*If $p$ is moved to $S$ (*i.e. all the necessary elements to prove its validity are in $W_{0}\cup S_{0}$) we have:

[TABLE]

By definition we have $S_{0}\subseteq\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{0}}}(S_{0})$, hence

[TABLE]

Notice that $S_{1}\cup W_{1}=S_{0}\cup W_{0}$. Then, by definition of $\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{{\cal R}}}$ we get $\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{0}}}(S_{0})=\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{1}}}(S_{1})$. Thus,

[TABLE]

The set on the left-hand side is exactly $S_{1}$. Moreover, since the necessary elements to consider $p$ a valid pair are in $S_{1}\cup W_{1}$, we have $p\in\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{1}}}(S_{1})$. Finally, we conclude

[TABLE]

• •

If $p$ is invalidated we have:

[TABLE]

where $Q$ contains the parents of $p$ that belong to $S_{0}$. We proceed to show that $S_{1}\subseteq\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{1}}}(S_{1})$. Assume toward a contradiction that there exists $s\in S_{1}$ such that $s\notin\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{1}}}(S_{1})$. Then $s$ cannot have an empty support set. Moreover, from $S_{1}\subseteq S_{0}$ we know $s\in S_{0}$.

On the other hand, from $s\notin\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{1}}}(S_{1})$ we deduce that there exists an element in the support set of $s$ that is not in $S_{1}\cup W_{1}$ but belongs to $S_{0}\cup W_{0}$, since $S_{0}$ is $\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W_{0}}}(S_{0})$-dense. By the equalities above, the only possible such element is $p$. Thus, $s$ is a parent of $p$. Given that the algorithm moves to $W_{1}$ all the parents of $p$ that belong to $S_{0}$, we should have $s\in W_{1}$. This leads to a contradiction since $s\in S_{1}$ and the sets $W_{1},S_{1},F_{1}$ form a partition of $U$.

The contradiction comes from assuming the existence of such $s$, hence we conclude

[TABLE]

When the main cycle ends we know that $W$ is empty, and therefore that $S\subseteq\Phi_{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}(S)$. The coinduction principle then yields $S\subseteq\mathbin{\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$ (*i.e. * every pair in $S$ is valid) and therefore we are left to verify whether the original pair of types is in $S$ or $F$.

5.2.3. Complexity

The first phase consists of identifying relevant pairs of sub-terms in both types being evaluated. If we call $N$ and $N^{\prime}$ the size of such types (considering nodes and edges in their representations) we have that the size and cost of building the universe $U$ can be bounded by ${\mathcal{O}}(NN^{\prime})$. As we shall see, the total cost of the algorithm is governed by the amount of operations in the second phase.

As stated in [7], since any pair can be invalidated at most once (in which case $u(p)$ nodes are transferred back to $W$ for reconsideration) the amount of iterations in the refinement stage can be bounded by

[TABLE]

Assuming that set operations can be performed in constant time, the cost of evaluating each node in the main loop is that of deciding whether to suspend or invalidate the pair and, in the later case, the cost of the invalidation process. The decision of where to transfer the node is computed in the function $\mathsf{check}$, which always performs a constant amount of operations for pairs of non-union types. The worst case involves checking pairs of the form $\langle{{{\oplus}}^{n}_{i}{A}_{i}},{{{\oplus}}^{m}_{j}{B}_{i}}\rangle$, which can be resolved by maintaining in each node a table indicating, for every $A_{i}$, the amount of pairs $\langle{A_{i}},{B_{j}}\rangle$ that have not yet been invalidated. Using this approach, this check can be performed in ${\mathcal{O}}(d)$ operations, where $d$ is a bound on the size of both unions. Whenever a pair is invalidated, all tables present in its immediate parents are updated as necessary.

Finally we resort to an argument introduced in [7] to argue that the cost of invalidating an element can be seen as ${\mathcal{O}}(1)$: a new iteration will be performed for each of the $u(p)$ pairs added to $W$ when invalidating $p$. Because of this, a more precise bound for the cost of the complete execution of the algorithm can be obtained if we consider the cost of adding each of these elements to $W$ as part of the iteration itself, yielding an amortized cost of ${\mathcal{O}}(d)$ operations for each iteration. This leaves a total cost of ${\mathcal{O}}(size(U)d)$ for the subtyping check, expressed as ${\mathcal{O}}(NN^{\prime}d)$ in terms of the size of the input automata.

Let us call $n$ and $n^{\prime}$ the amount of constructors in types $A$ and $B$, respectively. $N$ and $N^{\prime}$ are the sizes of automata representing these types, and can consequently be bounded by ${\mathcal{O}}(n^{2})$ and ${\mathcal{O}}(n^{\prime 2})$. Therefore, the complexity of the algorithm can be expressed as ${\mathcal{O}}(n^{2}n^{\prime 2}d)$.

5.3. Equivalence Checking

In this section we adapt the previous algorithm to obtain one proper of equivalence checking with the same complexity cost. Fig. 15 introduces an equivalence relation up-to ${\cal R}$ over $\mathfrak{T}^{\mathfrak{n}}$ which can be used to compute $\simeq_{\mu}$ via the translation $\llbracket{\bullet}\rrbracket^{\mathfrak{n}}$.

Proposition 5.8**.**

$A\simeq_{\mu}B$* iff $\llbracket{\llbracket{A}\rrbracket^{\mathfrak{T}}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\llbracket{B}\rrbracket^{\mathfrak{T}}}\rrbracket^{\mathfrak{n}}$.*

As done before for subtyping, we prove this by resorting to Prop. 3.5 and 5.9 below:

Proposition 5.9**.**

$\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$* iff $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$.*

Proof 5.10**.**

$\Rightarrow)$* We prove this part by showing that ${\cal R}\triangleq\left\{{\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\mathrel{|}\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}}\right\}$ is $\Phi_{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$-dense. We proceed by analyzing the shape of any possible element of ${\cal R}$.*

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{a},{a}\rangle$. Then $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\in\Phi_{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}({\cal R})$.

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\mathscr{T}^{\prime}}\mathrel{@}{\mathscr{T}^{\prime\prime}}},{{\mathscr{S}^{\prime}}\mathrel{@}{\mathscr{S}^{\prime\prime}}}\rangle$. Note that the translation of a type in $\mathfrak{T}$ can only have symbol $\mathrel{@}$ at the root if the original type already does. Then, we know that $\mathscr{A}$ must be of the form ${\mathscr{D}}\mathrel{@}{\mathscr{A}^{\prime}}$, where $\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime}$ and $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime\prime}$. Similarly, we have $\mathscr{B}={\mathscr{D}^{\prime}}\mathrel{@}{\mathscr{B}^{\prime}}$ with $\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime}$ and $\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime\prime}$.

By definition of ${\cal R}$ we have $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$, and by rule (e-comp-t) both $\mathscr{D}\simeq_{\mathfrak{T}}\mathscr{D}^{\prime}$ and $\mathscr{A}^{\prime}\simeq_{\mathfrak{T}}\mathscr{B}^{\prime}$ hold. Then $\langle{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle,\langle{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$. Thus, $\langle{{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}}\rangle\in\Phi_{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}({\cal R})$. Finally, by Def. 5.1, we have

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\mathscr{T}^{\prime}}\supset{\mathscr{T}^{\prime\prime}}},{{\mathscr{S}^{\prime}}\supset{\mathscr{S}^{\prime\prime}}}\rangle$. Similarly to the previous case, by Def. 5.1, we have $\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{A}^{\prime}}\supset{\mathscr{A}^{\prime\prime}}},{{\mathscr{B}^{\prime}}\supset{\mathscr{B}^{\prime\prime}}}\rangle$ with $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime}$, $\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{T}^{\prime\prime}$, $\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime}$ and $\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}=\mathscr{S}^{\prime\prime}$. Then, from $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$ we get $\langle{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}\rangle,\langle{\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ and thus

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{{\oplus}}^{n}_{i}{\mathscr{T}_{i}}},{\mathscr{S}}\rangle$* with $\mathscr{S}\neq\oplus$. A tree of the form ${{\oplus}}^{n}_{i}{\mathscr{T}_{i}}$ can only result from translating a maximal union of $n>1$ elements, thus $\mathscr{A}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}$ where $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}=\mathscr{T}_{i}$. On the other hand, $\mathscr{S}\neq\oplus$ implies $\mathscr{B}\neq\oplus$. From $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$, by (e-union-t), we know $\mathscr{A}_{i}\simeq_{\mathfrak{T}}\mathscr{B}$ for every $i\in 1..n$. Thus, $\langle{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ for every $i\in 1..n$ and we conclude*

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{\mathscr{T}},{{{\oplus}}^{m}_{j}{\mathscr{S}_{j}}}\rangle$* with $\mathscr{T}\neq\oplus$. This case is similar to the previous one. We have $\mathscr{A}\neq\oplus$ and $\mathscr{B}={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}$ with $m>1$ and $\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}=\mathscr{S}_{j}$. From $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$ we know, by (e-union-t), that $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}_{j}$ for every $j\in 1..m$. Thus, $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$ and we conclude*

[TABLE]

• •

$\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{{\oplus}}^{n}_{i}{\mathscr{T}_{i}}},{{{\oplus}}^{m}_{j}{\mathscr{S}_{j}}}\rangle$. With a similar argument to the two previous cases we have maximal union types $\mathscr{A}={{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}$ and $\mathscr{B}={{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}$ with $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}=\mathscr{T}_{i}$ and $\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}=\mathscr{S}_{j}$. By (e-union-t) once again, from $\mathscr{A}\simeq_{\mathfrak{T}}\mathscr{B}$ we know that there exists a function

[TABLE]

Thus, $\langle{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}_{f(i)}}\rrbracket^{\mathfrak{n}}}\rangle,\langle{\llbracket{\mathscr{A}_{g(j)}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}\rangle\in{\cal R}$. and we resort to $\Phi_{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$ and Def. 5.1 to conclude

[TABLE]

$\Leftarrow)$* Similarly, we define ${\cal R}\triangleq\left\{{\langle{\mathscr{A}},{\mathscr{B}}\rangle\mathrel{|}\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\right\}$ and show that it is $\Phi_{\simeq_{\mathfrak{T}}}$-dense. We proceed my analyzing the shape of $\langle{\mathscr{A}},{\mathscr{B}}\rangle\in R$:*

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{a},{a}\rangle$. Then $\langle{\mathscr{A}},{\mathscr{B}}\rangle\in\Phi_{\simeq_{\mathfrak{T}}}({\cal R})$ trivially.

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{D}}\mathrel{@}{\mathscr{A}^{\prime}}},{{\mathscr{D}^{\prime}}\mathrel{@}{\mathscr{B}^{\prime}}}\rangle$. By Def 5.1, $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}}\mathrel{@}{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}}\rangle$. Moreover, since $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$, we have $\llbracket{\mathscr{D}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{D}^{\prime}}\rrbracket^{\mathfrak{n}}$ and $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}$. Then $\langle{\mathscr{D}},{\mathscr{D}^{\prime}}\rangle,\langle{\mathscr{A}^{\prime}},{\mathscr{B}^{\prime}}\rangle\in{\cal R}$ and

[TABLE]

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{\mathscr{A}^{\prime}}\supset{\mathscr{A}^{\prime\prime}}},{{\mathscr{B}^{\prime}}\supset{\mathscr{B}^{\prime\prime}}}\rangle$. As in the previous case we resort to Def. 5.1 to get $\langle{\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}},{\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}}\rangle=\langle{{\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}}\supset{\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}},{{\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}}\supset{\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}}}\rangle$. Then, from $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ we get $\llbracket{\mathscr{A}^{\prime}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}^{\prime}}\rrbracket^{\mathfrak{n}}$ and $\llbracket{\mathscr{A}^{\prime\prime}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}^{\prime\prime}}\rrbracket^{\mathfrak{n}}$, by (e-func-up). Thus, $\langle{\mathscr{A}^{\prime}},{\mathscr{B}^{\prime}}\rangle,\langle{\mathscr{A}^{\prime\prime}},{\mathscr{B}^{\prime\prime}}\rangle\in{\cal R}$ and

[TABLE]

• •

$\langle{\mathscr{A}},{\mathscr{B}}\rangle=\langle{{{\oplus}}_{\begin{subarray}{c}i\in 1..n\end{subarray}}{\mathscr{A}_{i}}},{{{\oplus}}_{\begin{subarray}{c}j\in 1..m\end{subarray}}{\mathscr{B}_{j}}}\rangle$* with $n+m>2$ and $\mathscr{A}_{i},\mathscr{B}_{i}\neq\oplus$. Then we need to distinguish three cases:*

• –

If $m=1$, then $n>1$ and $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{n}_{i}{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}}$. From $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ we have $\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}$ for every $i\in 1..n$, by (e-union-l-up). Then, $\langle{\mathscr{A}_{i}},{\mathscr{B}}\rangle\in{\cal R}$. and by definition of $\Phi_{\simeq_{\mathfrak{T}}}$ we get

[TABLE]

• –

If $n=1$, then $m>1$ and $\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{m}_{j}{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}$. Here, by (e-union-r-up), we have $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}$ for every $j\in 1..m$, and thus $\langle{\mathscr{A}},{\mathscr{B}_{j}}\rangle\in{\cal R}$. Finally we conclude

[TABLE]

• –

If $n>1$ and $m>1$, then both $\mathscr{A}$ and $\mathscr{B}$ are maximal union types with at least two elements each. Here it applies (e-union-up) and we have $\llbracket{\mathscr{A}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{n}_{i}{\llbracket{\mathscr{A}_{i}}\rrbracket^{\mathfrak{n}}}$, $\llbracket{\mathscr{B}}\rrbracket^{\mathfrak{n}}={{\oplus}}^{m}_{j}{\llbracket{\mathscr{B}_{j}}\rrbracket^{\mathfrak{n}}}$, and there exists

[TABLE]

Then, $\langle{\mathscr{A}_{i}},{\mathscr{B}_{f(i)}}\rangle,\langle{\mathscr{A}_{g(j)}},{\mathscr{B}_{j}}\rangle\in{\cal R}$ and we conclude

[TABLE]

The algorithm is the result of adapting the scheme presented for subtyping to the new relation $\preceq_{\vec{\mu}}{{\cal R}}$. This is done by redefining functions $\mathsf{children}$ and $\mathsf{check}$ from the first and second phase respectively (*cf. *Fig. 16). For the former the only difference is on rule (e-func-up), where we need to add pair $\langle{\mathscr{A}^{\prime}},{\mathscr{B}^{\prime}}\rangle$ instead of $\langle{\mathscr{B}^{\prime}},{\mathscr{A}^{\prime}}\rangle$, added for subtyping. We could have omitted this by using the same rule for functional types as before and resorting to the symmetry of the resulting relation (which does not depend on this rule), but we wanted to emphasize the fact that phase one can easily be adapted if needed. For the refinement phase we need to properly check the premises of rules (e-union-up) and (e-union-r-up), while the others remain the same.

With these considerations is easy to see that, in each iteration, $S$ consists of pairs in the relation $\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{W}$, getting $S\subseteq\mathbin{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{\varnothing}}$ at the end of the process.

Proposition 5.11**.**

The algorithm preserves the following invariant:

• •

$\langle{W},{S},{F}\rangle$* is a partition of $U$*

• •

$F$* is composed solely of invalid pairs*

• •

$S\subseteq\Phi_{\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{W}}(S)$**

Proof 5.12**.**

Analysis here is exactly the same as the case for subtyping. The only difference is when proving the second condition. For that, we just need to make sure that pairs are considered valid according to the rules of Fig.15. We present next the cases that differ between $\preceq_{\mathfrak{T}^{\mathfrak{n}}}^{W}$ and $\simeq_{\mathfrak{T}^{\mathfrak{n}}}^{W}$:

• •

$p=\langle{{\mathscr{A}}\supset{\mathscr{B}}},{{\mathscr{A}^{\prime}}\supset{\mathscr{B}^{\prime}}}\rangle$*. This case corresponds to (e-func-up). Here the algorithm checks for $\langle{\mathscr{A}},{\mathscr{A}^{\prime}}\rangle$ instead of $\langle{\mathscr{A}^{\prime}},{\mathscr{A}}\rangle$. That is the reason why $\mathsf{children}$ was redefined (*cf. Fig. 16).

• •

$p=\langle{{{\oplus}}^{n}_{i}{\mathscr{A}_{i}}},{{{\oplus}}^{m}_{j}{\mathscr{B}_{j}}}\rangle$. In the case of subtyping, the algorithm checks if for each $\mathscr{A}_{i}$ there exists $\mathscr{B}_{j}$ not yet invalidated, to assure the existence of $f$ (cf. (s-union-up)). Here it extends the check to verify that for each $\mathscr{B}_{j}$ there is a $\mathscr{A}_{i}$ not yet invalidating, thus assuring the existence of $g$ too (cf. (e-union-up)).

• •

$p=\langle{\mathscr{A}},{{{\oplus}}^{m}_{j}{\mathscr{B}_{j}}}\rangle$. Here, by rule (e-union-r-up), there must be a pair $\langle{\mathscr{A}},{\mathscr{B}_{j}}\rangle$ in $S\cup W$ for each $j\in 1..m$, to keep $p$ in the set of conditionally valid pairs.

For the complexity analysis, notice that the size of the built universe is the same as before and phase one is governed by phase two, which has at most ${\mathcal{O}}(NN^{\prime})$ iterations. For the cost of each iteration it is enough to analyze the complexity of $\mathsf{check}$, since the rest of the scheme remains the same. As we remarked before, the only difference in $\mathsf{check}$ between subtyping and equality is in the cases involving unions. Here the worst case is when checking rule (e-union-up) that requires the existence of two functions $f$ and $g$ relating elements of each type. This can be done in linear time by maintaining tables with the count of non-invalidated pairs of descendants, as indicated in Sec. 5.2.3. Thus, the cost of an iteration is ${\mathcal{O}}(d)$, resulting in an overall cost of ${\mathcal{O}}(NN^{\prime}d)$ as before.

5.4. Type Checking

Let us revisit type-checking ($\mathsf{tc}$). As already discussed, it linearly traverses the input term, the most costly operations being those that deal with application and abstraction. These cases involve calling $\mathsf{subtype}$. Notice that these calls do not depend directly on the input to $\mathsf{tc}$. However, a linear correspondence can be established between the size of the types being considered in $\mathsf{subtype}$ and the input to the algorithm, since such expressions are built from elements of $\Gamma$ (the input context) or from annotations in the input term itself. Consider for instance $\mathsf{subtype}({\varnothing},{A},{B})$ with $a$ and $b$ the size of each type resp. This has complexity ${\mathcal{O}}(a^{2}b^{2}d)$ and, from the discussion above, we can refer to it as ${\mathcal{O}}(n^{4}d)$, where $n$ is the size of the input to $\mathsf{tc}$ (*i.e. *that of $\Gamma$ plus $t$). Similarly, we may say that $\mathsf{unfold}$ is linear in $n$.

We now analyze the application and abstraction cases of the algorithm in detail:

**Application: **

First it performs a linear check on the type to verify if it is a datatype. If so it returns. Otherwise, a second linear check is required ($\mathsf{unfold}$) in order to then perform as many calls to $\mathsf{subtype}$ as elements there are in the union of the functional types. This yields a local complexity of ${\mathcal{O}}(n^{4}d^{2})$.

**Abstraction: **

First there are as many calls to $\mathsf{tcp}$ (the algorithm for type-checking patterns) as branches the abstraction has. Note that $\mathsf{tcp}$ has linear complexity in the size of its input and this call is instantiated with arguments $p_{i}$ and $\theta_{i}$ which occur in the original term. All these calls, taken together, may thus be considered to have linear time complexity with respect to the input of $\mathsf{tcp}$. Then it is necessary to perform a quadratic number (in the number of branches) of checks on compatibility. We have already analyzed that compatibility in the worst case involves checking subtyping. If we assume a linear number of branches w.r.t. the input, we obtain a total complexity of ${\mathcal{O}}(n^{6}d)$ for this case.

Finally, the total complexity of $\mathsf{tc}$ is governed by the case of the abstraction, and is therefore ${\mathcal{O}}(n^{7}d)$.

5.5. Prototype implementation

A prototype in Scala is available [10]. It implements $\mathsf{tc}$ but resorts to the efficient algorithm for subtyping and type equivalence described above. It also includes further optimizations. For example, following a suggestion in [7], the order in which elements in $W$ are selected for evaluation relies on detecting strongly connected components, using Tarjan’s [9] algorithm of linear cost and topologically sorting them in reverse order. In the absence of cycles this results in evaluating every pair only after all its children have already been considered. For cyclic types pairs for which no order can be determined are encapsulated within the same strongly connected component.

6. Conclusions

We address efficient type-checking for path polymorphism. We start off with the type system of [19] which includes singleton types, union types, type application and recursive types. The union type constructor is assumed associative, commutative and idempotent. First we formulate a syntax-directed presentation. Then we devise invertible coinductive presentations of type-equivalence and subtyping. This yields a naïve but correct type-checking algorithm. However, it proves to be inefficient (exponential in the size of the type). This prompts us to change the representation of type expressions and use automata techniques to considerably improve the efficiency. Indeed, the final algorithm has complexity ${\mathcal{O}}(n^{7}d)$ where $n$ is the size of the input and $d$ is the maximum arity of the unions occurring in it.

Regarding future work an outline of possible avenues follows. These are aimed at enhancing the expressiveness of CAP itself and then adapting the techniques presented here to obtain efficient type checking algorithms.

• •

Addition of parametric polymorphism (presumably in the style of F*<:* [5, 17, 6]). We believe this should not present major difficulties.

• •

Strong normalization requires devising a notion of positive/negative occurrence in the presence of strong $\mu$-type equality, which is known not to be obvious [2, page 515].

• •

A more ambitious extension is that of dynamic patterns, namely patterns that may be computed at run-time, PPC being the prime example of a calculus supporting this feature.