Factoring Derivation Spaces via Intersection Types (Extended Version)

TL;DR

This paper introduces a confluent non-idempotent intersection type system for lambda-calculus that enables unique factorization of derivation spaces into garbage-free and garbage parts, improving understanding of resource usage.

Contribution

It presents a novel confluent intersection type system with proof term syntax, establishing a unique factorization of derivation spaces using a Grothendieck construction.

Findings

The system enjoys subject reduction and strong normalization.

Derivation spaces can be uniquely factorized into garbage-free and garbage parts.

A correspondence with lambda-calculus via simulation theorems is established.

Abstract

In typical non-idempotent intersection type systems, proof normalization is not confluent. In this paper we introduce a confluent non-idempotent intersection type system for the lambda-calculus. Typing derivations are presented using proof term syntax. The system enjoys good properties: subject reduction, strong normalization, and a very regular theory of residuals. A correspondence with the lambda-calculus is established by simulation theorems. The machinery of non-idempotent intersection types allows us to track the usage of resources required to obtain an answer. In particular, it induces a notion of garbage: a computation is garbage if it does not contribute to obtaining an answer. Using these notions, we show that the derivation space of a lambda-term may be factorized using a variant of the Grothendieck construction for semilattices. This means, in particular, that any derivation in the lambda-calculus can be uniquely written as a garbage-free prefix followed by garbage.

Equations

$$(1+1,2\ast 3+1)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$(\lambda x.xx)(Kz)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{array}[]{rcl@{\hspace{2cm}}rcl}\mathcal{A}&::=&\alpha\ \mid\ \mathcal{M}\to\mathcal{A}\hfil\hskip 56.9055pt&\mathcal{M}&::=&[\mathcal{A}_{i}]_{i=1}^{n}\hskip 14.22636pt\text{with $n\geq 0$}\\ \end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 19.57188pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=39.14377pt\hbox{\kern 2.70003pt$\texttt{{var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x:[\mathcal{A}]\vdash\mathcal{A}$}}}}\end{array}\hskip 4.26773pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\oplus(x:\mathcal{M})\vdash t:\mathcal{A}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=67.51881pt\hbox{\kern 2.70003pt$\texttt{{lam}}$}}}\hbox{\kern 4.62498pt\hbox{$\displaystyle\Gamma\vdash\lambda x.t:\mathcal{M}\to\mathcal{A}$}}}}\end{array}\hskip 4.26773pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:[\mathcal{B}_{i}]_{i=1}^{n}\to\mathcal{A}\hskip 14.22636pt(\Delta_{i}\vdash s:\mathcal{B}_{i})_{i=1}^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=123.38196pt\hbox{\kern 2.70003pt$\texttt{{app}}$}}}\hbox{\kern 32.31273pt\hbox{$\displaystyle\Gamma+_{i=1}^{n}\Delta_{i}\vdash t\,s:\mathcal{A}$}}}}\end{array}$$

$${\small\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 52.99901pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=105.99802pt\hbox{\kern 2.70003pt$\texttt{{var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x:[\alpha,\alpha]\to\beta\vdash x:[\alpha,\alpha]\to\beta$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}\begin{array}[]{c}\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 26.15106pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=52.30212pt\hbox{\kern 2.70003pt$\texttt{{var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x:[\alpha]\vdash x:\alpha$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}\begin{array}[]{c}\hskip 4.5pt plus 1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 26.15106pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=52.30212pt\hbox{\kern 2.70003pt$\texttt{{var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x:[\alpha]\vdash x:\alpha$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}\vspace{.1cm}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=369.81819pt\hbox{\kern 2.70003pt$\texttt{{app}}$}}}\hbox{\kern 132.08821pt\hbox{$\displaystyle x:[[\alpha,\alpha]\to\beta,\alpha,\alpha]\vdash xx:\beta$}}}}\hskip 4.5pt plus 1.0fil\penalty 2\end{array}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.225pt,depth=0.225pt,width=425.11517pt\hbox{\kern 2.70003pt$\texttt{{lam}}$}}}\hbox{\kern 154.1117pt\hbox{$\displaystyle\vdash\lambda x.xx:[[\alpha,\alpha]\to\beta,\alpha,\alpha]\to\beta$}}}}\end{array}}$$

$$(\lambda x.y^{[\alpha ]\to [\alpha ]\to \beta }[x^{\alpha }][x^{\alpha }])[z^{[\gamma ]\to \alpha }[z^{\gamma }],z^{[]\to \alpha }[]]$$

$${\small\begin{array}[]{|c|c|c|}\hline\cr\begin{array}[]{r@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l}\epsilon\,\rho\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\rho\\ \rho\,\epsilon\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\rho\\ \epsilon/\rho\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\epsilon\\ \rho/\epsilon\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\rho\\ \rho/\sigma\tau\hskip 2.84544pt&=\hfil\hskip 2.84544pt&(\rho/\sigma)/\tau\\ \rho\sigma/\tau\hskip 2.84544pt&=\hfil\hskip 2.84544pt&(\rho/\tau)(\sigma/(\tau/\rho))\\ \rho/\rho\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\epsilon\end{array}&\begin{array}[]{r@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l}\rho\sqsubseteq\sigma\hskip 2.84544pt&\overset{\mathrm{def}}{\iff}\hfil\hskip 2.84544pt&\rho/\sigma=\epsilon\\ \rho\equiv\sigma\hskip 2.84544pt&\overset{\mathrm{def}}{\iff}\hfil\hskip 2.84544pt&\rho\sqsubseteq\sigma\land\sigma\sqsubseteq\rho\\ \rho\sqcup\sigma\hskip 2.84544pt&\overset{\mathrm{def}}{=}\hfil\hskip 2.84544pt&\rho(\sigma/\rho)\\ \rho\equiv\sigma\hskip 2.84544pt&\implies\hfil\hskip 2.84544pt&\tau/\rho=\tau/\sigma\\ \rho\sqsubseteq\sigma\hskip 2.84544pt&\iff\hfil\hskip 2.84544pt&\exists\tau.\ \rho\tau\equiv\sigma\\ \rho\sqsubseteq\sigma\hskip 2.84544pt&\iff\hfil\hskip 2.84544pt&\rho\sqcup\sigma\equiv\sigma\end{array}&\begin{array}[]{r@{\hspace{0.1cm}}c@{\hspace{0.1cm}}l}\rho\sqsubseteq\sigma\hskip 2.84544pt&\implies\hfil\hskip 2.84544pt&\rho/\tau\sqsubseteq\sigma/\tau\\ \rho\sqsubseteq\sigma\hskip 2.84544pt&\iff\hfil\hskip 2.84544pt&\tau\rho\sqsubseteq\tau\sigma\\ \rho\sqcup\sigma\hskip 2.84544pt&\equiv\hfil\hskip 2.84544pt&\sigma\sqcup\rho\\ (\rho\sqcup\sigma)\sqcup\tau\hskip 2.84544pt&=\hfil\hskip 2.84544pt&\rho\sqcup(\sigma\sqcup\tau)\\ \rho\hskip 2.84544pt&\sqsubseteq\hfil\hskip 2.84544pt&\rho\sqcup\sigma\\ (\rho\sqcup\sigma)/\tau\hskip 2.84544pt&=\hfil\hskip 2.84544pt&(\rho/\tau)\sqcup(\sigma/\tau)\\ \end{array}\\ \hline\cr\end{array}}$$

$$\begin{array}[]{rcl@{\hspace{2cm}}rcl}\mathcal{A}&::=&\alpha^{\ell}\mid\mathcal{M}\overset{\ell}{\to}\mathcal{A}\hfil\hskip 56.9055pt&\mathcal{M}&::=&[\mathcal{A}_{i}]_{i=1}^{n}\hskip 14.22636pt\text{with $n\geq 0$}\\ \end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 29.48183pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=58.96365pt\hbox{\kern 3.00003pt$\texttt{{var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x:[\mathcal{A}]\vdash x^{\mathcal{A}}:\mathcal{A}$}}}}\end{array}\hskip 14.22636pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\oplus(x:\mathcal{M})\vdash t:\mathcal{B}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=74.60391pt\hbox{\kern 3.00003pt$\texttt{{lam}}$}}}\hbox{\kern 0.49995pt\hbox{$\displaystyle\Gamma\vdash\lambda^{\ell}x.t:\mathcal{M}\overset{\ell}{\to}\mathcal{B}$}}}}\end{array}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1\Gamma\vdash t:[\mathcal{B}_{1},\ldots,\mathcal{B}_{n}]\overset{\ell}{\to}\mathcal{A}\hskip 14.22636pt\left(\Delta_{i}\vdash s_{i}:\mathcal{B}_{i}\right)_{i=1}^{n}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=156.89214pt\hbox{\kern 3.00003pt$\texttt{{app}}$}}}\hbox{\kern 29.96257pt\hbox{$\displaystyle\Gamma+_{i=1}^{n}\Delta_{i}\vdash t[s_{1},\ldots,s_{n}]:\mathcal{A}$}}}}\end{array}$$

$$\begin{array}[]{rcll}x^{\mathcal{A}}\{x:=[s]\}&\overset{\mathrm{def}}{=}&s\\ y^{\mathcal{A}}\{x:=[]\}&\overset{\mathrm{def}}{=}&y^{\mathcal{A}}&\text{ if $x\neq y$}\\ (\lambda^{\ell}y.u)\{x:=\bar{s}\}&\overset{\mathrm{def}}{=}&\lambda^{\ell}y.u\{x:=\bar{s}\}&\text{ if $x\neq y$ and $y\not\in\mathsf{fv}({\bar{s}})$}\\ u_{0}[u_{j}]_{j=1}^{m}\{x:=\bar{s}\}&\overset{\mathrm{def}}{=}&u_{0}\{x:=\bar{s}_{0}\}[u_{j}\{x:=\bar{s}_{j}\}]_{j=1}^{m}\end{array}$$

$$({\lambda }^{1}x.x^{[{\alpha }^2]\stackrel{3}{\to }{\alpha }^2}[x^{{\alpha }^2}])[I^3,I^4[z^{{\alpha }^2}]]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$({\lambda }^{\ell }x.({\lambda }^{{\ell }^{\prime }}y.u)\bar{r})\bar{s}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$({\lambda }^{\ell }x.t)[{\bar{s}}_1,({\lambda }^{{\ell }^{\prime }}y.u)\bar{r},{\bar{s}}_2]\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 11.70416pt\hbox{$\displaystyle\penalty 1$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=23.40833pt\hbox{\kern 3.00003pt$\texttt{{r-var}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle x^{\mathcal{A}}\mathrel{\ltimes}x$}}}}\end{array}\hskip 14.22636pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 17.15971pt\hbox{$\displaystyle\penalty 1t^{\prime}\mathrel{\ltimes}t$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=50.85945pt\hbox{\kern 3.00003pt$\texttt{{r-lam}}$}}}\hbox{\kern 0.0pt\hbox{$\displaystyle\lambda^{\ell}x.t^{\prime}\mathrel{\ltimes}\lambda x.t$}}}}\end{array}\hskip 14.22636pt\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{$\displaystyle\penalty 1t^{\prime}\mathrel{\ltimes}t\hskip 14.22636pts^{\prime}_{i}\mathrel{\ltimes}s\text{ for all $i=1..n$}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule height=0.25002pt,depth=0.25002pt,width=118.65656pt\hbox{\kern 3.00003pt$\texttt{{r-app}}$}}}\hbox{\kern 38.28056pt\hbox{$\displaystyle t^{\prime}[s^{\prime}_{i}]_{i=1}^{n}\mathrel{\ltimes}ts$}}}}\end{array}$$

$$({\lambda }^{1}x.x^{[]\stackrel{2}{\to }{\alpha }^3}[])[y^{[]\stackrel{2}{\to }{\alpha }^3}]({\lambda }^{1}x.x^{[{\alpha }^2]\stackrel{3}{\to }{\beta }^4}[x^{{\alpha }^2}])[y^{[{\alpha }^2]\stackrel{3}{\to }{\beta }^4},y^{{\alpha }^2}]$$

$$({\lambda }^{1}x.x^{[{\alpha }^2,{\beta }^3]\stackrel{4}{\to }{\gamma }^5}[x^{{\alpha }^2},x^{{\beta }^3}])[y^{[{\alpha }^2,{\beta }^3]\stackrel{4}{\to }{\gamma }^5},y^{{\alpha }^2},y^{{\beta }^3}]$$

$$x((\lambda x.x)y)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$t\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{array}[]{c@{\hspace{.5cm}}c@{\hspace{.5cm}}c@{\hspace{.5cm}}c}\epsilon/t^{\prime}\overset{\mathrm{def}}{=}\epsilon\hfil\hskip 14.22636pt&R\sigma/t^{\prime}\overset{\mathrm{def}}{=}(R/t^{\prime})(\sigma/(t^{\prime}/R))\hfil\hskip 14.22636pt&t^{\prime}/\epsilon\overset{\mathrm{def}}{=}t^{\prime}\hfil\hskip 14.22636pt&t^{\prime}/R\sigma\overset{\mathrm{def}}{=}(t^{\prime}/R)/\sigma\\ \end{array}$$

$$(\lambda x.yxx)(Iz)\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

$$\begin{array}[]{rrlll}\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})&:&\mathcal{G}({[\rho]})&\to&\mathcal{G}({[\sigma]})\\ &&{[\alpha]}&\mapsto&{[\rho\alpha/\sigma]}\end{array}$$

$$\begin{array}[]{rcl}\mathbb{D}^{\lambda}(t)&\to&\int_{\mathcal{F}}{\mathcal{G}}\\ {[\rho]}&\mapsto&({[\rho\Downarrow t^{\prime}]},{[\rho/(\rho\Downarrow t^{\prime})]}\\ \end{array}\hskip 14.22636pt\begin{array}[]{rcl}\int_{\mathcal{F}}{\mathcal{G}}&\to&\mathbb{D}^{\lambda}(t)\\ ({[\rho]},{[\sigma]})&\mapsto&{[\rho\sigma]}\\ \end{array}$$

$$\begin{array}[]{ccc}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 17.16702pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&\\&&\\&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 36.70708pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[\epsilon]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 8.24332pt\raise-14.03781pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 74.90076pt\raise-14.03789pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern 77.99367pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 98.66151pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-11.01286pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[R_{1}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-38.57181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 27.34735pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 27.34735pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[R_{1}S_{21}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 44.51437pt\raise-38.57181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 71.86172pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[S]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 63.32411pt\raise-44.71692pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern-17.16702pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[R_{1}S_{11}]}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 25.70293pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 25.70293pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{{[R_{1}\sqcup S]}}$}}}}}}}\ignorespaces}}}}\ignorespaces&\raisebox{-24.18501pt}{$\simeq$}&\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 28.08543pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern 0.0pt\offinterlineskip\halign{\entry@#!@&&\entry@@#!@\cr&&&\\&&\\&\crcr}}}\ignorespaces{\hbox{\kern-3.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 50.1057pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[\epsilon]},{[\epsilon]})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 14.31702pt\raise-14.03767pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 117.26814pt\raise-14.03618pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern 126.62773pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 158.21399pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern-21.93127pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[R_{1}]},{[\epsilon]})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 0.0pt\raise-38.57181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 42.7755pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 42.7755pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[R_{1}]},{[S_{21}]})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 68.8314pt\raise-38.57181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 109.57738pt\raise-24.5359pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[S]},{[\epsilon]})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}\ignorespaces{}{}{}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}}{\hbox{\kern 101.04211pt\raise-43.73709pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{}{{}}{{}{}{}\lx@xy@spline@}{}}}}\ignorespaces{}\ignorespaces\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{{}{}{{}}{{}{}{}}{}}}}\ignorespaces{}{\hbox{\kern-28.08543pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[R_{1}S_{11}]},{[\epsilon]})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern 36.62134pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern 36.62134pt\raise-49.07181pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise 0.0pt\hbox{$\textstyle{({[R_{1}S_{11}]},{[S_{22}]})}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{array}$$

$$\begin{array}[]{rcl}\Lambda(x^{\mathcal{A}})&\overset{\mathrm{def}}{=}&[\,]\\ \Lambda(\lambda^{\ell}x.t)&\overset{\mathrm{def}}{=}&[\ell]+\Lambda(t)\\ \Lambda(t[s_{i}]_{i=1}^{n})&\overset{\mathrm{def}}{=}&\Lambda(t)+_{i=1}^{n}\Lambda(s_{i})\\ \end{array}$$

$$\begin{array}[]{rcl}&&(r[r_{1},\ldots,r_{n}])\{x:=\bar{s}\}\{y:=\bar{u}\}\\ &=&(r\{x:=\bar{s}_{0}\}[r_{i}\{x:=\bar{s}_{i}\}]_{i=0}^{n})\{y:=\bar{u}\}\\ &=&r\{x:=\bar{s}_{0}\}\{y:=\bar{u}_{0}\}[r_{i}\{x:=\bar{s}_{i}\}\{y:=\bar{u}_{i}\}]_{i=0}^{n}\\ &\overset{\mathrm{h.i.}}{=}&r\{y:=\bar{u}_{0,1}\}\{x:=\bar{s}_{0}\{y:=\bar{u}_{0,2}\}\}[r_{i}\{y:=\bar{u}_{i,1}\}\{x:=\bar{s}_{0}\{y:=\bar{u}_{i,2}\}\}]_{i=0}^{n}\\ &=&(r\{y:=\bar{u}_{0,1}\}[r_{i}\{y:=\bar{u}_{i,1}\}]_{i=0}^{n})\{x:=\sum_{i=1}^{n}\bar{s}_{i}\{y:=\bar{u}_{i,2}\}\}\\ \end{array}$$

$$\begin{array}[]{rcll}\bar{v}_{1}+\bar{v}_{2}&=&(\sum_{i=0}^{n}\bar{u}_{i,1})+(\sum_{i=0}^{n}\bar{u}_{i,2})\\ &\approx&\sum_{i=0}^{n}\bar{u}_{i,1}+\bar{u}_{i,2}\\ &\approx&\sum_{i=0}^{n}\bar{u}_{i}&\text{by {\em i.h.} on each index $i=0..n$}\\ &=&\bar{u}\end{array}$$

$$t\{x:=[s_1,\dots ,s_{i-1},s_i,s_{i+1},\dots ,s_n]\}\stackrel{\ell }{\to }t\{x:=[s_1,\dots ,s_{i-1},s_i^{\prime },s_{i+1},\dots ,s_n]\}$$

$$({\lambda }^{\ell }x.\mathtt{C}⟨({\lambda }^{{\ell }^{\prime }}y.r)\bar{u}⟩)\bar{s}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}\text{ignorespaces}$$

Full text

1 Introduction

Our goal in this paper is attempting to understand the spaces of computations of programs. Consider a hypothetical functional programming language with arithmetic expressions and tuples. All the possible computations starting from the tuple $(1+1,\ 2*3+1)$ can be arranged to form its “space of computations”:

[TABLE]

In this case, the space of computations is quite easy to understand, because the subexpressions $(1+1)$ and $(2*3+1)$ cannot interact with each other. Indeed, the space of computations of a tuple $(A,B)$ can always be understood as the product of the spaces of $A$ and $B$. In the general case, however, the space of computations of a program may have a much more complex structure. For example, it is not easy to characterize the space of computations of a function application $f(A)$. The difficulty is that $f$ may use the value of $A$ zero, one, or possibly many times.

The quintessential functional programming language is the pure $\lambda$-calculus. Computations in the $\lambda$-calculus have been thoroughly studied since its conception in the 1930s. The well-known theorem by Church and Rosser [10] states that $\beta$-reduction in the $\lambda$-calculus is confluent, which means, in particular, that terminating programs have unique normal forms. Another result by Curry and Feys [12] states that computations in the $\lambda$-calculus may be standardized, meaning that they may be converted into a computation in canonical form. A refinement of this theorem by Lévy [25] asserts that the canonical computation thus obtained is equivalent to the original one in a strong sense, namely that they are permutation equivalent. In a series of papers [29, 30, 31, 32], Melliès generalized many of these results to the abstract setting of axiomatic rewrite systems.

Let us discuss “spaces of computations” more precisely. The derivation space of an object $x$ in some rewriting system is the set of all derivations, i.e. sequences of rewrite steps, starting from $x$. In this paper, we will be interested in the pure $\lambda$-calculus, and we will study finite derivations only. In the $\lambda$-calculus, a transitive relation between derivations may be defined, the prefix order. A derivation $\rho$ is a prefix of a derivation $\sigma$, written $\rho\sqsubseteq\sigma$, whenever $\rho$ performs less computational work than $\sigma$. Formally, $\rho\sqsubseteq\sigma$ is defined to hold whenever the projection $\rho/\sigma$ is empty111The notion of projection defined by means of residuals is the standard one, see e.g. [4, Chapter 12] or [33, Section 8.7].. For example, if $K=\lambda x.\lambda y.x$, the derivation space of the term $(\lambda x.xx)(Kz)$ can be depicted with the reduction graph below. Derivations are directed paths in the reduction graph, and $\rho$ is a prefix of $\sigma$ if there is a directed path from the target of $\rho$ to the target of $\sigma$. For instance, $SR_{2}$ is a prefix of $RS^{\prime}T^{\prime}$:

[TABLE]

Remark that $\sqsubseteq$ is reflexive and transitive but not antisymmetric, i.e. it is a quasi-order but not an order. For example $RS^{\prime}\sqsubseteq SR_{1}R_{2}^{\prime}\sqsubseteq RS^{\prime}$ but $RS^{\prime}\neq SR_{1}R_{2}^{\prime}$. Antisymmetry may be recovered as usual when in presence of a quasi-order, by working modulo permutation equivalence: two derivations $\rho$ and $\sigma$ are said to be permutation equivalent, written $\rho\equiv\sigma$, if $\rho\sqsubseteq\sigma$ and $\sigma\sqsubseteq\rho$. Working modulo permutation equivalence is reasonable because Lévy’s formulation of the standardization theorem ensures that permutation equivalence is decidable.

Derivation spaces are known to exhibit various regularities [25, 35, 24, 28, 26, 2]. In his PhD thesis, Lévy [25] showed that the derivation space of a term is an upper semilattice: any two derivations $\rho,\sigma$ from a term $t$ have a least upper bound $\rho\sqcup\sigma$, defined as $\rho(\sigma/\rho)$, unique up to permutation equivalence. On the other hand, the derivation space of a term $t$ is not an easy structure to understand in general222Problem 2 in the RTA List of Open Problems [13] poses the open-ended question of investigating the properties of “spectra”, i.e. derivation spaces.. For example, relating the derivation space of an application $ts$ with the derivation spaces of $t$ and $s$ appears to be a hard problem. Lévy also noted that the greatest lower bound of two derivations does not necessarily exist, meaning that the derivation space of a term does not form a lattice in general. Even when it forms a lattice, it may not necessarily be a distributive lattice, as observed for example by Laneve [24]. In [29], Melliès showed that derivation spaces in any rewriting system satisfying certain axioms may be factorized using two spaces, one of external and one of internal derivations.

The difficulty to understand derivation spaces is due to three pervasive phenomena of interaction between computations. The first phenomenon is duplication: in the reduction graph of above, the step $S$ duplicates the step $R$, resulting in two copies of $R$: the steps $R_{1}$ and $R_{2}$. In such situation, one says that $R_{1}$ and $R_{2}$ are residuals of $R$, and, conversely, $R$ is an ancestor of $R_{1}$ and $R_{2}$. The second phenomenon is erasure: in the diagram above, the step $T$ erases the step $R^{\prime}_{1}$, resulting in no copies of $R^{\prime}_{1}$. The third phenomenon is creation: in the diagram above, the step $R_{2}$ creates the step $T$, meaning that $T$ is not a residual of a step that existed prior to executing $R_{2}$; that is, $T$ has no ancestor.

These three interaction phenomena, especially duplication and erasure, are intimately related with the management of resources. In this work, we aim to explore the hypothesis that having an explicit representation of resource management may provide insight on the structure of derivation spaces.

There are many existing $\lambda$-calculi that deal with resource management explicitly [6, 15, 20, 21], most of which draw inspiration from Girard’s Linear Logic [18]. Recently, calculi endowed with non-idempotent intersection type systems, have received some attention [14, 5, 7, 8, 19, 34, 22]. These type systems are able to statically capture non-trivial dynamic properties of terms, particularly normalization, while at the same time being amenable to elementary proof techniques by induction. Intersection types were originally proposed by Coppo and Dezani-Ciancaglini [11] to study termination in the $\lambda$-calculus. They are characterized by the presence of an intersection type constructor $\mathcal{A}\cap\mathcal{B}$. Non-idempotent intersection type systems are distinguished from their usual idempotent counterparts by the fact that intersection is not declared to be idempotent, i.e. $\mathcal{A}$ and $\mathcal{A}\cap\mathcal{A}$ are not equivalent types. Rather, intersection behaves like a multiplicative connective in linear logic. Arguments to functions are typed many times, typically once per each time that the argument will be used. Non-idempotent intersection types were originally formulated by Gardner [17], and later reintroduced by de Carvalho [9].

In this paper, we will use a non-idempotent intersection type system based on system $\mathcal{W}$ of [8] (called system $\mathcal{H}$ in [7]). Let us recall its definition. Terms are as usual in the $\lambda$-calculus ($t::=x\mid\lambda x.t\mid t\,t$). Types $\mathcal{A},\mathcal{B},\mathcal{C},\ldots$ are defined by the grammar:

[TABLE]

where $\alpha$ ranges over one of denumerably many base types, and $\mathcal{M}$ represents a multiset of types. Here $[\mathcal{A}_{i}]_{i=1}^{n}$ denotes the multiset $\mathcal{A}_{1},\ldots,\mathcal{A}_{n}$ with their respective multiplicities. A multiset $[\mathcal{A}_{i}]_{i=1}^{n}$ intuitively stands for the (non-idempotent) intersection $\mathcal{A}_{1}\cap\ldots\cap\mathcal{A}_{n}$. The sum of multisets $\mathcal{M}+\mathcal{N}$ is defined as their union (adding multiplicities). A typing context $\Gamma$ is a partial function mapping variables to multisets of types. The domain of $\Gamma$ is the set of variables $x$ such that $\Gamma(x)$ is defined. We assume that typing contexts always have finite domain and hence they may be written as $x_{1}:\mathcal{M}_{1},\ldots,x_{n}:\mathcal{M}_{n}$. The sum of contexts $\Gamma+\Delta$ is their pointwise sum, i.e. $(\Gamma+\Delta)(x):=\Gamma(x)+\Delta(x)$ if $\Gamma(x)$ and $\Delta(x)$ are both defined, $(\Gamma+\Delta)(x):=\Gamma(x)$ if $\Delta(x)$ is undefined, and $(\Gamma+\Delta)(x):=\Delta(x)$ if $\Gamma(x)$ is undefined. We write $\Gamma+_{i=1}^{n}\Delta_{i}$ to abbreviate $\Gamma+\Delta_{1}+\ldots+\Delta_{n}$. The disjoint sum of contexts $\Gamma\oplus\Delta$ stands for $\Gamma+\Delta$, provided that the domains of $\Gamma$ and $\Delta$ are disjoint. A typing judgment is a triple $\Gamma\vdash t:\mathcal{A}$, representing the knowledge that the term $t$ has type $\mathcal{A}$ in the context $\Gamma$. Type assignment rules for system $\mathcal{W}$ are as follows.

Definition 1 (System $\mathcal{W}$)

[TABLE]

Observe that the app rule has $n+1$ premises, where $n\geq 0$. System $\mathcal{W}$ enjoys various properties, nicely summarized in [8].

There are two obstacles to adopting system $\mathcal{W}$ for studying derivation spaces. The first obstacle is mostly a matter of presentation—typing derivations use a tree-like notation, which is cumbersome. One would like to have an alternative notation based on proof terms. For example, one may define proof terms for the typing rules above using the syntax $\pi::=x^{\mathcal{A}}\mid\lambda x.\pi\mid\pi[\pi,\ldots,\pi]$, in such a way that $x^{\mathcal{A}}$ encodes an application of the var axiom, $\lambda x.\pi$ encodes an application of the lam rule to the typing derivation encoded by $\pi$, and $\pi_{1}[\pi_{2},\ldots,\pi_{n}]$ encodes an application of the app rule to the typing derivations encoded by $\pi_{1},\pi_{2},\ldots,\pi_{n}$. For example, using this notation $\lambda x.x^{[\alpha,\alpha]\to\beta}[x^{\alpha},x^{\alpha}]$ would represent the following typing derivation:

[TABLE]

The second obstacle is a major one for our purposes: proof normalization in this system is not confluent. The reason is that applications take multiple arguments, and a $\beta$-reduction step must choose a way to distribute these arguments among the occurrences of the formal parameters. For instance, the following critical pair cannot be closed:

[TABLE]

The remainder of this paper is organized as follows:

• •

In Sec. 2, we review some standard notions of order and rewriting theory.

• •

In Sec. 3, we introduce a confluent calculus $\lambda^{\texttt{{\#}}}$ based on system $\mathcal{W}$. The desirable properties of system $\mathcal{W}$ of [8] still hold in $\lambda^{\texttt{{\#}}}$. Moreover, $\lambda^{\texttt{{\#}}}$ is confluent. We impose confluence forcibly, by decorating subtrees with distinct labels, so that a $\beta$-reduction step may distribute the arguments in a unique way. Derivation spaces in $\lambda^{\texttt{{\#}}}$ have very regular structure, namely they are distributive lattices.

• •

In Sec. 4, we establish a correspondence between derivation spaces in the $\lambda$-calculus and the $\lambda^{\texttt{{\#}}}$-calculus via simulation theorems, which defines a morphism of upper semilattices.

• •

In Sec. 5, we introduce the notion of a garbage derivation. Roughly, a derivation in the $\lambda$-calculus is garbage if it maps to an empty derivation in the $\lambda^{\texttt{{\#}}}$-calculus. This gives rise to an orthogonal notion of garbage-free derivation. The notion of garbage-free derivation is closely related with the notions of needed step [33, Section 8.6], typed occurrence of a redex [8], and external derivation [29]. Using this notion of garbage we prove a factorization theorem reminiscent of Melliès’ [29]. The upper semilattice of derivations of a term in the $\lambda$-calculus is factorized using a variant of the Grothendieck construction. Every derivation is uniquely decomposed as a garbage-free prefix followed by a garbage suffix.

• •

In Sec. 6, we conclude.

Note. Proofs including a $\clubsuit$ symbol are spelled out in detail in the appendix.

2 Preliminaries

We recall some standard definitions. An upper semilattice is a poset $(A,\leq)$ with a least element or bottom $\bot\in A$, and such that for every two elements $a,b\in A$ there is a least upper bound or join $(a\lor b)\in A$. A lattice is an upper semilattice with a greatest element or top $\top\in A$, and such that for every two elements $a,b\in A$ there is a greatest lower bound or meet $(a\land b)\in A$. A lattice is distributive if $\land$ distributes over $\lor$ and vice versa. A morphism of upper semilattices is given by a monotonic function $f:A\to B$, i.e. $a\leq b$ implies $f(a)\leq f(b)$, preserving the bottom element, i.e. $f(\bot)=\bot$, and joins, i.e. $f(a\lor b)=f(a)\lor f(b)$ for all $a,b\in A$. Similarly for morphisms of lattices. Any poset $(A,\leq)$ forms a category whose objects are the elements of $A$ and morphisms are of the form $a\hookrightarrow b$ for all $a\leq b$. The category of posets with monotonic functions is denoted by $\mathsf{Poset}$. In fact, we regard it as a 2-category: given morphisms $f,g:A\to B$ of posets, we have that $f\leq g$ whenever $f(a)\leq g(a)$ for all $a\in A$.

An axiomatic rewrite system (cf. [28, Def. 2.1]) is given by a set of objects $\mathsf{Obj}$, a set of steps $\mathsf{Stp}$, two functions $\mathsf{src},\mathsf{tgt}:\mathsf{Stp}\to\mathsf{Obj}$ indicating the source and target of each step, and a residual function $(/)$ such that given any two steps $R,S\in\mathsf{Stp}$ with the same source, yields a set of steps $R/S$ such that $\mathsf{src}(R^{\prime})=\mathsf{tgt}(S)$ for all $R^{\prime}\in R/S$. Steps are ranged over by $R,S,T,\ldots$. A step $R^{\prime}\in R/S$ is called a residual of $R$ after $S$, and $R$ is called an ancestor of $R^{\prime}$. Steps are coinitial (resp. cofinal) if they have the same source (resp. target). A derivation is a possibly empty sequence of composable steps $R_{1}\ldots R_{n}$. Derivations are ranged over by $\rho,\sigma,\tau,\ldots$. The functions $\mathsf{src}$ and $\mathsf{tgt}$ are extended to derivations. Composition of derivations is defined when $\mathsf{tgt}(\rho)=\mathsf{src}(\sigma)$ and written $\rho\,\sigma$. Residuals after a derivation can be defined by $R_{n}\in R_{0}/S_{1}\ldots S_{n}$ if and only if there exist $R_{1},\ldots,R_{n-1}$ such that $R_{i+1}\in R_{i}/S_{i+1}$ for all $0\leq i\leq n-1$. Let $\mathcal{M}$ be a set of coinitial steps. A development of $\mathcal{M}$ is a (possibly infinite) derivation $R_{1}\ldots R_{n}\ldots$ such that for every index $i$ there exists a step $S\in\mathcal{M}$ such that $R_{i}\in S/R_{1}\ldots R_{i-1}$. A development is complete if it is maximal.

An orthogonal axiomatic rewrite system (cf. [28, Sec. 2.3]) has four additional axioms333In [28], Autoerasure is called Axiom A, Finite Residuals is called Axiom B, and Semantic Orthogonality is called PERM. We follow the nomenclature of [1].:

Autoerasure. $R/R=\varnothing$ for all $R\in\mathsf{Stp}$. 2. 2.

Finite Residuals. The set $R/S$ is finite for all coinitial $R,S\in\mathsf{Stp}$. 3. 3.

Finite Developments. If $\mathcal{M}$ is a set of coinitial steps, all developments of $\mathcal{M}$ are finite. 4. 4.

Semantic Orthogonality. Let $R,S\in\mathsf{Stp}$ be coinitial steps. Then there exist a complete development $\rho$ of $R/S$ and a complete development $\sigma$ of $S/R$ such that $\rho$ and $\sigma$ are cofinal. Moreover, for every step $T\in\mathsf{Stp}$ such that $T$ is coinitial to $R$, the following equality between sets holds: $T/(R\sigma)=T/(S\rho)$.

In [28], Melliès develops the theory of orthogonal axiomatic rewrite systems. A notion of projection $\rho/\sigma$ may be defined between coinitial derivations, essentially by setting $\epsilon/\sigma\overset{\mathrm{def}}{=}\epsilon$ and $R\rho^{\prime}/\sigma\overset{\mathrm{def}}{=}(R/\sigma)(\rho^{\prime}/(\sigma/R))$ where, by abuse of notation, $R/\sigma$ stands for a (canonical) complete development of the set $R/\sigma$. Using this notion, one may define a transitive relation of prefix ($\rho\sqsubseteq\sigma$), a permutation equivalence relation ($\rho\equiv\sigma$), and the join of derivations ($\rho\sqcup\sigma$). Some of their properties are summed up in the figure below:

Summary of properties of orthogonal axiomatic rewrite systems

[TABLE]

Let ${[\rho]}=\{\sigma\ |\ \rho\equiv\sigma\}$ denote the permutation equivalence class of $\rho$. In an orthogonal axiomatic rewrite system, the set $\mathbb{D}(x)=\{{[\rho]}\ |\ \mathsf{src}(\rho)=x\}$ forms an upper semilattice [28, Thm. 2.2,Thm. 2.3]. The order ${[\rho]}\sqsubseteq{[\sigma]}$ is declared to hold if $\rho\sqsubseteq\sigma$, the join is ${[\rho]}\sqcup{[\sigma]}={[\rho\sqcup\sigma]}$, and the bottom is $\bot={[\epsilon]}$. The $\lambda$-calculus is an example of an orthogonal axiomatic rewrite system. Our structures of interest are the semilattices of derivations of the $\lambda$-calculus, written $\mathbb{D}^{\lambda}(t)$ for any given $\lambda$-term $t$. As usual, $\beta$-reduction in the $\lambda$-calculus is written $t\mathrel{\to_{\beta}}s$ and defined by the contextual closure of the axiom $(\lambda x.t)s\mathrel{\to_{\beta}}t\{x:=s\}$.

3 The Distributive $\lambda$-Calculus

In this section we introduce the distributive $\lambda$-calculus ($\lambda^{\texttt{{\#}}}$), and we prove some basic results. Terms of the $\lambda^{\texttt{{\#}}}$-calculus are typing derivations of a non-idempotent intersection type system, written using proof term syntax. The underlying type system is a variant of system $\mathcal{W}$ of [7, 8], the main difference being that $\lambda^{\texttt{{\#}}}$ uses labels and a suitable invariant on terms, to ensure that the formal parameters of all functions are in 1–1 correspondence with the actual arguments that they receive.

Definition 2 (Syntax of the $\lambda^{\texttt{{\#}}}$-calculus)

Let $\mathscr{L}=\{\ell,\ell^{\prime},\ell^{\prime\prime},\ldots\}$ be a denumerable set of labels. The set of types is ranged over by $\mathcal{A},\mathcal{B},\mathcal{C},\ldots$, and defined inductively as follows:

[TABLE]

where $\alpha$ ranges over one of denumerably many base types, and $\mathcal{M}$ represents a multiset of types. In a type like $\alpha^{\ell}$ and $\mathcal{M}\overset{\ell}{\to}\mathcal{A}$, the label $\ell$ is called the external label. The typing contexts are defined as in Sec. 1 for system $\mathcal{W}$. We write $\operatorname{dom}\Gamma$ for the domain of $\Gamma$. A type $\mathcal{A}$ is said to occur inside another type $\mathcal{B}$, written $\mathcal{A}\preceq\mathcal{B}$, if $\mathcal{A}$ is a subformula of $\mathcal{B}$. This is extended to say that a type $\mathcal{A}$ occurs in a multiset $[\mathcal{B}_{1},\ldots,\mathcal{B}_{n}]$, declaring that $\mathcal{A}\preceq[\mathcal{B}_{1},\ldots,\mathcal{B}_{n}]$ if $\mathcal{A}\preceq\mathcal{B}_{i}$ for some $i=1..n$, and that a type $\mathcal{A}$ occurs in a typing context $\Gamma$, declaring that $\mathcal{A}\preceq\Gamma$ if $\mathcal{A}\preceq\Gamma(x)$ for some $x\in\operatorname{dom}\Gamma$.

The set of terms, ranged over by $t,s,u,\ldots$, is given by the grammar $t::=x^{\mathcal{A}}\mid\lambda^{\ell}x.t\mid t\,\bar{t}$, where $\bar{t}$ represents a (possibly empty) finite list of terms. The notations $[x_{i}]_{i=1}^{n}$, $[x_{1},\ldots,x_{n}]$, and $\bar{x}$ all stand simultaneously for multisets and for lists of elements. Note that there is no confusion since we only work with multisets of types, and with lists of terms. The concatenation of the lists $\bar{x},\bar{y}$ is denoted by $\bar{x}+\bar{y}$. A sequence of $n$ lists $(\bar{x}_{1},\ldots,\bar{x}_{n})$ is a partition of $\bar{x}$ if $\bar{x}_{1}+\ldots+\bar{x}_{n}$ is a permutation of $\bar{x}$. The set of free variables of a term $t$ is written $\mathsf{fv}({t})$ and defined as expected. We also write $\mathsf{fv}({[t_{i}]_{i=1}^{n}})$ for $\cup_{i=1}^{n}\mathsf{fv}({t_{i}})$. A context is a term $\mathtt{C}$ with an occurrence of a distinguished hole $\Box$. We write $\mathtt{C}\langle t\rangle$ for the capturing substitution of $\Box$ by $t$. Typing judgments are triples $\Gamma\vdash t:\mathcal{A}$ representing the knowledge that the term $t$ has type $\mathcal{A}$ in the context $\Gamma$. Type assignment rules are:

[TABLE]

[TABLE]

For example $\vdash\lambda^{1}x.x^{[\alpha^{2},\alpha^{3}]\overset{4}{\to}\beta^{5}}[x^{\alpha^{3}},x^{\alpha^{2}}]:[[\alpha^{2},\alpha^{3}]\overset{4}{\to}\beta^{5},\alpha^{2},\alpha^{3}]\overset{1}{\to}\beta^{5}$ is a derivable judgment (using integer labels).

Remark 1 (Unique typing)

Let $\Gamma\vdash t:\mathcal{A}$ and $\Delta\vdash t:\mathcal{B}$ be derivable judgments. Then $\Gamma=\Delta$ and $\mathcal{A}=\mathcal{B}$. Moreover, the derivation trees coincide.

This can be checked by induction on $t$. It means that $\lambda^{\texttt{{\#}}}$ is an à la Church type system, that is, types are an intrinsic property of the syntax of terms, as opposed to an à la Curry type system like ${\mathcal{W}}$, in which types are extrinsic properties that a given term might or might not have.

To define a confluent rewriting rule, we impose a further constraint on the syntax of terms, called correctness. The $\lambda^{\texttt{{\#}}}$-calculus will be defined over the set of correct terms.

Definition 3 (Correct terms)

A multiset of types $[\mathcal{A}_{1},\ldots,\mathcal{A}_{n}]$ is sequential if the external labels of $\mathcal{A}_{i}$ and $\mathcal{A}_{j}$ are different for all $i\neq j$. A typing context $\Gamma$ is sequential if $\Gamma(x)$ is sequential for every $x\in\operatorname{dom}\Gamma$. A term $t$ is correct if it is typable and it verifies the following three conditions:

Uniquely labeled lambdas. If $\lambda^{\ell}x.s$ and $\lambda^{\ell^{\prime}}y.u$ are subterms of $t$ at different positions, then $\ell$ and $\ell^{\prime}$ must be different labels. 2. 2.

Sequential contexts. If $s$ is a subterm of $t$ and $\Gamma\vdash s:\mathcal{A}$ is derivable, then $\Gamma$ must be sequential. 3. 3.

Sequential types. If $s$ is a subterm of $t$, the judgment $\Gamma\vdash s:\mathcal{A}$ is derivable, and there exists a type such that $(\mathcal{M}\overset{\ell}{\to}\mathcal{B}\preceq\Gamma)\lor(\mathcal{M}\overset{\ell}{\to}\mathcal{B}\preceq\mathcal{A})$, then $\mathcal{M}$ must be sequential.

The set of correct terms is denoted by $\mathcal{T}^{\texttt{{\#}}}$.

For example, $x^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}[x^{\alpha^{1}}]$ is a correct term, $\lambda^{1}x.\lambda^{1}y.y^{\alpha^{2}}$ is not a correct term since labels for lambdas are not unique, and $\lambda^{1}x.x^{\alpha^{2}\overset{3}{\to}[\beta^{4},\beta^{4}]\overset{5}{\to}\gamma^{6}}$ is not a correct term since $[\beta^{4},\beta^{4}]$ is not sequential.

Substitution is defined explicitly below. If $t$ is typable, $\mathtt{T}_{x}(t)$ stands for the multiset of types of the free occurrences of $x$ in $t$. If $t_{1},\ldots,t_{n}$ are typable, $\mathtt{T}([t_{1},\ldots,t_{n}])$ stands for the multiset of types of $t_{1},\ldots,t_{n}$. For example, $\mathtt{T}_{x}(x^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}[x^{\alpha^{1}}])=\mathtt{T}([y^{\alpha^{1}},z^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}])=[[\alpha^{1}]\overset{2}{\to}\beta^{3},\alpha^{1}]$. To perform a substitution $t\{x:=[s_{1},\ldots,s_{n}]\}$ we will require that $\mathtt{T}_{x}(t)=\mathtt{T}([s_{1},\ldots,s_{n}])$.

Definition 4 (Substitution)

Let $t$ and $s_{1},\ldots,s_{n}$ be correct terms such that $\mathtt{T}_{x}(t)=\mathtt{T}([s_{1},\ldots,s_{n}])$. The capture-avoiding substitution of $x$ in $t$ by $\bar{s}=[s_{1},\ldots,s_{n}]$ is denoted by $t\{x:=\bar{s}\}$ and defined as follows:

[TABLE]

In the last case, $(\bar{s}_{0},\ldots,\bar{s}_{m})$ is a partition of $\bar{s}$ such that $\mathtt{T}_{x}(u_{j})=\mathtt{T}(\bar{s}_{j})$ for all $j=0..m$.

Remark 2

Substitution is type-directed: the arguments $[s_{1},\ldots,s_{n}]$ are propagated throughout the term so that $s_{i}$ reaches the free occurrence of $x$ that has the same type as $s_{i}$. Note that the definition of substitution requires that $\mathtt{T}_{x}(t)=\mathtt{T}([s_{1},\ldots,s_{n}])$, which means that the types of the terms $s_{1},\ldots,s_{n}$ are in 1–1 correspondence with the types of the free occurrences of $x$. Moreover, since $t$ is a correct term, the multiset $\mathtt{T}_{x}(t)$ is sequential, which implies in particular that each free occurrence of $x$ has a different type. Hence there is a unique correspondence matching the free occurrences of $x$ with the arguments $s_{1},\ldots,s_{n}$ that respects their types. As a consequence, in the definition of substitution for an application $u_{0}[u_{j}]_{j=1}^{m}\{x:=\bar{s}\}$ there is essentially a unique way to split $\bar{s}$ into $n+1$ lists $(\bar{s}_{0},\bar{s}_{1},\ldots,\bar{s}_{n})$ in such a way that $\mathtt{T}_{x}(u_{i})=\mathtt{T}(\bar{s}_{i})$. More precisely, if $(\bar{s}_{0},\bar{s}_{1},\ldots,\bar{s}_{n})$ and $(\bar{u}_{0},\bar{u}_{1},\ldots,\bar{u}_{n})$ are two partitions of $\bar{s}$ with the stated property, then $\bar{s}_{i}$ is a permutation of $\bar{u}_{i}$ for all $i=0..n$. Using this argument, it is easy to check by induction on $t$ that the value of $t\{x:=\bar{s}\}$ is uniquely determined and does not depend on this choice.

For example, $(x^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}[x^{\alpha^{1}}])\{x:=[y^{[\alpha^{1}]\overset{2}{\to}\beta^{3}},z^{\alpha^{1}}]\}=y^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}z^{\alpha^{1}}$ while, on the other hand, $(x^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}[x^{\alpha^{1}}])\{x:=[y^{\alpha^{1}},z^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}]\}=z^{[\alpha^{1}]\overset{2}{\to}\beta^{3}}y^{\alpha^{1}}$.

The operation of substitution preserves term correctness and typability:

Lemma 1 (Subject Reduction)

If $\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle$ is a correct term such that the judgment $\Gamma\vdash\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle:\mathcal{A}$ is derivable, then $\mathtt{C}\langle t\{x:=\bar{s}\}\rangle$ is correct and $\Gamma\vdash\mathtt{C}\langle t\{x:=\bar{s}\}\rangle:\mathcal{A}$ is derivable.

Proof

$\clubsuit$ By induction on $\mathtt{C}$.

Definition 5 (The $\lambda^{\texttt{{\#}}}$-calculus)

The $\lambda^{\texttt{{\#}}}$-calculus is the rewriting system whose objects are the set of correct terms $\mathcal{T}^{\texttt{{\#}}}$. The rewrite relation $\mathrel{\to_{\texttt{{\#}}}}$ is the closure under arbitrary contexts of the rule $(\lambda^{\ell}x.t)\bar{s}\mathrel{\to_{\texttt{{\#}}}}t\{x:=\bar{s}\}$. Lem. 1 justifies that $\mathrel{\to_{\texttt{{\#}}}}$ is well-defined, i.e. that the right-hand side is a correct term. The label of a step is the label $\ell$ decorating the contracted lambda. We write $t\mathrel{\xrightarrow{\ell}_{\texttt{{\#}}}}s$ whenever $t\mathrel{\to_{\texttt{{\#}}}}s$ and the label of the step is $\ell$.

Example 1

Let $I^{3}\overset{\mathrm{def}}{=}\lambda^{3}x.x^{\alpha^{2}}$ and $I^{4}\overset{\mathrm{def}}{=}\lambda^{4}x.x^{\alpha^{2}}$. The reduction graph of the term $(\lambda^{1}x.x^{[\alpha^{2}]\overset{3}{\to}\alpha^{2}}[x^{\alpha^{2}}])[I^{3},I^{4}[z^{\alpha^{2}}]]$ is:

[TABLE]

Note that numbers over arrows are the labels of the steps, while $R,R^{\prime},S,...$ are metalanguage names to refer to the steps. Next, we state and prove some basic properties of $\lambda^{\texttt{{\#}}}$.

Proposition 1 (Strong Normalization)

There is no infinite reduction $t_{0}\mathrel{\to_{\texttt{{\#}}}}t_{1}\mathrel{\to_{\texttt{{\#}}}}\ldots$.

Proof

Observe that a reduction step $\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}\langle t\{x:=\bar{s}\}\rangle$ decreases the number of lambdas in a term by exactly 1, because substitution is linear, i.e. the term $t\{x:=[s_{1},\ldots,s_{n}]\}$ uses $s_{i}$ exactly once for all $i=1..n$. Note: this is an adaptation of [8, Theorem 4.1].

The substitution operator may be extended to work on lists, by defining $[t_{i}]_{i=1}^{n}\{x:=\bar{s}\}\overset{\mathrm{def}}{=}[t_{i}\{x:=\bar{s}_{i}\}]_{i=1}^{n}$ where $(\bar{s}_{1},\ldots,\bar{s}_{n})$ is a partition of $\bar{s}$ such that $\mathtt{T}_{x}(t_{i})=\mathtt{T}(\bar{s}_{i})$ for all $i=1..n$.

Lemma 2 (Substitution Lemma)

Let $x\neq y$ and $x\not\in\mathsf{fv}({\bar{u}})$. If $(\bar{u}_{1},\bar{u}_{2})$ is a partition of $\bar{u}$ then $t\{x:=\bar{s}\}\{y:=\bar{u}\}=t\{y:=\bar{u}_{1}\}\{x:=\bar{s}\{y:=\bar{u}_{2}\}\}$, provided that both sides of the equation are defined. Note: there exists a list $\bar{u}$ that makes the left-hand side defined if and only if there exist lists $\bar{u}_{1},\bar{u}_{2}$ that make the right-hand side defined.

Proof

$\clubsuit$ By induction on $t$.

Proposition 2 (Permutation)

If $t_{0}\mathrel{\xrightarrow{\ell_{1}}_{\texttt{{\#}}}}t_{1}$ and $t_{0}\mathrel{\xrightarrow{\ell_{2}}_{\texttt{{\#}}}}t_{2}$ are different steps, then there exists a term $t_{3}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t_{1}\mathrel{\xrightarrow{\ell_{2}}_{\texttt{{\#}}}}t_{3}$ and $t_{2}\mathrel{\xrightarrow{\ell_{1}}_{\texttt{{\#}}}}t_{3}$.

Proof

$\clubsuit$ By exhaustive case analysis of permutation diagrams. Two representative cases are depicted below. The proof uses the Substitution Lemma (Lem. 2).

[TABLE]

[TABLE]

As a consequence of Prop. 2, reduction is subcommutative, i.e. $(\mathrel{\leftarrow_{\texttt{{\#}}}}\circ\mathrel{\to_{\texttt{{\#}}}})\ \subseteq(\mathrel{\to_{\texttt{{\#}}}}^{=}\circ\mathrel{\leftarrow_{\texttt{{\#}}}}^{=})$ where $\mathrel{\leftarrow_{\texttt{{\#}}}}$ denotes $(\mathrel{\to_{\texttt{{\#}}}})^{-1}$ and $R^{=}$ denotes the reflexive closure of $R$. Moreover, it is well-known that subcommutativity implies confluence, i.e. $(\mathrel{\leftarrow_{\texttt{{\#}}}}^{*}\circ\mathrel{\to_{\texttt{{\#}}}}^{*})\ \subseteq(\mathrel{\to_{\texttt{{\#}}}}^{*}\circ\mathrel{\leftarrow_{\texttt{{\#}}}}^{*})$; see [33, Prop. 1.1.10] for a proof of this fact.

Proposition 3 (Orthogonality)

$\lambda^{\texttt{{\#}}}$ is an orthogonal axiomatic rewrite system.

Proof

Let $R:t\mathrel{\to_{\texttt{{\#}}}}s$ and $S:t\mathrel{\to_{\texttt{{\#}}}}u$. Define the set of residuals $R/S$ as the set of steps starting on $u$ that have the same label as $R$. Note that $R/S$ is empty if $R=S$, and it is a singleton if $R\neq S$, since terms are correct so their lambdas are uniquely labeled. Then it is immediate to observe that axioms Autoerasure and Finite Residuals hold. The Finite Developments axiom is a consequence of Strong Normalization (Prop. 1). The Semantic Orthogonality axiom is a consequence of Permutation (Prop. 2).

For instance, in the reduction graph of Ex. 1, $ST/RS^{\prime}=T^{\prime}$, $S\sqcup R=SR^{\prime}$, and $SR^{\prime}T^{\prime}\equiv RS^{\prime}T^{\prime}$. Observe that in Ex. 1 there is no duplication or erasure of steps. This is a general phenomenon. Indeed, Permutation (Prop. 2) ensures that all non-trivial permutation diagrams are closed with exactly one step on each side.

Let us write $\mathbb{D}^{\texttt{{\#}}}(t)$ for the set of derivations of $t$ in the $\lambda^{\texttt{{\#}}}$-calculus, modulo permutation equivalence. As a consequence of Orthogonality (Prop. 3) and axiomatic results [28], the set $\mathbb{D}^{\texttt{{\#}}}(t)$ is an upper semilattice. Actually, we show that moreover the space $\mathbb{D}^{\texttt{{\#}}}(t)$ is a distributive lattice. To prove this, let us start by mentioning the property that we call Full Stability. This is a strong version of stability in the sense of Lévy [26]. It means that steps are created in an essentially unique way. In what follows, we write $\mathsf{lab}(R)$ for the label of a step, and $\mathsf{labs}(R_{1}\ldots R_{n})=\{\mathsf{lab}(R_{i})\ |\ 1\leq i\leq n\}$ for the set of labels of a derivation.

Lemma 3 (Full Stability)

Let $\rho,\sigma$ be coinitial derivations with disjoint labels, i.e. $\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)=\varnothing$. Let $T_{1},T_{2},T_{3}$ be steps such that $T_{3}=T_{1}/(\sigma/\rho)=T_{2}/(\rho/\sigma)$. Then there is a step $T_{0}$ such that $T_{1}=T_{0}/\rho$ and $T_{2}=T_{0}/\sigma$.

Proof

$\clubsuit$ The proof is easily reduced to a Basic Stability result: a particular case of Full Stability when $\rho$ and $\sigma$ consist of single steps. Basic Stability is proved by exhaustive case analysis.

Proposition 4

$\mathbb{D}^{\texttt{{\#}}}(t)$ is a lattice.

Proof

$\clubsuit$ The missing components are the top and the meet. The top element is given by $\top:={[\rho]}$ where $\rho:t\mathrel{\to_{\texttt{{\#}}}}^{*}s$ is a derivation to normal form, which exists by Strong Normalization (Prop. 1). The meet of $\{{[\rho]},{[\sigma]}\}$ is constructed using Full Stability (Lem. 15). If $\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)=\varnothing$, define $(\rho\sqcap\sigma):=\epsilon$. Otherwise, the stability result ensures that there is a step $R$ coinitial to $\rho$ and $\sigma$ such that $\mathsf{lab}(R)\in\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)$. Let $R$ be one such step, and, recursively, define $(\rho\sqcap\sigma):=R((\rho/R)\sqcap(\sigma/R))$. It can be checked that recursion terminates, because $\mathsf{labs}(\rho/R)\subset\mathsf{labs}(\rho)$ is a strict inclusion. Moreover, $\rho\sqcap\sigma$ is the greatest lower bound of $\{\rho,\sigma\}$, up to permutation equivalence.

For instance, in Ex. 1 we have that $ST\sqcap R=\epsilon$, $ST\sqcap RS^{\prime}=S$, and $ST\sqcap RS^{\prime}T^{\prime}=ST$.

Proposition 5

There is a monomorphism of lattices $\mathbb{D}^{\texttt{{\#}}}(t)\to\mathcal{P}(X)$ for some set $X$. The lattice $(\mathcal{P}(X),\subseteq,\varnothing,\cup,X,\cap)$ consists of the subsets of $X$, ordered by inclusion.

Proof

$\clubsuit$ The morphism is the function $\mathsf{labs}$, mapping each derivation to its set of labels.

This means that a derivation in $\lambda^{\texttt{{\#}}}$ is characterized, up to permutation equivalence, by the set of labels of its steps. Since $\mathcal{P}(X)$ is a distributive lattice, in particular we have:

Corollary 1

$\mathbb{D}^{\texttt{{\#}}}(t)$ is a distributive lattice.

4 Simulation of the $\lambda$-Calculus in the $\lambda^{\texttt{{\#}}}$-Calculus

In this section we establish a precise relationship between derivations in the $\lambda$-calculus and derivations in $\lambda^{\texttt{{\#}}}$. To begin, we need a way to relate $\lambda$-terms and correct terms ($\mathcal{T}^{\texttt{{\#}}}$):

Definition 6 (Refinement)

A correct term $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ refines a $\lambda$-term $t$, written $t^{\prime}\mathrel{\ltimes}t$, according to the following inductive definition:

[TABLE]

A $\lambda$-term may have many refinements. For example, the following terms refine $(\lambda x.xx)y$:

[TABLE]

[TABLE]

The refinement relation establishes a relation of simulation between the $\lambda$-calculus and $\lambda^{\texttt{{\#}}}$.

Proposition 6 (Simulation)

Let $t^{\prime}\mathrel{\ltimes}t$. Then:

If $t\mathrel{\to_{\beta}}s$, there exists $s^{\prime}$ such that $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$ and $s^{\prime}\mathrel{\ltimes}s$. 2. 2.

If $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}s^{\prime}$, there exist $s$ and $s^{\prime\prime}$ such that $t\mathrel{\to_{\beta}}s$, $s^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime\prime}$, and $s^{\prime\prime}\mathrel{\ltimes}s$.

Proof

$\clubsuit$ By case analysis. The proof is constructive. Moreover, in item 1, the derivation $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$ is shown to be a multistep, i.e. the complete development of a set $\{R_{1},\ldots,R_{n}\}$.

The following example illustrates that a $\beta$-step in the $\lambda$-calculus may be simulated by zero, one, or possibly many steps in $\lambda^{\texttt{{\#}}}$, depending on the refinement chosen.

Example 2

The following are simulations of the step $x\,((\lambda x.x)y)\mathrel{\to_{\beta}}x\,y$ using $\mathrel{\to_{\texttt{{\#}}}}$-steps:

[TABLE]

[TABLE]

The next result relates typability and normalization. This is an adaptation of existing results from non-idempotent intersection types, e.g. [8, Lemma 5.1]. Recall that a head normal form is a term of the form $\lambda x_{1}.\ldots\lambda x_{n}.y\,t_{1}\,\ldots\,t_{m}$.

Proposition 7 (Typability characterizes head normalization)

The following are equivalent:

There exists $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t^{\prime}\mathrel{\ltimes}t$. 2. 2.

There exists a head normal form $s$ such that $t\mathrel{\to_{\beta}}^{*}s$.

Proof

$\clubsuit$ The implication $(1\implies 2)$ relies on Simulation (Prop. 6). The implication $(2\implies 1)$ relies on the fact that head normal forms are typable, plus an auxiliary result of Subject Expansion.

The first item of Simulation (Prop. 6) ensures that every step $t\mathrel{\to_{\beta}}s$ can be simulated in $\lambda^{\texttt{{\#}}}$ starting from a term $t^{\prime}\mathrel{\ltimes}t$. Actually, a finer relationship can be established between the derivation spaces $\mathbb{D}^{\lambda}(t)$ and $\mathbb{D}^{\texttt{{\#}}}(t^{\prime})$. For this, we introduce the notion of simulation residual.

Definition 7 (Simulation residuals)

Let $t^{\prime}\mathrel{\ltimes}t$ and let $R:t\mathrel{\to_{\beta}}s$ be a step. The constructive proof of Simulation (Prop. 6) associates the $\mathrel{\to_{\beta}}$-step $R$ to a possibly empty set of $\mathrel{\to_{\texttt{{\#}}}}$-steps $\{R_{1},\ldots,R_{n}\}$ all of which start from $t^{\prime}$. We write $R/t^{\prime}\overset{\mathrm{def}}{=}\{R_{1},\ldots,R_{n}\}$, and we call $R_{1},\ldots,R_{n}$ the simulation residuals of $R$ after $t^{\prime}$. All the complete developments of $R/t^{\prime}$ have a common target, which we denote by $t^{\prime}/R$, called the simulation residual of $t^{\prime}$ after $R$.

Recall that, by abuse of notation, $R/t^{\prime}$ stands for some complete development of the set $R/t^{\prime}$. By Simulation (Prop. 6), the following diagram always holds given $t^{\prime}\mathrel{\ltimes}t\mathrel{\to_{\beta}}s$:

[TABLE]

Example 3 (Simulation residuals)

Let $R:x\,((\lambda x.x)y)\mathrel{\to_{\beta}}x\,y$ and consider the terms:

• $t^{\prime}_{0}=(x^{[\alpha^{1},\beta^{2}]\overset{3}{\to}\gamma^{4}}\,[(\lambda^{5}x.x^{\alpha^{1}})[y^{\alpha^{1}}],(\lambda^{6}x.x^{\beta^{2}})[y^{\beta^{2}}]])$
• $t^{\prime}_{1}=x^{[\alpha^{1},\beta^{2}]\overset{3}{\to}\gamma^{4}}\,[y^{\alpha^{1}},(\lambda^{6}x.x^{\beta^{2}})[y^{\beta^{2}}]$
• $t^{\prime}_{2}=x^{[\alpha^{1},\beta^{2}]\overset{3}{\to}\gamma^{4}}\,[(\lambda^{5}x.x^{\alpha^{1}})[y^{\alpha^{1}}],y^{\beta^{2}}]$
• $t^{\prime}_{3}=x^{[\alpha^{1},\beta^{2}]\overset{3}{\to}\gamma^{4}}\,[y^{\alpha^{1}},y^{\beta^{2}}]$

Then $t^{\prime}_{0}/R=t^{\prime}_{3}$ and $R/t^{\prime}_{0}=\{R_{1},R_{2}\}$, where $R_{1}:t^{\prime}_{0}\mathrel{\to_{\texttt{{\#}}}}t^{\prime}_{1}$ and $R_{2}:t^{\prime}_{0}\mathrel{\to_{\texttt{{\#}}}}t^{\prime}_{2}$.

The notion of simulation residual can be extended for many-step derivations.

Definition 8 (Simulation residuals of/after derivations)

If $t^{\prime}\mathrel{\ltimes}t$ and $\rho:t\mathrel{\to_{\beta}}^{*}s$ is a derivation, then $\rho/t^{\prime}$ and $t^{\prime}/\rho$ are defined as follows by induction on $\rho$:

[TABLE]

It is then easy to check that $\rho/t^{\prime}:t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}t^{\prime}/\rho$ and $t^{\prime}/\rho\mathrel{\ltimes}s$, by induction on $\rho$. Moreover, simulation residuals are well-defined modulo permutation equivalence:

Proposition 8 (Compatibility)

If $\rho\equiv\sigma$ and $t\mathrel{\ltimes}\mathsf{src}(\rho)$ then $\rho/t\equiv\sigma/t$ and $t/\rho=t/\sigma$.

Proof

$\clubsuit$ By case analysis, studying how permutation diagrams in the $\lambda$-calculus are transported to permutation diagrams in $\lambda^{\texttt{{\#}}}$ via simulation.

The following result resembles the usual Cube Lemma [4, Lemma 12.2.6]:

Lemma 4 (Cube)

If $t\mathrel{\ltimes}\mathsf{src}(\rho)=\mathsf{src}(\sigma)$, then $(\rho/\sigma)/(t/\sigma)\equiv(\rho/t)/(\sigma/t)$.

Proof

$\clubsuit$ By induction on $\rho$ and $\sigma$, relying on an auxiliary result, the Basic Cube Lemma, when $\rho$ and $\sigma$ are single steps, proved by exhaustive case analysis.

As a result, $(\rho\sqcup\sigma)/t=\rho(\sigma/\rho)/t=(\rho/t)((\sigma/\rho)/(t/\rho))\equiv(\rho/t)((\sigma/t)/(\sigma/\rho))=(\rho/t)\sqcup(\sigma/t)$. Moreover, if $\rho\sqsubseteq\sigma$ then $\rho\tau\equiv\sigma$ for some $\tau$. So we have that $\rho/t\sqsubseteq(\rho/t)(\tau/(t/\rho))=\rho\tau/t\equiv\sigma/t$ by Compatibility (Prop. 8). Hence we may formulate a stronger simulation result:

Corollary 2 (Algebraic Simulation)

Let $t^{\prime}\mathrel{\ltimes}t$. Then the mapping $\mathbb{D}^{\lambda}(t)\to\mathbb{D}^{\texttt{{\#}}}(t^{\prime})$ given by ${[\rho]}\mapsto{[\rho/t^{\prime}]}$ is a morphism of upper semilattices.

Example 4

Let $I=\lambda x.x$ and $\Delta=(\lambda^{5}x.x^{\alpha^{2}})[z^{\alpha^{2}}]$ and let $\hat{y}=y^{[\alpha^{2}]\overset{3}{\to}[\,]\overset{4}{\to}\beta^{5}}$. The refinement $t^{\prime}:=(\lambda^{1}x.\hat{y}[x^{\alpha^{2}}][\,])[\Delta]\mathrel{\ltimes}(\lambda x.yxx)(Iz)$ induces a morphism between the upper semilattices represented by the following reduction graphs:

[TABLE]

For example $(R_{1}\sqcup S)/t^{\prime}=(R_{1}S_{11}S_{22})/t^{\prime}=R^{\prime}_{1}S^{\prime}_{1}=R^{\prime}_{1}\sqcup S^{\prime}=R_{1}/t^{\prime}\sqcup S/t^{\prime}$. Note that the step $S_{22}$ is erased by the simulation: $S_{22}/(\hat{y}[z^{\alpha^{2}}][\,])=\varnothing$. Intuitively, $S_{22}$ is “garbage” with respect to the refinement $\hat{y}[z^{\alpha^{2}}][\,]$, because it lies inside an untyped argument.

5 Factoring Derivation Spaces

In this section we prove that the upper semilattice $\mathbb{D}^{\lambda}(t)$ may be factorized using a variant of the Grothendieck construction. We start by formally defining the notion of garbage.

Definition 9 (Garbage)

Let $t^{\prime}\mathrel{\ltimes}t$. A derivation $\rho:t\mathrel{\to_{\beta}}^{*}s$ is $t^{\prime}$-garbage if $\rho/t^{\prime}=\epsilon$.

The informal idea is that each refinement $t^{\prime}\mathrel{\ltimes}t$ specifies that some subterms of $t$ are “useless”. A subterm $u$ is useless if it lies inside the argument of an application $s(...u...)$ in such a way that the argument is not typed, i.e. the refinement is of the form $s^{\prime}[\,]\mathrel{\ltimes}s(...u...)$. A single step $R$ is $t^{\prime}$-garbage if the pattern of the contracted redex lies inside a useless subterm. A sequence of steps $R_{1}R_{2}\ldots R_{n}$ is $t^{\prime}$-garbage if $R_{1}$ is $t^{\prime}$-garbage, $R_{2}$ is $(t^{\prime}/R_{1})$-garbage, $\ldots$, $R_{i}$ is $(t^{\prime}/R_{1}\ldots R_{i-1})$-garbage, $\ldots$, and so on.

Usually we say that $\rho$ is just garbage, when $t^{\prime}$ is clear from the context. For instance, in Ex. 4, $S_{21}$ is garbage, since $S_{21}/(\hat{y}[\Delta][\,])=\epsilon$. Similarly, $S_{22}$ is garbage, since $S_{22}/(\hat{y}[z^{\alpha^{2}}][\,])=\epsilon$. On the other hand, $R_{1}S_{21}$ is not garbage, since $R_{1}S_{21}/((\lambda^{1}x.\hat{y}[x^{\alpha^{2}}][\,])[\Delta])=R^{\prime}_{1}\neq\epsilon$. For each $t^{\prime}\mathrel{\ltimes}t$, the set of $t^{\prime}$-garbage derivations forms an ideal of the upper semilattice $\mathbb{D}^{\lambda}(t)$. More precisely:

Proposition 9 (Properties of garbage)

Let $t^{\prime}\mathrel{\ltimes}t$. Then:

If $\rho$ is $t^{\prime}$-garbage and $\sigma\sqsubseteq\rho$, then $\sigma$ is $t^{\prime}$-garbage. 2. 2.

The composition $\rho\sigma$ is $t^{\prime}$-garbage if and only if $\rho$ is $t^{\prime}$-garbage and $\sigma$ is $(t^{\prime}/\rho)$-garbage. 3. 3.

If $\rho$ is $t^{\prime}$-garbage then $\rho/\sigma$ is $(t^{\prime}/\sigma)$-garbage. 4. 4.

The join $\rho\sqcup\sigma$ is $t^{\prime}$-garbage if and only if $\rho$ and $\sigma$ are $t^{\prime}$-garbage.

Proof

$\clubsuit$ The proof is easy using Prop. 8 and Lem. 4.

Our aim is to show that given $\rho:t\mathrel{\to_{\beta}}^{*}s$ and $t^{\prime}\mathrel{\ltimes}t$, there is a unique way of decomposing $\rho$ as $\sigma\tau$, where $\tau$ is $t^{\prime}$-garbage and $\sigma$ “has no $t^{\prime}$-garbage”. Garbage is well-defined modulo permutation equivalence, i.e. given $\rho\equiv\sigma$, we have that $\rho$ is garbage if and only if $\sigma$ is garbage. In contrast, it is not immediate to give a well-defined notion of “having no garbage”. For example, in Ex. 4, $SR_{2}$ has no garbage steps, so it appears to have no garbage; however, it is permutation equivalent to $R_{1}S_{11}S_{22}$, which does contain a garbage step ($S_{22}$). The following definition seems to capture the right notion of having no garbage:

Definition 10 (Garbage-free derivation)

Let $t^{\prime}\mathrel{\ltimes}t$. A derivation $\rho:t\mathrel{\to_{\beta}}^{*}s$ is $t^{\prime}$-garbage-free if for any derivation $\sigma$ such that $\sigma\sqsubseteq\rho$ and $\rho/\sigma$ is $(t^{\prime}/\sigma)$-garbage, then $\rho/\sigma=\epsilon$.

Again, we omit the $t^{\prime}$ if clear from the context. Going back to Ex. 4, the derivation $SR_{2}$ is not garbage-free, because $R_{1}S_{11}\sqsubseteq SR_{2}$ and $SR_{2}/R_{1}S_{11}=S_{22}$ is garbage but non-empty. Note that Def. 10 is defined in terms of the prefix order ($\sqsubseteq$), so:

Remark 3

If $\rho\equiv\sigma$, then $\rho$ is $t^{\prime}$-garbage-free if and only if $\sigma$ is $t^{\prime}$-garbage-free.

Next, we define an effective procedure (sieving) to erase all the garbage from a derivation. The idea is that if $\rho:t\mathrel{\to_{\beta}}^{\star}s$ is a derivation in the $\lambda$-calculus and $t^{\prime}\mathrel{\ltimes}t$ is any refinement, we may constructively build a $t^{\prime}$-garbage-free derivation $(\rho\Downarrow t^{\prime}):t\mathrel{\to_{\beta}}^{\star}u$ by erasing all the $t^{\prime}$-garbage from $\rho$. Our goal will then be to show that $\rho\equiv(\rho\Downarrow t^{\prime})\sigma$ where $\sigma$ is garbage.

Definition 11 (Sieving)

Let $t^{\prime}\mathrel{\ltimes}t$ and $\rho:t\mathrel{\to_{\beta}}^{\star}s$. A step $R$ is coarse for $(\rho,t^{\prime})$ if $R\sqsubseteq\rho$ and $R/t^{\prime}\neq\varnothing$. The sieve of $\rho$ with respect to $t^{\prime}$, written $\rho\Downarrow t^{\prime}$, is defined as follows.

• •

If there are no coarse steps for $(\rho,t^{\prime})$, then $(\rho\Downarrow t^{\prime})\overset{\mathrm{def}}{=}\epsilon$.

• •

If there is a coarse step for $(\rho,t^{\prime})$, then $(\rho\Downarrow t^{\prime})\overset{\mathrm{def}}{=}R_{0}((\rho/R_{0})\Downarrow(t^{\prime}/R_{0}))$ where $R_{0}$ is the leftmost such step.

Lemma 5

The sieving operation $\rho\Downarrow t^{\prime}$ is well-defined.

Proof

$\clubsuit$ To see that recursion terminates, consider the measure $M$ given by $M(\rho,t^{\prime}):=\#\mathsf{labs}(\rho/t^{\prime})$, and note that $M(\rho,t^{\prime})>M(\rho/R_{0},t^{\prime}/R_{0})$.

For example, in Ex. 4, we have that $S\Downarrow t^{\prime}=S$ and $SR_{2}\Downarrow t^{\prime}=R_{1}S_{11}$.

Proposition 10 (Properties of sieving)

Let $t^{\prime}\mathrel{\ltimes}t$ and $\rho:t\mathrel{\to_{\beta}}^{*}s$. Then:

$\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free and $\rho\Downarrow t^{\prime}\sqsubseteq\rho$. 2. 2.

$\rho/(\rho\Downarrow t^{\prime})$ is $(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage. 3. 3.

$\rho$ is $t^{\prime}$-garbage if and only if $\rho\Downarrow t^{\prime}=\epsilon$. 4. 4.

$\rho$ is $t^{\prime}$-garbage-free if and only if $\rho\Downarrow t^{\prime}\equiv\rho$.

Proof

$\clubsuit$ By induction on the length of $\rho\Downarrow t^{\prime}$, using various technical lemmas.

As a consequence of the definition of the sieving construction and its properties, given any derivation $\rho:t\mathrel{\to_{\beta}}^{*}s$ and any refinement $t^{\prime}\mathrel{\ltimes}t$, we can always write $\rho$, modulo permutation equivalence, as of the form $\rho\equiv\sigma\tau$ in such a way that $\sigma$ is garbage-free and $\tau$ is garbage. To prove this take $\sigma:=\rho\Downarrow t^{\prime}$ and $\tau:=\rho/(\rho\Downarrow t^{\prime})$, and note that $\sigma$ is garbage-free by item 1. of Prop. 10, $\tau$ is garbage by item 2. of Prop. 10, and $\rho\equiv\sigma(\rho/\sigma)=\sigma\tau$ because $\sigma\sqsubseteq\rho$ by item 1. of Prop. 10.

In the following we give a stronger version of this result. The Factorization theorem below (Thm. 5.1) states that this decomposition is actually an isomorphism of upper semilattices. This means, on one hand, that given any derivation $\rho:t\mathrel{\to_{\beta}}^{*}s$ and any refinement $t^{\prime}\mathrel{\ltimes}t$ there is a unique way to factor $\rho$ as of the form $\rho\equiv\sigma\tau$ where $\sigma$ is garbage-free and $\tau$ is garbage. On the other hand, it means that the decomposition $\rho\mapsto(\rho\Downarrow t^{\prime},\rho/(\rho\Downarrow t^{\prime}))$ mapping each derivation to a of a garbage-free plus a garbage derivation is functorial. This means, essentially, that the set of pairs $(\sigma,\tau)$ such that $\sigma$ is garbage-free and $\tau$ is garbage can be given the structure of an upper semilattice in such a way that:

• •

If $\rho\mapsto(\sigma,\tau)$ and $\rho^{\prime}\mapsto(\sigma^{\prime},\tau^{\prime})$ then $\rho\sqsubseteq\rho^{\prime}\iff(\sigma,\tau)\leq(\sigma^{\prime},\tau^{\prime})$.

• •

If $\rho\mapsto(\sigma,\tau)$ and $\rho^{\prime}\mapsto(\sigma^{\prime},\tau^{\prime})$ then $(\rho\sqcup\rho^{\prime})\mapsto(\sigma,\tau)\lor(\sigma^{\prime},\tau^{\prime})$.

The upper semilattice structure of the set of pairs $(\sigma,\tau)$ is given using a variant of the Grothendieck construction:

Definition 12 (Grothendieck construction for partially ordered sets)

Let $A$ be a poset, and let $B:A\to\mathsf{Poset}$ be a mapping associating each object $a\in A$ to a poset $B(a)$. Suppose moreover that $B$ is a lax 2-functor. More precisely, for each $a\leq b$ in $A$, the function $B(a\hookrightarrow b):B(a)\to B(b)$ is monotonic and such that:

$B(a\hookrightarrow a)=\mathsf{id}_{B(a)}$ for all $a\in A$, 2. 2.

$B((b\hookrightarrow c)\circ(a\hookrightarrow b))\leq B(b\hookrightarrow c)\circ B(a\hookrightarrow b)$ for all $a\leq b\leq c$ in $A$.

The Grothendieck construction $\int_{A}{B}$ is defined as the poset given by the set of objects $\{(a,b)\ |\ a\in A,\ b\in B(a)\}$ and such that $(a,b)\leq(a^{\prime},b^{\prime})$ is declared to hold if and only if $A\leq a^{\prime}\text{ and }B(a\hookrightarrow a^{\prime})(b)\leq b^{\prime}$.

The following proposition states that garbage-free derivations form a finite lattice, while garbage derivations form an upper semilattice.

Proposition 11 (Garbage-free and garbage semilattices)

Let $t^{\prime}\mathrel{\ltimes}t$.

The set F=\{{[\rho]}\ |\ \mathsf{src}(\rho)=t\text{ and }\rho\text{ is t^{\prime}-garbage-free}\} of $t^{\prime}$-garbage-free derivations forms a finite lattice $\mathbb{F}(t^{\prime},t)=(F,\unlhd,\bot,\triangledown,\top,\!\vartriangle\!)$, with:

• •

Partial order: {[\rho]}\unlhd{[\sigma]}\overset{\mathrm{def}}{\iff}\rho/\sigma\text{ is (t^{\prime}/\sigma)-garbage}.

• •

Bottom: $\bot:={[\epsilon]}$.

• •

Join: ${[\rho]}\triangledown{[\sigma]}\overset{\mathrm{def}}{=}{[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}$.

• •

Top: $\top$, defined as the join of all the ${[\tau]}$ such that $\tau$ is $t^{\prime}$-garbage-free.

• •

Meet: ${[\rho]}\!\vartriangle\!{[\sigma]}$, defined as the join of all the ${[\tau]}$ such that ${[\tau]}\unlhd{[\rho]}$ and ${[\tau]}\unlhd{[\sigma]}$. 2. 2.

The set G=\{{[\rho]}\ |\ \mathsf{src}(\rho)=t\text{ and }\rho\text{ is t^{\prime}-garbage}\} of $t^{\prime}$-garbage derivations forms an upper semilattice $\mathbb{G}(t^{\prime},t)=(G,\sqsubseteq,\bot,\sqcup)$, with the structure inherited from $\mathbb{D}^{\lambda}(t)$.

Proof

$\clubsuit$ The proof relies on the properties of garbage and sieving (Prop. 9, Prop. 10).

Suppose that $t^{\prime}\mathrel{\ltimes}t$, and let $\mathcal{F}\overset{\mathrm{def}}{=}\mathbb{F}(t^{\prime},t)$ denote the lattice of $t^{\prime}$-garbage-free derivations. Let $\mathcal{G}:\mathcal{F}\to\mathsf{Poset}$ be the lax 2-functor $\mathcal{G}({[\rho]})\overset{\mathrm{def}}{=}\mathbb{G}(t^{\prime}/\rho,\mathsf{tgt}(\rho))$ with the following action on morphisms:

[TABLE]

Using the previous proposition (Prop. 11) it can be checked that $\mathcal{G}$ is indeed a lax 2-functor, and that the Grothendieck construction $\int_{\mathcal{F}}{\mathcal{G}}$ forms an upper semilattice. The join is given by $(a,b)\lor(a^{\prime},b^{\prime})=(a\triangledown a^{\prime},\mathcal{G}(a\hookrightarrow a\triangledown a^{\prime})(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow a\triangledown a^{\prime})(b^{\prime}))$. Finally we can state the main theorem:

Theorem 5.1 (Factorization)

The following maps form an isomorphism of upper semilattices:

[TABLE]

Proof

$\clubsuit$ The proof consists in checking that both maps are morphisms of upper semilattices and that they are mutual inverses, resorting to Prop. 9 and Prop. 10.

Example 5

Let $t=(\lambda x.yxx)(Iz)$ and $t^{\prime}$ be as in Ex. 4. The upper semilattice $\mathbb{D}^{\lambda}(t)$ can be factorized as $\int_{\mathcal{F}}{\mathcal{G}}$ as follows. Here posets are represented by their Hasse diagrams:

[TABLE]

For example $({[S]},{[\epsilon]})\leq({[R_{1}S_{11}]},{[S_{22}]})$ because ${[S]}\unlhd{[R_{1}S_{11}]}$, that is, $S/R_{1}S_{11}=S_{22}$ is garbage, and $\mathcal{G}({[S]}\hookrightarrow{[R_{1}S_{11}]})({[\epsilon]})={[S/R_{1}S_{11}]}={[S_{22}]}\sqsubseteq{[S_{22}]}$.

6 Conclusions

We have defined a calculus ($\lambda^{\texttt{{\#}}}$) based on non-idempotent intersection types. Its syntax and semantics are complex due to the presence of an admittedly ad hoc correctness invariant for terms, enforced so that reduction is confluent. In contrast, derivation spaces in this calculus turn out to be very simple structures: they are representable as rings of sets (Prop. 5) and as a consequence they are distributive lattices (Coro. 1). Derivation spaces in the $\lambda$-calculus can be mapped to these much simpler spaces using a strong notion of simulation (Coro. 2) inspired by residual theory. Building on this, we showed how the derivation space of any typable $\lambda$-term may be factorized as a “twisted product” of garbage-free and garbage derivations (Thm. 5.1).

We believe that this validates the (soft) hypothesis that explicitly representing resource management can provide insight on the structure of derivation spaces.

Related work. The Factorization theorem (Thm. 5.1) is reminiscent of Melliès’ abstract factorization result [29]. Given an axiomatic rewriting system fulfilling a number of axioms, Melliès proves that every derivation can be uniquely factorized as an external prefix followed by an internal suffix. We conjecture that each refinement $t^{\prime}\mathrel{\ltimes}t$ should provide an instantiation of Melliès’ axioms, in such a way that our $t^{\prime}$-garbage-free/$t^{\prime}$-garbage factorization coincides with his external/internal factorization. Melliès notes that any evaluation strategy that always selects external steps is hypernormalizing. A similar result should hold for evaluation strategies that always select non-garbage steps.

The notion of garbage-free derivation is closely related with the notion of $X$-neededness [3]. A step $R$ is $X$-needed if every reduction to a term $t\in X$ contracts a residual of $R$. Recently, Kesner et al. [22] have related typability in a non-idempotent intersection type system $\mathcal{V}$ and weak-head neededness. Using similar techniques, it should be possible to prove that $t^{\prime}$-garbage-free steps are $X$-needed, where $X=\{s\ |\ s^{\prime}\mathrel{\ltimes}s\}$ and $s^{\prime}$ is the $\mathrel{\to_{\texttt{{\#}}}}$-normal form of $t^{\prime}$.

There are several resource calculi in the literature which perhaps could play a similar role as $\lambda^{\texttt{{\#}}}$ to recover factorization results akin to Thm. 5.1. Kfoury [23] embeds the $\lambda$-calculus in a linear $\lambda$-calculus that has no duplication nor erasure. Ehrard and Regnier prove that the Taylor expansion of $\lambda$-terms [16] commutes with normalization, similarly as in Algebraic Simulation (Coro. 2). Mazza et al. [27] study a general framework for polyadic approximations, corresponding roughly to the notion of refinement in this paper.

Acknowledgements. To Eduardo Bonelli and Delia Kesner for introducing the first author to these topics. To Luis Scoccola and the anonymous reviewers for helpful suggestions.

Appendix 0.A Appendix

This technical appendix includes the detailed proofs of the results stated in the main body of the paper that have been marked with the $\clubsuit$ symbol.

0.A.1 Proof of Lem. 1 – Subject Reduction

We are to prove that if $\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle$ is correct then $\mathtt{C}\langle t\{x:=\bar{s}\}\rangle$ is correct, and, moreover, that their unique typings are under the same typing context and have the same type. We need a few auxiliary results:

Lemma 6

If $\bar{s}$ is a permutation of $\bar{u}$, then $t\{x:=\bar{s}\}=t\{x:=\bar{u}\}$.

Proof

By induction on $t$.

Lemma 7

If $t$ is correct, then any subterm of $t$ is correct.

Proof

Note, by definition of correctness (Def. 3), that if $t$ is a correct abstraction $t=\lambda^{\ell}x.s$ then $s$ is correct, and if $t$ is a correct application $t=s[u_{1},\ldots,u_{n}]$ then $s$ and $u_{1},\ldots,u_{n}$ are correct. This allows us to conclude by induction on $t$.

Lemma 8 (Relevance)

If $\Gamma\vdash t:\mathcal{A}$ and $x\in\operatorname{dom}\Gamma$ then $x\in\mathsf{fv}({t})$.

Proof

By induction on $t$.

Definition 13

$\Lambda(t)$ stands for the multiset of labels decorating the lambdas of $t$:

[TABLE]

For example, $\Lambda((\lambda^{1}x.x^{[\alpha^{2}]\overset{3}{\to}\alpha^{2}})[\lambda^{3}x.x^{\alpha^{2}}])=[1,3]$.

Lemma 9

Let $t,s_{1},\ldots,s_{n}$ be correct terms. Then $\Lambda(t\{x:=[s_{i}]_{i=1}^{n}\})=\Lambda(t)+_{i=1}^{n}\Lambda(s_{i})$.

Proof

By induction on $t$.

To prove Lem. 1, we first show that substitution preserves typing, and then that it preserves correctness.

0.A.1.1 Substitution preserves typing

More precisely, let us show that if $\Gamma\vdash\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle:\mathcal{A}$ is derivable, then $\Gamma\vdash\mathtt{C}\langle t\{x:=\bar{s}\}\rangle:\mathcal{A}$ is derivable. By induction on the context $\mathtt{C}$.

Empty, $\mathtt{C}=\Box$.

By induction on $t$.

1. 1.1

Variable (same), $t=x^{\mathcal{A}}$, $\bar{s}=[s]$. We have that $x:[\mathcal{A}]\vdash x^{\mathcal{A}}:\mathcal{A}$ and $\Delta\vdash s:\mathcal{B}$ are derivable, so we are done. 2. 1.2

Variable (different), $t=y^{\mathcal{A}}$, $y\neq x$, $\bar{s}=[]$. We have that $y:[\mathcal{A}]\vdash y^{\mathcal{A}}:\mathcal{A}$ is derivable, so we are done. 3. 1.3

Abstraction, $t=\lambda^{\ell}y.u$. Let $\Gamma\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}\vdash\lambda^{\ell}x.u:\mathcal{M}\overset{\ell}{\to}\mathcal{A}$ be derivable and $\Delta_{i}\vdash s_{i}:\mathcal{B}_{i}$ be derivable for all $i=1..n$. By inversion of the lam rule, we have that $\Gamma\oplus y:\mathcal{M}\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}\vdash u:\mathcal{A}$ is derivable, so by i.h. $(\Gamma\oplus y:\mathcal{M})+_{i=1}^{n}\Delta_{i}\vdash u\{x:=[s_{i}]_{i=1}^{n}\}:\mathcal{A}$ is derivable. Observe that $y\not\in\mathsf{fv}({s_{i}})$ so $y\not\in\operatorname{dom}\Delta_{i}$ by Lem. 8. Hence the previous judgment can be written as $(\Gamma+_{i=1}^{n}\Delta_{i})\oplus y:\mathcal{M}\vdash u\{x:=[s_{i}]_{i=1}^{n}\}:\mathcal{A}$. Applying the lam rule we obtain $\Gamma+_{i=1}^{n}\Delta_{i}\vdash\lambda^{\ell}y.u\{x:=[s_{i}]_{i=1}^{n}\}:\mathcal{M}\overset{\ell}{\to}\mathcal{A}$ as required. 4. 1.4

Application, $t=u[r_{j}]_{j=1}^{m}$. Let $\Gamma\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}\vdash u[r_{j}]_{j=1}^{m}:\mathcal{A}$ be derivable and $\Delta_{i}\vdash s_{i}:\mathcal{B}_{i}$ be derivable for all $i=1..n$. By inversion of the app rule, the multiset of types $[\mathcal{B}_{i}]_{i=1}^{n}$ may be partitioned as $[\mathcal{B}_{i}]_{i=1}^{n}=\sum_{j=0}^{m}\mathcal{M}_{j}$, and the typing context $\Gamma$ may be partitioned as $\Gamma=\sum_{j=0}^{m}\Gamma_{j}$ in such a way that $\Gamma_{0}\oplus x:\mathcal{M}_{0}\vdash u:[\mathcal{C}_{j}]_{j=1}^{m}\overset{\ell}{\to}\mathcal{A}$ is derivable and $\Gamma_{j}\oplus x:\mathcal{M}_{j}\vdash r_{j}:\mathcal{C}_{j}$ is derivable for all $j=1..m$. Consider a partition $(\bar{s}_{0},\ldots,\bar{s}_{j})$ of the list $\bar{s}$ such that for every $j=0..m$ we have $\mathtt{T}(\bar{s}_{j})=\mathcal{M}_{j}$. Observe that this partition exists since $\mathtt{T}(\bar{s}_{0}+\ldots+\bar{s}_{j})=\mathtt{T}(\bar{s})=\sum_{j=0}^{m}\mathcal{M}_{j}=[\mathcal{B}_{i}]_{i=1}^{n}=\mathtt{T}_{x}(t)$.

Moreover, let $\Theta_{j}=\sum_{i:s_{i}\in\bar{s}_{j}}\Delta_{i}$ for all $j=0..m$. By i.h. we have that $\Gamma_{0}+\Theta_{0}\vdash u\{x:=\bar{s}_{0}\}:[\mathcal{C}_{j}]_{j=1}^{m}\overset{\ell}{\to}\mathcal{A}$ is derivable and $\Gamma_{j}+\Theta_{j}\vdash r_{j}\{x:=\bar{s}_{j}\}:\mathcal{C}_{j}$ is derivable for all $j=1..m$. Applying the app rule we obtain that $\sum_{j=0}^{m}\Gamma_{j}+\sum_{j=0}^{m}\Theta_{j}\vdash u[r_{j}]\{x:=\sum_{j=0}^{m}\bar{s}_{j}\}:\mathcal{A}$ is derivable. By definition of $\Gamma_{0},\ldots,\Gamma_{m}$ and $\Theta_{0},\ldots,\Theta_{m}$ this judgment equals $\Gamma+_{i=1}^{n}\Delta_{i}\vdash u[r_{j}]\{x:=\sum_{j=0}^{m}\bar{s}_{j}\}:\mathcal{A}$. By definition of $\bar{s}_{0},\ldots,\bar{s}_{m}$ and Lem. 6 this in turn equals $\Gamma+_{i=1}^{n}\Delta_{i}\vdash u[r_{j}]\{x:=\bar{s}\}:\mathcal{A}$, as required. 2. 2.

Under an abstraction, $\mathtt{C}=\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}$. Straightforward by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}\bar{u}$. Straightforward by i.h.. 4. 4.

Right of an application, $\mathtt{C}=u[\bar{r}_{1},\mathtt{C}^{\prime},\bar{r}_{2}]$. Straightforward by i.h..

0.A.1.2 Substitution preserves correctness

More precisely, let us show that if $\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle$ is correct then $\mathtt{C}\langle t\{x:=\bar{s}\}\rangle$ is correct. By induction on $\mathtt{C}$:

Empty, $\mathtt{C}=\Box$.

Let $\bar{s}=[s_{1},\ldots,s_{n}]$. Observe that if $(\lambda^{\ell}x.t)[s_{1},\ldots,s_{n}]$ is correct then:

• •

[c1] $\Gamma\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}\vdash t:\mathcal{A}$ and $\Delta_{i}\vdash s_{i}:\mathcal{B}_{i}$ are derivable for all $i=1..n$,

• •

[c2] $t,s_{1},\ldots,s_{n}$ are correct,

• •

[c3] there are no free occurrences of $x$ among $s_{1},\ldots,s_{n}$,

• •

[c4] all the lambdas occurring in $t,s_{1},\ldots,s_{n}$ have pairwise distinct labels,

• •

[c5] $\Gamma+_{i=1}^{n}\Delta_{i}$ is a sequential context.

Condition [c1] holds by inversion of the typing rules, condition [c2] holds by Lem. 7, condition [c3] holds by Barendregt’s convention, and conditions [c4] and [c5] hold because the source term is supposed to be correct.

By induction on $t$, we check that if $(\lambda^{\ell}x.t)[s_{1},\ldots,s_{n}]$ is correct, then $t\{x:=\bar{s}\}$ is correct.

1. 1.1

Variable (same), $t=x^{\mathcal{A}}$, $\bar{s}=[s]$. Note that $t\{x:=\bar{s}\}=s$. Conclude by [c2]. 2. 1.2

Variable (different), $t=y^{\mathcal{A}}$, $\bar{s}=[]$ with $x\neq y$. Note that $t\{x:=\bar{s}\}=y^{\mathcal{A}}$. Conclude by [c2]. 3. 1.3

Abstraction, $t=\lambda^{\ell^{\prime}}y.u$.

Then $\mathcal{A}=\mathcal{M}\overset{\ell^{\prime}}{\to}\mathcal{C}$ and by inversion $\Gamma\oplus y:\mathcal{M}\vdash u:\mathcal{C}$ is derivable. Note that $(\lambda^{\ell}x.u)\bar{s}$ is correct, so by i.h. $u\{x:=\bar{s}\}$ is correct. The variable $y$ does not occur free in $\bar{s}$, so $(\Gamma\oplus y:\mathcal{M})+_{i=1}^{n}\Delta_{i}=(\Gamma+_{i=1}^{n}\Delta_{i})\oplus(y:\mathcal{M})$. Let us check that $\lambda^{\ell^{\prime}}y.u\{x:=\bar{s}\}$ is correct:

1. 1.3.1

Uniquely labeled lambdas. Let $\ell_{1}$ and $\ell_{2}$ be two labels decorating different lambdas of $\lambda^{\ell^{\prime}}y.u\{x:=\bar{s}\}$, and let us show that $\ell_{1}\neq\ell_{2}$. There are two subcases, depending on whether one of the labels decorates the outermost lambda:

1. 1.3.1.1

If $\ell_{1}$ or $\ell_{2}$ decorates the outermost lambda. Suppose without loss of generality that $\ell_{1}=\ell^{\prime}$ is the label decorating the outermost lambda. Then by Lem. 9, there are two cases: either $\ell_{2}$ decorates a lambda of $u$, or $\ell_{2}$ decorates a lambda of some term in the list $\bar{s}$. If $\ell_{2}$ decorates a lambda of $u$, then $\ell_{1}\neq\ell_{2}$ since we knew that $\lambda^{\ell^{\prime}}y.u$ was a correct term by [c2]. If $\ell_{2}$ decorates a lambda of some term in the list $\bar{s}$, then $\ell_{1}\neq\ell_{2}$ by condition [c4]. 2. 1.3.1.2

If $\ell_{1}$ and $\ell_{2}$ do not decorate the outermost lambda. Then $\ell_{1}$ and $\ell_{2}$ decorate different lambdas of the term $u\{x:=\bar{s}\}$, and we conclude by i.h.. 2. 1.3.2

Sequential contexts.

Let $t^{\prime}$ be a subterm of $\lambda^{\ell^{\prime}}x.u\{x:=\bar{s}\}$. If $t^{\prime}$ is a subterm of $u\{x:=\bar{s}\}$, we conclude by i.h.. Otherwise $t^{\prime}$ is the whole term and the context is $\Gamma+_{i=1}^{n}\Delta_{i}$, which is sequential by hypothesis [c5]. 3. 1.3.3

Sequential types.

Let $t^{\prime}$ be a subterm of $\lambda^{\ell^{\prime}}x.u\{x:=\bar{s}\}$. If $t^{\prime}$ is a subterm of $u\{x:=\bar{s}\}$, we conclude by i.h.. Otherwise $t^{\prime}$ is the whole term. Then $\Gamma+_{i=1}^{n}\Delta_{i}\vdash t^{\prime}:\mathcal{A}$ is derivable, since we have already shown that substitution preserves typing. Let $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}$ be a type such that $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\Gamma+_{i=1}^{n}\Delta_{i}$ or $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\mathcal{A}$, and let us show that $\mathcal{N}$ is sequential. In the first case, i.e. if $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\Gamma+_{i=1}^{n}\Delta_{i}$ holds, then either $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\Gamma$ or $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\Delta_{i}$ for some $i=1..n$, and we have that $\mathcal{N}$ is sequential because all the terms $t,s_{1},\ldots,s_{n}$ are correct by [c2]. In the second case, i.e. if $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}\preceq\mathcal{A}$ holds, then we have that $\mathcal{N}$ is sequential because $t$ is correct by [c2]. 4. 1.4

Application, $t=u\,\bar{r}$.

Let $\bar{r}=[r_{1},\ldots,r_{m}]$. Note that $(\lambda^{\ell}x.u)\bar{s}_{0}$ is correct and $(\lambda^{\ell}x.r_{j})\bar{s}_{j}$ is correct for all $j=1..m$, which means that we may apply the i.h. in all these cases. Let us show that $u[r_{j}]_{j=1}^{m}\{x:=\bar{s}\}$ is correct:

1. 1.4.1

Uniquely labeled lambdas. Let $\ell_{1}$ and $\ell_{2}$ be two labels decorating different lambdas of $u[r_{j}]_{j=1}^{m}\{x:=\bar{s}\}$, and let us show that $\ell_{1}\neq\ell_{2}$. Observe that the term $u[r_{j}]_{j=1}^{m}\{x:=\bar{s}\}=u\{x:=\bar{s}_{0}\}[r_{j}\{x:=\bar{s}_{j}\}]_{j=1}^{m}$ has $m+1$ immediate subterms, namely $u\{x:=\bar{s}_{0}\}$ and $r_{j}\{x:=\bar{s}_{j}\}$ for each $j=1..m$. We consider two subcases, depending on whether $\ell_{1}$ and $\ell_{2}$ decorate two lambdas in the same immediate subterm or in different immediate subterms.

1. 1.4.1.1

The labels $\ell_{1}$ and $\ell_{2}$ decorate the same immediate subterm. That is, $\ell_{1}$ and $\ell_{2}$ both decorate lambdas in $u\{x:=\bar{s}_{0}\}$ or both decorate lambdas in some $r_{j}\{x:=\bar{s}_{j}\}$ for some $j=1..m$. Then we conclude, since both $u\{x:=\bar{s}_{0}\}$ and the $r_{j}\{x:=\bar{s}_{j}\}$ are correct by i.h.. 2. 1.4.1.2

The labels $\ell_{1}$ and $\ell_{2}$ decorate different subterms. Let $r_{0}:=u$. Then we have that $\ell_{1}$ decorates a lambda in $r_{j}\{x:=\bar{s}_{j}\}$ for some $j=0..m$ and $\ell_{2}$ decorates a lambda in $r_{k}\{x:=\bar{s}_{k}\}$ for some $k=0..m$, $j\neq k$. By Lem. 9, $\ell_{1}$ decorates a lambda in $r_{j}$ or a lambda in a term of the list $\bar{s}_{j}$, and similarly $\ell_{2}$ decorates a lambda in $r_{k}$ or a lambda in a term of the list $\bar{s}_{k}$. This leaves four possibilities, which are all consequence of [c4]. 2. 1.4.2

Sequential contexts. Similar to item 1.3.2. 3. 1.4.3

Sequential types. Similar to item 1.3.3. 2. 2.

Under an abstraction, $\mathtt{C}=\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}$. Note that $\Gamma\vdash\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle:\mathcal{M}\overset{\ell^{\prime}}{\to}\mathcal{A}$ is derivable. Let us check the three conditions to see that $\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ is correct:

1. 2.1

Uniquely labeled lambdas. Any two lambdas in $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ have different labels by i.h.. We are left to check that $\ell^{\prime}$ does not decorate any lambda in $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$. Let $\ell_{1}$ be a label that decorates a lambda in $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$. Then we have that $\ell_{1}$ decorates a lambda in $\mathtt{C}^{\prime}$, or it decorates a lambda in $t\{x:=\bar{s}\}$. By what we proved in item 1 this in turn means that it decorates a lambda in $t$ or a lambda in some of the terms of the list $\bar{s}$. In any of these cases we have that $\ell_{1}\neq\ell^{\prime}$ since $\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle$ is correct. 2. 2.2

Sequential contexts. Let $t^{\prime}$ be a subterm of $\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ and let us check that its typing context is sequential. If $t^{\prime}$ is a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ we conclude by i.h.. We are left to check the property for $t^{\prime}$ being the whole term, i.e. that $\Gamma$ is sequential. By i.h., $\Gamma\oplus y:\mathcal{M}$ is sequential, which implies that $\Gamma$ is sequential. 3. 2.3

Sequential types. Let $t^{\prime}$ be a subterm of $\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ and let us check that, if $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}$ is any type occurring in the typing context or in the type of $t^{\prime}$, then $\mathcal{N}$ is sequential. If $t^{\prime}$ is a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ we conclude by i.h.. We are left to check the property for $t^{\prime}$ being the whole term.

If $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\Gamma$, then $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\Gamma\oplus y:\mathcal{N}$ which is the type of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$, so by i.h. $\mathcal{N}$ is sequential.

If $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\mathcal{M}\overset{\ell^{\prime\prime}}{\to}\mathcal{A}$, there are three subcases:

1. 2.3.1

If $\mathcal{N}=\mathcal{M}$, then note that $\mathcal{M}$ is sequential because $\Gamma\oplus y:\mathcal{M}$ is the typing context of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$, which is sequential by i.h.. 2. 2.3.2

If $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\mathcal{B}$ where $\mathcal{B}$ is one of the types of $\mathcal{M}$, then $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\mathcal{M}\overset{\ell^{\prime\prime}}{\to}\mathcal{A}$ which is the typing context of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$, and we conclude for this term has sequential types by i.h.. 3. 2.3.3

If $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}\preceq\mathcal{A}$, note that $\mathcal{A}$ is the type of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$, and we conclude for this term has sequential types by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}\bar{u}$.

Note that $\Gamma\vdash\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle:[\mathcal{B}_{j}]_{j=1}^{m}\overset{\ell^{\prime}}{\to}\mathcal{A}$ is derivable. Moreover the list of arguments is of the form $\bar{u}=[u_{1},\ldots,u_{m}]$ where all the $u_{j}$ are correct and $\Delta_{j}\vdash u_{j}:\mathcal{B}_{j}$ is derivable for all $j=1..m$. Then $\Gamma+_{j=1}^{m}\Delta_{j}\vdash\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle[u_{j}]_{j=1}^{m}:\mathcal{A}$ is derivable. Let us check the three conditions to see that $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle[u_{j}]_{j=1}^{m}$ is correct:

1. 3.1

Uniquely labeled lambdas. Let $\ell_{1}$ and $\ell_{2}$ be two labels decorating different lambdas in $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle[u_{j}]_{j=1}^{m}$. There are three subcases.

1. 3.1.1

If $\ell_{1}$ and $\ell_{2}$ both decorate lambdas in the subterm $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ then $\ell_{1}\neq\ell_{2}$ since $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ is correct by i.h.. 2. 3.1.2

If $\ell_{1}$ and $\ell_{2}$ both decorate lambdas somewhere in $[u_{1},\ldots,u_{m}]$ then $\ell_{1}\neq\ell_{2}$ since $\mathtt{C}^{\prime}\langle t\rangle[u_{1},\ldots,u_{m}]$ is correct by hypothesis. 3. 3.1.3

If $\ell_{1}$ decorates a lambda in $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ and $\ell_{2}$ decorates a lambda in one of the terms $u_{j}$ for some $j=1..m$, then note that $\ell_{1}$ must either decorate a lambda in $\mathtt{C}^{\prime}$ or a lambda in $t\{x:=\bar{s}\}$. By what we proved in item 1 this in turn means that it decorates a lambda in $t$ or a lambda in some of the terms of the list $\bar{s}$. In any of these cases we have that $\ell_{1}\neq\ell_{2}$ since $\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle[u_{j}]_{j=1}^{m}$ is correct by hypothesis. 2. 3.2

Sequential contexts. Let $t^{\prime}$ be a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle[u_{j}]_{j=1}^{m}$ and let us show that its typing context is sequential. If $t^{\prime}$ is a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ we conclude by i.h.. If $t^{\prime}$ is a subterm of one of the $u_{j}$ for some $j=1..m$, we conclude using that $u_{j}$ is correct by hypothesis. It remains to check that the whole term is correct, i.e. that $\Gamma+_{j=1}^{m}\Delta_{j}$ is sequential. Observe that $\Gamma+_{j=1}^{m}\Delta_{j}$ is also the typing context of $\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle[u_{j}]_{j=1}^{m}$, which is correct by hypothesis. 3. 3.3

Sequential types. Let $t^{\prime}$ be a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle[u_{j}]_{j=1}^{m}$ and let us show if $\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{C}$ is a type that occurs in the typing context or in the type of $t^{\prime}$, then $\mathcal{N}$ is sequential. If $t^{\prime}$ is a subterm of $\mathtt{C}^{\prime}\langle t\{x:=\bar{s}\}\rangle$ we conclude by i.h.. If $t^{\prime}$ is a subterm of one of the $u_{j}$ for some $j=1..m$, we conclude using that $u_{j}$ is correct by hypothesis. We are left to check the property for $t^{\prime}$ being the whole term.

If $\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{C}\preceq\Gamma+_{j=1}^{m}\Delta_{j}$, we conclude by observing that $\Gamma+_{j=1}^{m}\Delta_{j}$ is also the typing context of $\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle[u_{j}]_{j=1}^{m}$, which is correct by hypothesis, so it has sequential types.

Similarly, if $\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{C}\preceq\mathcal{A}$, we conclude by observing that $\mathcal{A}$ is also the type of $\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle[u_{j}]_{j=1}^{m}$. 4. 4.

Right of an application, $\mathtt{C}=u[\bar{r}_{1},\mathtt{C}^{\prime},\bar{r}_{2}]$. Similar to item 3.

0.A.2 Proof of Lem. 2 – Substitution Lemma

Let us prove that $t\{x:=\bar{s}\}\{y:=\bar{u}\}=t\{y:=\bar{u}_{1}\}\{x:=\bar{s}\{y:=\bar{u}_{2}\}\}$ by induction on $t$. The interesting case is the application. Let $t=r[r_{1},\ldots,r_{n}]$. Then:

[TABLE]

Given that $\sum_{i=0}^{n}\bar{s}_{i}$ is a permutation of $\bar{s}$, by defining $\bar{v}_{2}:=\sum_{i=0}^{n}\bar{u}_{i,2}$, the last term equals $(r\{y:=\bar{u}_{0,1}\}[r_{i}\{y:=\bar{u}_{i,1}\}]_{i=0}^{n})\{x:=\bar{s}\{y:=\bar{v}_{2}\}\}$. Finally, by defining $\bar{v}_{1}:=\sum_{i=0}^{n}\bar{u}_{i,1}$, we obtain $(r[r_{1},\ldots,r_{n}])\{y:=\bar{v}_{1}\}\{x:=\bar{s}\{y:=\bar{v}_{2}\}\}$. To conclude observe that $\bar{v}_{1}+\bar{v}_{2}$ is indeed a permutation of $\bar{u}$:

[TABLE]

where $\bar{x}\approx\bar{y}$ is the equivalence relation on lists that holds whenever $\bar{x}$ is a permutation of $\bar{y}$.

0.A.3 Proof of Prop. 2 – Permutation

Let us extend the operation of substitution to operate on contexts by declaring that $\mathtt{T}_{x}(\Box)=[\,]$ and $\Box\{x:=[\,]\}=\Box$. We need two auxiliary lemmas:

Lemma 10 (Substitution lemma for contexts)

If both sides of the equation are defined and $(\bar{s}_{1},\bar{s}_{2})$ is a partition of $\bar{s}$ then $\mathtt{C}\langle t\rangle\{x:=\bar{s}\}=\mathtt{C}\{x:=\bar{s_{1}}\}\langle t\{x:=\bar{s}_{2}\}\rangle$.

Proof

The proof is similar to the Substitution Lemma, by induction on $\mathtt{C}$.

Lemma 11 (Reduction inside a substitution)

Let $1\leq i\leq n$ and $s_{i}\overset{\ell}{\to}s^{\prime}_{i}$. Then:

[TABLE]

.

Proof

Straightforward by induction on $s$.

The proof of Prop. 2 proceeds as follows. Let $R:t_{0}\mathrel{\xrightarrow{\ell}_{\texttt{{\#}}}}t_{1}$ and $S:t_{0}\mathrel{\xrightarrow{\ell^{\prime}}_{\texttt{{\#}}}}t_{2}$ be coinitial steps, and let us show that the diagram may be closed. The step $R$ is of the form $t_{0}=\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle\mathrel{\xrightarrow{\ell}_{\texttt{{\#}}}}\mathtt{C}\langle t\{x:=\bar{s}\}\rangle=t_{1}$. Recall that $R\neq S$ by hypothesis. We proceed by induction on $\mathtt{C}$.

Empty context, $\mathtt{C}=\Box$. Then $R:t_{0}=(\lambda^{\ell}x.t)\bar{s}\mathrel{\xrightarrow{\ell}_{\texttt{{\#}}}}t\{x:=\bar{s}\}=t_{1}$. There are two subcases, depending on whether the pattern of $S$ is inside $t$ or inside $\bar{s}$:

1. 1.1

The pattern of $S$ is in $t$.

Using Lem. 10, the situation is:

[TABLE]

where $(\bar{s}_{1},\bar{s}_{2},\bar{s}_{3})$ and $(\bar{s}_{1},\bar{s}_{4})$ are partitions of $\bar{s}$. Note that $(\bar{s}_{2},\bar{s}_{3})$ is a partition of $\bar{s}_{4}$, so it suffices to show that $r\{y:=\bar{u}\}\{x:=\bar{s}_{4}\}=r\{x:=\bar{s}_{2}\}\{y:=\bar{u}\{x:=\bar{s}_{3}\}\}$, which is an immediate consequence of the Substitution Lemma (Lem. 2). 2. 1.2

The pattern of $S$ is inside $\bar{s}$.

In this case, $\bar{s}=[\bar{s}_{1},\mathtt{C}\langle(\lambda^{\ell^{\prime}}y.r)\bar{u}\rangle,\bar{s}_{2}]$.

[TABLE]

The arrow of the bottom of the diagram exists as a consequence of Lem. 11. 2. 2.

Under an abstraction, $\mathtt{C}=\lambda^{\ell^{\prime\prime}}y.\mathtt{C}^{\prime}$. Straightforward by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}\bar{u}$. There are three subcases, depending on whether the redex $S$ is at the root, to the left of the application, or to the right of the application.

1. 3.1

The pattern of $S$ is at the root. Then $\mathtt{C}^{\prime}\langle(\lambda^{\ell^{\prime}}x.t)\bar{s}\rangle$ must have a lambda at the root, so it is of the form $\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime\prime\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle$. Hence, the starting term is $(\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime\prime\prime}\langle(\lambda^{\ell}x.t)\bar{s}\rangle)\bar{u}$. The symmetric case has already been studied in item 1.1. 2. 3.2

The pattern of $S$ is inside $\mathtt{C}^{\prime}$. Straightforward by i.h.. 3. 3.3

The pattern of $S$ is inside $\bar{u}$. It is immediate to close the diagram since the steps are at disjoint positions:

[TABLE] 4. 4.

Right of an application, $\mathtt{C}=r[u_{1},\ldots,u_{i-1},\mathtt{C}^{\prime},u_{i+1},\ldots,u_{n}]$. There are four subcases, depending on whether the redex $S$ is at the root, to the left of the application (that is, inside $r$), or to the right of the application (that is, either inside $\mathtt{C}^{\prime}$ or $u_{j}$ for some $j$).

1. 4.1

The pattern of $S$ is at the root. Then $r$ has a lambda at the root, i.e. it is of the form $\lambda^{\ell^{\prime}}y.u$. Hence the starting term is $(\lambda^{\ell^{\prime}}y.u)[u_{1:i-1},\mathtt{C}^{\prime}\langle(\lambda^{\ell}x.t)s\rangle,u_{i+1:n}]$. The symmetric case has already been studied in item 1.2. 2. 4.2

The pattern of $S$ is inside $r$. The steps are disjoint, so it is immediate. 3. 4.3

The pattern of $S$ is inside $u_{j}$ for some $j\neq i$. The steps are disjoint, so it is immediate. 4. 4.4

The pattern of $S$ is inside $\mathtt{C}^{\prime}$. Straightforward by i.h..

0.A.4 Full Stability

In this section, we state and prove a strong version of Stability in the sense of Lévy [26], called Full Stability (Lem. 15). This lemma is crucial in establishing that $\mathbb{D}^{\texttt{{\#}}}(t)$ forms a distributive lattice (Prop. 4). First we need a few auxiliary results:

Definition 14 (Alternative Substitution)

An alternative definition for capture-avoiding substitution, written $t\{\!\!\{x:=\bar{s}\}\!\!\}$, may be defined as follows, provided that $\mathtt{T}_{x}(t)\subseteq\mathtt{T}(\bar{s})$ and the multiset of types of $\bar{s}=[s_{1},\ldots,s_{m}]$ is sequential:

[TABLE]

Moreover, $[t_{1},\ldots,t_{n}]\{\!\!\{x:=\bar{s}\}\!\!\}$ stands for $[t_{1}\{\!\!\{x:=\bar{s}\}\!\!\},\ldots,t_{n}\{\!\!\{x:=\bar{s}\}\!\!\}]$, whenever each substitution $t_{i}\{\!\!\{x:=\bar{s}\}\!\!\}$ is well-defined.

Lemma 12

Let $t,\bar{s},\bar{u}$ be correct terms such that $\mathtt{T}_{x}(t)=\mathtt{T}(\bar{s})$ and suppose that $\bar{s}$ is contained in $\bar{u}$, i.e. there exists a list $\bar{r}$ such that $(\bar{s},\bar{r})$ is a partition of $\bar{u}$. Then $t\{x:=\bar{s}\}=t\{\!\!\{x:=\bar{u}\}\!\!\}$.

Proof

Straightforward by induction on $t$.

Lemma 13 (Creation)

If $R$ creates $S$ then it is according to one of the following cases:

[crI]: $\mathtt{C}\langle(\lambda^{\ell}x.x^{\mathcal{A}})\,[\lambda^{\ell^{\prime}}y.t]\,\bar{s}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle(\lambda^{\ell^{\prime}}y.t)\,\bar{s}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle t\{\!\!\{y:=\bar{s}\}\!\!\}\rangle$. 2. 2.

[crII]: $\mathtt{C}\langle(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.t)\,\bar{s}\,\bar{u}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle(\lambda^{\ell^{\prime}}y.t^{\prime})\,\bar{u}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle t^{\prime}\{\!\!\{y:=\bar{u}\}\!\!\}\rangle$, where $t^{\prime}=t\{\!\!\{x:=\bar{s}\}\!\!\}$. 3. 3.

[crIII]: $\mathtt{C}_{1}\langle(\lambda^{\ell}x.\mathtt{C}_{2}\langle x^{\mathcal{A}}\,\bar{t}\rangle)\bar{s}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}_{1}\langle\mathtt{C}^{\prime}_{2}\langle(\lambda^{\ell^{\prime}}y.u)\,\bar{t^{\prime}}\rangle\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}_{1}\langle\mathtt{C}^{\prime}_{2}\langle u\{\!\!\{y:=\bar{t^{\prime}}\}\!\!\}\rangle\rangle$, where

[TABLE]

Proof

Let $R:\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle$ be a step, and let $S:\mathtt{C}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle\mathrel{\to_{\texttt{{\#}}}}p$ another step such that $R$ creates $S$. The redex contracted by the step $S$ is below a context $\mathtt{C}_{1}$, so let $\mathtt{C}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle=\mathtt{C}_{1}\langle(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle$, where $(\lambda^{\ell^{\prime}}y.u)\bar{r}$ is the redex contracted by $S$. We consider three cases, depending on the relative positions of the holes of $\mathtt{C}$ and $\mathtt{C}_{1}$, namely they may be disjoint, $\mathtt{C}$ may be a prefix of $\mathtt{C}_{1}$, or $\mathtt{C}_{1}$ may be a prefix of $\mathtt{C}$:

If the holes of $\mathtt{C}$ and $\mathtt{C}_{1}$ are disjoint. Then there is a two-hole context $\hat{\mathtt{C}}$ such that $\mathtt{C}=\hat{\mathtt{C}}\langle\Box,(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle$ and $\mathtt{C}_{1}=\hat{\mathtt{C}}\langle t\{\!\!\{x:=\bar{s}\}\!\!\},\Box\rangle$. So $\hat{\mathtt{C}}\langle(\lambda^{\ell}x.t)\bar{s},(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\hat{\mathtt{C}}\langle t\{\!\!\{x:=\bar{s}\}\!\!\},(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\hat{\mathtt{C}}\langle t\{\!\!\{x:=\bar{s}\}\!\!\},u\{\!\!\{y:=r\}\!\!\}\rangle$. Observe that $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible. 2. 2.

If $\mathtt{C}$ is a prefix of $\mathtt{C}_{1}$. Then there exists a context $\mathtt{C}_{2}$ such that $\mathtt{C}_{1}=\mathtt{C}\langle\mathtt{C}_{2}\rangle$, and we have that $t\{\!\!\{x:=\bar{s}\}\!\!\}=\mathtt{C}_{2}\langle(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle$. We consider two subcases, depending on whether the position of the hole $\mathtt{C}_{2}$ lies inside the term $t$, or it reaches a free occurrence of $x$ in $t$ and “jumps” to one of the arguments in the list $\bar{s}$.

1. 2.1

If the position of the hole of $\mathtt{C}_{2}$ lies in $t$. More precisely, there is a context $\mathtt{C}^{\prime}_{2}$ and a term $t^{\prime}$ such that: $t=\mathtt{C}^{\prime}_{2}\langle t^{\prime}\rangle$, $\mathtt{C}_{2}=\mathtt{C}^{\prime}_{2}\{\!\!\{x:=\bar{s}\}\!\!\}$, and $(\lambda^{\ell^{\prime}}y.u)\bar{r}=t^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\}$. We consider three further subcases for the term $t^{\prime}$. It cannot be an abstraction, so it may be a variable $x^{\mathcal{A}}$, or an application. Besides, if it is an application, the head may be a variable $x^{\mathcal{A}}$ or an abstraction.

1. 2.1.1

Variable, i.e. $t^{\prime}=x^{\mathcal{A}}$. Then the list $\bar{s}$ may be split as $\bar{s}=[\bar{s_{1}},(\lambda^{\ell^{\prime}}y.u)\bar{r},\bar{s_{2}}]$, and: $\mathtt{C}\langle(\lambda^{\ell}x.\mathtt{C}^{\prime}_{2}\langle x^{\mathcal{A}}\rangle)[\bar{s_{1}},(\lambda^{\ell^{\prime}}y.u)\bar{r},\bar{s_{2}}]\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle u\{\!\!\{y:=\bar{r}\}\!\!\}\rangle\rangle$. Observe that $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible. 2. 2.1.2

Application of a variable, i.e. $t^{\prime}=x^{\mathcal{A}}\,\bar{r^{\prime}}$. Given that $(\lambda^{\ell^{\prime}}y.u)\bar{r}=t^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\}$, we have $\bar{r}=\bar{r^{\prime}}\{\!\!\{x:=\bar{s}\}\!\!\}$, and the list $\bar{s}$ may be split as $\bar{s}=[\bar{s_{1}},\lambda^{\ell^{\prime}}y.u,\bar{s_{2}}]$. Then $\mathtt{C}\langle(\lambda^{\ell}x.\mathtt{C}_{2}^{\prime}\langle x^{\mathcal{A}}\,\bar{r^{\prime}}\rangle)[\bar{s_{1}},\lambda^{\ell^{\prime}}y.u,\bar{s_{2}}]\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle(\lambda^{\ell^{\prime}}y.u)\,\bar{r}\rangle\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle u\{\!\!\{y:=\bar{r}\}\!\!\}\rangle\rangle$, and we are in the situation of [crIII]. 3. 2.1.3

Application of an abstraction, i.e. $t^{\prime}=(\lambda^{\ell}y.u^{\prime})\,\bar{r^{\prime}}$. Given that $(\lambda^{\ell^{\prime}}y.u)\bar{r}=t^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\}$, we have $\bar{u}=\bar{u^{\prime}}\{\!\!\{x:=\bar{s}\}\!\!\}$ and $\bar{r}=\bar{r^{\prime}}\{\!\!\{x:=\bar{s}\}\!\!\}$. Then: $\mathtt{C}\langle(\lambda^{\ell}x.\mathtt{C}_{2}^{\prime}\langle(\lambda^{\ell}y.u^{\prime})\,\bar{r^{\prime}}\rangle)\bar{s}\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle(\lambda^{\ell}y.u)\,\bar{r}\rangle\rangle\ \mathrel{\to_{\texttt{{\#}}}}\ \mathtt{C}\langle\mathtt{C}_{2}\langle u\{\!\!\{z:=\bar{r}\}\!\!\}\rangle\rangle$. Then $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible. 2. 2.2

If the position of the hole of $\mathtt{C}_{2}$ “jumps” through a free occurrence of $x$. More precisely, there exist $\mathtt{C}_{3}$, $\mathcal{A}$, $\bar{s_{1}}$, $\bar{s_{2}}$, and $\mathtt{C}_{4}$ such that: $t=\mathtt{C}_{3}\langle x^{\mathcal{A}}\rangle\hskip 14.22636pt\bar{s}=[\bar{s_{1}},\mathtt{C}_{4}\langle(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle,\bar{s_{2}}]$ in such a way that $\mathtt{T}(\mathtt{C}_{4}\langle(\lambda^{\ell^{\prime}}y.u)\bar{r}\rangle)=\mathtt{T}_{x}(x^{\mathcal{A}})$, and $\mathtt{C}_{2}=\mathtt{C}_{3}\{\!\!\{x:=\bar{s}\}\!\!\}\langle\mathtt{C}_{4}\rangle$. Then:

[TABLE]

Then $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible. 3. 3.

If $\mathtt{C}_{1}$ is a prefix of $\mathtt{C}$. Then there exists a context $\mathtt{C}_{2}$ such that $\mathtt{C}=\mathtt{C}_{1}\langle\mathtt{C}_{2}\rangle$. This means that $\mathtt{C}_{2}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle=(\lambda^{\ell^{\prime}}y.u)\bar{r}$. We consider three subcases, depending on whether $\mathtt{C}_{2}$ is empty, or the hole of $\mathtt{C}_{2}$ lies to the left or to the right of the application.

1. 3.1

Empty, $\mathtt{C}_{2}=\Box$. Then $\mathtt{C}=\mathtt{C}_{1}$ so $\mathtt{C}$ is a prefix of $\mathtt{C}_{1}$. We have already considered this case. 2. 3.2

Left, $\mathtt{C}_{2}=\mathtt{C}^{\prime}_{2}\,\bar{r}$. Then the step $R$ is of the form $R:\mathtt{C}_{1}\langle\mathtt{C}^{\prime}_{2}\langle(\lambda^{\ell}x.t)\bar{s}\rangle\,\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}_{1}\langle\mathtt{C}^{\prime}_{2}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle\,\bar{r}\rangle$. In particular we know that $\mathtt{C}^{\prime}_{2}\langle t\{\!\!\{x:=\bar{s}\}\!\!\}\rangle=\lambda^{\ell^{\prime}}y.u$. There are two cases, depending on whether $\mathtt{C}^{\prime}_{2}$ is empty or non-empty.

1. 3.2.1

Empty, $\mathtt{C}^{\prime}_{2}=\Box$ Then we have that $t\{\!\!\{x:=\bar{s}\}\!\!\}=\lambda^{\ell^{\prime}}y.u$. We consider two further subcases, depending on whether $t$ is an occurrence of the variable $x$.

1. 3.2.1.1

If $t=x^{\mathcal{A}}$ for some type $\mathcal{A}$. Then the list $\bar{s}$ must be of the form $[\lambda^{\ell^{\prime}}y.u]$ where the external label of $\mathcal{A}$ is precisely $\ell^{\prime}$. Then $\mathtt{C}_{1}\langle(\lambda^{\ell}x.x^{\mathcal{A}})[\lambda^{\ell^{\prime}}y.u]\,\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}_{1}\langle(\lambda^{\ell^{\prime}}y.u)\,\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}_{1}\langle u\{\!\!\{y:=\bar{r}\}\!\!\}\rangle$, and we are in the situation of [crI]. 2. 3.2.1.2

If $t\neq x^{\mathcal{A}}$ for any type $\mathcal{A}$. Then $t$ must be an abstraction, namely $t=\lambda^{\ell^{\prime}}y.u^{\prime}$ where $u^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\}=u$. Then $\mathtt{C}_{1}\langle(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.u^{\prime})\,\bar{s}\,\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}_{1}\langle(\lambda^{\ell^{\prime}}y.u^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\})\,\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}_{1}\langle u^{\prime}\{\!\!\{x:=\bar{s}\}\!\!\}\{\!\!\{y:=\bar{r}\}\!\!\}\rangle$, and we are in the situation of [crII]. 2. 3.2.2

Non-empty, $\mathtt{C}^{\prime}_{2}\neq\Box$ Then necessarily $\mathtt{C}^{\prime}_{2}$ must be an abstraction, namely $\mathtt{C}^{\prime}_{2}=\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime\prime}_{2}$. Then:

[TABLE]

Then $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible. 3. 3.3

Right, $\mathtt{C}_{2}=(\lambda^{\ell^{\prime}}y.u)[\bar{r}_{1},\mathtt{C}^{\prime}_{2},\bar{r}_{2}]$. Then:

[TABLE]

Then $S$ has an ancestor $S_{0}$, contradicting the hypothesis that $R$ creates $S$. So this case is impossible.

Lemma 14 (Basic Stability)

Let $R\neq S$. If $T_{3}\in T_{1}/(S/R)$ and $T_{3}\in T_{2}/(R/S)$ then there exists a step $T_{0}$ such that $T_{1}\in T_{0}/R$ and $T_{2}\in T_{0}/S$.

Proof

We prove an equivalent statement. Namely, we prove that if $R,S$ are different coinitial steps such that $R$ creates a step $T$, then $R/S$ creates the step $T/(S/R)$. It is easy to see that these are equivalent since in $\lambda^{\texttt{{\#}}}$ there is no erasure or duplication.

Let $R:\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}\langle t\{x:=\bar{s}\}\rangle$, let $S\neq R$ be a step coinitial to $R$, and suppose that $R$ creates a step $T$. By induction on the context $\mathtt{C}$ we argue that $R/S$ creates $T/(S/R)$.

Empty context, $\mathtt{C}=\Box$. Then $R:(\lambda^{\ell}x.t)\bar{s}\mathrel{\to_{\texttt{{\#}}}}t\{\!\!\{x:=\bar{s}\}\!\!\}$. There are two cases for $S$, depending on whether it is internal to $t$ or internal to one of the arguments of the list $\bar{s}$.

1. 1.1

If $S$ is internal to $t$. Then $t=\mathtt{C}_{1}\langle\Sigma\rangle$ where $\Sigma$ is the redex contracted by $S$. Let $\Sigma^{\prime}$ denote the contractum of $\Sigma$. Then:

[TABLE]

By Creation (Lem. 13), $T$ must be created by [crIII], since there are no applications surrounding the subterm contracted by $R$. This means that $\mathtt{C}_{1}\langle\Sigma\rangle=\mathtt{C}_{2}\langle x^{\mathcal{A}}\,\bar{u}\rangle$ where, moreover, $\bar{s}$ may be split as $[\bar{s}_{1},\lambda^{\ell^{\prime}}y.r,\bar{s}_{2}]$ in such a way that $\ell^{\prime}$ is the external label of $\mathcal{A}$. We consider three subcases, depending on whether the contexts $\mathtt{C}_{1}$ and $\mathtt{C}_{2}$ are disjoint, $\mathtt{C}_{1}$ is a prefix of $\mathtt{C}_{2}$, or $\mathtt{C}_{2}$ is a prefix of $\mathtt{C}_{1}$.

1. 1.1.1

If $\mathtt{C}_{1}$ and $\mathtt{C}_{2}$ are disjoint. Then there is a two-hole context $\hat{\mathtt{C}}$ such that $\hat{\mathtt{C}}\langle\Box,x^{\mathcal{A}}\bar{u}\rangle=\mathtt{C}_{1}$ and $\hat{\mathtt{C}}\langle\Sigma,\Box\rangle=\mathtt{C}_{2}$. Given any term, context, or list of terms $\mathtt{X}$ let us write $\mathtt{X}^{*}$ to denote $\mathtt{X}\{\!\!\{x:=\bar{s}\}\!\!\}$. Then $R/S$ creates $T/(S/R)$:

[TABLE] 2. 1.1.2

If $\mathtt{C}_{1}$ is a prefix of $\mathtt{C}_{2}$. Then $\mathtt{C}_{2}=\mathtt{C}_{1}\langle\mathtt{C}^{\prime}_{2}\rangle$ which means that $\Sigma=\mathtt{C}^{\prime}_{2}\langle x^{\mathcal{A}}\bar{u}\rangle$. Recall that $\Sigma$ is a redex, so let us write $\Sigma=(\lambda^{\ell^{\prime\prime}}z.p)\bar{q}$. We consider two further subcases, depending on whether the hole of $\mathtt{C}^{\prime}_{2}$ lies to the left or to the right of the application (observe that it cannot be at the root since $\lambda^{\ell^{\prime\prime}}z.p$ is not a variable).

1. 1.1.2.1

If the hole of $\mathtt{C}^{\prime}_{2}$ lies to the left of $(\lambda^{\ell^{\prime\prime}}z.p)\bar{q}$. More precisely, we have that $\mathtt{C}^{\prime}_{2}=(\lambda^{\ell^{\prime\prime}}z.\mathtt{C}^{\prime\prime}_{2})\bar{q}$ and $p=\mathtt{C}^{\prime\prime}_{2}\langle x^{\mathcal{A}}\bar{u}\rangle$. Given any term, context, or list of terms $\mathtt{X}$ let us write $\mathtt{X}^{*}$ to denote $\mathtt{X}\{\!\!\{x:=\bar{s}\}\!\!\}$. Then $R/S$ creates $T/(S/R)$:

[TABLE] 2. 1.1.2.2

If the hole of $\mathtt{C}^{\prime}_{2}$ lies to the right of $(\lambda^{\ell^{\prime\prime}}z.p)\bar{q}$. More precisely, we have that $\mathtt{C}^{\prime}_{2}=(\lambda^{\ell^{\prime\prime}}z.p)[\bar{q}_{1},\mathtt{C}^{\prime\prime}_{2},\bar{q}_{2}]$ and $\bar{q}=[\bar{q}_{1},\mathtt{C}^{\prime\prime}_{2}\langle x^{\mathcal{A}}\,\bar{u}\rangle,\bar{q}_{2}]$. Given any term, context, or list of terms $\mathtt{X}$ let us write $\mathtt{X}^{*}$ to denote $\mathtt{X}\{\!\!\{x:=\bar{s}\}\!\!\}$. Moreover, since parameters are in 1–1 correspondence with arguments, there is exactly one free occurrence of $z$ in $p$ whose type coincides with the type of $\mathtt{C}^{\prime\prime}_{2}\langle x^{\mathcal{A}}\,\bar{u}\rangle$. Let $p=\mathtt{C}_{3}\langle z^{\mathcal{B}}\rangle$ where the hole of $\mathtt{C}_{3}$ marks the position of such occurrence. Then:

[TABLE]

Moreover, if we write $\mathtt{C}^{\prime}_{3}$ for the context $\mathtt{C}_{3}\{\!\!\{z:=\bar{q}\}\!\!\}$:

[TABLE]

by the Substitution Lemma for contexts (Lem. 10). Then:

[TABLE]

The labels of the steps $T$ and $T/(S/R)$ are both $\ell^{\prime}$, which means that $R/S$ creates $T/(S/R)$. 3. 1.1.3

If $\mathtt{C}_{2}$ is a prefix of $\mathtt{C}_{1}$. Then $\mathtt{C}_{1}=\mathtt{C}_{2}\langle\mathtt{C}^{\prime}_{1}\rangle$ which means $x^{\mathcal{A}}\,\bar{u}=\mathtt{C}^{\prime}_{1}\langle\Sigma\rangle$. Since $\Sigma$ is a redex, $\mathtt{C}^{\prime}_{1}$ must be of the form $x^{\mathcal{A}}\,[\bar{u}_{1},\mathtt{C}^{\prime\prime}_{1},\bar{u}_{2}]$ and $\bar{u}=[\bar{u}_{1},\mathtt{C}^{\prime\prime}_{1}\langle\Sigma\rangle,\bar{u}_{2}]$. Given any term, context, or list of terms $\mathtt{X}$ let us write $\mathtt{X}^{*}$ to denote $\mathtt{X}\{\!\!\{x:=\bar{s}\}\!\!\}$. Then: $R/S$ creates $T/(S/R)$:

[TABLE] 2. 1.2

If $S$ is internal to $\bar{s}$. Then $\bar{s}=[\bar{s}_{1},\mathtt{C}_{1}\langle\Sigma\rangle,\bar{s}_{2}]$ where $\Sigma$ is the redex contracted by $S$. Let $\Sigma^{\prime}$ denote the contractum of $\Sigma$. Then:

[TABLE]

By Creation (Lem. 13), $T$ must be created by [crIII], since there are no applications surrounding the subterm contracted by $R$. This means that $t=\mathtt{C}_{2}\langle x^{\mathcal{A}}\,\bar{u}\rangle$, and there is a term in the list $[\bar{s}_{1},\mathtt{C}_{1}\langle\Sigma\rangle,\bar{s}_{2}]$ of the form $\lambda^{\ell^{\prime}}y.r$ such that $\ell^{\prime}$ is also the external label of the type $\mathcal{A}$. There are two subcases, depending on whether such term is $\mathtt{C}_{1}\langle\Sigma\rangle$ or a different term in the list $[\bar{s}_{1},\mathtt{C}_{1}\langle\Sigma\rangle,\bar{s}_{2}]$.

1. 1.2.1

If $\lambda^{\ell^{\prime}}y.r=\mathtt{C}_{1}\langle\Sigma\rangle$. Note that $\mathtt{C}_{1}$ cannot be empty, since this would imply that $\lambda^{\ell^{\prime}}y.r=\Sigma$; however $\Sigma$ is a redex, and in particular an application, so this cannot be the case. Hence the context $\mathtt{C}_{1}$ must be non-empty, i.e. $\mathtt{C}_{1}=\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime}_{1}$ with $r=\mathtt{C}^{\prime}_{1}\langle\Sigma\rangle$. Given any term, context, or list of terms $\mathtt{X}$ let us write $\mathtt{X}^{*}$ to denote $\mathtt{X}\{\!\!\{x:=[\bar{s}_{1},\bar{s}_{2}]\}\!\!\}$. Then $R/S$ creates $T/(S/R)$:

[TABLE] 2. 1.2.2

If $\lambda^{\ell^{\prime}}y.r\neq\mathtt{C}_{1}\langle\Sigma\rangle$. Then $\lambda^{\ell^{\prime}}y.r$ is either one of the terms in the list $\bar{s}_{1}$ or one of the terms in the list $\bar{s}_{2}$. Given any term, context, or list of terms $\mathtt{X}$ let $\mathtt{X}^{*}$ denote $\mathtt{X}\{\!\!\{x:=[\bar{s}_{1},\mathtt{C}_{1}\langle\Sigma\rangle\bar{s}_{2}]\}\!\!\}$ and let $\mathtt{X}^{\dagger}$ denote $\mathtt{X}\{\!\!\{x:=[\bar{s}_{1},\mathtt{C}_{1}\langle\Sigma^{\prime}\rangle\bar{s}_{2}]\}\!\!\}$. Then $R/S$ creates $T/(S/R)$:

[TABLE] 2. 2.

Under an abstraction, $\mathtt{C}=\lambda^{\ell}y.\mathtt{C}^{\prime}$.

Straightforward by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}\bar{u}$. Let $\Delta$ be the redex contracted by $R$, and let $\Delta^{\prime}$ denote its contractum. The step $R$ is of the form $\mathtt{C}^{\prime}\langle\Delta\rangle\bar{u}\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}^{\prime}\langle\Delta^{\prime}\rangle\bar{u}$. We consider three subcases, according to Creation (Lem. 13), depending on whether $T$ is created by [crI], [crII], or [crIII].

1. 3.1

[crI] Then $\mathtt{C}^{\prime}$ is empty and $\Delta$ has the following particular shape: $\Delta=(\lambda^{\ell}x.x^{\mathcal{A}})[\lambda^{\ell^{\prime}}y.r]$. The step $S$ can be either internal to the subterm $r$, or internal to one of the subterms in the list $\bar{u}$. If $S$ is internal to $r$, let $r^{\prime}$ denote the term that results from $r$ after the step $S$. Then:

[TABLE]

Note that $R/S$ creates $T/(S/R)$, as required. If, on the other hand, $S$ is internal to $\bar{u}$, the situation is similar. 2. 3.2

[crII] Then $\mathtt{C}^{\prime}$ is empty and $\Delta$ has the following particular shape: $\Delta=(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r)\,\bar{s}$. The step $S$ can be either internal to $r$, internal to $\bar{s}$, or internal to $\bar{u}$. If $S$ is internal to $r$, let $r^{\prime}$ denote the term that results from $r$ after the step $S$. Then:

[TABLE]

Note that $R/S$ creates $T/(S/R)$, as required. If, on the other hand, $S$ is internal to $\bar{s}$ or $\bar{u}$, the situation is similar. 3. 3.3

[crIII] Recall that the step $R$ is of the form $R:\mathtt{C}^{\prime}\langle\Delta\rangle\,\bar{u}\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}^{\prime}\langle\Delta^{\prime}\rangle\,\bar{u}$. Since the step $T$ is created by [crIII], it does not take place at the root of $\mathtt{C}^{\prime}[\Delta^{\prime}]\,\bar{u}$, but rather it is internal to $\mathtt{C}^{\prime}[\Delta^{\prime}]$. We consider three subcases, depending on whether the step $S$ takes place at the root, to the left of the application or to the right of the application.

1. 3.3.1

If $S$ takes place at the root. Then $\mathtt{C}^{\prime}\langle\Delta\rangle$ is an abstraction, so $\mathtt{C}^{\prime}$ cannot be empty, i.e. we have that $\mathtt{C}^{\prime}=\lambda^{\ell^{\prime}}y.\mathtt{C}^{\prime\prime}$. Moreover, since $T$ is created by [crIII], we have that $\Delta$ has the following specific shape: $\Delta=(\lambda^{\ell}x.\mathtt{C}_{2}\langle x^{\mathcal{A}}\,\bar{r}\rangle)\,\bar{s}$ where $\bar{s}=[\bar{s}_{1},\lambda^{\ell^{\prime\prime}}z.p,\bar{s}_{2}]$ and such that $\ell^{\prime\prime}$ is the external label of $\mathcal{A}$.

Given any term, context, or list of terms $\mathtt{X}$ let $\mathtt{X}^{*}$ denote $\mathtt{X}\{\!\!\{x:=\bar{s}\}\!\!\}$ and let $\mathtt{X}^{\dagger}$ denote $\mathtt{X}\{\!\!\{y:=\bar{u}\}\!\!\}$. Note also that by the Substitution lemma (Lem. 10) we have that $\mathtt{X}^{\dagger}\{\!\!\{x:=\bar{s}^{\dagger}\}\!\!\}={\mathtt{X}^{*}}^{\dagger}$. Then $R/S$ creates $T/(S/R)$:

[TABLE] 2. 3.3.2

If $S$ is internal to $\mathtt{C}^{\prime}\langle\Delta\rangle$. Then it is straightforward by i.h.. 3. 3.3.3

If $S$ is internal to $\bar{u}$.

Then:

[TABLE]

It is immediate to note in this case that $R/S$ creates $T/(S/R)$, since the two-step sequences $RT$ and $(R/S)(T/(S/R))$ are both isomorphic to $\mathtt{C}^{\prime}\langle\Delta\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}^{\prime}\langle\Delta^{\prime}\rangle\mathrel{\to_{\texttt{{\#}}}}p$, only going below different contexts. 4. 4.

Right of an application, $\mathtt{C}=u[\bar{r}_{1},\mathtt{C}^{\prime},\bar{r}_{2}]$. Let $\Delta$ be the redex contracted by $R$, and let $\Delta^{\prime}$ denote its contractum. The step $R$ is of the form $u[\bar{r}_{1},\mathtt{C}^{\prime}\langle\Delta\rangle,\bar{r}_{2}]\mathrel{\to_{\texttt{{\#}}}}u[\bar{r}_{1},\mathtt{C}^{\prime}\langle\Delta^{\prime}\rangle,\bar{r}_{2}]$. We consider three subcases, depending on whether the step $S$ takes place at the root, to the left of the application, or to the right of the application.

1. 4.1

If $S$ takes place at the root. Then $u$ is an abstraction $u=\lambda^{\ell^{\prime}}y.u^{\prime}$. Moreover, since parameters are in 1–1 correspondence with arguments, there is a free occurrence of $y$ in $u^{\prime}$ whose type is also the type of the argument $\mathtt{C}^{\prime}\langle\Delta\rangle$. Let us write $u^{\prime}$ as $u^{\prime}=\mathtt{C}_{1}\langle y^{\mathcal{A}}\rangle$, where the hole of $\mathtt{C}_{1}$ marks the position of such occurrence. Given any term, context, or list of terms $\mathtt{X}$ let $\mathtt{X}^{*}$ denote $\mathtt{X}\{\!\!\{x:=\bar{r}_{1},\bar{r}_{2}\}\!\!\}$. Then:

[TABLE]

So $R/S$ creates $T/(S/R)$, since the two-step sequences $RT$ and $(R/S)(T/(S/R))$ are both isomorphic to $\mathtt{C}^{\prime}\langle\Delta\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}^{\prime}\langle\Delta^{\prime}\rangle\mathrel{\to_{\texttt{{\#}}}}p$, only going below different contexts. 2. 4.2

If $S$ is internal to the left of the application. Then:

[TABLE]

Then since $RT$ and $(R/S)(T/(S/R))$ are isomorphic, it is immediate to conclude, similarly as in item 3.3.3 of this lemma. 3. 4.3

If $S$ is internal to the right of the application. We consider two further subcases, depending on whether $S$ is internal to the argument $\mathtt{C}^{\prime}\langle\Delta\rangle$, or otherwise.

1. 4.3.1

If $S$ is internal to the argument $\mathtt{C}^{\prime}\langle\Delta\rangle$. Then it is straightforward by i.h.. 2. 4.3.2

If $S$ is not internal to the argument $\mathtt{C}^{\prime}\langle\Delta\rangle$. Then it is either internal to $\bar{r}_{1}$ or to $\bar{r}_{2}$. If it is internal to $\bar{r}_{1}$, then:

[TABLE]

Then since $RT$ and $(R/S)(T/(S/R))$ are isomorphic, it is immediate to conclude, similarly as in item 3.3.3 of this lemma.

Lemma 15 (Full Stability)

Let $\rho,\sigma$ be coinitial derivations such that $\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)=\varnothing$. Let $T_{1},T_{2},T_{3}$ be steps such that $T_{3}=T_{1}/(\sigma/\rho)=T_{2}/(\rho/\sigma)$. Then there is a step $T_{0}$ such that $T_{1}=T_{0}/\rho$ and $T_{2}=T_{0}/\sigma$.

Proof

The proof of Full Stability (Lem. 15) is straightforward using Basic Stability (Lem. 14). Consider the diagram formed by $\rho=R_{1}\ldots R_{n}$ and $\sigma=S_{1}\ldots S_{m}$. By Permutation (Prop. 2) the diagram can be tiled using squares, as in $\lambda^{\texttt{{\#}}}$ there is no erasure or duplication. Note that for all $i\neq j$ we have that $R_{i}\neq S_{j}$, since $\mathsf{labs}(\rho)$ and $\mathsf{labs}(\sigma)$ are disjoint. It suffices to apply Basic Stability $n\times m$ times, once for each tile.

0.A.5 Proof of Prop. 4 – $\mathbb{D}^{\texttt{{\#}}}(t)$ is a lattice

Let ${[\rho]}$ denote the permutation equivalence class of a derivation $\rho$, and let $\mathbb{D}^{\texttt{{\#}}}(t)=\{{[\rho]}\ |\ \mathsf{src}(\rho)=t\}$ be the set of $\mathrel{\to_{\texttt{{\#}}}}$-derivations starting on $t$, modulo permutation equivalence. We already know that $(\mathbb{D}^{\texttt{{\#}}}(t),\sqsubseteq)$ is an upper semilattice, where the order is given by ${[\rho]}\sqsubseteq{[\sigma]}\overset{\mathrm{def}}{\iff}\rho\sqsubseteq\sigma$, the bottom is $\bot={[\epsilon]}$ and the join is ${[\rho]}\sqcup{[\sigma]}={[\rho\sqcup\sigma]}$.

Note that $\mathbb{D}^{\texttt{{\#}}}(t)$ has a top element: given that $\lambda^{\texttt{{\#}}}$ is strongly normalizing (Prop. 1), consider a derivation $\rho:t\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}^{*}s$ to normal form. Then for any other derivation $\sigma:t\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}^{*}u$ we have that $\sigma/\rho=\epsilon$, so it suffices to take $\top={[\rho]}$.

To see that $\mathbb{D}^{\texttt{{\#}}}(t)$ is a lattice for all $t\in\mathcal{T}^{\texttt{{\#}}}$, we are left to show that any two coinitial derivations $\rho,\sigma$ have a meet $\rho\sqcap\sigma$ with respect to the prefix order $\sqsubseteq$, and define ${[\rho]}\sqcap{[\sigma]}\overset{\mathrm{def}}{=}{[\rho\sqcap\sigma]}$. To this purpose, we prove various auxiliary results.

Definition 15

A step $R$ belongs to a coinitial derivation $\rho$, written $R\in\rho$, if and only if some residual of $R$ is contracted along $\rho$. More precisely, $R\in\rho$ if there exist $\rho_{1},R^{\prime},\rho_{2}$ such that $\rho=\rho_{1}R\rho_{2}$ and $R^{\prime}\in R/\rho_{1}$, We write $R\not\in\rho$ if it is not the case that $R\in\rho$.

Lemma 16 (Characterization of belonging)

Let $R$ be a step and $\rho$ a coinitial derivation in $\lambda^{\texttt{{\#}}}$. Then the following are equivalent:

$R\in\rho$, 2. 2.

$R\sqsubseteq\rho$, 3. 3.

$\mathsf{lab}(R)\in\mathsf{labs}(\rho)$.

Note: the hypothesis that $R$ and $\rho$ are coinitial is crucial. In particular, $(1)$ and $(2)$ by definition only hold when $R$ and $\rho$ are coinitial, while $(3)$ might hold even if $R$ and $\rho$ are not coinitial.

Proof

$(1\Rightarrow 2)$ Let $\rho=\rho_{1}S\sigma_{2}$ where $S$ is a residual of $R$. Suppose moreover, without loss of generality, that $\rho_{1}$ is minimal, i.e. that $R\not\in\rho_{1}$. Since in $\lambda^{\texttt{{\#}}}$ there is no duplication or erasure, $R/\rho_{1}$ is a singleton, so $R/\rho_{1}=S$. This means that $R/\rho_{1}S\rho_{2}=\varnothing$, so indeed $R\sqsubseteq\rho_{1}S\rho_{2}$.

$(2\Rightarrow 3)$ By induction on $\rho$. If $\rho$ is empty, the implication is vacuously true, so let $\rho=S\sigma$ and consider two subcases, depending on whether $R=S$. If $R=S$, then indeed the first step of $\rho=R\sigma$ has the same label as $R$. On the other hand, if $R\neq S$, since in $\lambda^{\texttt{{\#}}}$ there is no duplication or erasure, we have that $R/S=R^{\prime}$, where $\mathsf{lab}(R)=\mathsf{lab}(R^{\prime})$. Note that $R\sqsubseteq S\sigma$ so $R/S=R^{\prime}\sqsubseteq\sigma$. By applying the i.h. we obtain that there must be a step in $\sigma$ whose label is $\mathsf{lab}(R)=\mathsf{lab}(R^{\prime})$, and we are done.

$(3\Rightarrow 1)$ By induction on $\rho$. If $\rho$ is empty, the implication is vacuously true, so let $\rho=S\sigma$ and consider two subcases, depending on whether $\mathsf{lab}(R)=\mathsf{lab}(S)$. If $\mathsf{lab}(R)=\mathsf{lab}(S)$ then $R$ and $S$ must be the same step, since terms are correct, which means that labels decorating lambdas are pairwise distinct. Hence $R\in\rho=R\sigma$. On the other hand, if $\mathsf{lab}(R)\neq\mathsf{lab}(S)$, then $R\neq S$ so since in $\lambda^{\texttt{{\#}}}$ there is no duplication or erasure we have that $R/S=R^{\prime}$, where $\mathsf{lab}(R)=\mathsf{lab}(R^{\prime})$. By hypothesis, there is a step in the derivation $\rho=S\sigma$ whose label is $\mathsf{lab}(R)$, and it is not $S$, so there must be at least one step in the derivation $\sigma$ whose label is $\mathsf{lab}(R)=\mathsf{lab}(R^{\prime})$. By i.h. $R^{\prime}\in\sigma$ and then, since $R^{\prime}$ is a residual of $R$, we conclude that $R\in S\sigma$, as required.

It is immediate to note that, when composing derivations $\rho,\sigma$, the set of labels of $\rho\sigma$ results from the union of the labels of $\rho$ and $\sigma$:

Remark 4

$\mathsf{labs}(\rho\sigma)=\mathsf{labs}(\rho)\cup\mathsf{labs}(\sigma)$

Indeed, a stronger results holds. Namely, the union is disjoint:

Lemma 17

$\mathsf{labs}(\rho\sigma)=\mathsf{labs}(\rho)\uplus\mathsf{labs}(\sigma)$

Proof

Let $\rho:t\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}s$. By induction on $\rho$ we argue that the set of labels decorating the lambdas in $s$ is disjoint from $\mathsf{labs}(\rho)$. The base case is immediate, so let $\rho=T\tau$. The step $T$ is of the form: $T:t=\mathtt{C}\langle(\lambda^{\ell}x.u)\bar{r}\rangle\mathrel{\to_{\texttt{{\#}}}}\mathtt{C}\langle u\{x:=\bar{r}\}\rangle$. Hence the target of $T$ has no lambdas decorated with the label $\ell$. Moreover, the derivation $\tau$ is of the form: $\tau:\mathtt{C}\langle u\{x:=\bar{r}\}\rangle\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}s$ and by i.h. the set of labels decorating the lambdas in $s$ is disjoint from $\mathsf{labs}(\tau)$. As a consequence, the set of labels decorating the lambdas in $s$ is disjoint from both $\mathsf{labs}(\tau)$ and $\{\ell\}$. This completes the proof.

As an easy consequence:

Corollary 3

If $|\rho|$ denotes the length of $\rho$, then $|\rho|=\#(\mathsf{labs}(\rho))$.

Lemma 18

Let $\rho$ and $\sigma$ be coinitial. Then $\mathsf{labs}(\rho/\sigma)=\mathsf{labs}(\rho)\setminus\mathsf{labs}(\sigma)$

Proof

First we claim that $\mathsf{labs}(\rho/R)=\mathsf{labs}(\rho)\setminus\{\mathsf{lab}(R)\}$. By induction on $\rho$. The base case is immediate, so let $\rho=S\sigma$ and consider two subcases, depending on whether $R=S$. If $R=S$, then $\mathsf{labs}(\rho/R)=\mathsf{labs}(R\sigma/R)=\mathsf{labs}(\sigma)=\mathsf{labs}(R\sigma)\setminus\{\mathsf{lab}(R)\}$. On the other hand if $R\neq S$, then since in $\lambda^{\texttt{{\#}}}$ there is no duplication or erasure we have that $R/S=R^{\prime}$ where $\mathsf{lab}(R)=\mathsf{lab}(R^{\prime})$ and, similarly, $S/R=S^{\prime}$, where $\mathsf{lab}(S)=\mathsf{lab}(S^{\prime})$. Hence:

[TABLE]

which completes the claim. To see that $\mathsf{labs}(\rho/\sigma)=\mathsf{labs}(\rho)\setminus\mathsf{labs}(\sigma)$ for an arbitrary derivation $\sigma$, proceed by induction on $\sigma$. If $\sigma$ is empty it is trivial, so consider the case in which $\sigma=R\tau$.

[TABLE]

Proposition 12 (Prefixes as subsets)

Let $\rho,\sigma$ be coinitial derivations in the distributive lambda-calculus. Then $\rho\sqsubseteq\sigma$ if and only if $\mathsf{labs}(\rho)\subseteq\mathsf{labs}(\sigma)$.

Proof

By induction on $\rho$. The base case is immediate since $\epsilon\sqsubseteq\sigma$ and $\varnothing\subseteq\mathsf{labs}(\sigma)$ both hold. So let $\rho=T\tau$. First note that the following equivalence holds:

[TABLE]

Indeed:

• $(\Rightarrow)$ Suppose that $T\tau\sqsubseteq\sigma$. Then, on one hand, $T\sqsubseteq T\tau\sqsubseteq\sigma$. On the other hand, projection is monotonic, so $\tau=T\tau/T\sqsubseteq\sigma/T$.
• $(\Leftarrow)$ Since $\tau\sqsubseteq\sigma/T$ we have that $T\tau\sqsubseteq T(\sigma/T)\equiv\sigma(T/\sigma)=\sigma$ since $T/\sigma=\epsilon$.

So we have that:

[TABLE]

To justify the very last equivalence, the $(\Rightarrow)$ direction is immediate. For the $(\Leftarrow)$ direction, the difficulty is ensuring that $\mathsf{labs}(\tau)\subseteq\mathsf{labs}(\sigma)\setminus\{\mathsf{lab}(T)\}$ from the fact that $\mathsf{labs}(T\tau)\subseteq\mathsf{labs}(\sigma)$. To see this it suffices to observe that by Lem. 17, $\mathsf{labs}(T\tau)$ is the disjoint union $\mathsf{labs}(T)\uplus\mathsf{labs}(\tau)$, which means that $\mathsf{lab}(T)\not\in\mathsf{labs}(\tau)$.

As an easy consequence:

Corollary 4 (Permutation equivalence in terms of labels)

Let $\rho,\sigma$ be coinitial derivations in $\lambda^{\texttt{{\#}}}$. Then $\rho\equiv\sigma$ if and only if $\mathsf{labs}(\rho)=\mathsf{labs}(\sigma)$.

Lemma 19 (Projections are decreasing)

Let $R\in\rho$. Then $|\rho|=1+|\rho/R|$.

Proof

Observe that $R\sqsubseteq\rho$ by Lem. 16. So $\rho\equiv R(\rho/R)$, which gives us that:

[TABLE]

The proof of Prop. 4 proceeds as follows. If $\rho$ and $\sigma$ are derivations, we say that a step $R$ is a common (to $\rho$ and $\sigma$) whenever $R\in\rho$ and $R\in\sigma$. Define $\rho\sqcap\sigma$ as follows, by induction on the length of $\rho$:

[TABLE]

In the second case of the definition, there might be more than one $R$ common to $\rho$ and $\sigma$. Any such step may be chosen and we make no further assumptions. To see that this recursive construction is well-defined, note that the length of $\rho/R$ is lesser than the length of $\rho$ by the fact that projections are decreasing (Lem. 19). To conclude the construction, we show that $\rho\sqcap\sigma$ is an infimum, i.e. a greatest lower bound:

Lower bound. Let us show that $\rho\sqcap\sigma\sqsubseteq\rho$ by induction on the length of $\rho$. There are two subcases, depending on whether there is a step common to $\rho$ and $\sigma$.

If there is no common step, then $\rho\sqcap\sigma=\epsilon$ trivially verifies $\rho\sqcap\sigma\sqsubseteq\rho$.

On the other hand, if there is a common step, we have by definition that $\rho\sqcap\sigma=R((\rho/R)\sqcap(\sigma/R))$ where $R$ is common to $\rho$ and $\sigma$. Recall that projections are decreasing (Lem. 19) so $|\rho|>|\rho/R|$. This allows us to apply the i.h. and conclude:

[TABLE]

Showing that $\rho\sqcap\sigma\sqsubseteq\sigma$ is symmetric, by induction on the length of $\sigma$. 2. 2.

Greatest lower bound. Let $\tau$ be a lower bound for $\{\rho,\sigma\}$, i.e. $\tau\sqsubseteq\rho$ and $\tau\sqsubseteq\sigma$, and let us show that $\tau\sqsubseteq\rho\sqcap\sigma$. We proceed by induction on the length of $\rho$. There are two subcases, depending on whether there is a step common to $\rho$ and $\sigma$.

If there is no common step, we claim that $\tau$ must be empty. Otherwise we would have that $\tau=T\tau^{\prime}\sqsubseteq\rho$ so in particular $T\sqsubseteq\rho$ and $T\in\rho$ by Lem. 16. Similarly, $T\in\sigma$ so $T$ is a step common to $\rho$ and $\sigma$, which is a contradiction. We obtain that $\tau$ is empty, so trivially $\tau=\epsilon\sqsubseteq\rho\sqcap\sigma$.

On the other hand, if there is a common step, we have by definition that $\rho\sqcap\sigma=R((\rho/R)\sqcap(\sigma/R))$ where $R$ is common to $\rho$ and $\sigma$. Moreover, since $\tau\sqsubseteq\rho$ and $\tau\sqsubseteq\sigma$, by projecting along $R$ we know that $\tau/R\sqsubseteq\rho/R$ and $\tau/R\sqsubseteq\sigma/R$. So:

[TABLE]

Finally, observe that the meet of $\{\rho,\sigma\}$ is unique modulo permutation equivalence, since if $\tau$ and $\tau^{\prime}$ both have the universal property of being a greatest lower bound, then $\tau\sqsubseteq\tau^{\prime}$ and $\tau^{\prime}\sqsubseteq\tau$.

0.A.6 Proof of Prop. 5 – The function $\mathsf{labs}$ is a morphism of lattices

We need the following auxiliary result:

Lemma 20 (Disjoint derivations)

Let $\rho$ and $\sigma$ be coinitial derivations in $\lambda^{\texttt{{\#}}}$. The following are equivalent:

$\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)=\varnothing$. 2. 2.

$\rho\sqcap\sigma=\epsilon$. 3. 3.

There is no step common to $\rho$ and $\sigma$.

In this case we say that $\rho$ and $\sigma$ are disjoint.

Proof

The implication $(1\implies 2)$ is immediate since if we suppose that $\rho\sqcap\sigma$ is non-empty then the first step of $\rho\sqcap\sigma$ is a step $T$ such that $T\in\rho$ and $T\in\sigma$. By Lem. 16, this means that $\mathsf{lab}(T)\in\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)$, contradicting the fact that $\mathsf{lab}(T)$ and $\mathsf{labs}(\rho)$ are disjoint.

The implication $(2\implies 3)$ is immediate by the definition of $\rho\sqcap\sigma$ (defined in Prop. 4).

Let us check that the implication $(3\implies 1)$ holds. By the contrapositive, suppose that $\mathsf{labs}(\rho)$ and $\mathsf{labs}(\sigma)$ are not disjoint, and let us show that there is a step common to $\rho$ and $\sigma$. Since $\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)\neq\varnothing$, we know that the derivation $\rho$ can be written as $\rho=\rho_{1}R\rho_{2}$ where $\mathsf{lab}(R)\in\mathsf{labs}(\sigma)$. Without loss of generality we may suppose that $R$ is the first step in $\rho$ with that property, i.e. that $\mathsf{labs}(\rho_{1})\cap\mathsf{labs}(\sigma)=\varnothing$. Moreover, let us write $\sigma$ as $\sigma=\sigma_{1}S\sigma_{2}$ where $\mathsf{lab}(R)=\mathsf{lab}(S)$.

Observe that the label of $R$ does not appear anywhere along the sequence of steps $\rho_{1}$, i.e. that $\mathsf{lab}(R)\not\in\mathsf{labs}(\rho_{1})$, as a consequence of the fact that no labels are ever repeated in any sequence of steps (Lem. 17). This implies that $\mathsf{lab}(S)\not\in\mathsf{labs}(\rho_{1}/\sigma_{1})$. Indeed:

[TABLE]

This means that $S$ is not erased by the derivation $\rho_{1}/\sigma_{1}$. More precisely, $S/(\rho_{1}/\sigma_{1})$ is a singleton.

Symmetrically, $R/(\sigma_{1}/\rho_{1})$ is a singleton. Moreover, $\mathsf{lab}(S/(\rho_{1}/\sigma_{1}))=\mathsf{lab}(S)=\mathsf{lab}(R)=\mathsf{lab}(R/(\sigma_{1}/\rho_{1}))$ so we have that $S/(\rho_{1}/\sigma_{1})=R/(\sigma_{1}/\rho_{1})$. The situation is the following, where $\mathsf{labs}(\rho_{1})\cap\mathsf{labs}(\sigma_{1})=\varnothing$:

[TABLE]

By Full stability (Lem. 15) this means that there exists a step $T$ such that $T/\rho_{1}=R$ and $T/\sigma_{1}=S$. Then $T\in\rho_{1}R\rho_{2}=\rho$ and also $T\in\sigma_{1}S\sigma_{2}=\sigma$ so $T$ is common to $\rho$ and $\sigma$, by which we conclude.

Let $X$ be the set of labels of the steps involved in some derivation to normal form. More precisely, let $\rho_{0}:t\mathrel{\to_{\texttt{{\#}}}}^{*}s$ be a derivation to normal form, which exists by virtue of Strong Normalization (Prop. 1), and let $X=\mathsf{labs}(\rho_{0})$. Then we claim that:

[TABLE]

is a monomorphism of lattices. Note that $\mathsf{labs}$ is well-defined over permutation equivalence classes since if $\rho\equiv\sigma$ then $\mathsf{labs}(\rho)=\mathsf{labs}(\sigma)$ by Coro. 4. We are to show that $\mathsf{labs}$ is monotonic, that it preserves bottom, joins, top, and meets, and finally that it is a monomorphism:

Monotonic, i.e. ${[\rho]}\sqsubseteq{[\sigma]}$ implies $\mathsf{labs}(\rho)\subseteq\mathsf{labs}(\sigma)$. By Prop. 12. 2. 2.

Preserves bottom. Indeed, $\mathsf{labs}({[\epsilon]})=\varnothing$. 3. 3.

Preserves joins, i.e. $\mathsf{labs}({[\rho]}\sqcup{[\sigma]})=\mathsf{labs}(\rho)\cup\mathsf{labs}(\sigma)$. Indeed:

[TABLE] 4. 4.

Preserves top. Recall that $\top={[\rho_{0}]}$ where $\rho_{0}:t\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}^{*}s$ is the derivation to normal form. Note moreover that all derivations to normal form are permutation equivalent in an orthogonal axiomatic rewrite system, so the choice does not matter. To conclude, observe that $\mathsf{labs}(\rho_{0})=X$ by definition of $X$, and $X$ is indeed the top element of $\mathcal{P}(X)$. 5. 5.

Preserves meets, i.e. $\mathsf{labs}({[\rho]}\sqcap{[\sigma]})=\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)$. We show the two inclusions:

1. 5.1

$(\subseteq)$ It suffices to check that $\mathsf{labs}(\rho\sqcap\sigma)\subseteq\mathsf{labs}(\rho)$ (the inclusion $\mathsf{labs}(\rho\sqcap\sigma)\subseteq\mathsf{labs}(\sigma)$ is symmetric). By induction on the length of $\rho\sqcap\sigma$. If $\rho\sqcap\sigma$ is empty it is immediate. If it is non-empty, $\rho\sqcap\sigma=T(\rho/T\sqcap\sigma/T)$, where $T$ is a step common to $\rho$ and $\sigma$. Then since $T$ is common to $\rho$ and $\sigma$, we have that $\mathsf{lab}(T)\in\mathsf{labs}(\rho)$. Moreover, by i.h. $\mathsf{labs}(\rho/T\sqcap\sigma/T)\subseteq\mathsf{labs}(\rho/T)$. So:

[TABLE] 2. 5.2

$(\supseteq)$ To show $\mathsf{labs}(\rho)\cap\mathsf{labs}(\sigma)\subseteq\mathsf{labs}(\rho\sqcap\sigma)$, we first prove the following claim:

Claim. $\mathsf{labs}(\rho/(\rho\sqcap\sigma))\cap\mathsf{labs}(\sigma/(\rho\sqcap\sigma)=\varnothing$.

Proof of the claim. By Lem. 20 it suffices to show that $(\rho/(\rho\sqcap\sigma))\sqcap(\sigma/(\rho\sqcap\sigma))=\epsilon$. By contradiction, suppose that there is a step $T$ common to the derivations $\rho/(\rho\sqcap\sigma)$ and $\sigma/(\rho\sqcap\sigma)$. Then the derivation $(\rho\sqcap\sigma)T$ is a lower bound for $\{\rho,\sigma\}$, i.e. $(\rho\sqcap\sigma)T\sqsubseteq\rho$ and $(\rho\sqcap\sigma)T\sqsubseteq\sigma$. Since $\rho\sqcap\sigma$ is the greatest lower bound for $\{\rho,\sigma\}$, we have that $(\rho\sqcap\sigma)T\sqsubseteq\rho\sqcap\sigma$. But this implies that $T\sqsubseteq\epsilon$, which is a contradiction. End of claim.

Note that $\rho\sqcap\sigma\sqsubseteq\rho$, so we have that $\rho\equiv(\rho\sqcap\sigma)(\rho/(\rho\sqcap\sigma))$, and this in turn implies that $\mathsf{labs}(\rho)=\mathsf{labs}((\rho\sqcap\sigma)(\rho/(\rho\sqcap\sigma)))$ by Coro. 4. Symmetrically, $\mathsf{labs}(\sigma)=\mathsf{labs}((\rho\sqcap\sigma)(\sigma/(\rho\sqcap\sigma)))$. Then:

[TABLE] 6. 6.

Monomorphism. It suffices to show that $\mathsf{labs}$ is injective. Indeed, suppose that $\mathsf{labs}({[\rho]})=\mathsf{labs}({[\sigma]})$. By Coro. 4 we have that $\rho\equiv\sigma$, so ${[\rho]}={[\sigma]}$.

0.A.7 Proof of Prop. 6 – Simulation

To prove Prop. 6 we need an auxiliary lemma.

Lemma 21 (Refinement of a substitution: composition)

If $t^{\prime}\mathrel{\ltimes}t$ and $s^{\prime}_{i}\mathrel{\ltimes}s$ for all $1\leq i\leq n$, then $t^{\prime}\{x:=[s_{1}^{\prime},\ldots,s_{n}^{\prime}]\}\mathrel{\ltimes}t\{x:=s\}$.

Proof

Straightforward by induction on $t$.

We prove items 1 and 2 of Prop. 6 separately:

0.A.7.1 Item 1 of Prop. 6: simulation of $\mathrel{\to_{\beta}}$ with $\mathrel{\to_{\texttt{{\#}}}}$

Let $t^{\prime}\mathrel{\ltimes}t$ and let $t=\mathtt{C}\langle(\lambda x.p)q\rangle\mathrel{\to_{\beta}}\mathtt{C}\langle p\{x:=q\}\rangle=s$. We prove that there exists a term $s^{\prime}$ such that $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$ and $s^{\prime}\mathrel{\ltimes}s$ by induction on $\mathtt{C}$.

Empty context, $\mathtt{C}=\Box$. Then $t=(\lambda x.p)q\to{p\{x:=q\}}=s$ and $t^{\prime}$ is of the form $(\lambda^{\ell}x.p^{\prime})[q_{1}^{\prime},\ldots,q_{n}^{\prime}]$. We conclude by taking $s^{\prime}=p^{\prime}\{x:=[q_{1}^{\prime},\ldots,q_{n}^{\prime}]\}$, using Lem. 21. 2. 2.

Under an abstraction, $\mathtt{C}=\lambda y.\mathtt{C}^{\prime}$. Immediate by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}u$. Immediate by i.h.. 4. 4.

Right of an application, $\mathtt{C}=u\mathtt{C}^{\prime}$. Then $t=u\,\mathtt{C}^{\prime}\langle(\lambda x.p)q\rangle\mathrel{\to_{\beta}}u\,\mathtt{C}^{\prime}\langle p\{x:=q\}\rangle=s$ and $t^{\prime}=u^{\prime}[u^{\prime}_{1},\ldots,u^{\prime}_{n}]$, with $u^{\prime}\mathrel{\ltimes}u$ and $u^{\prime}_{i}\mathrel{\ltimes}\mathtt{C}^{\prime}\langle(\lambda x.p)q\rangle$ for all $i=1..n$. Applying the i.h. on $u^{\prime}_{i}$ for each $i=1..n$, we have:

[TABLE]

So we may conclude as follows:

[TABLE]

0.A.7.2 Item 2 of Prop. 6: simulation of $\mathrel{\to_{\texttt{{\#}}}}$ with $\mathrel{\to_{\beta}}$

Let $t^{\prime}\mathrel{\ltimes}t$ and $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}s^{\prime}$. We prove that there exist terms $s$ and $s^{\prime\prime}$ such that $t\mathrel{\to_{\beta}}s$, $s^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime\prime}$, and $s^{\prime\prime}\mathrel{\ltimes}s$ by induction on $t^{\prime}$. Moreover, $s^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime\prime}$ is a multistep.

Variable $t^{\prime}=x$. Impossible. 2. 2.

Abstraction, $t^{\prime}=\lambda^{\ell}y.r^{\prime}$ Immediate by i.h.. 3. 3.

Application, $t^{\prime}=u^{\prime}[r^{\prime}_{1},\ldots,r^{\prime}_{n}]$ Then $t=ur$ where $u^{\prime}\mathrel{\ltimes}u$ and $r^{\prime}_{i}\mathrel{\ltimes}r$ for all $i=1..n$. There are three subcases, depending on whether the step $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}s^{\prime}$ takes place at the root, inside $u^{\prime}$, or inside $r^{\prime}_{i}$ for some $i=1..n$,

1. 3.1

Reduction at the root. In this case $u^{\prime}=\lambda^{\ell}x.s^{\prime}$. Then by Lem. 21:

[TABLE] 2. 3.2

Reduction in $u^{\prime}$. Immediate by i.h.. 3. 3.3

Reduction in $r^{\prime}_{i}$ for some $i=1..n$. We have that $r^{\prime}_{i}\mathrel{\to_{\texttt{{\#}}}}r^{\prime\prime}_{i}$, so by i.h. there exist $p^{\prime}_{i}$ and $p$ such that:

[TABLE]

For every $j=1..n$, $j\neq i$, we have that $r^{\prime}_{j}\mathrel{\ltimes}r$ and $r\mathrel{\to_{\beta}}p$. By item 1 of Simulation (Prop. 6), which we have just proved, we have the following diagram:

[TABLE]

So:

[TABLE]

0.A.8 Proof of Prop. 7 – Typability characterizes head normalization

Before proving Prop. 7, we need a few auxiliary results.

Definition 16 (Head normal forms)

A $\lambda$-term $t$ is a head normal form if it is of the form $t=\lambda x_{1}.\ldots\lambda x_{n}.y\,t_{1}\,\ldots\,t_{m}$ where $n\geq 0$ and $m\geq 0$. Note that $y$ might be or not be among the variables $x_{1},\ldots,x_{n}$. Similarly, a correct term $t\in\mathcal{T}^{\texttt{{\#}}}$ of $\lambda^{\texttt{{\#}}}$ a head normal form if it is of the form $t=\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{\mathcal{A}}\,\bar{t}_{1}\,\ldots\,\bar{t}_{m}$ where $n\geq 0$ and $m\geq 0$.

Lemma 22

If $t$ is a head normal form, there exists $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t^{\prime}\mathrel{\ltimes}t$. Moreover $t^{\prime}$ can be taken to be of the form $\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{[\,]\overset{\ell^{\prime}_{1}}{\to}\ldots[\,]\overset{\ell^{\prime}_{m}}{\to}\alpha^{\ell^{\prime\prime}}}[\,]\ldots[\,]$.

Proof

Let $t=\lambda x_{1}.\ldots\lambda x_{n}.yt_{1}\ldots t_{m}$. Let $\{\ell_{1},\ldots,\ell_{n},\ell^{\prime}_{1},\ldots,\ell^{\prime}_{m},\ell^{\prime\prime}\}$ be a set of $n+m+1$ pairwise distinct labels and let $\alpha$ be a base type. Take t^{\prime}:=\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{[\,]\overset{\ell^{\prime}_{1}}{\to}\ldots[\,]\overset{\ell^{\prime}_{m}}{\to}\alpha^{\ell^{\prime\prime}}}\underbrace{[\,]\ldots[\,]}_{\text{m times}}. Observe that $t^{\prime}$ is correct and $t^{\prime}\mathrel{\ltimes}t$.

Lemma 23 ($\mathrel{\to_{\texttt{{\#}}}}$-normal forms refine head normal forms)

Let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a $\mathrel{\to_{\texttt{{\#}}}}$-normal form and $t^{\prime}\mathrel{\ltimes}t$. Then $t$ is a head normal form.

Proof

Observe, by induction on $t^{\prime}$ that if $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ is a $\mathrel{\to_{\texttt{{\#}}}}$-normal form, it must be of the form $\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{\mathcal{A}}\bar{s}_{1}\ldots\bar{s}_{m}$, as it cannot have a subterm of the form $(\lambda^{\ell^{\prime}}z.u)\bar{r}$. Then $\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{\mathcal{A}}\bar{s}_{1}\ldots\bar{s}_{m}\mathrel{\ltimes}t$. So $t$ is of the form $\lambda x_{1}.\ldots\lambda x_{n}.ys_{1}\ldots s_{n}$, that is, $t$ is a head normal form.

The following lemma is an adaptation of Subject Expansion in [8].

Lemma 24 (Subject Expansion)

If $\Gamma\vdash\mathtt{C}\langle t\{x:=\bar{s}\}\rangle:\mathcal{A}$ is derivable, then $\Gamma\vdash\mathtt{C}\langle(\lambda^{\ell}x.t)\bar{s}\rangle:\mathcal{A}$ is derivable.

Proof

The proof proceeds by induction on $\mathtt{C}$, and the base case by induction on $t$, similar to the proof that substitution preserves typing in the proof of Subject Reduction (Sec. 0.A.1.1).

Correctness is not necessarily preserved by $\mathrel{\to_{\texttt{{\#}}}}$-expansion. We need a stronger invariant, strong sequentiality, that will be shown to be preserved by expansion under appropiate conditions:

Definition 17 (Subterms and free subterms)

The set of subterms $\mathsf{sub}(t)$ of a term $t$ is formally defined as follows:

[TABLE]

The set of free subterms $\mathsf{sub}^{\circ}(t)$ of a term $t$ is defined similarly, except for the abstraction case, which requires that the subterm in question do not include occurrences of bound variables:

[TABLE]

Definition 18 (Strong sequentiality)

A term $t$ is strongly sequential if it is correct and, moreover, for every subterm $s\in\mathsf{sub}(t)$ and any two free subterms $s_{1},s_{2}\in\mathsf{sub}^{\circ}(s)$ lying at disjoint positions of $s$, the types of $s_{1}$ and $s_{2}$ have different external labels.

Example 6

The following examples illustrate the notion of strong sequentiality:

The term $t=(\lambda^{1}x.y^{\alpha^{2}})[\,]$ is strongly sequential. Note that $t$ and $y^{\alpha^{2}}$ have the same type, namely $\alpha^{2}$, but they do not occur at disjoint positions. 2. 2.

The term $t=(\lambda^{1}x.x^{\alpha^{2}})[y^{\alpha^{2}}]$ is strongly sequential. Note that $x^{\alpha^{2}}$ and $y^{\alpha^{2}}$ both have type $\alpha^{2}$, but they are not simultaneously free subterms of the same subterm of $t$. 3. 3.

The term $t=\lambda^{1}y.x^{[\alpha^{2}]\overset{3}{\to}[\alpha^{2}]\overset{4}{\to}\beta^{5}}[y^{\alpha^{2}}][z^{\alpha^{2}}]$ is not strongly sequential, since $y^{\alpha^{2}}$ and $z^{\alpha^{2}}$ have the same type and they are both free subterms of $x^{[\alpha^{2}]\overset{3}{\to}[\alpha^{2}]\overset{4}{\to}\beta^{5}}[y^{\alpha^{2}}][z^{\alpha^{2}}]\in\mathsf{sub}(t)$.

Lemma 25 (Refinement of a substitution: decomposition)

If $u^{\prime}\mathrel{\ltimes}t\{x:=s\}$ and $u^{\prime}$ is strongly sequential, then $u^{\prime}$ is of the form $t^{\prime}\{x:=[s^{\prime}_{i}]_{i=1}^{n}\}$. Moreover, given a fresh label $\ell$, the term $(\lambda^{\ell}x.t^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential, $t^{\prime}\mathrel{\ltimes}t$ and $s^{\prime}_{i}\mathrel{\ltimes}s$ for all $i=1..n$.

Proof

By induction on $t$.

Variable (same), $t=x$. Then $u^{\prime}\mathrel{\ltimes}s$. Let $\mathcal{A}$ be the type of $u^{\prime}$. Taking $t^{\prime}:=x^{\mathcal{A}}\mathrel{\ltimes}x$ we have that $(\lambda^{\ell}x.x^{\mathcal{A}})[u^{\prime}]$ is strongly sequential. Regarding strong sequentiality, observe that $x^{\mathcal{A}}$ and $u^{\prime}$ have the same type, but they are not simultaneously the free subterms of any subterm of $(\lambda^{\ell}x.x^{\mathcal{A}})[u^{\prime}]$. 2. 2.

Variable (different), $t=y\neq x$. Then $u^{\prime}\mathrel{\ltimes}y$, so $u^{\prime}$ is of the form $y^{\mathcal{A}}$. Taking $t^{\prime}:=y^{\mathcal{A}}$ we have that $(\lambda^{\ell}x.y^{\mathcal{A}})[\,]$ is strongly sequential. 3. 3.

Abstraction, $t=\lambda y.r$. Then $u^{\prime}\mathrel{\ltimes}\lambda y.r\{x:=s\}$ so $u^{\prime}$ is of the form $\lambda^{\ell^{\prime}}y.u^{\prime\prime}$ where $u^{\prime\prime}\mathrel{\ltimes}r\{x:=s\}$. By i.h., $u^{\prime\prime}$ is of the form $r^{\prime}\{x:=[s^{\prime}_{i}]_{i=1}^{n}\}$ where $(\lambda^{\ell}x.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential, $r^{\prime}\mathrel{\ltimes}r$ and $s^{\prime}_{i}\mathrel{\ltimes}s$ for all $i=1..n$. Taking $t^{\prime}:=\lambda^{\ell^{\prime}}y.r^{\prime}$, we have that $t^{\prime}=\lambda^{\ell^{\prime}}y.r^{\prime}\mathrel{\ltimes}\lambda y.r=t$. Moreover, the term $(\lambda^{\ell}x.t^{\prime})[s_{i}]_{i=1}^{n}=(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n}$ is strongly sequential. Typability is a consequence of Subject Expansion (Lem. 24). The remaining properties are:

1. 3.1

Uniquely labeled lambdas. The multiset of labels decorating the lambdas of $(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n}$ is given by $\Lambda((\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n})=[\ell,\ell^{\prime}]+\Lambda(r^{\prime})+_{i=1}^{n}\Lambda(s_{i})$. It suffices to check that this multiset has no repeats. The label $\ell$ is assumed to be fresh, so it occurs only once. By i.h., $u^{\prime\prime}=r^{\prime}\{x:=[s^{\prime}_{i}]_{i=1}^{n}\}$, so using Lem. 9 we have $\Lambda(u^{\prime})=\Lambda(\lambda^{\ell^{\prime}}y.u^{\prime})=[\ell^{\prime}]+\Lambda(u^{\prime\prime})=[\ell^{\prime}]+\Lambda(r^{\prime}\{x:=[s^{\prime}_{i}]_{i=1}^{n}\})=[\ell^{\prime}]+\Lambda(r^{\prime})+_{i=1}^{n}\Lambda(s^{\prime}_{i})$. Moreover, the term $u^{\prime}=\lambda^{\ell^{\prime}}y.u^{\prime\prime}$ is correct, so this multiset has no repeats. 2. 3.2

Sequential contexts. Let $q$ be a subterm of $(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$. If $q$ is a subterm of $r^{\prime}$ or a subterm of $s^{\prime}_{i}$ for some $i=1..n$ we conclude by i.h. since $(\lambda^{\ell}x.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is known to be correct. Moreover, if $\Gamma\oplus x:\mathcal{M}\oplus y:\mathcal{N}$ is the typing context for $r^{\prime}$, the typing contexts of $\lambda^{\ell^{\prime}}y.r^{\prime}$ and $\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime}$ are respectively $\Gamma\oplus x:\mathcal{M}$ and $\Gamma$, which are also sequential. Finally, if $\Delta_{i}$ is the typing context for $s^{\prime}_{i}$, for each $i=1..n$, the typing context for $(\lambda^{\ell}x.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is of the form $\Gamma+_{i=1}^{n}\Delta_{i}+y:\mathcal{N}$, and it is sequential by i.h.. Hence the typing context for the whole term is $\Gamma+_{i=1}^{n}\Delta_{i}$, and it is sequential. 3. 3.3

Sequential types.

Let $q$ be a subterm $(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$, and let $\mathcal{P}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}$ be a type that occurs in the typing context or the type of $q$. As in the previous case, we have that $\Gamma\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}\oplus y:\mathcal{N}\vdash r^{\prime}:\mathcal{A}$ is derivable and $\Delta_{i}\vdash s^{\prime}_{i}:\mathcal{B}_{i}$ is derivable for all $i=1..n$. Moreover, they are correct by i.h., so if $q$ is a subterm of $r^{\prime}$ or a subterm of some $s^{\prime}_{i}$, we are done. There are three cases left for $q$:

1. 3.3.1

Case $q=\lambda^{\ell^{\prime}}y.r^{\prime}$. The typing context is $\Gamma\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}$ and the type $\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{A}$. 2. 3.3.2

Case $q=\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime}$. The typing context is $\Gamma$ and the type $[\mathcal{B}_{i}]_{i=1}^{n}\overset{\ell}{\to}\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{A}$. 3. 3.3.3

Case $q=(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n}$. The typing context is $\Gamma$ and the type $\mathcal{N}\overset{\ell^{\prime}}{\to}\mathcal{A}$.

In all three cases, if $\mathcal{P}\overset{\ell^{\prime\prime}}{\to}\mathcal{C}$ occurs in the typing context or the type of $q$, then $\mathcal{P}$ can be shown to be sequential using the i.h.. 4. 3.4

Strong sequentiality.

Let $q\in\mathsf{sub}((\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n})$ be a subterm, and let $q_{1},q_{2}\in\mathsf{sub}^{\circ}(q)$ be free subterms lying at disjoint positions of $q$. We argue that the types of $q_{1}$ and $q_{2}$ have different external labels. Consider the following five possibilities for $q_{1}$:

1. 3.4.1

Case $q_{1}=(\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime})[s_{i}]_{i=1}^{n}$. Impossible since $q_{2}$ must be at a disjoint position. 2. 3.4.2

Case $q_{1}=\lambda^{\ell}x.\lambda^{\ell^{\prime}}y.r^{\prime}$. Then the external label of the type of $q_{1}$ is the label $\ell$, which is fresh, so it cannot coincide with the type of any other subterm. 3. 3.4.3

Case $q_{1}=\lambda^{\ell^{\prime}}y.r^{\prime}$. Then $q_{2}$ must be a subterm of $s_{i}$ for some $i=1..n$. Note that $q$ must be the whole term, and $n>0$, so there is at least one free occurrence of $x$ in $\lambda^{\ell^{\prime}}y.r^{\prime}$. This means that $q_{1}\not\in\mathsf{sub}^{\circ}(q)$, so this case is impossible. 4. 3.4.4

Case $q_{1}$ is a subterm of $r^{\prime}$. If $q_{2}$ is also a subterm of $r^{\prime}$, we conclude since by i.h. $(\lambda^{\ell}x.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential. Otherwise, $q_{2}$ is a subterm of $s_{i}$ for some $i=1..n$, and we also conclude by i.h.. 5. 3.4.5

Case $q_{1}$ is a subterm of $s_{i}$ for some $i=1..n$. If $q_{2}$ is a subterm of $s_{j}$ for some $j=1..n$, we conclude since by i.h. $(\lambda^{\ell}x.r^{\prime})[s^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential. If $q_{2}$ is any other subterm, note that the symmetric case has already been considered in one of the previous cases. 4. 4.

Application, $t=rp$. Then $u^{\prime}\mathrel{\ltimes}(rp)\{x:=s\}$, so it is of the form $u^{\prime}_{0}[u^{\prime}_{j}]_{j=1}^{m}$ where $u^{\prime}_{0}\mathrel{\ltimes}r\{x:=s\}$ and $u^{\prime}_{j}\mathrel{\ltimes}p\{x:=s\}$ for all $j=1..m$. By i.h. we have that $u^{\prime}_{0}$ is of the form $r^{\prime}\{x:=\bar{s}_{0}\}$ and for all $j=1..m$ the term $u^{\prime}_{j}$ is of the form $p^{\prime}_{j}\{x:=\bar{s}_{j}\}$, where $r^{\prime}\mathrel{\ltimes}r$ and $p^{\prime}_{j}\mathrel{\ltimes}p$ for all $j=1..m$. Moreover, the length of the list $\bar{s}_{j}$ is $k_{j}$ and $\bar{s}_{j}=[s^{(j)}_{i}]_{i=1}^{k_{j}}$ for all $j=0..m$, and we have that $s^{(j)}_{i}\mathrel{\ltimes}s$ for all $j=0..m,i=1..k_{j}$. By i.h. we also know that $(\lambda^{\ell}x.r^{\prime})\bar{s}_{0}$ is strongly sequential and $(\lambda^{\ell}x.p^{\prime}_{j})\bar{s}_{j}$ is strongly sequential for all $j=1..m$.

Let $t^{\prime}:=r^{\prime}[p^{\prime}_{j}]_{j=1}^{m}$, let $n:=\sum_{j=0}^{m}k_{j}$, and let $[s^{\prime}_{1},\ldots,s^{\prime}_{n}]:=\sum_{j=0}^{m}\bar{s}_{j}$. Note that $t^{\prime}=r^{\prime}[p^{\prime}_{j}]_{j=1}^{m}\mathrel{\ltimes}rp=t$ and $s^{\prime}_{i}\mathrel{\ltimes}s$ for all $i=1..n$.

Moreover, we have to check that $u^{\prime}=t^{\prime}\{x:=[s^{\prime}_{1},\ldots,s^{\prime}_{n}]\}$. To prove this, note that $t^{\prime}\{x:=[s^{\prime}_{1},\ldots,s^{\prime}_{n}]\}=(r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})\{x:=[s^{\prime}_{1},\ldots,s^{\prime}_{n}]\}$. Suppose that the multiset $\mathtt{T}([s^{\prime}_{1},\ldots,s^{\prime}_{n}])$ were sequential. Then the list of terms $[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$ would be partitioned as $(\bar{u}_{0},\ldots,\bar{u}_{m})$ where $\bar{u}_{j}$ is a permutation of $\bar{s}_{j}$ for all $j=0..m$, and we would have indeed:

[TABLE]

To see that $\mathtt{T}([s^{\prime}_{1},\ldots,s^{\prime}_{n}])$ is sequential, note that for every $i\neq j$, the terms $s^{\prime}_{i}$ and $s^{\prime}_{j}$ are free subterms of $u^{\prime}$ and they lie at disjoint positions of $u^{\prime}$. Since $u^{\prime}$ is strongly sequential, the types of $s^{\prime}_{i}$ and $s^{\prime}_{j}$ have different external labels. Hence $\mathtt{T}([s^{\prime}_{1},\ldots,s^{\prime}_{n}])$ is sequential.

To conclude, we are left to check that $(\lambda^{\ell}x.t^{\prime})[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$ is strongly sequential:

1. 4.1

Uniquely labeled lambdas. The multiset of labels decorating the lambdas of $(\lambda^{\ell}x.t^{\prime})[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$ is given by $\Lambda((\lambda^{\ell}x.t^{\prime})[s^{\prime}_{1},\ldots,s^{\prime}_{n}])=[\ell]+\Lambda(t^{\prime})+_{i=1}^{n}\Lambda(s^{\prime}_{i})$. It suffices to check that this multiset has no repeats. The label $\ell$ is assumed to be fresh, so it occurs only once. We have already argued that $u^{\prime}=t^{\prime}\{x:=[s^{\prime}_{1},\ldots,s^{\prime}_{n}]\}$, so using Lem. 9 we have $\Lambda(u^{\prime})=\Lambda(t^{\prime})+_{i=1}^{n}\Lambda(s^{\prime}_{i})$. Moreover $u^{\prime}$ is correct, so this multiset has no repeats. 2. 4.2

Sequential contexts. Suppose that $\Gamma_{0}\oplus x:\mathcal{M}_{0}\vdash r^{\prime}:[\mathcal{C}_{j}]_{j=1}^{m}\overset{\ell^{\prime}}{\to}\mathcal{A}$ is derivable, $\Gamma_{j}\oplus x:\mathcal{M}_{j}\vdash p^{\prime}_{j}:\mathcal{C}_{j}$ is derivable for all $j=1..m$, and $\Delta_{i}\vdash s^{\prime}_{i}:\mathcal{B}_{i}$ is derivable for all $i=1..n$. Note that $\sum_{j=0}^{m}\mathcal{M}_{j}=[\mathcal{B}_{i}]_{i=1}^{n}$.

Let $q$ be a subterm of $(\lambda^{\ell}x.r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$. Consider four cases for $q$:

1. 4.2.1

Case $q=(\lambda^{\ell}x.r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$. The typing context is $\sum_{j=0}^{m}\Gamma_{j}+\sum_{i=1}^{n}\Delta_{i}$. By Subject Expansion (Lem. 24) the typing context of $(r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})\{x:=[s^{\prime}_{1},\ldots,s^{\prime}_{n}]\}=u^{\prime}$ is also $\sum_{j=0}^{m}\Gamma_{j}+\sum_{i=1}^{n}\Delta_{i}$ and $u^{\prime}$ is correct by hypothesis. So $\sum_{j=0}^{m}\Gamma_{j}+\sum_{i=1}^{n}\Delta_{i}$ is sequential. 2. 4.2.2

Case $q=\lambda^{\ell}x.r^{\prime}[p^{\prime}_{j}]_{j=1}^{m}$. The typing context is $\sum_{j=0}^{m}\Gamma_{j}$, which is sequential because $\sum_{j=0}^{m}\Gamma_{j}+\sum_{i=1}^{n}\Delta_{i}$ is sequential. 3. 4.2.3

Case $q=r^{\prime}[p^{\prime}_{j}]_{j=1}^{m}$. The typing context is $\sum_{j=0}^{m}\Gamma_{j}\oplus x:[\mathcal{B}_{i}]_{i=1}^{n}$, which is sequential because $\sum_{j=0}^{m}\Gamma_{j}$ is sequential and, moreover, $[\mathcal{B}_{i}]_{i=1}^{n}=\mathtt{T}([\mathcal{B}^{\prime}_{1},\ldots,\mathcal{B}^{\prime}_{n}])$ which we have already shown to be sequential. 4. 4.2.4

Otherwise. Then $q$ is a subterm of $r^{\prime}$, a subterm of $p^{\prime}_{j}$ for some $j=1..m$, or a subterm of some $s^{\prime}_{i}$ for some $i=1..n$. Then we conclude since by i.h. $(\lambda^{\ell}x.r^{\prime})\bar{s}_{0}$ and all the $(\lambda^{\ell}x.p^{\prime}_{j})\bar{s}_{j}$ are strongly sequential. 3. 4.3

Sequential types. Let $q$ be a subterm of $(\lambda^{\ell}x.r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})[s^{\prime}_{1},\ldots,s^{\prime}_{n}]$. We claim that if $\mathcal{N}\overset{\ell^{\prime\prime}}{\to}\mathcal{D}$ occurs in the context or in the type of $q$, then $\mathcal{N}$ is sequential. The proof is similar as for subcase . 4. 4.4

Strong sequentiality. Let $q\in\mathsf{sub}((\lambda^{\ell}x.r^{\prime}[p^{\prime}_{j}]_{j=1}^{m})[s^{\prime}_{1},\ldots,s^{\prime}_{n}])$ be a subterm, and let $q_{1},q_{2}\in\mathsf{sub}^{\circ}(q)$ be free subterms lying at disjoint positions of $q$. We claim that the types of $q_{1}$ and $q_{2}$ have different external labels. The proof is similar as for subcase .

Lemma 26 (Backwards Simulation)

Let $t,s\in\mathcal{T}$ be $\lambda$-terms and let $s^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a strongly sequential term such that $t\mathrel{\to_{\beta}}s$ and $s^{\prime}\mathrel{\ltimes}s$. Then there exists a strongly sequential term $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that:

[TABLE]

Proof

Let $t=\mathtt{C}\langle(\lambda x.u)r\rangle\mathrel{\to_{\beta}}\mathtt{C}\langle u\{x:=r\}\rangle=s$. The proof proceeds by induction on $\mathtt{C}$.

Empty, $\mathtt{C}=\Box$. By Lem. 25 we have that $s^{\prime}$ is of the form $u^{\prime}\{x:=[r^{\prime}_{1},\ldots,r^{\prime}_{n}]\}$ where $u^{\prime}\mathrel{\ltimes}u$ and $r^{\prime}_{i}\mathrel{\ltimes}r$ for all $i=1..n$. Moreover, taking $\ell$ to be a fresh label, $(\lambda^{\ell}x.u^{\prime})[r^{\prime}_{1},\ldots,r^{\prime}_{n}]$ is strongly sequential and $(\lambda^{\ell}x.u^{\prime})[r^{\prime}_{1},\ldots,r^{\prime}_{n}]\mathrel{\ltimes}(\lambda x.u)r$. 2. 2.

Under an abstraction, $\mathtt{C}=\lambda x.\mathtt{C}^{\prime}$. Straightforward by i.h.. 3. 3.

Left of an application, $\mathtt{C}=\mathtt{C}^{\prime}\,u$ Straightforward by i.h.. 4. 4.

Right of an application, $\mathtt{C}=u\,\mathtt{C}^{\prime}$ Then $t=u\,r\mathrel{\to_{\beta}}u\,p=s$ where $r\mathrel{\to_{\beta}}p$ and $s^{\prime}\mathrel{\ltimes}s$. Then $s^{\prime}$ is of the form $u^{\prime}[p^{\prime}_{1},\ldots,p^{\prime}_{n}]$ where $p^{\prime}_{i}\mathrel{\ltimes}p$ for all $i=1..n$. By i.h., for all $i=1..n$ we have that there exist $r^{\prime}_{1},\ldots,r^{\prime}_{n}$ such that:

[TABLE]

Moreover, $u^{\prime}[r^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential, which can be concluded from the facts that $u^{\prime}[p^{\prime}_{i}]_{i=1}^{n}$ is strongly sequential by hypothesis, $r^{\prime}_{i}$ is strongly sequential for all $i=1..n$ by i.h., and $r^{\prime}_{i}$ and $p^{\prime}_{i}$ have the same types by Subject Expansion (Lem. 24).

To prove the equivalence $(1\iff 2)$ of Prop. 7, we claim that the following three statements are equivalent:

There exists $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t^{\prime}\mathrel{\ltimes}t$. 2. 1’.

There exists $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t^{\prime}\mathrel{\ltimes}t$ and $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{\mathcal{A}}[]\ldots[]$. 3. 2.

There exists a head normal form $s$ such that $t\mathrel{\to_{\beta}}^{*}s$.

Let us prove the chain of implications $1\implies 2\implies 1^{\prime}\implies 1$:

• •

$(1\implies 2)$ Let $t^{\prime}\mathrel{\ltimes}t$. By Strong Normalization (Prop. 1), reduce $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$ to normal form. We claim that there exists a term $s$ such that $t\mathrel{\to_{\beta}}^{*}s$ and $s^{\prime}\mathrel{\ltimes}s$. Observe that, since $\lambda^{\texttt{{\#}}}$ is strongly normalizing (Prop. 1) and finitely branching, König’s lemma ensures that there is a bound for the length of $\mathrel{\to_{\texttt{{\#}}}}$-derivations going out from a term $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$. (Alternatively, according to the proof of Strong Normalization in Prop. 1, the bound may be explicitly taken to be the number of lambdas in $t^{\prime}$). Call this bound the weight of $t^{\prime}$.

We proceed by induction on the weight of $t^{\prime}$. If the derivation is empty, we are done by taking $s:=t$. If the derivation is non-empty, it is of the form $t^{\prime}\mathrel{\to_{\texttt{{\#}}}}u^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$. By Simulation (Prop. 6) there exist terms $u$ and $u^{\prime\prime}$ such that $u^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}u^{\prime\prime}\mathrel{\ltimes}u$ and $t\mathrel{\to_{\beta}}u$. Since the $\lambda^{\texttt{{\#}}}$-calculus is confluent (Prop. 2) and $s^{\prime}$ is a normal form, we have that $u^{\prime\prime}\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}s^{\prime}$. Note that the weight of $t^{\prime}$ is strictly larger than the weight of $u^{\prime\prime}$, so by i.h. there exists $s$ such that $u\mathrel{\to_{\beta}}^{*}s$ and $s^{\prime}\mathrel{\ltimes}s$:

[TABLE]

Finally, since $s^{\prime}$ is a $\mathrel{\to_{\texttt{{\#}}}}$-normal form and $s^{\prime}\mathrel{\ltimes}s$, Lem. 23 ensures that $s$ is a head normal form, as required.

• •

$(1^{\prime}\implies 1)$ Obvious.

• •

$(2\implies 1^{\prime})$ Let $t\mathrel{\to_{\beta}}^{*}s$ be a derivation to head normal form. We claim that there exists $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ such that $t^{\prime}$ is strongly sequential, and the normal form of $t^{\prime}$ is of the form $\lambda^{\ell_{1}}x_{1}.\ldots\lambda^{\ell_{n}}x_{n}.y^{\mathcal{A}}[]\ldots[]$. By induction on the length of the derivation $t\mathrel{\to_{\beta}}^{*}s$. If the derivation is empty, $t=s$ is a head normal form and we conclude by Lem. 22, observing that the constructed term $t^{\prime}\mathrel{\ltimes}t$ is strongly sequential. If the derivation is non-empty, conclude using the i.h. and Backwards Simulation (Lem. 26).

0.A.9 Proof of Prop. 8 – Compatibility

We need a few auxiliary results.

Lemma 27 (Simulation residuals and composition)

If $\rho,\sigma$ are composable derivations and $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$, then:

$t^{\prime}/\rho\sigma=(t^{\prime}/\rho)/\sigma$ 2. 2.

$\rho\sigma/t^{\prime}=(\rho/t^{\prime})(\sigma/(t^{\prime}/\rho))$

Proof

Straightforward by induction on $\rho$.

An $n$-hole context $\mathtt{C}^{\prime}$ is a term with $n$ ocurrences of a hole $\Box$. We extend refinement for contexts by setting $\Box\mathrel{\ltimes}\Box$. We write $\mathtt{C}\langle t_{1},\ldots,t_{n}\rangle$ for the capturing substitution of the $i$-th occurrence of $\Box$ in $\mathtt{C}$ by $t_{i}$ for all $i=1..n$. If $R:t\mathrel{\to_{\beta}}s$ is a step, we write $\mathtt{C}\langle R\rangle$ for the step $\mathtt{C}\langle R\rangle:\mathtt{C}\langle t\rangle\mathrel{\to_{\beta}}\mathtt{C}\langle s\rangle$. Note that in general a context $\mathtt{C}$ may be refined by an $n$-hole context, for example a [math]-hole context, $x^{[]\overset{1}{\to}\alpha^{2}}[\,]\mathrel{\ltimes}x(y\,\Box)$, or a $2$-hole context, $x^{[\alpha^{1},\beta^{2}]\overset{3}{\to}\gamma^{4}}[\Box,\Box]\mathrel{\ltimes}x\Box$.

Lemma 28 (Simulation of contexts)

Let $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}$, let $t^{\prime}_{1},\ldots,t^{\prime}_{n}\in\mathcal{T}^{\texttt{{\#}}}$ and $t\in\mathcal{T}$ such that $t^{\prime}_{i}\mathrel{\ltimes}t^{\prime}$ for each $i\in\{1,\ldots,n\}$, and $\mathtt{C}^{\prime}\langle t^{\prime}_{1},\ldots,t^{\prime}_{n}\rangle\mathrel{\ltimes}\mathtt{C}\langle t\rangle$. Moreover, let $R:t\mathrel{\to_{\beta}}s$. Then $\mathtt{C}^{\prime}\langle t^{\prime}_{1},\ldots,t^{\prime}_{n}\rangle/\mathtt{C}\langle R\rangle=\mathtt{C}^{\prime}\langle t_{1}/R,\ldots,t_{n}/R\rangle$, and $\mathsf{labs}(\mathtt{C}\langle R\rangle/\mathtt{C}^{\prime}\langle t^{\prime}_{1},\ldots,t^{\prime}_{n}\rangle)=\sum_{i=1}^{n}\mathsf{labs}(R/t^{\prime}_{i})$.

Proof

Straightforward by induction on $\mathtt{C}$.

In the proof of the following lemma (Lem. 29), sometimes we will use the previous lemma (Lem. 28) implicitly.

Lemma 29 (Basic Cube Lemma for simulation residuals)

Let $R:t\mathrel{\to_{\beta}}s$ and $S:t\mathrel{\to_{\beta}}u$ be coinitial steps, and let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a correct term such that $t^{\prime}\mathrel{\ltimes}t$. Then the following equality between sets of coinitial steps holds: $(R/t^{\prime})/(S/t^{\prime})=(R/S)/(t^{\prime}/S)$.

Proof

If $R=S$ then it is easy to see that the proposition holds, so we can assume that $R\neq S$. Also, note that it is enough to see that $\mathsf{labs}((R/t^{\prime})/(S/t^{\prime}))=\mathsf{labs}(((R/S)/(t^{\prime}/S))$, as we will do that in some cases. We proceed by induction on $t$.

Variable $t=x$. Impossible. 2. 2.

Abstraction, $t=\lambda x.u$. Immediate by i.h.. 3. 3.

Application, $t=pq$. Three cases, depending on the position of $R$.

1. 3.1

If $R$ is at the root. Then $t=(\lambda x.r)q$, and $R:(\lambda x.r)q\to r\{x:=q\}$. Then $S$ may be inside $r$ or inside $q$. In any case, the situation is:

[TABLE]

Note that $(R/t^{\prime})/(S/t^{\prime})$ has only one element $R_{1}$, namely the step contracting the lambda labeled with $\ell$. Note that $R/S$ also happens to have only one element, $R_{2}:(\lambda x.r^{\circ})q^{\circ}\mathrel{\to_{\beta}}r^{\circ}\{x:=q^{\circ}\}$. It is easy to see that $R_{2}/((\lambda^{\ell}x.r^{\prime})\bar{q})=\{R_{1}\}$, as required. 2. 3.2

If $R$ is in $p$. We consider three subcases, depending on the position of $S$.

1. 3.2.1

If $S$ is at the root. Then $p=\lambda x.\mathtt{C}\langle(\lambda y.u)v\rangle$ and (for appropiate $\mathtt{C}^{\circ},u^{\circ},v^{\circ}$):

[TABLE]

[TABLE]

Note that $\mathsf{labs}((R/t^{\prime})/(S/t^{\prime}))=\{\ell_{1},\ldots,\ell_{n}\}$. Similarly, $\mathsf{labs}((R/S)/(t^{\prime}/S))=\{\ell_{1},\ldots,\ell_{n}\}$, as required. 2. 3.2.2

If $S$ is in $p$. Straightforward by i.h.. 3. 3.2.3

If $S$ is in $q$. Straightforward since the steps are disjoint. 3. 3.3

If $R$ is in $q$. We consider three subcases, depending on the position of $S$.

1. 3.3.1

If $S$ is at the root. Then $p=\lambda x.s$ and $t=(\lambda x.s)\mathtt{C}\langle(\lambda y.u)v\rangle$.

[TABLE]

[TABLE]

Note that $R/S$ has as many elements as there are free occurrences of $x$ in $s$. In particular, $S$ may erase or multiply $R$. In turn $s^{\prime}$ has a number of free occurrences of $x$, more precisely $n$ free occurrences of $x$, i.e. the cardinality of the argument of the application. By Lem. 28, each step in $R/S$, when projected onto $t^{\prime}/S$ yields a set of labels $\{\ell_{i,1},\ldots,\ell_{i,m_{i}}\}$. So $\mathsf{labs}((R/S)/(t^{\prime}/S))=\sum_{i=1}^{n}\{\ell_{i,1},\ldots,\ell_{i,m_{i}}\}=\mathsf{labs}((R/t^{\prime})/(S/t^{\prime}))$ as required. 2. 3.3.2

If $S$ is in $p$. Straightforward since the steps are disjoint. 3. 3.3.3

If $S$ is in $q$. Straightforward by i.h..

Lemma 30 (Simulation residual of a development)

Let $\mathcal{M}$ be a set of coinitial steps in the $\lambda$-calculus, let $\rho$ be a complete development of $\mathcal{M}$, and let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a correct term such that $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$. Then $\rho/t^{\prime}$ is a complete development of $\mathcal{M}/t^{\prime}$.

Proof

Recall that developments are finite and the $\lambda$-calculus is finitely branching so, by König’s lemma, the length of a development of a set $\mathcal{M}$ is bounded. This bound is called the depth of $\mathcal{M}$. We proceed by induction on the depth of $\mathcal{M}$.

Base case. Immediate. 2. 2.

Induction. Then $\mathcal{M}$ must be non-empty. Let $\mathcal{M}=\{R_{1},\ldots,R_{n},S\}$ for some $n\geq 0$, and let $\rho$ be a complete development of $\mathcal{M}$. Without loss of generality, we may assume that $\rho=S\rho^{\prime}$, where $\rho^{\prime}$ is a complete development of $\mathcal{M}^{\prime}=\mathcal{M}/S$. Note that the depth of $\mathcal{M}^{\prime}$ is strictly lesser than the depth of $\mathcal{M}$. By i.h., $\rho^{\prime}/(t^{\prime}/S)$ is a complete development of $\mathcal{M}^{\prime}/(t^{\prime}/S)=\bigcup_{i=1}^{n}\frac{R_{i}/S}{t^{\prime}/S}$. By the Basic Cube Lemma (Lem. 29) this set is equal to $\bigcup_{i=1}^{n}\frac{R_{i}/t^{\prime}}{S/t^{\prime}}$. Then $(S/t^{\prime})(\rho^{\prime}/(t^{\prime}/S))$ is a complete development of $\mathcal{M}/t^{\prime}=(R_{1}/t^{\prime})\cup\ldots\cup(R_{n}/t^{\prime})\cup(S/t^{\prime})$. To conclude, note that $\rho/t^{\prime}=S\rho^{\prime}/t^{\prime}=(S/t^{\prime})(\rho^{\prime}/(t^{\prime}/S))$ so we are done.

Lemma 31 (Compatibility for developments)

Let $\mathcal{M}$ be a set of coinitial steps, and let $\rho$ and $\sigma$ be complete developments of $\mathcal{M}$, and let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a correct term such that $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$. Then $\rho/t^{\prime}\equiv\sigma/t^{\prime}$.

Proof

This is an immediate consequence of Lem. 30, since $\rho/t^{\prime}$ and $\sigma/t^{\prime}$ are both complete developments of $\mathcal{M}/t^{\prime}$, hence permutation equivalent.

The proof of Prop. 8 proceeds as follows. Let $\rho\equiv\sigma$ be permutation equivalent derivations in the $\lambda$-calculus, let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a correct term such that $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$, and let us show that:

$t^{\prime}/\rho=t^{\prime}/\sigma$ 2. 2.

$\rho/t^{\prime}\equiv\sigma/t^{\prime}$

Recall that, in an orthogonal axiomatic rewrite system, permutation equivalence may be defined as the reflexive and transitive closure of the permutation axiom $\tau_{1}R\sigma\tau_{2}\equiv\tau_{1}S\rho\tau_{2}$, where $\tau_{1}$ and $\tau_{2}$ are arbitrary derivations, $\sigma$ is a complete development of $S/R$, and $\rho$ is a complete development of $R/S$. For this definition of permutation equivalence, see for example [28, Def. 2.17], and . We prove each item separately:

For the first item, we proceed by induction on the derivation that $\rho\equiv\sigma$. Reflexivity and transitivity are trivial, so we concentrate on the permutation axiom itself. Let $\tau_{1}R\sigma\tau_{2}\equiv\tau_{1}S\rho\tau_{2}$, where $\tau_{1}$ and $\tau_{2}$ are arbitrary derivations, $\sigma$ is a complete development of $S/R$, and $\rho$ is a complete development of $R/S$, and let us show that $t^{\prime}/\tau_{1}R\sigma\tau_{2}=t^{\prime}/\tau_{1}S\rho\tau_{2}$. By Lem. 27 we have that:

[TABLE]

so, without loss of generality, it suffices to show that for an arbitrary term $s^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$, we have $s^{\prime}/R\sigma=s^{\prime}/S\rho$. By definition of simulation residual, the derivations below have the indicated sources and targets:

[TABLE]

Moreover:

[TABLE]

So $R\sigma/s^{\prime}$ and $S\rho/s^{\prime}$ are permutation equivalent. In particular, they have the same target, so $s^{\prime}/R\sigma=s^{\prime}/S\rho$ as required. 2. 2.

The proof of the second item is also by induction on the derivation that $\rho\equiv\sigma$. Let $\tau_{1}R\sigma\tau_{2}\equiv\tau_{1}S\rho\tau_{2}$, where $\tau_{1}$ and $\tau_{2}$ are arbitrary derivations, $\sigma$ is a complete development of $S/R$, and $\rho$ is a complete development of $R/S$, and let us show that $\tau_{1}R\sigma\tau_{2}/t^{\prime}=\tau_{1}S\rho\tau_{2}/t^{\prime}$. By Lem. 27 we have that:

[TABLE]

where $s^{\prime}=t^{\prime}/\tau_{1}$, $u^{\prime}=s^{\prime}/\tau_{1}R\sigma$, and $u^{\prime\prime}=s^{\prime}/\tau_{1}S\rho$. Similarly as before, we can prove that $R\sigma/s^{\prime}\equiv S\rho/s^{\prime}$. By item 1 of this proposition, we have $u^{\prime}=u^{\prime\prime}$, so $\tau_{2}/u^{\prime}\equiv\tau_{2}/u^{\prime\prime}$, which finishes the proof.

0.A.10 Proof of Lem. 4 – Cube Lemma for simulation residuals

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and $\sigma:t\mathrel{\twoheadrightarrow_{\beta}}u$ be coinitial derivations, and let $t^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ be a correct term such that $t^{\prime}\mathrel{\ltimes}t$. The statement of Lem. 4 claims that the following equivalence holds:

[TABLE]

Before proving Lem. 4, we prove three auxiliary lemmas, all of which are particular cases of the main result.

Lemma 32

$(R/t^{\prime})/(\sigma/t^{\prime})\equiv(R/\sigma)/(t^{\prime}/\sigma)$.

Proof

By induction on $\sigma$:

Empty, $\sigma=\epsilon$. Immediate since $R/t^{\prime}=R/t^{\prime}$. 2. 2.

Non-empty, $\sigma=S\sigma^{\prime}$. Then:

[TABLE]

Lemma 33

Let $\mathcal{M}$ be a set of coinitial steps in the $\lambda$-calculus. Then $(\mathcal{M}/t^{\prime})/(S/t^{\prime})$ and $(\mathcal{M}/S)/(t^{\prime}/S)$ are equal as sets.

Proof

Using Lem. 29:

[TABLE]

Lemma 34

Let $\mathcal{M}$ be a set of coinitial steps in the $\lambda$-calculus, and let $\mathcal{M}$ also stand for some (canonical) complete development of $\mathcal{M}$. Then $(\rho/t^{\prime})/(\mathcal{M}/t^{\prime})\equiv(\rho/\mathcal{M})/(t^{\prime}/\mathcal{M})$.

Proof

By induction on $\rho$:

Empty, $\rho=\epsilon$. Immediate since $\epsilon=\epsilon$. 2. 2.

Non-empty, $\rho=R\rho^{\prime}$. Then:

[TABLE]

For the equality marked with ($\star$), observe that $(t^{\prime}/R)/(\mathcal{M}/R)=t^{\prime}/(R\sqcup\mathcal{M})$ and $(t^{\prime}/\mathcal{M})/(R/\mathcal{M})=t^{\prime}/(\mathcal{M}\sqcup R)$ by definition. Moreover $R\sqcup\mathcal{M}\equiv\mathcal{M}\sqcup R$, so by Compatibility (Prop. 8), $(t^{\prime}/R)/(\mathcal{M}/R)=(t^{\prime}/\mathcal{M})/(R/\mathcal{M})$.

Now the proof of Lem. 4 proceeds by induction on $\rho$:

Empty $\rho=\epsilon$. Immediate since $\epsilon=\epsilon$. 2. 2.

Non-empty, $\rho=R\rho^{\prime}$. Then:

[TABLE]

For the equality marked with ($\star$), observe that $(t^{\prime}/\sigma)/(R/\sigma)=t^{\prime}/(\sigma\sqcup R)$ and $(t^{\prime}/R)/(\sigma/R)=t^{\prime}/(R\sqcup\sigma)$ by definition. Moreover $\sigma\sqcup R\equiv R\sqcup\sigma$, so by Compatibility (Prop. 8), $(t^{\prime}/\sigma)/(R/\sigma)=(t^{\prime}/R)/(\sigma/R)$.

0.A.11 Proof of Prop. 9 – Properties of garbage

Let $\sigma\sqsubseteq\rho$. Then $\sigma\tau\equiv\rho$ for some $\tau$, so $\sigma/t^{\prime}\sqsubseteq(\sigma/t^{\prime})(\tau/(t^{\prime}/\sigma))=\sigma\tau/t^{\prime}\equiv\rho/t^{\prime}$ by Compatibility (Prop. 8). 2. 2.

Note that $\rho\sigma/t^{\prime}=(\rho/t^{\prime})(\sigma/(t^{\prime}/\rho))$. So $\rho\sigma/t^{\prime}$ is empty if and only if $\rho/t^{\prime}$ and $\sigma/(t^{\prime}/\rho)$ are empty. 3. 3.

Suppose that $\rho/t^{\prime}=\epsilon$. Then $(\rho/\sigma)/(t^{\prime}/\sigma)=(\rho/t^{\prime})/(\sigma/t^{\prime})$ by the Cube Lemma (Lem. 4). 4. 4.

By the Cube Lemma (Lem. 4): $(\rho\sqcup\sigma)/t^{\prime}=\rho(\sigma/\rho)/t^{\prime}=(\rho/t^{\prime})((\sigma/\rho)/(t^{\prime}/\rho)\equiv(\rho/t^{\prime})((\sigma/t^{\prime})/(\rho/t^{\prime}))=(\rho/t^{\prime})\sqcup(\sigma/t^{\prime})$. So $(\rho\sqcup\sigma)/t^{\prime}$ is empty if and only if $\rho/t^{\prime}$ and $\sigma/t^{\prime}$ are empty.

0.A.12 Proof of Lem. 5 – Sieving is well-defined

Note that $t^{\prime}/R_{0}\mathrel{\ltimes}\rho/R_{0}$ by definition of simulation residual, so the recursive call can be made.

To see that recursion is well-founded, consider the measure given by $M(\rho,t^{\prime})=\#\mathsf{labs}(\rho/t^{\prime})$. Let $R_{0}$ be a coarse step for $(\rho,t^{\prime})$. Observe that $R_{0}\sqsubseteq\rho$ so $R_{0}/t^{\prime}\sqsubseteq\rho/t^{\prime}$ by Coro. 2. Then $\mathsf{labs}(R_{0}/t^{\prime})\subseteq\mathsf{labs}(\rho/t^{\prime})$ by Prop. 12. So we have:

[TABLE]

as required.

0.A.13 Proof of Prop. 10 – Properties of sieving

To prove Prop. 10 we first prove various auxiliary results.

Lemma 35 (The sieve is a prefix)

Let $\rho:t\mathrel{\to_{\beta}}^{*}s$ and $t^{\prime}\mathrel{\ltimes}t$. Then $\rho\Downarrow t^{\prime}\sqsubseteq\rho$.

Proof

By induction on the length of $\rho\Downarrow t^{\prime}$. If there are no coarse steps for $(\rho,t^{\prime})$, then trivially $\rho\Downarrow t^{\prime}=\epsilon\sqsubseteq\rho$. If there is a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the leftmost such step. Then:

[TABLE]

We also need the following technical lemma:

Lemma 36 (Refinement of a context)

The following are equivalent:

$t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle s\rangle$, 2. 2.

$t^{\prime}$ is of the form $\mathtt{C}^{\prime}\langle s^{\prime}_{1},\ldots,s^{\prime}_{n}\rangle$, where $\mathtt{C}^{\prime}$ is an $n$-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}$ and $s^{\prime}_{i}\mathrel{\ltimes}s$ for all $1\leq i\leq n$. Note that $n$ might be [math], in which case $\mathtt{C}^{\prime}$ is a term.

Moreover, in the implication $(1\implies 2)$, the decomposition is unique, i.e. the context $\mathtt{C}^{\prime}$, the number of holes $n\geq 0$, and the terms $s^{\prime}_{1},\ldots,s^{\prime}_{n}$ are the unique possible such objects.

Proof

Straightforward by induction on $\mathtt{C}$.

Lemma 37 (Garbage only interacts with garbage)

The following hold:

Garbage only creates garbage. Let $R$ and $S$ be composable steps in the $\lambda$-calculus, and let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(R)$. If $R$ creates $S$ and $R$ is $t^{\prime}$-garbage, then $S$ is $(t^{\prime}/R)$-garbage. 2. 2.

Garbage only duplicates garbage. Let $R$ and $S$ be coinitial steps in the $\lambda$-calculus and let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(R)$. If $R$ duplicates $S$, i.e. $\#(S/R)>1$, and $R$ is $t^{\prime}$-garbage, then $S$ is $(t^{\prime}/R)$-garbage.

Proof

We prove each item separately:

According to Lévy [25], there are three creation cases in the $\lambda$-calculus. We consider the three possibilities for $R$ creating $S$:

1. 1.1

Case I, $\mathtt{C}\langle(\lambda x.x)(\lambda y.s)u\rangle\mathrel{\xrightarrow{R}_{\beta}}\mathtt{C}\langle(\lambda y.s)u\rangle\mathrel{\xrightarrow{S}_{\beta}}\mathtt{C}\langle s\{y:=u\}\rangle$. Then by Lem. 36, the term $t^{\prime}$ is of the form $\mathtt{C}^{\prime}\langle\Delta_{1},\ldots,\Delta_{n}\rangle$ where $\mathtt{C}^{\prime}$ is an $n$-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,u\rangle$ and $\Delta_{i}\mathrel{\ltimes}(\lambda x.x)(\lambda y.s)$ for all $1\leq i\leq n$. Since $R$ is garbage, we know that actually $n=0$. So $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,u\rangle$ and $R/t^{\prime}:t^{\prime}\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}t^{\prime}=t^{\prime}/R$ in zero steps. Hence $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle(\lambda y.s)u\rangle$, so by Lem. 36, the term $t^{\prime}$ can be written in a unique way as $\mathtt{C}^{\prime\prime}\langle\Sigma_{1},\ldots,\Sigma_{m}\rangle$, where $\mathtt{C}^{\prime\prime}$ is an $m$-hole context such that $\mathtt{C}^{\prime\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,u\rangle$ and $\Sigma_{i}\mathrel{\ltimes}\lambda y.s$ for all $1\leq i\leq m$. Since the decomposition is unique and $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,u\rangle$, we conclude that $m=0$. Hence $S$ is $(t^{\prime}/R)$-garbage. 2. 1.2

Case II, $\mathtt{C}\langle(\lambda x.\lambda y.s)\,u\,r\rangle\mathrel{\xrightarrow{R}_{\beta}}\mathtt{C}\langle(\lambda y.s\{x:=u\})\,r\rangle\mathrel{\xrightarrow{S}_{\beta}}\mathtt{C}\langle s\{x:=u\}\{y:=r\}\rangle$. Then by Lem. 36, the term $t^{\prime}$ is of the form $\mathtt{C}^{\prime}\langle\Delta_{1},\ldots,\Delta_{n}\rangle$ where $\mathtt{C}^{\prime}$ is an $n$-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,r\rangle$ and $\Delta_{i}\mathrel{\ltimes}(\lambda x.\lambda y.s)\,u$ for all $1\leq i\leq n$. Since $R$ is garbage, we know that actually $n=0$. So $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,r\rangle$ and $R/t^{\prime}:t^{\prime}\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}t^{\prime}=t^{\prime}/R$ in zero steps. Hence $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle(\lambda y.s\{x:=u\})\,r\rangle$, so by Lem. 36, the term $t^{\prime}$ can be written in a unique way as $\mathtt{C}^{\prime\prime}\langle\Sigma_{1},\ldots,\Sigma_{n}\rangle$, where $\mathtt{C}^{\prime\prime}$ is an $m$-hole context such that $\mathtt{C}^{\prime\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,r\rangle$ and $\Sigma_{i}\mathrel{\ltimes}\lambda y.s\{x:=u\}$ for all $1\leq i\leq m$. Since the decomposition is unique and $t^{\prime}\mathrel{\ltimes}\mathtt{C}\langle\Box\,r\rangle$, we conclude that $m=0$. Hence $S$ is $(t^{\prime}/R)$-garbage. 3. 1.3

Case III, $\mathtt{C}_{1}\langle(\lambda x.\mathtt{C}_{2}\langle x\,s\rangle)\,(\lambda y.u)\rangle\mathrel{\xrightarrow{R}_{\beta}}\mathtt{C}_{1}\langle\hat{\mathtt{C}}_{2}\langle(\lambda y.u)\,\hat{s}\rangle\rangle\mathrel{\xrightarrow{S}_{\beta}}\mathtt{C}_{1}\langle\hat{\mathtt{C}}_{2}\langle u\{y:=\hat{s}\}\rangle\rangle$, where $\hat{\mathtt{C}}_{2}=\mathtt{C}_{2}\{x:=\lambda y.u\}$ and $\hat{t}=t\{x:=\lambda y.u\}$. Then by Lem. 36, the term $t^{\prime}$ is of the form $\mathtt{C}^{\prime}\langle\Delta_{1},\ldots,\Delta_{n}\rangle$ where $\mathtt{C}^{\prime}$ is an $n$-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}$ and $\Delta_{i}\mathrel{\ltimes}(\lambda x.\mathtt{C}_{2}\langle x\,s\rangle)\,(\lambda y.u)$ for all $1\leq i\leq n$. Since $R$ is garbage, we know that actually $n=0$. So $t^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}$ and $R/t^{\prime}:t^{\prime}\mathrel{\twoheadrightarrow_{\texttt{{\#}}}}t^{\prime}=t^{\prime}/R$ in zero steps. Hence $t^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}\langle\hat{\mathtt{C}}_{2}\langle(\lambda y.u)\,\hat{s}\rangle\rangle$, so by Lem. 36, the term $t^{\prime}$ can be written in a unique way as $\mathtt{C}^{\prime\prime}\langle\Sigma_{1},\ldots,\Sigma_{m}\rangle$, where $\mathtt{C}^{\prime\prime}\mathrel{\ltimes}\mathtt{C}_{1}$ and $\Sigma_{i}\mathrel{\ltimes}\hat{\mathtt{C}}_{2}\langle(\lambda y.u)\,\hat{s}\rangle$ for all $1\leq i\leq m$. Since the decomposition is unique and $t^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}$, we conclude that $m=0$. Hence $S$ is $(t^{\prime}/R)$-garbage. 2. 2.

Since $R$ duplicates $S$, the redex contracted by $S$ lies inside the argument of $R$, that is, the source term is of the form $\mathtt{C}_{1}\langle(\lambda x.t)\mathtt{C}_{2}\langle(\lambda y.s)u\rangle\rangle$ where the pattern of $R$ is $(\lambda x.t)\mathtt{C}_{2}\langle(\lambda y.s)u\rangle$, and the pattern of $S$ is $(\lambda y.s)u$. By Lem. 36, the term $t^{\prime}$ is of the form $\mathtt{C}^{\prime}\langle\Delta_{1},\ldots,\Delta_{n}\rangle$ where $\mathtt{C}^{\prime}$ is an $n$-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}$ and $\Delta_{i}\mathrel{\ltimes}(\lambda x.t)\mathtt{C}_{2}\langle(\lambda y.s)u\rangle$ for all $1\leq i\leq n$. Since $R$ is garbage, we know that $n=0$. By Lem. 36, the term $t^{\prime}$ can be written as $\mathtt{C}^{\prime\prime}\langle\Sigma_{1},\ldots,\Sigma_{m}\rangle$ where $\mathtt{C}^{\prime\prime}\mathrel{\ltimes}\mathtt{C}_{1}\langle(\lambda x.t)\mathtt{C}_{2}\rangle$ and $\Sigma_{i}\mathrel{\ltimes}(\lambda y.s)u$ for all $1\leq i\leq m$. Note that $t^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}$ so $t^{\prime}\mathrel{\ltimes}\mathtt{C}_{1}\langle(\lambda x.t)\mathtt{C}_{2}\rangle$, as can be checked by induction on $\mathtt{C}_{1}$. Since the decomposition is unique, this means that $m=0$, and thus $S$ is garbage.

Proposition 13 (Characterization of garbage)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and $t^{\prime}\mathrel{\ltimes}t$. The following are equivalent:

$\rho\Downarrow t^{\prime}=\epsilon$. 2. 2.

There are no coarse steps for $(\rho,t^{\prime})$. 3. 3.

The derivation $\rho$ is $t^{\prime}$-garbage.

Proof

It is immediate to check that items 1 and 2 are equivalent, by definition of sieving, so let us prove $2\implies 3$ and $3\implies 2$:

• •

$(2\implies 3)$ We prove the contrapositive, namely that if $\rho$ is not garbage, there is a coarse step for $(\rho,t^{\prime})$. Suppose that $\rho$ is not garbage, i.e. $\rho/t^{\prime}\neq\epsilon$. Then by Prop. 9 we have that $\rho$ can be written as $\rho=\rho_{1}R\rho_{2}$ where all the steps in $\rho_{1}$ are garbage and $R$ is not garbage. By the fact that garbage only creates garbage (Lem. 37) the step $R$ has an ancestor $R_{0}$, i.e. $R\in R_{0}/\rho_{1}$. Moreover, since garbage only duplicates garbage (Lem. 37) we have that $R_{0}/\rho_{1}=R$. Given that $R$ is not garbage, we have that:

[TABLE]

Since $(R_{0}/t^{\prime})/(\rho_{1}/t^{\prime})\neq\varnothing$, in particular, $R_{0}/t^{\prime}\neq\varnothing$, which means that $R_{0}$ is not garbage. Moreover, $R_{0}\sqsubseteq\rho_{1}R\rho_{2}=\rho$. So $R_{0}$ is coarse for $(\rho,t^{\prime})$.

• •

$(3\implies 2)$ Let $\rho$ be garbage, suppose that there is a coarse step $R$ for $(\rho,t^{\prime})$, and let us derive a contradiction. Since $R$ is coarse for $(\rho,t^{\prime})$, we have that $R\sqsubseteq\rho$, so $R/t^{\prime}\sqsubseteq\rho/t^{\prime}$ by Coro. 2. But $\rho/t^{\prime}$ is empty because $\rho$ is $t^{\prime}$-garbage, that is, $R/t^{\prime}\sqsubseteq\sigma/t^{\prime}=\epsilon$, which means that $R$ is also $t^{\prime}$-garbage. This contradicts the fact that $R$ is coarse for $(\rho,t^{\prime})$.

Lemma 38 (The leftmost coarse step has at most one residual)

Let $R_{0}$ be the leftmost coarse step for $(\rho,t^{\prime})$, and let $\sigma\sqsubseteq\rho$. Then $\#(R_{0}/\sigma)\leq 1$.

Proof

By induction on the length of $\sigma$. The base case is immediate. For the inductive step, let $\sigma=S\tau\sqsubseteq\rho$. Then in particular $S\sqsubseteq\rho$. We consider two cases, depending on whether $R_{0}=S$.

Equal, $R_{0}=S$. Then $R_{0}/\sigma=R_{0}/R_{0}\tau=\varnothing$ and we are done. 2. 2.

Non-equal, $R_{0}\neq S$. First we argue that $R_{0}/S$ has exactly one residual $R_{1}\in R_{0}/S$. To see this, we consider two further cases, depending on whether $S$ is $t^{\prime}$-garbage or not:

1. 2.1

If $S$ is not $t^{\prime}$-garbage. Then $S\sqsubseteq\rho$ and $S/t^{\prime}=\varnothing$, so $S$ is coarse for $(\rho,t^{\prime})$. Since $R_{0}$ is the leftmost coarse step, this means that $R$ is to the left of $S$. So $R_{0}$ has exactly one residual $R_{1}\in R_{0}/S$. 2. 2.2

If $S$ is $t^{\prime}$-garbage. Let us write the term $t$ as $t=\mathtt{C}\langle(\lambda x.s)u\rangle$, where $(\lambda x.s)u$ is the pattern of the redex $S$. By Lem. 36 the term $t^{\prime}$ is of the form $t^{\prime}=\mathtt{C}^{\prime}[\Delta_{1},\ldots,\Delta_{n}]$, where $\mathtt{C}^{\prime}$ is a many-hole context such that $\mathtt{C}^{\prime}\mathrel{\ltimes}\mathtt{C}$ and $\Delta_{i}\mathrel{\ltimes}(\lambda x.s)u$ for all $1\leq i\leq n$. We know that $S$ is garbage, so $n=0$ and $t^{\prime}=\mathtt{C}^{\prime}$ is actually a [math]-hole context (i.e. a term). On the other hand, $R_{0}$ is coarse for $(\rho,t^{\prime})$, so in particular it is not $t^{\prime}$-garbage. This means that the pattern of the redex $R_{0}$ cannot occur inside the argument $u$ of the redex $S$. So $S$ does not erase or duplicate $R$, i.e. $R_{0}$ has exactly one residual $R_{1}\in R_{0}/S$.

Now we have that $R_{0}/S\tau=R_{1}/\tau$. We are left to show that $\#(R_{0}/S\tau)\leq 1$. Let us show that we may apply the i.h. on $R_{1}$. More precisely, observe that $\tau\sqsubseteq\rho/S$ since $S\tau\sqsubseteq\rho$. To apply the i.h. it suffices to show that $R_{1}$ is coarse for $(\rho/S,t^{\prime}/S)$. Indeed, we may check the two conditions for the definition that $R_{1}$ is coarse for $(\rho/S,t^{\prime}/S)$.

1. 2.1

Firstly, $R_{1}=R_{0}/S\sqsubseteq\rho/S$ holds, as a consequence of the fact that $R_{0}\sqsubseteq\rho$. 2. 2.2

Secondly, we may check that $R_{1}$ is not $(t^{\prime}/S)$-garbage. To see this, i.e. that $R_{1}/(t^{\prime}/S)$ is non-empty, we check that $\mathsf{labs}(R_{1}/(t^{\prime}/S))$ is non-empty.

[TABLE]

For the last step, note that $\mathsf{labs}(R_{0}/t^{\prime})$ and $\mathsf{labs}(S/t^{\prime})$ are disjoint, since $R_{0}\neq S$.

Applying the i.h., we obtain that $\#(R_{0}/S\tau)=\#(R_{1}/\tau)\leq 1$.

Lemma 39

Let $R$ be a step, let $\rho$ a coinitial derivation, and let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(R)$. Suppose that $R$ is not $t^{\prime}$-garbage, and that $R/\rho_{1}$ is a singleton for every prefix $\rho_{1}\sqsubseteq\rho$. Then $R/\rho$ is not $(t^{\prime}/\rho)$-garbage.

Proof

By induction on $\rho$. The base case, when $\rho=\epsilon$, is immediate since we know that $R$ is not garbage. For the inductive step, suppose that $\rho=S\sigma$. We know that $R/S$ is a singleton, so let $R_{1}=R/S$. Note that $R_{1}/(t^{\prime}/S)=(R/S)/(t^{\prime}/S)=(R/t^{\prime})/(S/t^{\prime})$ by Lem. 4. We know that $R/t^{\prime}$ is non-empty, because $R$ is not garbage. Moreover, $\mathsf{labs}(R/t^{\prime})$ and $\mathsf{labs}(S/t^{\prime})$ are disjoint since $R\neq S$. So $\#\mathsf{labs}((R/t^{\prime})/(S/t^{\prime}))=\mathsf{labs}(R/t^{\prime})$ by Lem. 18. This means that the set $R_{1}/(t^{\prime}/S)$ is non-empty, so $R_{1}$ is not $(t^{\prime}/S)$-garbage . By i.h. we obtain that $R_{1}/\sigma$ is not $((t^{\prime}/S)/\sigma)$-garbage, which means that $(R/S\sigma)/(t^{\prime}/S\sigma)\neq\varnothing$, i.e. that $R/S\sigma$ is not garbage, as required. To be able to apply the i.h., observe that if $\sigma_{1}$ is a prefix of $\sigma$, then $S\sigma_{1}$ is a prefix of $\rho$, so the fact that $R$ has a single residual after $S\sigma_{1}$ implies that the step $R_{1}=R/S$ has a single residual after $\sigma_{1}$.

Proposition 14 (Characterization of garbage-free derivations)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and $t^{\prime}\mathrel{\ltimes}t$. The following are equivalent:

$\rho$ is $t^{\prime}$-garbage-free. 2. 2.

$\rho\equiv\rho\Downarrow t^{\prime}$. 3. 3.

$\rho\equiv\sigma\Downarrow t^{\prime}$ for some derivation $\sigma$.

Proof

Let us prove $1\implies 2\implies 3\implies 1$:

• •

$(1\implies 2)$ Suppose that $\rho$ is $t^{\prime}$-garbage-free, and let us show that $\rho\equiv\rho\Downarrow t^{\prime}$ by induction on the length of $\rho\Downarrow t^{\prime}$.

If there are no coarse steps for $(\rho,t^{\prime})$, By Prop. 13, any derivation with no coarse steps is garbage. So $\rho$ is $t^{\prime}$-garbage. Since $\rho$ is garbage-free, this means that $\rho=\epsilon$. Hence $\rho=\epsilon=\rho\Downarrow t^{\prime}$, as required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the leftmost such step. Note that $\rho\equiv R_{0}(\rho/R_{0})$ since $R_{0}\sqsubseteq\rho$. Moreover, we claim that $\rho/R_{0}$ is $(t^{\prime}/R_{0})$-garbage-free. Let $\sigma\sqsubseteq\rho/R_{0}$ such that $(\rho/R_{0})/\sigma$ is garbage with respect to the term $(t^{\prime}/R_{0})/\sigma=t^{\prime}/R_{0}\sigma$, and let us show that $(\rho/R_{0})/\sigma$ is empty. Note that:

[TABLE]

Moreover, we know that the derivation $\rho/R_{0}\sigma=(\rho/R_{0})/\sigma$ is $(t^{\prime}/R_{0}\sigma)$-garbage. So, given that $\rho$ is $t^{\prime}$-garbage-free, we conclude that $\rho/R_{0}\sigma=\epsilon$, that is $(\rho/R_{0})/\sigma=\epsilon$, which completes the proof of the claim that $\rho/R_{0}$ is $(t^{\prime}/R_{0})$-garbage-free. We conclude as follows:

[TABLE]

• •

$(2\implies 3)$ Obvious, taking $\sigma:=\rho$.

• •

$(3\implies 1)$ Let $\rho\equiv\sigma\Downarrow t^{\prime}$. Let us show that $\rho$ is garbage-free by induction on the length of $\sigma\Downarrow t^{\prime}$.

If there are no coarse steps for $(\sigma,t^{\prime})$, then $\rho\equiv\sigma\Downarrow t^{\prime}=\epsilon$, which means that $\rho=\epsilon$. Observe that the empty derivation is trivially garbage-free.

If there exists a coarse step for $(\sigma,t^{\prime})$, let $R_{0}$ be the leftmost such step. Then $\rho\equiv\sigma\Downarrow t^{\prime}=R_{0}((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))$. To see that $\rho$ is $t^{\prime}$-garbage-free, let $\tau\sqsubseteq\rho$ such that $\rho/\tau$ is garbage, and let us show that $\rho/\tau$ is empty. We know that $\rho/\tau$ is of the following form (modulo permutation equivalence):

[TABLE]

That is, we know that the following derivation is $(t^{\prime}/\tau)$-garbage, and it suffices to show that it is empty:

[TABLE]

Recall that, in general, $AB$ is garbage if and only if $A$ and $B$ are garbage (Prop. 9). Similarly, $AB$ is empty if and only if $A$ and $B$ are empty. So it suffices to prove the two following implications:

[TABLE]

Let us check that each implication holds:

• –

(A) Suppose that $R_{0}/\tau$ is $(t^{\prime}/\tau)$-garbage, and let us show that $R_{0}/\tau$ is empty. Knowing that the derivation $R_{0}/\tau$ is garbage means that $(R_{0}/\tau)/(t^{\prime}/\tau)=\varnothing$. Since $R_{0}$ is the leftmost step coarse for $(\sigma,t^{\prime})$, by Lem. 38 we have that $\#(R_{0}/\tau)\leq 1$. If $R_{0}/\tau$ is empty we are done, since this is what we wanted to prove.

The remaining possibility is that $R_{0}/\tau$ be a singleton. We argue that this case is impossible. Note that for every prefix $\tau_{1}\sqsubseteq\tau$, the set $R_{0}/\tau_{1}$ is also a singleton, since otherwise it would be empty, as a consequence of Lem. 38. So we may apply Lem. 39 and conclude that, since $R_{0}$ is not $t^{\prime}$-garbage then $R_{0}/\tau$ is not $(t^{\prime}/\tau)$-garbage. This contradicts the hypothesis.

• –

(B) Suppose that $((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))/(\tau/R_{0})$ is garbage with respect to the term $(t^{\prime}/R_{0})/(\tau/R_{0})$, and let us show that it is empty. Since $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$ is a shorter derivation than $\sigma\Downarrow t^{\prime}$, we may apply the i.h. we obtain that $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$ is $(t^{\prime}/R_{0})$-garbage-free. Moreover, the following holds:

[TABLE]

So, by definition of $(\sigma/R_{0})\Downarrow(t^{\prime}/R_{0})$ being garbage-free, the fact that the derivation $((\sigma/R_{0})\Downarrow(t^{\prime}/R_{0}))/(\tau/R_{0})$ is garbage implies that it is empty, as required.

Lemma 40 (The projection after a sieve is garbage)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and $t^{\prime}\mathrel{\ltimes}t$. Then $\rho/(\rho\Downarrow t^{\prime})$ is $(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage.

Proof

By induction on the length of $\rho\Downarrow t^{\prime}$.

If there are no coarse steps for $(\rho,t^{\prime})$, then $\rho\Downarrow t^{\prime}=\epsilon$. Moreover, by Prop. 13, a derivation with no coarse steps is garbage. So $\rho/(\rho\Downarrow t^{\prime})=\rho$ is garbage, as required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the leftmost such step, and let $\sigma=\rho/R_{0}$ and $s^{\prime}=t^{\prime}/R_{0}$. Then:

[TABLE]

By i.h., $\sigma/(\sigma\Downarrow s^{\prime})$ is $(s^{\prime}/(\sigma\Downarrow s^{\prime}))$-garbage. That is:

[TABLE]

Unfolding the definitions of $\sigma$ and $s^{\prime}$ we have that:

[TABLE]

Equivalently:

[TABLE]

Finally, by definition of sieve,

[TABLE]

which means that $\rho/(\rho\Downarrow t^{\prime})$ is $(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage, as required.

The proof of Prop. 10 is a consequence of the preceding results, namely:

**Proof that $\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free and $\rho\Downarrow t^{\prime}\sqsubseteq\rho$.

**Note that $\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free by Prop. 14. Moreover, $\rho\Downarrow t^{\prime}\sqsubseteq\rho$ by Lem. 35. 2. 2.

**Proof that $\rho/(\rho\Downarrow t^{\prime})$ is $(t^{\prime}/(\rho\Downarrow t^{\prime}))$-garbage.

**This is precisely Lem. 40. 3. 3.

**Proof that $\rho$ is $t^{\prime}$-garbage if and only if $\rho\Downarrow t^{\prime}=\epsilon$.

**An immediate consequence of Prop. 13. 4. 4.

**Proof that $\rho$ is $t^{\prime}$-garbage-free if and only if $\rho\Downarrow t^{\prime}\equiv\rho$.

**An immediate consequence of Prop. 14.

0.A.14 Proof of Prop. 11 – Semilattices of garbage-free and garbage derivations

To prove Prop. 11 we need a few auxiliary lemmas:

Lemma 41

Let $\rho\equiv\sigma$. Then $\rho\Downarrow t^{\prime}=\sigma\Downarrow t^{\prime}$.

Proof

Observe that, given two permutation equivalent derivations $\rho$ and $\sigma$, a step $R$ is coarse for $(\rho,t^{\prime})$ if and only if $R$ is coarse for $(\sigma,t^{\prime})$, since $(R\sqsubseteq\rho)\iff(R/\rho=\varnothing)\iff(R/\sigma=\varnothing)\iff(R\sqsubseteq\sigma)$. Using this observation, the proof is straightforward by induction on the length of $\rho\Downarrow t^{\prime}$.

Lemma 42 (Sieving trailing garbage)

Let $\rho$ and $\sigma$ be composable derivations, and let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)$. If $\sigma$ is $(t^{\prime}/\rho)$-garbage, then $\rho\sigma\Downarrow t^{\prime}=\rho\Downarrow t^{\prime}$.

Proof

By induction on the length of $\rho\Downarrow t^{\prime}$. If there are no coarse steps for $(\rho,t^{\prime})$, then by Prop. 13, the derivation $\rho$ is $t^{\prime}$-garbage, so $\rho\sigma$ is $t^{\prime}$-garbage by Prop. 9. Resorting to Prop. 13 we obtain that $\rho\sigma\Downarrow t^{\prime}=\epsilon=\rho\Downarrow t^{\prime}$, as required.

If there exists a coarse step for $(\rho,t^{\prime})$, let $R_{0}$ be the leftmost such step. Then since $R_{0}\sqsubseteq\rho$ also $R_{0}\sqsubseteq\rho\sigma$, so $R_{0}$ is a coarse step for $(\rho\sigma,t^{\prime})$. In particular, since there exists at least one coarse step for $(\rho\sigma,t^{\prime})$, let $S_{0}$ be the leftmost such step. We argue that $R_{0}=S_{0}$. We consider two cases, depending on whether $S_{0}$ is coarse for $(\rho,t^{\prime})$:

If $S_{0}$ is coarse for $(\rho,t^{\prime})$. Then $R_{0}$ and $S_{0}$ are both simultaneously coarse for $(\rho,t^{\prime})$ and for $(\rho\sigma,t^{\prime})$. Note that $R_{0}$ cannot be to the left of $S_{0}$, since then $S_{0}$ would not be the leftmost coarse step for $(\rho\sigma,t^{\prime})$. Symmetrically, $S_{0}$ cannot be to the left of $R_{0}$, since then $R_{0}$ would not be the leftmost coarse step for $(\rho,t^{\prime})$. Hence $R_{0}=S_{0}$ as claimed. 2. 2.

If $S_{0}$ is not coarse for $(\rho,t^{\prime})$. We argue that this case is impossible. Note that $S_{0}\sqsubseteq\rho\sigma$ but it is not the case that $S_{0}\sqsubseteq\rho$, so $S_{0}/\rho$ is not empty. Note also that $S_{0}/\rho\sqsubseteq\sigma$, so by Coro. 2 we have that $(S_{0}/\rho)/(t^{\prime}/\rho)\sqsubseteq\sigma/(t^{\prime}/\rho)$. Moreover, $\sigma/(t^{\prime}/\rho)=\epsilon$ is empty because $\sigma$ is $(t^{\prime}/\rho)$-garbage. This means that $(S_{0}/\rho)/(t^{\prime}/\rho)=\epsilon$. Then we have the following chain of equalities:

[TABLE]

To justify the last step, start by noting that no residual of $S_{0}$ is contracted along the derivation $\rho$. Indeed, if $S_{0}$ had a residual, then $\rho=\rho_{1}S_{1}\rho_{2}$ where $S_{1}\in S_{0}/\rho$. But recall that $S_{0}$ is the leftmost coarse step for $(\rho\sigma,t^{\prime})$ and $\rho_{1}\sqsubseteq\rho\sigma$, so it has at most one residual (Lem. 38). This means that $S_{0}/\rho_{1}=S_{1}$, so $S_{0}/\rho=\varnothing$, which is a contradiction. Given that no residuals of $S_{0}$ are contracted along the derivation $\rho$, we have that the sets $\mathsf{labs}(S_{0}/t^{\prime})$ and $\mathsf{labs}(\rho/t^{\prime})$ are disjoint which justifies the last step.

According to the chain of equalities above, we have that $\mathsf{labs}(S_{0}/t^{\prime})=\varnothing$. This means that $S_{0}$ is $t^{\prime}$-garbage. This in turn contradicts the fact that $S_{0}$ is coarse for $(\rho\sigma,t^{\prime})$, confirming that this case is impossible.

We have just claimed that $R_{0}=S_{0}$. Then we conclude as follows:

[TABLE]

Let us check the two items of Prop. 11:

The set $\mathbb{F}(t^{\prime},t)$ forms a finite lattice. Let us check all the conditions:

1. 1.1

Partial order. First let us show that $\unlhd$ is a partial order.

1. 1.1.1

Reflexivity. It is immediate that ${[\rho]}\unlhd{[\rho]}$ holds since $\rho/\rho=\epsilon$ is garbage. 2. 1.1.2

Antisymmetry. Let ${[\rho]}\unlhd{[\sigma]}\unlhd{[\rho]}$. This means that $\rho/\sigma$ and $\sigma/\rho$ are garbage. Then:

[TABLE]

Since $\rho\equiv\sigma$ we conclude that ${[\rho]}={[\sigma]}$, as required. 3. 1.1.3

Transitivity. Let ${[\rho]}\unlhd{[\sigma]}\unlhd{[\tau]}$ and let us show that ${[\rho]}\unlhd{[\tau]}$. Note that $\rho/\sigma$ and $\sigma/\tau$ are garbage. By the fact that the projection of garbage is garbage (Prop. 9) the derivation $(\rho/\sigma)/(\sigma/\tau)$ is garbage. The composition of garbage is also garbage (Prop. 9), so $(\sigma/\tau)((\rho/\sigma)/(\sigma/\tau))$ is garbage. In general the following holds:

[TABLE]

So since any prefix of a garbage derivation is garbage (Prop. 9) we conclude that $\rho/\tau$ is garbage. This means that $[\rho]\unlhd[\tau]$, as required. 2. 1.2

Finite. Let us check that $\mathbb{F}(t^{\prime},t)$ is a finite lattice, i.e. that it has a finite number of elements. Recall that $\mathbb{F}(t^{\prime},t)$ is the set of equivalence classes ${[\rho]}$ where $\rho$ is $t^{\prime}$-garbage-free.

On one hand, recall that the $\lambda^{\texttt{{\#}}}$-calculus is finitely branching and strongly normalizing (Prop. 1). So by König’s lemma the set of $\mathrel{\to_{\texttt{{\#}}}}$-derivations starting from $t^{\prime}$ is bounded in length. More precisely, there is a constant $M$ such that for any $s^{\prime}\in\mathcal{T}^{\texttt{{\#}}}$ and any derivation $\rho:t^{\prime}\mathrel{\to_{\texttt{{\#}}}}^{*}s^{\prime}$ we have that the length $|\rho|$ is bounded by $M$.

On the other hand, let F=\{\rho\ |\ \rho\text{ is t^{\prime}-garbage-free and }\rho\Downarrow t^{\prime}=\rho\}. Consider the mapping $\varphi:\mathbb{F}(t^{\prime},t)\to F$ given by ${[\rho]}\mapsto\rho\Downarrow t^{\prime}$, and note that:

• •

$\varphi$ does not depend on the choice of representative, that is, if ${[\rho]}={[\sigma]}$ then $\varphi({[\rho]})=\rho\Downarrow t^{\prime}=\sigma\Downarrow t^{\prime}=\varphi({[\sigma]})$. This is a consequence of Lem. 41.

• •

$\varphi$ is a well-defined function, that is $\varphi({[\rho]})\in F$. This is because $\varphi({[\rho]})=\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free by Prop. 10. Moreover, we have that $\varphi({[\rho]})\Downarrow t^{\prime}=({[\rho]}\Downarrow t^{\prime})\Downarrow t^{\prime}={[\rho]}\Downarrow t^{\prime}=\varphi({[\rho]})$, which is also a consequence of Lem. 41, and the fact that ${[\rho]}\Downarrow t^{\prime}\equiv\rho$ (Prop. 10).

• •

$\varphi$ is injective. Indeed, suppose that $\varphi({[\rho]})=\varphi({[\sigma]})$, that is, $\rho\Downarrow t^{\prime}=\sigma\Downarrow t^{\prime}$. Then $\rho\equiv\rho\Downarrow t^{\prime}=\sigma\Downarrow t^{\prime}\equiv\sigma$ by Prop. 10 since $\rho$ and $\sigma$ are $t^{\prime}$-garbage-free. Hence ${[\rho]}={[\sigma]}$.

Since $\varphi:\mathbb{F}(t^{\prime},t)\to F$ is injective, it suffices to show that $F$ is finite to conclude that $\mathbb{F}(t^{\prime},t)$ is finite. Recall that the $\lambda$-calculus is finitely branching, so the number of derivations of a certain length is finite. To show that $F$ is finite, it suffices to show that the length of derivations in $F$ is bounded by some constant. Let $\rho$ be a derivation in $F$. We have that $\rho=\rho\Downarrow t^{\prime}$. By construction of the sieve, none of the steps of $\rho\Downarrow t^{\prime}$ are garbage. That is $\rho=\rho\Downarrow t^{\prime}=R_{1}\ldots R_{n}$ where for all $i$ we have that $R_{i}/(t^{\prime}/R_{1}\ldots R_{i-1})\neq\varnothing$. So we have that the length of $\rho/t^{\prime}$ is greater than the length of $\rho$ for all $\rho\in F$:

[TABLE]

As a consequence given any $\mathrel{\to_{\beta}}$-derivation $\rho\in F$ we have that $|\rho|\leq|\rho/t^{\prime}|\leq M$. This concludes the proof that $\mathbb{F}(t^{\prime},t)$ is finite. 3. 1.3

Bottom element. As the bottom element take $\bot_{(\mathbb{F}(t^{\prime},t))}:={[\epsilon]}$. Observe that this is well-defined since $\epsilon$ is $t^{\prime}$-garbage-free. Moreover, let us show that $\bot_{(\mathbb{F}(t^{\prime},t))}$ is the least element. Let $[\rho]$ be an arbitrary element of $\mathbb{F}(t^{\prime},t)$ and let us check that $\bot_{(\mathbb{F}(t^{\prime},t))}\unlhd[\rho]$. This is immediate since, by definition, $\bot_{(\mathbb{F}(t^{\prime},t))}\unlhd[\rho]$ if and only if $\epsilon/\rho$ is garbage. But $\epsilon/\rho=\epsilon$ is trivially garbage. 4. 1.4

Join. Let $[\rho],[\sigma]$ be arbitrary elements of $\mathbb{F}(t^{\prime},t)$, and let us check that $[\rho]\triangledown[\sigma]$ is the join. First observe that $[\rho]\triangledown[\sigma]$ is well-defined i.e. that $(\rho\sqcup\sigma)\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free, which is an immediate consequence of Prop. 14. Moreover, it is indeed the least upper bound of $\{[\rho],[\sigma]\}$:

1. 1.4.1

Upper bound. Let us show that $[\rho]\unlhd[\rho]\triangledown[\sigma]$; the proof for $[\sigma]$ is symmetrical. We must show that $\rho/((\rho\sqcup\sigma)\Downarrow t^{\prime})$ is garbage. Note that $\rho\sqsubseteq\rho\sqcup\sigma$, so in particular $\rho/((\rho\sqcup\sigma)\Downarrow t^{\prime})\sqsubseteq(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow t^{\prime})$. Given that any prefix of a garbage derivation is garbage (Prop. 9), it suffices to show that $(\rho\sqcup\sigma)/((\rho\sqcup\sigma)\Downarrow t^{\prime})$ is garbage. This is a straightforward consequence of the fact that projecting after a sieve is garbage (Lem. 40). 2. 1.4.2

Least upper bound. Let $[\rho],[\sigma]\unlhd[\tau]$, and let us show that $[\rho]\triangledown[\sigma]\unlhd[\tau]$. We know that $\rho/\tau$ and $\sigma/\tau$ are garbage, and we are to show that $((\rho\sqcup\sigma)\Downarrow t^{\prime})/\tau$ is garbage. Note that $(\rho\sqcup\sigma)\Downarrow t^{\prime}\sqsubseteq\rho\sqcup\sigma$ as a consequence of the fact that the sieve is a prefix (Lem. 35). So in particular $((\rho\sqcup\sigma)\Downarrow t^{\prime})/\tau\sqsubseteq(\rho\sqcup\sigma)/\tau$. Given that any prefix of a garbage derivation is garbage (Prop. 9), it suffices to show that $(\rho\sqcup\sigma)/\tau$ is garbage. But $(\rho\sqcup\sigma)/\tau\equiv\rho/\tau\sqcup\sigma/\tau$ so we conclude by the fact that the join of garbage is garbage (Prop. 9). 5. 1.5

Top element. Since $\mathbb{F}(t^{\prime},t)$ is finite, its elements are $\{{[\tau_{1}]},\ldots,{[\tau_{n}]}\}$. It suffices to take $\top:={[\tau_{1}]}\triangledown\ldots\triangledown{[\tau_{n}]}$ as the top element. 6. 1.6

Meet. Let ${[\rho]},{[\sigma]}\in\mathbb{F}(t^{\prime},t)$. Note that the set $L=\{{[\tau]}\in\mathbb{F}(t^{\prime},t)\ |\ {[\tau]}\unlhd{[\rho]}\text{ and }{[\tau]}\unlhd{[\sigma]}\}$ is finite because, as we have already proved, the set $\mathbb{F}(t^{\prime},t)$ is itself finite. Then $L=\{{[\tau_{1}]},\ldots,{[\tau_{n}]}\}$. Take ${[\rho]}\!\vartriangle\!{[\sigma]}:={[\tau_{1}]}\triangledown\ldots\triangledown{[\tau_{n}]}$. It is straightforward to show that ${[\rho]}\!\vartriangle\!{[\sigma]}$ thus defined is the greatest lower bound for $\{{[\rho]},{[\sigma]}\}$. 2. 2.

The set $\mathbb{G}(t^{\prime},t)$ forms an upper semilattice. The semilattice structure of $\mathbb{G}(t^{\prime},t)$ is inherited from $\mathbb{D}^{\lambda}(t)$. More precisely, ${[\rho]}\sqsubseteq{[\sigma]}$ is declared to hold if $\rho\sqsubseteq\sigma$, the bottom element is ${[\epsilon]}$, and the join is ${[\rho]}\sqcup{[\sigma]}={[\rho\sqcup\sigma]}$. Let us check that this is an upper semilattice:

1. 2.1

Partial order. The relation $(\sqsubseteq)$ is a partial order on $\mathbb{G}(t^{\prime},t)$ because it is already a partial order in $\mathbb{D}^{\lambda}(t)$. 2. 2.2

Bottom element. It suffices to note that the empty derivation $\epsilon:t\mathrel{\to_{\beta}}^{*}t$ is $t^{\prime}$-garbage, so ${[\epsilon]}\in\mathbb{G}(t^{\prime},t)$ is the least element. 3. 2.3

Join. By Prop. 9 we know that if $\rho$ and $\sigma$ are $t^{\prime}$-garbage then $\rho\sqcup\sigma$ is $t^{\prime}$-garbage, so ${[\rho]}\sqcup{[\sigma]}$ is indeed the least upper bound of $\{{[\rho]},{[\sigma]}\}$.

0.A.15 Proof of Thm. 5.1 – Factorization

We need a few auxiliary lemmas:

Lemma 43 (Garbage-free/garbage decomposition)

Let $\rho:t\mathrel{\twoheadrightarrow_{\beta}}s$ and $t^{\prime}\mathrel{\ltimes}t$. Then there exist $\rho_{1},\rho_{2}$ such that:

$\rho\equiv\rho_{1}\rho_{2}$ 2. 2.

$\rho_{1}$ is $t^{\prime}$-garbage-free, 3. 3.

$\rho_{2}$ is $t^{\prime}$-garbage.

Moreover, $\rho_{1}$ and $\rho_{2}$ are unique modulo permutation equivalence, and we have that $\rho_{1}\equiv\rho\Downarrow t^{\prime}$ and $\rho_{2}\equiv\rho/(\rho\Downarrow t^{\prime})$.

Proof

Let us prove that said decomposition exists and that it is unique:

• •

Existence. Take $\rho_{1}:=\rho\Downarrow t^{\prime}$ and $\rho_{2}:=\rho/(\rho\Downarrow t^{\prime})$. Then we may check the three conditions in the statement:

Recall that $\rho\Downarrow t^{\prime}\sqsubseteq\rho$ holds by Lem. 35, so:

[TABLE]

as required. 2. 2.

The derivation $\rho_{1}=\rho\Downarrow t^{\prime}$ is $t^{\prime}$-garbage-free. This is as an immediate consequence of Prop. 14, namely the result of sieving is always garbage-free. 3. 3.

The derivation $\rho_{2}=\rho/(\rho\Downarrow t^{\prime})$ is garbage. This is an immediate consequence of Lem. 40, namely projection after a sieve is always garbage.

• •

Uniqueness, modulo permutation equivalence. Let $\rho\equiv\sigma_{1},\sigma_{2}$ where $\sigma_{1}$ is $t^{\prime}$-garbage-free, and $\sigma_{2}$ is $t^{\prime}$-garbage. Then we argue that $\sigma_{1}\equiv\rho_{1}$ and $\sigma_{2}\equiv\rho_{2}$.

Since $\rho_{1}\rho_{2}\equiv\rho\equiv\sigma_{1}\sigma_{2}$ and sieving is compatible with permutation equivalence (Lem. 41) we have that $\rho_{1}\rho_{2}\Downarrow t^{\prime}\equiv\sigma_{1}\sigma_{2}\Downarrow t^{\prime}$. By Lem. 42, we know that trailing garbage does not affect sieving, hence $\rho_{1}\Downarrow t^{\prime}\equiv\sigma_{1}\Downarrow t^{\prime}$. Moreover, $\rho_{1}$ and $\sigma_{1}$ are garbage-free, which by Prop. 14 means that $\rho_{1}\equiv\sigma_{1}$. This means that $\rho_{1}$ is unique, modulo permutation equivalence. Finally, since $\rho_{1}\rho_{2}\equiv\sigma_{1}\sigma_{2}$ and $\rho_{1}\equiv\sigma_{1}$, we have that $\rho_{1}\rho_{2}/\rho_{1}\equiv\sigma_{1}\sigma_{2}/\sigma_{1}$, that is $\rho_{2}\equiv\sigma_{2}$. This means that $\rho_{2}$ is unique, modulo permutation equivalence.

Lemma 44

Let $t^{\prime}\mathrel{\ltimes}\mathsf{src}(\rho)=\mathsf{src}(\sigma)$. Then ${[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}={[\rho\Downarrow t^{\prime}]}\triangledown{[\sigma\Downarrow t^{\prime}]}$.

Proof

Let:

[TABLE]

Note that $\alpha$ and $\beta$ are garbage by Lem. 40 and hence $\gamma$ is also garbage, as a consequence of the facts that the join of garbage is garbage and that the projection of garbage is garbage (Prop. 9). Remark that, in general, $AB\sqcup CD\equiv(A\sqcup C)(B/(C/A)\sqcup D/(A/C))$. Then the statement of this lemma is a consequence of the following chain of equalities:

[TABLE]

To prove Thm. 5.1, let us check that $\int_{\mathcal{F}}{\mathcal{G}}$ is well-defined, that it is an upper semilattice, and finally that $\mathbb{D}^{\lambda}(t)\simeq\int_{\mathcal{F}}{\mathcal{G}}$ are isomorphic as upper semilattices.

The Grothendieck construction $\int_{\mathcal{F}}{\mathcal{G}}$ is well-defined. This amounts to checking that $\mathcal{G}$ is indeed a lax 2-functor:

1. 1.1

The mapping $\mathcal{G}$ is well-defined on objects. Note that $\mathcal{G}({[\rho]})=\mathbb{G}(t^{\prime}/\rho,\mathsf{tgt}(\rho))$, which is a poset. Moreover, the choice of the representative $\rho$ of the equivalence class ${[\rho]}$ does not matter, since if $\rho$ and $\sigma$ are permutation equivalent derivations, then $t^{\prime}/\rho=t^{\prime}/\sigma$ (by Prop. 8) and $\mathsf{tgt}(\rho)=\mathsf{tgt}(\sigma)$. 2. 1.2

The mapping $\mathcal{G}$ is well-defined on morphisms. Let us check that given ${[\rho]},{[\sigma]}\in\mathcal{F}$ such that ${[\rho]}\unlhd{[\sigma]}$ then $\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]}):\mathcal{G}({[\rho]})\to\mathcal{G}({[\sigma]})$ is a morphism of posets, i.e. a monotonic function.

First, we can see that it is well-defined, since if ${[\alpha]}\in\mathcal{G}([\rho])$ then the image $\mathcal{G}({[\rho]})({[\alpha]}\hookrightarrow{[\sigma]})={[\rho\alpha/\sigma]}$ is an element of $\mathcal{G}([\sigma])$, since $\rho\alpha/\sigma=(\rho/\sigma)(\alpha/(\sigma/\rho))$ is garbage, as it is the composition of garbage derivations (Prop. 9): the derivation $\rho/\sigma$ is garbage since ${[\rho]}\unlhd{[\sigma]}$ (by definition), and the derivation $\alpha/(\sigma/\rho)$ is garbage since $\alpha$ is garbage (Prop. 9). Moreover, the choice of representative does not matter, since if $\rho_{1}\equiv\rho_{2}$ and $\sigma_{1}\equiv\sigma_{2}$ and $\alpha_{1}\equiv\alpha_{2}$ then $\rho_{1}\alpha_{1}/\sigma_{1}\equiv\rho_{2}\alpha_{2}/\sigma_{2}$.

We are left to verify that $\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$ is monotonic. Let ${[\alpha]},{[\beta]}\in\mathcal{G}([\rho])$ such that ${[\alpha]}\sqsubseteq{[\beta]}$, and let us show that $\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})({[\alpha]})\sqsubseteq\mathcal{G}([\rho]\hookrightarrow[\sigma])({[\beta]})$. Indeed, $\alpha\sqsubseteq\beta$, so $\rho\alpha/\sigma=(\rho/\sigma)(\alpha/(\sigma/\rho))\sqsubseteq(\rho/\sigma)(\beta/(\sigma/\rho))=\rho\beta/\sigma$. 3. 1.3

Identity. Let ${[\rho]}\in\mathcal{F}$. Let us check that $\mathcal{G}({[\rho]}\hookrightarrow{[\rho]})=\mathsf{id}_{\mathcal{G}({[\rho]})}$ is the identity morphism. Indeed, if ${[\alpha]}\in\mathcal{G}({[\rho]})$, then $\mathcal{G}({[\rho]}\hookrightarrow{[\rho]})({[\alpha]})={[\rho\alpha/\rho]}={[\alpha]}$. 4. 1.4

Composition. Let ${[\rho]},{[\sigma]},{[\tau]}\in\mathcal{F}$ such that ${[\rho]}\unlhd{[\sigma]}\unlhd{[\tau]}$. Let us check that there is a 2-cell $\mathcal{G}(({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}))\sqsubseteq\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})\circ\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$. Note that $({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}):{[\rho]}\unlhd{[\tau]}$ is a morphism in the upper semilattice $\mathcal{F}$ seen as a category. Moreover, since it is a semilattice, there a unique morphism ${[\rho]}\unlhd{[\tau]}$, namely ${[\rho]}\hookrightarrow{[\tau]}$, so we have that $({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]})={[\rho]}\hookrightarrow{[\tau]}$. Now if ${[\alpha]}\in\mathcal{G}{{[\rho]}}$, then:

[TABLE]

so $\mathcal{G}(({[\sigma]}\hookrightarrow{[\tau]})\circ({[\rho]}\hookrightarrow{[\sigma]}))\sqsubseteq\mathcal{G}({[\sigma]}\hookrightarrow{[\tau]})\circ\mathcal{G}({[\rho]}\hookrightarrow{[\sigma]})$ as required. 2. 2.

The Grothendieck construction $\int_{\mathcal{F}}{\mathcal{G}}$ is an upper semilattice.

1. 2.1

Partial order. Recall that $\int_{\mathcal{F}}{\mathcal{G}}$ is always poset with the order given by $(a,b)\leq(a^{\prime},b^{\prime})$ if and only if $a\unlhd a^{\prime}$ and $\mathcal{G}(a\hookrightarrow a^{\prime})(b)\sqsubseteq b^{\prime}$. 2. 2.2

Bottom element. We argue that $(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$ is the bottom element. Let $({[\rho]},{[\sigma]})\in\int_{\mathcal{F}}{\mathcal{G}}$. Then clearly $\bot_{\mathcal{F}}\unlhd{[\rho]}$. Moreover, $\mathcal{G}([\bot_{\mathcal{F}}]\hookrightarrow[\rho])(\bot_{\mathcal{G}})=[\epsilon/\rho]=[\epsilon]\sqsubseteq{[\sigma]}$. 3. 2.3

Join. Let us show that $(a,b)\lor(a^{\prime},b^{\prime})=(a\triangledown a^{\prime},\mathcal{G}(a\hookrightarrow(a\triangledown a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown a^{\prime}))(b^{\prime}))$. is the least upper bound of $\{(a,b),(a^{\prime},b^{\prime})\}$.

1. 2.3.1

Upper bound. Let us show that $(a,b)\leq(a,b)\lor(a^{\prime},b^{\prime})$. Recall that $(a,b)\lor(a^{\prime},b^{\prime})=(a\triangledown a,\mathcal{G}(a\hookrightarrow(a\lor a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown a^{\prime}))(b^{\prime}))$. First, we have $a\unlhd a\triangledown a^{\prime}$. Moreover, $\mathcal{G}(a\hookrightarrow(a\triangledown a^{\prime}))(b)\sqsubseteq\mathcal{G}(a\hookrightarrow(a\lor a^{\prime}))(b)\sqcup\mathcal{G}(a^{\prime}\hookrightarrow(a\triangledown a^{\prime}))(b^{\prime})$, as required. 2. 2.3.2

Least upper bound. Let $(a,b)=({[\rho]},{[\sigma]})$ and $(a^{\prime},b^{\prime})=({[\rho^{\prime}]},{[\sigma^{\prime}]})$. Moreover, let $({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$ be an upper bound, i.e. an element such that $({[\rho]},{[\sigma]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$ and $({[\rho^{\prime}]},{[\sigma^{\prime}]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$. Let us show that $({[\rho]},{[\sigma]})\lor({[\rho^{\prime}]},{[\sigma^{\prime}]})\leq({[\rho^{\prime\prime}]},{[\sigma^{\prime\prime}]})$. First note that ${[\rho]}\unlhd{[\rho^{\prime\prime}]}$ and ${[\rho^{\prime}]}\unlhd{[\rho^{\prime\prime}]}$ so ${[\rho]}\triangledown{[\rho^{\prime}]}\unlhd{[\rho^{\prime\prime}]}$.

Moreover, we know that:

[TABLE]

Let $\alpha:=(\rho\sqcup\rho^{\prime})\Downarrow t^{\prime}$. First we claim that $\alpha\sqsubseteq\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}$. Indeed, $\alpha=(\rho\sqcup\rho^{\prime})\Downarrow t^{\prime}\sqsubseteq\rho\sqcup\rho^{\prime}$ by Lem. 35, and it is easy to check that $\rho\sqcup\rho^{\prime}\sqsubseteq\rho\sigma\sqcup\rho^{\prime}\sigma^{\prime}$. What we have to check is the following inequality:

[TABLE]

Indeed:

[TABLE] 3. 3.

There is an isomorphism $\mathbb{D}^{\lambda}(t)\simeq\int_{\mathcal{F}}{\mathcal{G}}$ of upper semilattices. As stated, the isomorphism is given by:

[TABLE]

Note that $\varphi$ and $\psi$ are well-defined mappings, since their value does not depend on the choice of representative, due, in particular, to the fact that sieving is compatible with permutation equivalence (Lem. 41). Let us check that $\varphi$ and $\psi$ are morphisms of upper semilatices, and that they are mutual inverses:

1. 3.1

$\varphi$** is a morphism of upper semilattices.** Let us check the three conditions:

1. 3.1.1

Monotonic. Let ${[\rho]}\sqsubseteq{[\sigma]}$ in $\mathbb{D}^{\lambda}(t)$, and let us show that the following inequality holds:

[TABLE]

We check the two conditions (by definition of $\int_{\mathcal{F}}{\mathcal{G}}$):

1. 3.1.1.1

On the first hand, ${[\rho\Downarrow t^{\prime}]}\unlhd{[\sigma\Downarrow t^{\prime}]}$ since

[TABLE]

Note that this is garbage by Lem. 40. So by Prop. 9, $(\rho\Downarrow t^{\prime})/(\sigma\Downarrow t^{\prime})$ is also garbage, as required. 2. 3.1.1.2

On the other hand, let us show that $\mathcal{G}({[\rho\Downarrow t^{\prime}]}\hookrightarrow{[\sigma\Downarrow t^{\prime}]})({[\rho/(\rho\Downarrow t^{\prime})]})\sqsubseteq\sigma/(\sigma\Downarrow t^{\prime})$. In fact:

[TABLE] 2. 3.1.2

Preserves bottom. By definition: $\varphi(\bot_{\mathbb{D}^{\lambda}(t)})=({[\epsilon\Downarrow t^{\prime}]},{[\epsilon/(\epsilon\Downarrow t^{\prime})]})=({[\epsilon]},{[\epsilon]})=(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$. 3. 3.1.3

Preserves joins. Let ${[\rho]},{[\sigma]}\in\mathbb{D}^{\lambda}(t)$, and let us show that $\varphi({[\rho]}\sqcup{[\sigma]})=\varphi({[\sigma]})\lor\varphi({[\sigma]})$. Indeed, note that:

[TABLE]

where

[TABLE]

and

[TABLE]

where

[TABLE]

It suffices to show that $\alpha=\alpha^{\prime}$ and $\beta=\beta^{\prime}$. Let us show each separately:

1. 3.1.3.1

Proof of $\alpha=\alpha^{\prime}$. The equality $\alpha={[(\rho\sqcup\sigma)\Downarrow t^{\prime}]}={[\rho\Downarrow t^{\prime}]}\triangledown{[\sigma\Downarrow t^{\prime}]}=\alpha^{\prime}$ is an immediate consequence of Lem. 44. 2. 3.1.3.2

Proof of $\beta=\beta^{\prime}$. Note that:

[TABLE]

as required. 2. 3.2

$\psi$** is a morphism of upper semilattices.** Let us check the three conditions:

1. 3.2.1

Monotonic. Let $({[\rho_{1}]},{[\sigma_{1}]})\leq({[\rho_{2}]},{[\sigma_{2}]})$ in $\int_{\mathcal{F}}{\mathcal{G}}$ and let us show that $\psi({[\rho_{1}]},{[\sigma_{1}]})\sqsubseteq\psi({[\rho_{2}]},{[\sigma_{2}]})$ in $\mathbb{D}^{\lambda}(t)$. Indeed, we know that $\mathcal{G}({[\rho_{1}]}\hookrightarrow{[\rho_{2}]})({[\sigma_{1}]})\sqsubseteq{[\sigma_{2}]}$, that is to say $\rho_{1}\sigma_{1}/\rho_{2}\sqsubseteq\sigma_{2}$. Then:

[TABLE]

which means that $\rho_{1}\sigma_{1}\sqsubseteq\rho_{2}\sigma_{2}$. This immediately implies that $\psi({[\rho_{1}]},{[\sigma_{1}]})\sqsubseteq\psi({[\rho_{2}]},{[\sigma_{2}]})$. 2. 3.2.2

Preserves bottom. Recall that the bottom element $\bot_{(\int_{\mathcal{F}}{\mathcal{G}})}$ is defined as $(\bot_{\mathcal{F}},\bot_{\mathcal{G}(\bot_{\mathcal{F}})})$, that is $({[\epsilon]},{[\epsilon]})$. Therefore $\psi(\bot_{(\int_{\mathcal{F}}{\mathcal{G}})})={[\epsilon]}=\bot_{\mathbb{D}^{\lambda}(t)}$. 3. 3.2.3

Preserves joins. Let $({[\rho_{1}]},{[\sigma_{1}]})$ and $({[\rho_{2}]},{[\sigma_{2}]})$ be elements of $\int_{\mathcal{F}}{\mathcal{G}}$, and let us show that $\psi(({[\rho_{1}]},{[\sigma_{1}]})\lor({[\rho_{2}]},{[\sigma_{2}]}))=\psi({[\rho_{1}]},{[\sigma_{1}]})\sqcup\psi({[\rho_{2}]},{[\sigma_{2}]}))$.

Let:

[TABLE]

First we claim that $\alpha\sqsubseteq\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}$. This is because by Lem. 35 we know that $\alpha=(\rho_{1}\sqcup\rho_{2})\Downarrow t^{\prime}\sqsubseteq\rho_{1}\sqcup\rho_{2}$. Moreover, it is easy to check that $\rho_{1}\sqcup\rho_{2}\sqsubseteq\rho_{1}\sigma_{1}\sqcup\rho_{2}\sigma_{2}$. Using this fact we have:

[TABLE]

as required. 3. 3.3

Left inverse: $\psi\circ\varphi=\mathsf{id}$. Let ${[\rho]}\in\mathbb{D}^{\lambda}(t)$. Then by Lem. 43:

[TABLE] 4. 3.4

Right inverse: $\varphi\circ\psi=\mathsf{id}$. Let $({[\rho]},{[\sigma]})\in\int_{\mathcal{F}}{\mathcal{G}}$. Note that $\rho$ is $t^{\prime}$-garbage-free and $\sigma$ is $t^{\prime}$-garbage, so by Lem. 42 and Prop. 14 we know that $\rho\sigma\Downarrow t^{\prime}=\rho\Downarrow t^{\prime}\equiv\rho$. Hence:

[TABLE]