Characterisation of Approximation and (Head) Normalisation for $\lambda\mu$ using Strict Intersection Types

TL;DR

This paper investigates the strict type assignment for lambda-mu calculus, introducing approximants to characterize head normalisation, normalisation, and strong normalisation through assignable types.

Contribution

It defines approximants for lambda-mu-terms and establishes a semantics, providing new characterizations of normalisation properties via strict intersection types.

Findings

Approximants generate a semantics for lambda-mu-terms.

Typeability of an approximant matches the term's type.

Characterizations for head normal form, normal form, and strong normalisation.

Abstract

We study the strict type assignment for lambda-mu that is presented in [van Bakel'16]. We define a notion of approximants of lambda-mu-terms, show that it generates a semantics, and that for each typeable term there is an approximant that has the same type. We show that this leads to a characterisation via assignable types for all terms that have a head normal form, and to one for all terms that have a normal form, as well as to one for all terms that are strongly normalisable.

Full text

Introduction

The Intersection Type Discipline [14] is an extension of the standard, implicative type assignment known as Curry’s system [17] for the $\lambda$-calculus [16, 13]; the extension made consists of relaxing the requirement that a parameter for a function should have a single type, adding the type constructor \mathop{{\colourfortype\mbox{{\cap}}}} next to $\mathbin{\rightarrow}$. This simple extension allows for a great leap in complexity: not only can a (filter) model be built for the $\semcolour\lambda$-calculus using intersection types, also strong normalisation (termination) can be characterised via assignable types; however, type assignment becomes undecidable.

A natural question is whether or intersection type assignment yields a semantics also for other calculi, like ${\semcolour\lambda\mu}$ [20]. To answer that, in [9, 10, 11] a notion of intersection type assignment was defined for ${\semcolour\lambda\mu}$ that is a variant of the union-intersection system defined in [6]. Inspired by Streicher and Reus’s domain [24], ${\semcolour\lambda\mu}$-terms are separated into terms and streams; then ${\semcolour\lambda\mu}$’s names act as the destination of streams, the same way variables are the destination of terms. A type theory is defined following the domain construction; the main results for that system are the definition of a filter model, closure under conversion, and that the system is an extension of Parigot’s [9]; and that, in a restricted system, the terms that are typeable are exactly the strongly normalising ones [10].

One of the main disadvantages of taking the domain-directed approach to type assignment is that, naturally, intersection becomes a ‘top level’ type constructor, that lives at the same level as arrow, for example, which induces a contra-variant type inclusion relation ‘$\mathbin{{\colourfortype\leq}}$’ and type assignment rule $(\mathbin{{\colourfortype\leq}})$ that greatly hinder proofs and gives an intricate generation lemma. This problem is addressed in [8] where a strict version of the system of [11] is defined, in the spirit of that of [2, 7] that allows for more easily constructed proofs. The main restriction with respect to the system of [11] is limiting the type inclusion relation to a relation that is no longer contra-variant, and allows only for the selection of a component of an intersection type; this is accompanied by a restriction of the type language, essentially no longer allowing intersection on the right of an arrow. The main results shown in [8] are that the system is closed under conversion (i.e. under reduction and expansion), and that all terms typeable in a system that excludes the type constant $\omega$ are strongly normalisable. To that aim it shows that, in this system, cut-elimination is strongly normalisable, using the technique of derivation reduction [4] (see also [5, 7]).

In this paper, we will elaborate further on the strict system. As in [5, 7], in this paper we will show that the fact that derivation reduction is strongly normalisable also here leads to an approximation result. For that, we define a notion of approximation for ${\semcolour\lambda\mu}$, and show that this yields a semantics (Thm. 3.7). We then show that for every typeable term there exists an approximant of that term that can be assigned exactly the same types (Thm. 4.6). We then show that this approximation result naturally gives a characterisation of head normalisation (Thm 4.7), as well as a characterisation of normalisation (Thm 5.8). We also revisit the proof of characterisation of strong normalisation of terms through the assignable types (Thm 5.14), which thanks to the approximation result has a more elegant proof.

Because of the restricted available space, most of the (full) proofs are not presented here. A version of this paper with the proofs added in an appendix can be found at www.doc.ic.ac.uk/~svb/Research/Papers/ITRS16wapp.pdf.

Note: We will write $\underline{n}$ for the set $\{1,\ldots,n\}$ and use a vector notation for the abbreviation of sequences, so write \leavevmode\raise 6.83331pt\hbox{\psset{unit=1.0pt,linewidth=0.3pt}\begin{pspicture}(0.0pt,0.0pt)(0.0pt,2.09999pt){\psline{cc-cc}(2.5pt,1.5pt)(8.51942pt,1.5pt)}\hskip 8.51942pt\hbox{}\put(-0.25,1.5){{\pscurve{cc-cc}(0.0pt,0.0pt)(-0.59999pt,0.4pt)(-1.09999pt,1.0pt)(-1.5pt,1.7pt)}}\end{pspicture}\kern 1.65001pt}\kern-9.06943pt\kern-0.55pt\hbox{X}_{\underline{n}} for $X_{1},\ldots,X_{n}$, and $X$ if the number of elements in the sequence is not important.

1 The $\lambda\mu$-calculus

In this section we present Parigot’s pure $\lambda\mu$-calculus as introduced in [20]. It is an extension of the untyped $\lambda$-calculus obtained by adding names and a name-abstraction operator $\mu$ and was intended as a proof calculus for a fragment of classical logic. Derivable statements have the shape ${\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype A}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, where $A$ is the main (active) conclusion of the statement, and $\Delta$ contains the alternative conclusions, consisting of pairs of names and types; the left-hand context $\Gamma$, as usual, is a mapping from term variables to types, and represents the assumptions about free variables of $M$.

Definition 1.1** (Term Syntax [20]).**

Let $x,y,z,\ldots$ range over term variables, and $\alpha,\beta,\gamma,\delta,\ldots$ range over names. The terms, ranged over by $M,N,P,Q,\ldots$ are defined by the grammar:

• \begin{array}[]{rcl}M,N&::=&x\mid\lambda y.M\mid MN\mid\mu\alpha.[\beta]M\end{array}**

As usual, we consider $\lambda$ and $\mu$ to be binders; the sets $\mbox{\it\Itcol fv\hskip 1.1pt}\hskip 0.275pt({\ltermcol M})$ and $\textit{\semcolour fn}({\ltermcol M})$ of, respectively, free variables and free names in a term $M$ are defined in the usual way. We adopt Barendregt’s convention on terms, and will assume that free and bound variables and names are different.

Definition 1.2** (Substitution [20]).**

Substitution takes two forms:

• \begin{array}[]{l@{\hspace{2mm}}cll}\textit{term substitution:}\hfil\hskip 5.69054pt&M[N/x]&\textrm{(N$is substituted for$x$in$M)}\\ \textit{structural substitution:}\hfil\hskip 5.69054pt&M[L{\cdot}\gamma/\alpha]&\textrm{(every `subterm' [\alpha]N$of$M$is replaced by$[\gamma]NL)}\end{array}**

As usual, both substitutions are capture avoiding, using $\alpha$-conversion when necessary.

Definition 1.3** (Reduction [20]).**

Reduction in ${\semcolour\lambda\mu}$ is based on the following rules:

• \begin{array}[]{r@{\dquad\dquad}rll@{\dquad}l}(\beta):\quad\quad\quad\quad&(\lambda x.M)N&\mathrel{\rightarrow}&M[N/x]\hfil\quad\quad&(\textit{logical reduction})\\ (\mu):\quad\quad\quad\quad&\lx@intercol\kern-23.47351pt\left\{\begin{array}[]{@{}rcll}(\mu\beta.[\beta]P)Q&\mathrel{\rightarrow}&\mu\gamma.[\gamma](\,P[Q{\cdot}\gamma/\beta]\,)Q\\ (\mu\beta.[\delta]P)Q&\mathrel{\rightarrow}&\mu\gamma.[\delta]P[Q{\cdot}\gamma/\beta],&\textrm{if }\delta\not=\beta\\ \end{array}\right.\hfil\lx@intercol&(\textit{structural reduction})\\ (\textsc{Ren}):\quad\quad\quad\quad&\lx@intercol\kern-39.12253pt\left\{\begin{array}[]{@{}rcl@{\dquad}l}\mu\alpha.[\beta]\mu\gamma.[\gamma]M&\mathrel{\rightarrow}&\mu\alpha.[\beta]M[\beta/\gamma]\hfil\quad\quad\\ \mu\alpha.[\beta]\mu\gamma.[\delta]M&\mathrel{\rightarrow}&\mu\alpha.[\delta]M[\beta/\gamma],\hfil\quad\quad&\hskip 17.78296pt\textrm{if }\delta\not=\gamma\end{array}\right.\hfil\lx@intercol&(\textit{renaming})\end{array}111A more common notation for the second rule, for example, would be $(\mu\beta.[\delta]M)N\mathrel{\rightarrow}\mu\beta.[\delta]M[N/\beta]$. This implicitly uses the fact that $\beta$ disappears during reduction, and through $\alpha$-conversion can be picked as name for the newly created applications instead of $\gamma$. But, in fact, this is not the same $\beta$ (and the named term has changed), as reflected in the fact that its type changes during reduction. Moreover, when making the substitution explicit as in **[12*]**, it becomes clear that this other approach in fact is a short-cut, which our definition does without. ***

We write M\mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}N for the reduction relation that is the compatible closure of these rules, and $\mathbin{\semcolour=_{\beta\mu}}$ for the equivalence relation generated by it.

Confluence for this notion of reduction has been shown in [21].

We will need the concept of head-normal form for ${\semcolour\lambda\mu}$, which is defined as follows:

Definition 1.4** (Head-normal forms).**

The ${\semcolour\lambda\mu}$ head-normal forms (with respect to our notion of reduction \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}) are defined through the grammar:

• \begin{array}[]{rrl@{\quad}l}\mbox{\itbf H}&::=&xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}&(n\geq 0)\\ &\mid&\lambda x.\mbox{\itbf H}\\ &\mid&\ltermcol\mu\alpha.[\beta]\hskip 0.43999pt\mbox{\itbf H}&(\mbox{\itbf H}\not=\ltermcol\mu\gamma.[\delta]\hskip 0.43999pt\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}})\end{array}**

2 Strict type assignment

Intersection (and union) type assignment for ${\semcolour\lambda\mu}$ was first defined in [6]; this was followed by [9], in which an intersection type theory is developed departing from Streicher and Reus’s domain construction [24]. Terms can be typed with functional types $\delta$ and streams by continuation types $\kappa$ that are of the shape \delta_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\delta_{n}\mathord{\mbox{\typecol\typefont\times}}\omega, so essentially is a sequence of $\delta$s. This later [10] was followed by the proof that, as for the $\lambda$-calculus, the underlying intersection type system for ${\semcolour\lambda\mu}$ allows for the full characterisation of strongly normalisable terms; in that paper, renaming is not considered. These papers were later combined (and revised) into [11]. One of the main disadvantages of taking the domain-directed approach to type assignment is that, naturally, intersection becomes a ‘top level’ type constructor, that lives at the same level as arrow, for example. This in itself is not negative, since it gives readable types and easy-to-understand type assignment rules, but it also induces a contra-variant type inclusion relation ‘$\mathbin{{\colourfortype\leq}}$’ and type assignment rule $(\mathbin{{\colourfortype\leq}})$ that hinder proofs and give an intricate generation lemma (see [11] for details).

Therefore, in [8], a strict restriction of the system of [11] was presented, where the occurrence of intersections is limited to only appear as components of continuation types (so no intersections of continuation types), and type inclusion is no longer contra-variant and only allows for the selection of a component in an intersection type. It also uses $\Omega$ rather than $\omega$ to mark the end of a continuation type. But, more importantly, it removed the inference rule $(\mathbin{{\colourfortype\leq}})$, and changed the type assignment rules to explicitly state when a $\mathbin{{\colourfortype\leq}}$-step is allowed, as in rule $({\bluecol\textsl{Ax}})$.

This system is defined as follows:

Definition 2.1** (Strict Types [8]).**

Let $\upsilon$ range over a countable, infinite set of type constants. We define our strict types by the grammar:

• \begin{array}[]{rcl@{\quad}l@{\quad}l}\mbox{\kern 0.275pt\typefont A\kern 0.825pt},\mbox{\kern 0.275pt\typefont B\kern 0.825pt}&::=&\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon&&\textit{basic types}\\ \mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt},\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt},\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}&::=&\omega\mid\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}&(n\geq 1)&\textit{intersection types}\\ \mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\contfont{\typecol D}}&::=&\Omega\mid\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}&&\textit{continuation types}\end{array}**

On strict types, the type inclusion relation $\mathbin{\leq_{\hbox{{\sc s}}}}$ is the smallest partial order satisfying the rules:

• \begin{array}[]{c@{\colw}c@{\colw}c@{\colw}c@{\colw}c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 42.63261pt\hbox{\displaystyle\penalty 1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=85.76523pt\hbox{\kern 3.00003pt({\bluecol j\mathbin{\in}\underline{n},~{}n\geq 1})}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{1}\mathop{{\colourfortype\mbox{{$\cap$}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{$\cap$}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{n}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{j}}}}}\hfil\hskip 17.07164pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.37509pt\hbox{\displaystyle\penalty 1\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{i}\quad(\forall i\mathbin{\in}\underline{n})}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=88.69414pt\hbox{\kern 3.00003pt({\bluecol n\geq 1})}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{1}\mathop{{\colourfortype\mbox{{$\cap$}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{$\cap$}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{n}}}}}\hfil\hskip 17.07164pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 17.81367pt\hbox{\displaystyle\penalty 1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=36.12735pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\omega}}}}\hfil\hskip 17.07164pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 15.39584pt\hbox{\displaystyle\penalty 1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=31.29169pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{{\colourfortype\leq}}\Omega}}}}\hfil\hskip 17.07164pt&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 1.6042pt\hbox{\displaystyle\penalty 1\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\quad\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\contfont{\typecol D}}}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=97.54185pt\hbox{}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont$\times$}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathord{\mbox{\typecol\typefont$\times$}}\mbox{\contfont{\typecol D}}}}}}\end{array}**

For convenience, we will write \mbox{{\cap}}_{I}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i} for \mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i_{1}}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i_{n}} where $I=\{\,i_{1},\ldots,i_{n}\,\}$, \mbox{{\cap}}_{\raise-0.35pt\hbox to6.60004pt{\psset{unit=1.21pt,linewidth=0.38501pt} {\psset{linewidth=0.2475pt}\pscircle(3.78127pt,3.63002pt){3.02501pt}}{\psline{cc-cc}(2.11751pt,-0.9075pt)(5.14252pt,8.16754pt)}}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i} for $\omega$, so the second and third rule combine to

• {tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 4.37509pt\hbox{\displaystyle\penalty 1\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{i}\quad(\forall i\mathbin{\in}\underline{n})}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=88.69414pt\hbox{\kern 3.00003pt({\bluecol n\geq 0})}}}\hbox{\kern 0.0pt\hbox{\displaystyle\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{1}\mathop{{\colourfortype\mbox{{$\cap$}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{$\cap$}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}}}}}

and \mbox{{\cap}}_{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i} for \mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\ldots\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}. Notice that for any continuation type C there are $n\geq 0$ and $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{i}~{}(i\mathbin{\in}\underline{n})$ such that \mbox{\kern 0.275pt\contfont C\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\Omega.

Definition 2.2** (Strict Type Assignment [8]).**

A variable context $\Gamma$ is a mapping from term variables to intersection types, denoted as a finite set of statements $x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}$, such that the subject of the statements ($x$) are distinct. 2. 2.

We write $\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}$ for the context defined by:

• \begin{array}[]{rcll}\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\Gamma\mathrel{\cup}\{x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\},&\textrm{if \Gamma$is not defined on$x}\\ &\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\Gamma,&\textrm{if }x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma\end{array}**

We write $x\mathbin{\not\in}\Gamma$ if there exists no \typecolS such that $x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma$. 3. 3.

Name contexts* $\Delta$ and the notions $\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta$ and $\alpha\mathbin{\not\in}\Delta$ are defined in a similar way.* 4. 4.

We define strict type assignment for $\lambda\mu$-terms through the following natural deduction system:

• \begin{array}[t]{@{}rl@{~\quad}rl}({\bluecol\textsl{Ax}}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 56.25829pt\hbox{\displaystyle\penalty 1}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=113.01657pt\hbox{\kern 3.00003pt({\bluecol\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}})}}}\hbox{\kern 0.0pt\hbox{\displaystyle{\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathrel{{\blackcol{\vdash}}}{\ltermcol x}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\hfil~{}&(\mathop{{\colourfortype\mbox{{\cap}}}}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\quad(\raise-0.25pt\hbox{$\forall$}\hskip 1.1pti\mathbin{\in}I)}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=132.58835pt\hbox{\kern 3.00003pt({\bluecol I=\raise-0.35pt\hbox to6.60004pt{\psset{unit=1.21pt,linewidth=0.38501pt} {\psset{linewidth=0.2475pt}\pscircle(3.78127pt,3.63002pt){3.02501pt}}{\psline{cc-cc}(2.11751pt,-0.9075pt)(5.14252pt,8.16754pt)}}\mathrel{\vee}|I|\geq 2})}}}\hbox{\kern 11.21234pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{{$\cap$}}{I}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\\[14.22636pt] (\textit{Abs}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern 8.08339pt\hbox{\displaystyle\penalty 1{\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=152.3848pt\hbox{\kern 3.00003pt({\bluecol x\mathbin{\not\in}\Gamma})}}}\hbox{\kern 0.0pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol\lambda x.M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont$\times$}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\hfil~{}&(\mu):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=137.3165pt\hbox{\kern 3.00003pt({\bluecol\alpha\mathbin{\not\in}\Delta,\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}})}}}\hbox{\kern 0.21931pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol\mu\alpha.[\alpha]M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\\[14.22636pt] (\textit{App}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont$\times$}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\quad{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=241.21399pt\hbox{}}}\hbox{\kern 62.01534pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol MN}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\hfil~{}&(\mu^{\prime}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=158.95717pt\hbox{\kern 3.00003pt\mbox{\kern 0.55pt\parbox[r]{45.5244pt}{\begin{array}[]{l}\kern-4.95003pt(\bluecol\beta\not=\alpha\mathrel{\&}\alpha\mathbin{\not\in}\Delta,\\ \mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}})\end{array}}}}}}\hbox{\kern 0.58969pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol\mu\alpha.[\beta]M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont$\mathbin{\rightarrow}$}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt}}}}\end{array}**

We write ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ for judgements derivable using these rules, and prefix this with ‘${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{}$’ if we want to name the derivation. 5. 5.

The relation $\mathbin{\leq_{\hbox{{\sc s}}}}$ is naturally extended to variable contexts as follows:

• \begin{array}[]{rcl}\Gamma\mathbin{\leq_{\hbox{{\sc s}}}}\Gamma^{\prime}&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\raise-0.25pt\hbox{\forall}\hskip 1.1ptx{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma^{\prime}~{}\raise-0.25pt\hbox{\exists}\hskip 1.1ptx{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\in}\Gamma~{}[\hskip 1.1pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\hskip 1.1pt];\end{array}**

$\Delta\mathbin{\leq_{\hbox{{\sc s}}}}\Delta^{\prime}$* is defined similarly.*

Definition 2.3**.**

By abuse of notation, we allow the notation \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}, where \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{{\cap}}_{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i} and \mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}=\mbox{{\cap}}_{\underline{m}}\hskip 0.275pt\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{j}, which stands for \mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{m}. Given two contexts $\Gamma_{1}$ and $\Gamma_{2}$, we define the context \Gamma_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\Gamma_{2} as follows:

• \begin{array}[]{rcr@{~}l}\Gamma_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\Gamma_{2}&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\{\,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}\mid x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathbin{\in}\Gamma_{1}\mathrel{\&}x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}\mathbin{\in}\Gamma_{2}\,\}~{}&\mathrel{\cup}\\ &&\{\,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mid x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma_{1}\mathrel{\&}x\mathbin{\not\in}\Gamma_{2}\,\}~{}&\mathrel{\cup}\{\,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mid x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma_{2}\mathrel{\&}x\mathbin{\not\in}\Gamma_{1}\,\}\end{array}**

and write ${\cap_{\underline{n}}\hskip 0.43999pt}{\Gamma_{i}}$ for \Gamma_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\Gamma_{n}. We will also allow intersection of continuation types as short-hand notation: let \mbox{\contfont{\typecol D}}=\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n} \mathord{\mbox{\typecol\typefont\times}}\Omega, and \mbox{\kern 0.275pt\contfont C\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{m}\mathord{\mbox{\typecol\typefont\times}}\Omega and assume, that $n<m$; we define

• \begin{array}[]{rcl}\mbox{\contfont{\typecol D}}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{n+1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{m}\mathord{\mbox{\typecol\typefont\times}}\Omega.\end{array}**

(we need this notion in the proof of Thm. 4.7). Then \Delta_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\Delta_{2} is defined the same way as \Gamma_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\Gamma_{2}.

In [8] it is then shown that this notion of type assignment is closed under conversion, so can be used to define a (filter) semantics. That paper also defines a notion of cut-elimination, by defining derivation reduction \mathrel{\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\mbox{\scriptsize\sc Der}}}, where only those redexes in terms are contracted that are typed with a type different from $\omega$; it shows that this notion is strongly normalisable, which then leads to the proof that all terms typeable in a restriction of $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ that eliminates the type constant $\omega$, are strongly normalisable.

The main results shown in [8] that are relevant to this paper are:

Theorem 2.4** ([8]).**

*If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, $\Gamma^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\Gamma$, $\Delta^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\Delta$,222 The condition $\Delta^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\Delta$ might seem counterintuitive, since one might expect the inclusion relation to be reversed. To support intuition, we can see types in name contexts as negations, and \alpha{:}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\Omega as $\alpha{:}\neg\mbox{\kern 0.275pt\typefont A\kern 0.825pt}$. Notice that \mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\Omega\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\Omega; obviously we have \alpha{:}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\Omega\mathbin{\leq_{\hbox{{\sc s}}}}\alpha{:}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\Omega and \neg\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathbin{{\colourfortype\leq}}\neg\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\mathord{\hskip 0.55pt{\colourfortype\mbox{{\cup}}}\hskip 0.55pt}\neg\mbox{\kern 0.275pt\typefont B\kern 0.825pt}. * and $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}$, then ${\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt$. 2. 2.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ and $M\mathbin{\semcolour=_{\beta\mu}}N$, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 3. 3.

Let ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and {\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{\mbox{\typecol\typefont\mathbin{\rightarrow}}^{*}_{\mbox{\scriptsize\sc Der}}}{\orangecol\hskip 1.1pt\mathcal{D}}^{\prime}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, then M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N.* 4. 4.

If ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then $\textsl{SN}\hskip 0.43999pt({\orangecol\hskip 1.1pt\mathcal{D}})$ (${\orangecol\hskip 1.1pt\mathcal{D}}$* is strongly normalisable).*

3 Approximation semantics for ${\semcolour\lambda\mu}$

Following the approach of [25], we now define an approximation semantics for ${\semcolour\lambda\mu}$ with respect to \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}.

Essentially, approximants are partially evaluated expressions in which the locations of incomplete evaluation (i.e. where reduction may still take place) are explicitly marked by the element {\ltermcol\mbox{{\perp}}}; thus, they approximate the result of computations.

Approximation for $\semcolour{\Lambda\mu}$ (a variant of ${\semcolour\lambda\mu}$ where naming and $\mu$-binding are separated [18]) has been studied by others as well [23, 19]; weak approximants for ${\semcolour\lambda\mu}$ are studied in [12].

Definition 3.1** (Approximation for ${\semcolour\lambda\mu}$).**

We define {\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}} as an extension of ${\semcolour\lambda\mu}$ by adding the term constant {\ltermcol\mbox{{\perp}}}. 2. 2.

The set of ${\semcolour\lambda\mu}$’s approximants ${\semcolour\cal A}$ with respect to \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}} is defined through the grammar:

• \begin{array}[]{rrccl@{\quad}l}A&::=&\bot&\mid&xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}&(n\geq 0)\\ &&&\mid&\lambda x.A&(A\not=\bot)\\ &&&\mid&\mu\alpha.[\beta]A&(A\not=\mu\gamma[\delta]A^{\prime},~{}A\not=\bot)\end{array}**

The relation {\mathrel{\semcolour\sqsubseteq}}\subseteq{\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}^{2} is the smallest preorder that is the compatible extension of $\bot\mathrel{\semcolour\sqsubseteq}M$. 4. 4.

The set of approximants of $M$, $\semcolour{\cal A}({\ltermcol M})$, is defined as

• \begin{array}[]{rcl}\semcolour{\cal A}({\ltermcol M})&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\{\,A\mathbin{\in}{\semcolour\cal A}\mid\raise-0.25pt\hbox{\exists}\hskip 1.1ptN\mathbin{\in}{\semcolour\lambda\mu}~{}[\hskip 1.1ptM\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N\mathrel{\&}A\mathrel{\semcolour\sqsubseteq}N\hskip 1.1pt]\,\}.\end{array}**

Approximation equivalence* between terms is defined through: \begin{array}[]{@{}rcl}M\mathrel{{\semcolour\sim}\kern-2.20001pt_{\semcolour\cal A}}N&\mathrel{\semcolour\hbox{\raise-1.65001pt\hbox{=}\kern-3.8889pt\kern-2.91667pt\raise 4.40002pt\hbox{\hbox{{\scriptsize\Delta}}}\kern-2.91667pt\kern 3.8889pt}}&\semcolour{\cal A}({\ltermcol M})=\semcolour{\cal A}({\ltermcol N}).\end{array}*

The relationship between the approximation relation and reduction is characterised by:

Lemma 3.2**.**

If $A\mathrel{\semcolour\sqsubseteq}M$ and M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N, then $A\mathrel{\semcolour\sqsubseteq}N$.* 2. 2.

H* is a head-normal form if and only if there exists $A\mathbin{\in}{\semcolour\cal A}$ such that $A\mathrel{\semcolour\sqsubseteq}\mbox{\itbf H}$ and $A\not=\bot$.*

Proof 3.3**.**

By induction on the structure of approximants.

$A=\bot$

Trivial, since $\bot\mathrel{\sqsubseteq}N$.

$A=xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$

If $xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}$, with $A_{i}\mathrel{\sqsubseteq}M_{i}$ for all $i\mathbin{\in}\underline{n}$. If M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N, then $N=xN_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptN_{n}$ with M_{i}\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N_{i}, for all $i\mathbin{\in}\underline{n}$ (notice that the reduction can take place in many sub-terms, and need not take place in all). Then, by induction, $A_{i}\mathrel{\sqsubseteq}N_{i}$ for all $i\mathbin{\in}\underline{n}$, so $A\mathrel{\sqsubseteq}N$.

$A=\lambda x.A^{\prime}$, $A^{\prime}\not=\bot$

If $\lambda x.A^{\prime}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}\lambda x.M^{\prime}$, with $A^{\prime}\mathrel{\sqsubseteq}M^{\prime}$. If M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N, then $N=\lambda x.N^{\prime}$ with M^{\prime}\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N^{\prime}. Then, by induction, $A^{\prime}\mathrel{\sqsubseteq}N^{\prime}$, so $A\mathrel{\sqsubseteq}N$.

$A=\mu\alpha.[\beta]A^{\prime}$, $A^{\prime}\not=\mu\gamma[\delta]A^{\prime\prime}$, $A^{\prime}\not=\bot$

If $\mu\alpha.[\beta]A^{\prime}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}\mu\alpha.[\beta]M^{\prime}$, with $A^{\prime}\mathrel{\sqsubseteq}M^{\prime}$. Since $A^{\prime}\not=\mu\gamma[\delta]A^{\prime\prime}$, $M\not=\mu\alpha.[\beta]\mu\gamma[\delta]M^{\prime\prime}$, so any reduction in $M$ takes place inside $M^{\prime}$. So if M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N, then $N=\mu\alpha.[\beta]N^{\prime}$ with M^{\prime}\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N^{\prime}. Then, by induction, $A^{\prime}\mathrel{\sqsubseteq}N^{\prime}$, so $A\mathrel{\sqsubseteq}N$. 2. 2.

only if

By induction on the structure of head-normal forms:

$\mbox{\itbf H}=xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}$

Take $A=x\bot\hskip 0.43999pt{\cdots}\hskip 0.43999pt\bot$.

\mbox{\itbf H}=\lambda x.\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}

By induction, there exists $A\not=\bot$ such that A\mathrel{\sqsubseteq}\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}. Then \lambda x.A\mathrel{\sqsubseteq}\lambda x.\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}; notice that, since $A\not=\bot$, also $\lambda x.A\mathbin{\in}{\semcolour\cal A}$.

\mbox{\itbf H}=\ltermcol\mu\alpha.[\beta]\hskip 0.43999pt\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}},~{}\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}\not=\ltermcol\mu\gamma.[\delta]\hskip 0.43999pt\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}^{\prime}

By induction, there exists $A\not=\bot$ such that A\mathrel{\sqsubseteq}\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}. Then \ltermcol\mu\alpha.[\beta]\hskip 0.43999ptA\mathrel{\sqsubseteq}\ltermcol\mu\alpha.[\beta]\hskip 0.43999pt\mbox{\itbf H}\hskip 1.1pt\mbox{{{}^{\prime}}}; notice that, since $A\not=\ltermcol\mu\gamma.[\delta]\hskip 0.43999ptA^{\prime}$ and A\not={\ltermcol\mbox{{\perp}}}, also $\ltermcol\mu\alpha.[\beta]\hskip 0.43999ptA\mathbin{\in}{\semcolour\cal A}$.

if

If there exists $A\mathbin{\in}{\semcolour\cal A}$ such that $A\mathrel{\semcolour\sqsubseteq}M$ and $A\not=\bot$, then either:

$A=xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$

If $xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}$, so $M$ is in head-normal form.

$A=\lambda x.A^{\prime}$, $A^{\prime}\not=\bot$

If $\lambda x.A^{\prime}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}\lambda x.M^{\prime}$, with $A^{\prime}\mathrel{\sqsubseteq}M^{\prime}$. Since $A^{\prime}\not=\bot$, by induction $M^{\prime}$ is in head-normal form, so also $\lambda x.M^{\prime}$ is in head-normal form.

$A=\mu\alpha.[\beta]A^{\prime}$, $A^{\prime}\not=\mu\gamma[\delta]A^{\prime\prime}$, $A^{\prime}\not=\bot$

*If $\mu\alpha.[\beta]A^{\prime}\mathrel{\sqsubseteq}M$, then $M\mathrel{\equiv}\mu\alpha.[\beta]M^{\prime}$, with $A^{\prime}\mathrel{\sqsubseteq}M^{\prime}$. Since $A^{\prime}\not=\bot$, by induction $M^{\prime}$ is in head-normal form; since $A^{\prime}\not=\mu\gamma[\delta]A^{\prime\prime}$, also $M^{\prime}\not=\mu\gamma[\delta]M^{\prime\prime}$, so also $\mu\alpha.[\beta]M^{\prime}$ is in head-normal form.

---

The following definition introduces an operation of join on {\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}-terms.

Definition 3.4** (Join, compatible terms).**

The partial mapping join, {}\mathop{{\sqcup}}{}:{\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}^{2}\rightarrow{\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}, is defined by:

• \begin{array}[]{r@{\,}c@{\,}lcl}{\ltermcol\mbox{{\perp}}}{}\mathop{{\sqcup}}{}M\quad\mathrel{\equiv}\quad M&{}\mathop{{\sqcup}}{}&{\ltermcol\mbox{{\perp}}}&\mathrel{\equiv}&M\\ x&{}\mathop{{\sqcup}}{}&x&\mathrel{\equiv}&x\\ (\lambda x.M)&{}\mathop{{\sqcup}}{}&(\lambda x.N)&\mathrel{\equiv}&\lambda x.(M{}\mathop{{\sqcup}}{}N)\\ (\mu\alpha.[\beta]M)&{}\mathop{{\sqcup}}{}&(\mu\alpha.[\beta]N)&\mathrel{\equiv}&\mu\alpha.[\beta](M{}\mathop{{\sqcup}}{}N)\\ (M_{1}M_{2})&{}\mathop{{\sqcup}}{}&(N_{1}N_{2})&\mathrel{\equiv}&(M_{1}{}\mathop{{\sqcup}}{}N_{1})\,(M_{2}{}\mathop{{\sqcup}}{}N_{2})\end{array}333The last alternative in the definition of ${}\mathop{{\sqcup}}{}$ defines the join on applications in a more general way than Scott’s, that would state that \begin{array}[]{r@{\quad}c@{\quad}l}(M_{1}M_{2}){}\mathop{{\sqcup}}{}(N_{1}N_{2})&\mathrel{\sqsubseteq}&(M_{1}{}\mathop{{\sqcup}}{}N_{1})\,(M_{2}{}\mathop{{\sqcup}}{}N_{2}),\end{array} since it is not always sure if a join of two arbitrary terms exists. Since we will use our more general definition only on terms that are compatible, there is no real conflict.**

If $M{}\mathop{{\sqcup}}{}N$ is defined, then $M$ and $N$ are called compatible.

It is easy to show that ${}\mathop{{\sqcup}}{}$ is associative and commutative; we will use {}\mathop{{\sqcup}}{}_{\underline{\mbox{\scriptsizen}}}M_{i} for the term $M_{1}{}\mathop{{\sqcup}}{}\hskip 0.43999pt{\cdots}\hskip 0.43999pt{}\mathop{{\sqcup}}{}M_{n}$. Note that {\ltermcol\mbox{{\perp}}} can be defined as the empty join, i.e. if M\mathrel{\equiv}{}\mathop{{\sqcup}}{}_{\underline{\mbox{\scriptsize0}}}M_{i}, then M\mathrel{\equiv}{\ltermcol\mbox{{\perp}}}.

The following lemma shows that the join acts as least upper bound of compatible terms.

Lemma 3.5**.**

If $P\mathrel{\sqsubseteq}M$, and $Q\mathrel{\sqsubseteq}M$, then $P{}\mathop{{\sqcup}}{}Q$ is defined, and:

• \begin{array}[]{cccc}P\mathrel{\sqsubseteq}P{}\mathop{{\sqcup}}{}Q,&Q\mathrel{\sqsubseteq}P{}\mathop{{\sqcup}}{}Q,&\mbox{\it\Itcol and\hskip 1.1pt}&P{}\mathop{{\sqcup}}{}Q\mathrel{\sqsubseteq}M.\end{array}**

If $A_{1}$, $A_{2}\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$, then $A_{1}$ and $A_{2}$ are compatible.

Proof 3.6**.**

By easy induction on the definition of $\mathrel{\sqsubseteq}$. 2. 2.

If $A_{1}$, $A_{2}\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$, then there exist $N_{1}$, $N_{2}$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N_{i} and $A_{i}\mathrel{\sqsubseteq}N_{i}$, for $i=1,2$. Since \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}} is confluent, there exists $P$ such that N_{i}\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}P; then by Lem. 3.2, also $A_{i}\mathrel{\sqsubseteq}P$, for $i=1,2$. Then, by part (1), $A_{1}$ and $A_{2}$ are compatible.∎

We can also define $\mathord{{\hskip 0.43999pt\psset{unit=0.85417pt}\raise 8.25005pt\hbox{\put(12.0,2.0){{\psline{c-c}(0.0pt,0.0pt)(2.56252pt,0.0pt)}{\psline{cc-cc}(0.0pt,0.0pt)(0.0pt,-6.83337pt)}{\psline{cc-cc}(1.28125pt,0.0pt)(1.28125pt,-5.12503pt)}}}\kern 4.40002pt}{M}{\kern 3.30002pt\psset{unit=1.1pt}\hbox{\put(0.0,-2.0){{\psline{c-c}(0.0pt,0.0pt)(-3.30002pt,0.0pt)}{\psline{cc-cc}(-1.485pt,0.0pt)(-1.485pt,6.60004pt)}{\psline{cc-cc}(0.0pt,0.0pt)(0.0pt,8.80005pt)}}}\kern 2.20001pt}}=\sqcup\,\{\,A\mid A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})\,\}$ (which by the previous lemma is well defined); then $\mathord{{\hskip 0.43999pt\psset{unit=0.88pt}\raise 8.25005pt\hbox{\put(12.0,2.0){{\psline{c-c}(0.0pt,0.0pt)(2.64001pt,0.0pt)}{\psline{cc-cc}(0.0pt,0.0pt)(0.0pt,-7.04004pt)}{\psline{cc-cc}(1.32pt,0.0pt)(1.32pt,-5.28003pt)}}}\kern 4.40002pt}{\cdot}{\kern 3.30002pt\psset{unit=1.1pt}\hbox{\put(0.0,-2.0){{\psline{c-c}(0.0pt,0.0pt)(-3.30002pt,0.0pt)}{\psline{cc-cc}(-1.485pt,0.0pt)(-1.485pt,6.60004pt)}{\psline{cc-cc}(0.0pt,0.0pt)(0.0pt,8.80005pt)}}}\kern 2.20001pt}}$ corresponds to (a ${\semcolour\lambda\mu}$ variant of) Böhm trees [15, 13].

As is standard in other settings, interpreting a ${\semcolour\lambda\mu}$-term $M$ through its set of approximants $\semcolour{\cal A}({\ltermcol M})$ gives a semantics.

Theorem 3.7** (Approximation semantics for ${\semcolour\lambda\mu}$).**

If $M\mathbin{\semcolour=_{\beta\mu}}N$, then $M\mathrel{{\semcolour\sim}\kern-2.20001pt_{\semcolour\cal A}}N$.

• *Proof: *

By induction on the definition of $\mathbin{\semcolour=_{\beta\mu}}$, of which we only show the case M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N.

$\semcolour{\cal A}({\ltermcol M})\subseteq\semcolour{\cal A}({\ltermcol N})$

If $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$, then there exists $L$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}L and $A\mathrel{\sqsubseteq}L$. Since \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}} is Church-Rosser, there exists $R$ such that L\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}R and N\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}R, so also M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}R. Then by Lem. 3.2, $A\mathrel{\sqsubseteq}R$, and since N\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}R, we have $A\mathbin{\in}\semcolour{\cal A}({\ltermcol N})$.

$\semcolour{\cal A}({\ltermcol N})\subseteq\semcolour{\cal A}({\ltermcol M})$

If $A\mathbin{\in}\semcolour{\cal A}({\ltermcol N})$, then there exists $L$ such that N\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}L and $A\mathrel{\sqsubseteq}L$. But then also M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}L, so $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$.

The reverse implication of this result does not hold, since terms without head-normal form (which have only $\bot$ as approximant) are not all related by reduction, so approximation semantics is not fully abstract.

4 The approximation and head normalisation results for $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$

In this section we will show an approximation result, i.e. for every $M$, $\Gamma$, \typecolS, and $\Delta$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, there exists an $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. From this, the well-known characterisation of (head-)normalisation of ${\semcolour\lambda\mu}$-terms using intersection types follows easily, i.e. all terms having a (head) normal form are typeable in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ (with a type without $\omega$-occurrences). Another result is the well-known characterisation of strong normalisation of typeable ${\semcolour\lambda\mu}$-terms, i.e. all terms, typeable in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ without using the rule (\mathop{{\colourfortype\mbox{{\cap}}}}) with $I=\raise-0.35pt\hbox to6.60004pt{\psset{unit=1.21pt,linewidth=0.38501pt} {\psset{linewidth=0.2475pt}\pscircle(3.78127pt,3.63002pt){3.02501pt}}{\psline{cc-cc}(2.11751pt,-0.9075pt)(5.14252pt,8.16754pt)}}$, are strongly normalisable.

First we give some auxiliary definitions and results.

The rules of the system $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ are generalised to {\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}; therefore, if {\ltermcol\mbox{{\perp}}} occurs in a term $M$ and ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, in that derivation {\ltermcol\mbox{{\perp}}} has to appear in a position where the rule (\mathop{{\colourfortype\mbox{{\cap}}}}) is used with $I=\raise-0.35pt\hbox to6.60004pt{\psset{unit=1.21pt,linewidth=0.38501pt} {\psset{linewidth=0.2475pt}\pscircle(3.78127pt,3.63002pt){3.02501pt}}{\psline{cc-cc}(2.11751pt,-0.9075pt)(5.14252pt,8.16754pt)}}$, i.e., in a sub-term typed with $\omega$. Notice that \lambda x.{\ltermcol\mbox{{\perp}}}, {\ltermcol\mbox{{\perp}}}M_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}, and \mu\alpha.[\beta]{\ltermcol\mbox{{\perp}}} are typeable by $\omega$ only.

First we show that $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ is closed for $\mathrel{\sqsubseteq}$.

Lemma 4.1**.**

${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$* and $M\mathrel{\sqsubseteq}N$ then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.*

Proof 4.2**.**

By easy induction on the definition of $\mathrel{\sqsubseteq}$; the base case, {\ltermcol\mbox{{\perp}}}\mathrel{\sqsubseteq}N, follows from the fact that then $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\omega$. ∎

Next we define a notion of type assignment that is similar to that of Def. 2.2, but differs in that it assigns $\omega$ only to the term {\ltermcol\mbox{{\perp}}}.

Definition 4.3**.**

{\ltermcol\mbox{{\perp}}}-type assignment* and {\ltermcol\mbox{{\perp}}}-derivations are defined as $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$, with the exception of:*

• \begin{array}[t]{rl@{\dquad}rl}(\,{\mathop{{\colourfortype\mbox{{\cap}}}}}_{\perp}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\quad(\raise-0.25pt\hbox{$\forall$}\hskip 1.1pti\mathbin{\in}\underline{n})}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=134.3371pt\hbox{\kern 3.00003pt({\bluecol n=0\mathrel{\vee}n\geq 2})}}}\hbox{\kern 5.23926pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol{}\mathop{{\sqcup}}{}{\underline{\mbox{$n$}}}M_{i}}\mathbin{:}{\colourfortype\mbox{{$\cap$}}{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\hfil\quad\quad\end{array}**

We write ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ if this statement is derivable using a {\ltermcol\mbox{{\perp}}}-derivation.

Notice that, by rule (\,{\mathop{{\colourfortype\mbox{{\cap}}}}}_{\perp}), {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol{\ltermcol\mbox{{\perp}}}}\mathbin{:}{\colourfortype\omega}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, and that this is the only way to assign $\omega$ to a term. Moreover, in that rule, the terms $M_{j}$ need to be compatible (otherwise their join would not be defined).

Lemma 4.4**.**

If ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 2. 2.

If ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then there exists $M^{\prime}\mathrel{\sqsubseteq}M$ such that ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol M^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.

Proof 4.5**.**

By induction on the structure of derivations in $\mathbin{{\vdash}\kern-2.20001pt_{\perp}}$. We only show:

\,{\mathop{{\colourfortype\mbox{{\cap}}}}}_{\perp}

Then \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{{\cap}}_{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i}, M={}\mathop{{\sqcup}}{}_{\underline{\mbox{\scriptsizen}}}M_{i}, and, for every ${i}\mathbin{\in}{\underline{n}}$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol M_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Then, by induction, for every ${i}\mathbin{\in}{\underline{n}}$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Since, by Lem. 3.5, $M_{i}\mathrel{\sqsubseteq}M$ for all ${i}\mathbin{\in}{\underline{n}}$, by Lem. 4.1, for every ${i}\mathbin{\in}{\underline{n}}$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, so by (\mathop{{\colourfortype\mbox{{\cap}}}}), {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{{\cap}}_{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

All other cases follow by straightforward induction. 2. 2.

By induction on the structure of derivations in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$. We only show:

\mathop{{\colourfortype\mbox{{\cap}}}}

Then \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{{\cap}}_{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i} and, for every ${i}\mathbin{\in}{\underline{n}}$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$; by induction, for every ${i}\mathbin{\in}{\underline{n}}$ there exists $M_{i}\mathrel{\sqsubseteq}M$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol M_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ (notice that then these $M_{i}$ are compatible). Then, by rule (\,{\mathop{{\colourfortype\mbox{{\cap}}}}}_{\perp}), we have {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol{}\mathop{{\sqcup}}{}_{\underline{\mbox{\scriptsizen}}}M_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. Notice that, by Lem. 3.5, {}\mathop{{\sqcup}}{}_{\underline{\mbox{\scriptsizen}}}M_{i}\mathrel{\sqsubseteq}M.

All other cases follow by straightforward induction.∎

Notice that, since $M^{\prime}$ need not be the same as $M$, the second derivation in part (2) is not exactly the same; however, it has the same structure in terms of applied derivation rules.

Using Thm. 2.4(4) and Lem. 4.4, as for the BCD-system (see [22]) and the system of [3], the relation between types assignable to a ${\semcolour\lambda\mu}$-term and those assignable to its approximants can be formulated as:

Theorem 4.6** (Approximation).**

{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\mathrel{\hskip 1.0pt{\Leftarrow}\kern-6.60004pt{\Rightarrow}\hskip 1.0pt}\raise-0.25pt\hbox{\exists}\hskip 1.1ptA\mathbin{\in}\semcolour{\cal A}({\ltermcol M})~{}[\hskip 1.1pt{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\hskip 1.1pt].

• *Proof: *

$\mathrel{\Rightarrow}$

If ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then, by Thm. 2.4(4), $\textsl{SN}\hskip 0.43999pt({\orangecol\hskip 1.1pt\mathcal{D}})$. Let ${\orangecol\hskip 1.1pt\mathcal{D}}^{\prime}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ be a normal form of ${\orangecol\hskip 1.1pt\mathcal{D}}$ with respect to \mathrel{\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\mbox{\scriptsize\sc Der}}}, then by Thm. 2.4(3), $M\mathrel{\semcolour\rightarrow^{*}\kern-3.5pt\kern-1.1pt_{\beta}}N$ and, by Lem. 4.4 (2), there exists $N^{\prime}\mathrel{\sqsubseteq}N$ such that ${\orangecol\hskip 1.1pt\mathcal{D}}^{\prime}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol N^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. So, in particular, $N^{\prime}$ contains no redexes (no redexes typed with a type different form $\omega$ since ${\orangecol\hskip 1.1pt\mathcal{D}}^{\prime}$ is in normal form, and none typed with $\omega$ since only {\ltermcol\mbox{{\perp}}} can be typed with $\omega$), so $N^{\prime}\mathbin{\in}{\termcol\cal A}$, and therefore $N^{\prime}\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$.

$\mathrel{\Leftarrow}$

Let $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$ be such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Since $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$, there exists $N$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N and $A\mathrel{\sqsubseteq}N$. Then, by Lem. 4.1, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and, by Thm. 2.4(2), also ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. ∎

Using this last result, the characterisation of head-normalisation becomes easy to show.

Theorem 4.7** (Head-normalisation).**

There exists $\Gamma$, A, and $\Delta$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, if and only if $M$ has a head normal form.

• *Proof: *

only if

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then, by Thm. 4.6, there exists an $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\perp}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Then, by Def. 3.1, there exists $N$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N and $A\mathrel{\sqsubseteq}N$. Since $\mbox{\kern 0.275pt\typefont A\kern 0.825pt}\not=\omega$, A\not\mathrel{\equiv}{\ltermcol\mbox{{\perp}}}, so we know that $A$ is either $xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$ $(n\geq 0)$, $\lambda x.A^{\prime}$, or $\mu\alpha.[\beta]A^{\prime}$ with $A^{\prime}\not=\mu\gamma.[\delta]A^{\prime\prime}$. Since $A\mathrel{\sqsubseteq}N$, $N$ is either $xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}$ $(n\geq 0)$, $\lambda x.P$, or $\mu\alpha.[\beta]P$ with $P\not=\mu\gamma.[\delta]Q$. Then $N$ is in head-normal from and $M$ has a head-normal form.

if

If $M$ has a head-normal form, then there exists $N$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N and either:

$N\mathrel{\equiv}xM_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptM_{n}$

Take \Gamma=x{:}\omega\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\omega\mathord{\mbox{\typecol\typefont\times}}\Omega\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon (with $n$ times $\omega$) and \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\Omega\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon.

$N\mathrel{\equiv}\lambda x.P$

Since $P$ is in head-normal form, by induction there are $\Gamma^{\prime}$, C, $\upsilon$, and $\Delta^{\prime}$ such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt. If $x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\in}\Gamma^{\prime}$, take $\Gamma=\Gamma^{\prime}{\setminus}x$, and \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon; otherwise take $\Gamma=\Gamma^{\prime}$ and \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\omega\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon. In either case, by rule $(\textit{Abs})$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol\lambda x.P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt$

$N=\mu\alpha.[\alpha]P$

Since $P$ is in head-normal form, by induction there are $\Gamma^{\prime}$, C, \typecolD, $\upsilon$, and $\Delta^{\prime}$ such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta^{\prime}}}\hskip 1.1pt. Take \mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\contfont{\typecol D}}, then by Thm. 2.4 (1) also {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt, and since $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, by rule $(\mu)$ we get {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol\mu\alpha.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt.

$N=\mu\alpha.[\beta]P$, with $\alpha\not=\beta$

Since $P$ is in head-normal form, by induction there are C, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, \typecolD such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt and $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$. Take \mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\contfont{\typecol D}}, then by Thm. 2.4 (1) also {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta}}\hskip 1.1pt, and since $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$ we get {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol\mu\alpha.[\beta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}}}\hskip 1.1pt by $(\mu^{\prime})$.

Notice that in all cases, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, for some A, and by Thm. 2.4(2), ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. ∎

5 Type assignment for (strong) normalisation

In this section we show the characterisation of both normalisation and strong normalisation, for which we first define a notion of derivability obtained from $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ by restricting the use of the type assignment rule (\mathop{{\colourfortype\mbox{{\cap}}}}) to at least two sub-derivations, thereby eliminating the possibility to assign $\omega$ to a term.

Definition 5.1** (SN type assignment).**

*We define the $\omega$-free types by the grammar: *

• \begin{array}[]{rcl@{\quad}l@{\quad}l}\mbox{\kern 0.275pt\typefont A\kern 0.825pt},\mbox{\kern 0.275pt\typefont B\kern 0.825pt}&::=&\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon\\ \mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt},\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt},\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}&::=&\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}&(n\geq 1)\\ \mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\contfont{\typecol D}}&::=&\Omega\mid\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\end{array}**

SN type assignment* is defined using the natural deduction system of Def. 2.2, but allowing only $\omega$-free types, so restricting rule (\mathop{{\colourfortype\mbox{{\cap}}}}) to:*

• \begin{array}[t]{rl}(\mathop{{\colourfortype\mbox{{\cap}}}}):&{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\displaystyle\penalty 1{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\quad(\raise-0.25pt\hbox{$\forall$}\hskip 1.1pti\mathbin{\in}\underline{n})}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\kern-0.25pt\vrule height=0.25002pt,depth=0.25002pt,width=132.40782pt\hbox{\kern 3.00003pt({\bluecol n\geq 2})}}}\hbox{\kern 10.5726pt\hbox{\displaystyle{\colourfortype\Gamma}\mathrel{{\blackcol{\vdash}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{{$\cap$}}{\underline{n}}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt}}}}\end{array}**

We write ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ if this judgement is derivable using this system.

Notice that the only real change in the system compared to $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$ is that $\omega$ is no longer an intersection type, so in rule (\mathop{{\colourfortype\mbox{{\cap}}}}), the empty intersection $\omega$ is excluded.444With the aim of the characterisation of strong normalisation, it would have sufficed to only restrict rule (\mathop{{\colourfortype\mbox{{\cap}}}}); we restrict the set of types as well in order to be able to characterise normalisation as well.

The following properties hold:

Lemma 5.2**.**

If $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{{\colourfortype\leq}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}$, then \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{{\cap}}_{I}\hskip 0.275pt{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}_{i}, \mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}=\mbox{{\cap}}_{J}\hskip 0.275pt\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{j}, and for every $j\mathbin{\in}J$ there exists $i\mathbin{\in}I$ such that $\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}=\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{j}$. 2. 2.

${\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol x}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, if and only if $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}$. 3. 3.

${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\mathrel{\Rightarrow}{\colourfortype\{x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\in}\Gamma\mid x\mathbin{\in}\mbox{\it\Itcol fv\hskip 1.1pt}\hskip 0.275pt({\ltermcol M})\}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\in}\Delta\mid\alpha\mathbin{\in}\textit{\semcolour fn}({\ltermcol M})\}}}\hskip 1.1pt$. 4. 4.

${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\mathrel{\&}\Gamma^{\prime}\supseteq\Gamma\mathrel{\&}\Delta^{\prime}\supseteq\Delta\mathrel{\Rightarrow}{\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt$. 5. 5.

${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\mathrel{\hskip 1.0pt\Rightarrow\hskip 1.0pt}{\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.

Proof 5.3**.**

Straightforward.∎

As for $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$, we can show that $(\mathbin{\leq_{\hbox{{\sc s}}}})$ is an admissible rule in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$.

Lemma 5.4**.**

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and $\Gamma^{\prime}$, \typecolT, and $\Delta^{\prime}$ are all $\omega$-free and satisfy $\Gamma^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\Gamma$, $\Delta^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\Delta$, and $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}$, then ${\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt$.

• *Proof: *

Much the same as the proof for Thm. 2.4(1) in [8].∎

The following lemma shows a (limited) subject expansion result for $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$: it states that if a contraction of a redex is typeable, then so is the redex, provided that the operand $N$ is typeable in its own right; since $N$ might not appear in the contractum, we need to assume that separately. Notice that we demand that $N$ is typeable in the same contexts as the redex itself; this property would not hold once we consider contextual closure (in particular, when the reduction takes place under an abstraction); it might be that free names or variables in $N$ get bound in the context.

Lemma 5.5**.**

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M[N{\cdot}\gamma/\alpha]:\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}$ and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then there exists \typecolS such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.

• *Proof: *

By nested induction; the outermost is on the structure of types, and the innermost on the structure of terms. We only show:

$M\mathrel{\equiv}x$

Then $x[N{\cdot}\gamma/\alpha]=x$. Take $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{\kern 0.275pt\typefont B\kern 0.825pt}$, then by Lem. 5.2, also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol x}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt.

All other cases follow by induction.∎

To prepare the characterisation of terms by their assignable types, we first prove that a term in {\semcolour\lambda\mu}{\ltermcol\mbox{{\perp}}}-normal form is typeable without $\omega$, if and only if it does not contain {\ltermcol\mbox{{\perp}}}. This forms the basis for the result that all normalisable terms are typeable without $\omega$. Notice that the first result is stated for $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$.

Lemma 5.6**.**

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and $\Gamma$, A, and $\Delta$ are $\omega$-free, then $A$ is {\ltermcol\mbox{{\perp}}}-free. 2. 2.

If $A$ is {\ltermcol\mbox{{\perp}}}-free, then there are $\Gamma$, A, and $\Delta$, such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.

Proof 5.7**.**

By induction on the structure of approximate normal forms.

$A\mathrel{\equiv}x$

Immediate.

A\mathrel{\equiv}{\ltermcol\mbox{{\perp}}}

Impossible, by inspecting the rules of $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}$.

$A\mathrel{\equiv}\lambda x.A^{\prime}$

By $(\textit{Abs})$, \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, and {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. Of course also $\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}$, and \mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon are $\omega$-free, so by induction, $A^{\prime}$ is {\ltermcol\mbox{{\perp}}}-free, so also $\lambda x.A^{\prime}$ is {\ltermcol\mbox{{\perp}}}-free.

$A\mathrel{\equiv}xA_{0}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$

Then by $(\textit{App})$ and $({\bluecol\textsl{Ax}})$, ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and x{:}\mbox{{\cap}}_{\underline{m}}\hskip 0.275pt\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{i}\mathbin{\in}\Gamma, and, for some $j\mathbin{\in}m$, \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon=\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{j} and \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon. Since each $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{i}$ occurs in $\mbox{\kern 0.275pt\typefont B\kern 0.825pt}_{j}$, which occurs in $\Gamma$, all are $\omega$-free, so by induction each $A_{i}$ is {\ltermcol\mbox{{\perp}}}-free. Then also $xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$ is {\ltermcol\mbox{{\perp}}}-free.

$A\mathrel{\equiv}\mu\alpha.[\alpha]A^{\prime}$, with $A^{\prime}\not=\mu\gamma.[\delta]A^{\prime\prime}$

Then \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, and by $(\mu)$ there exists \typecolD such that $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt. Since $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and C is $\omega$-free, so is \typecolD; then, by induction, $A^{\prime}$ is {\ltermcol\mbox{{\perp}}}-free, so so is $\mu\alpha.[\alpha]A^{\prime}$.

$A\mathrel{\equiv}\mu\alpha.[\beta]A^{\prime}$, with $\alpha\not=\beta$ and $A^{\prime}\not=\mu\gamma.[\delta]A^{\prime\prime}$

Then \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, and by $(\mu^{\prime})$ there exists \typecolD, $\mbox{\contfont{\typecol D}}^{\prime}$ such that $\Delta=\beta{:}\mbox{\contfont{\typecol D}}^{\prime},\Delta^{\prime}$, $\mbox{\contfont{\typecol D}}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\contfont{\typecol D}}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. Since $\mbox{\contfont{\typecol D}}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and $\mbox{\contfont{\typecol D}}^{\prime}$ is $\omega$-free, so is \typecolD; then, by induction, $A^{\prime}$ is {\ltermcol\mbox{{\perp}}}-free, so so is $\mu\alpha.[\beta]A^{\prime}$. 2. 2.

$A\mathrel{\equiv}x$

Then {\colourfortype x{:}\Omega\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol x}\mathbin{:}{\colourfortype\Omega\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$A\mathrel{\equiv}\lambda x.A^{\prime}$

By induction {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. If $x$ does not occur in $\Gamma$, take a $\omega$-free \typecolT; otherwise, there exist $x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\in}\Gamma$ and \typecolT is $\omega$-free. In either case, by $(\textit{Abs})$ we obtain {\colourfortype\Gamma{\setminus}x}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda x.A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$A\mathrel{\equiv}xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}$

By induction there are ${\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}~{}(\forall iGn)$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ for every ${i}\mathbin{\in}{\underline{n}}$. Then {\colourfortype\Gamma\mathop{{\colourfortype\mbox{{\cap}}}}\{x{:}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont A\kern 0.825pt}_{n}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon\}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol xA_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptA_{n}}\mathbin{:}{\colourfortype\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$A\mathrel{\equiv}\mu\alpha.[\beta]A^{\prime}$, with $A^{\prime}\not=\mu\gamma.[\delta]A^{\prime\prime}$

By induction {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\contfont{\typecol D}},\Delta}}\hskip 1.1pt for some $\Gamma$, $\Delta$, C, \typecolD, and $\upsilon$. Then Lem. 5.4, also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\contfont{\typecol D}}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt, so by rule $(\mu)$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]A^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$A\mathrel{\equiv}\mu\alpha.[\beta]A^{\prime}$, with $\alpha\not=\beta$ and $A^{\prime}\not=\mu\gamma.[\delta]A^{\prime\prime}$

*By induction {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\contfont{\typecol D}},\Delta}}\hskip 1.1pt for some $\Gamma$, $\Delta$, C, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, \typecolD, and $\upsilon$. Then also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\contfont{\typecol D}}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt, so by rule $(\mu^{\prime})$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]A^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\contfont{\typecol D}}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt.

---

Now, as also shown in [2], it is possible to characterise normalisable terms.

Theorem 5.8** (Characterisation of Normalisation).**

There exists $\omega$-free $\Gamma$, $\Delta$, and A such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, if and only if $M$ has a normal form.

• *Proof: *

$\mathrel{\Rightarrow}$

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, by Thm. 4.6 there exists $A\mathbin{\in}\semcolour{\cal A}({\ltermcol M})$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol A}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Since $\Gamma$, A, and $\Delta$ are $\omega$-free, by Lem. 5.6(1), this $A$ is {\ltermcol\mbox{{\perp}}}-free. By Def. 3.1 there exists $N$ such that M\mathrel{{\semcolour\rightarrow}\hbox{\raise 4.95003pt\hbox{\scriptsize{\semcolour*}}\kern-9.8486pt\hbox{{\semcolour_{\beta\mu}}}}}N and $A\mathrel{\sqsubseteq}N$. Since $A$ contains no {\ltermcol\mbox{{\perp}}}, $A\equiv N$, so $N$ is a normal form, so $M$ has a normal form.

$\mathrel{\Leftarrow}$

If $N$ is the normal form of $M$, then it is a {\ltermcol\mbox{{\perp}}}-free approximate normal form. By Lem. 5.6(2) there are $\Gamma$, A, and $\Delta$ such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. By Lem. 5.2(5) also ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and by Thm. 2.4(2), ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, and $\Gamma$, \typecolS, and $\Delta$ are $\omega$-free.∎

In [8] it is shown that it is possible to characterise the set of all terms that are strongly normalisable with respect to \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}, using Thm. 2.4(4), and the proof for the property that all terms in normal form can be typed in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$, a property that follows here from Lem. 5.6 (see the proof of the previous result). Other than that, the proof is identical.

The following lemma shows that $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$ is closed under the expansion of redexes (notice that the result is not stated for arbitrary reduction steps, but only for terms that are proper redexes).

Lemma 5.9**.**

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M[N/x]:\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype\Delta}$ and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.M)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 2. 2.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\gamma]P[Q{\cdot}\gamma/\beta]Q:\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype\Delta}$ and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\mu\beta.[\beta]P)Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 3. 3.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\delta]P[Q{\cdot}\gamma/\beta]}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ (with $\beta\not=\delta$) and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\mu\beta.[\delta]P)Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 4. 4.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.([\delta]P)[\beta/\gamma]}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]\mu\gamma.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$.

Proof 5.10**.**

By nested induction on the structure of types and the structure of terms. We just show the case \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon.

$M\mathrel{\equiv}x$

Then $M[N/x]=N$ and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. We have \Gamma,x{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol x}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon} by rule $({\bluecol\textsl{Ax}})$. Then {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda x.x}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt by $(\textit{Abs})$ and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.x)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt by rule $(\textit{App})$.

$M\mathrel{\equiv}y\not=x$

We have $y[N/x]\mathrel{\equiv}y$ and $x\mathbin{\not\in}\mbox{\it\Itcol fv\hskip 1.1pt}\hskip 0.275pt({\ltermcol y})$; by Lem. 5.2, \Gamma,x{:}\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol y}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}. Then {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda x.y}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt by $(\textit{Abs})$ and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.y)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt by rule $(\textit{App})$.

$M\mathrel{\equiv}\lambda y.M^{\prime}$

If {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda y.M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, then there exist \typecolS, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, \typecolR such that {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt},y{:}\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and \mbox{\kern 0.275pt\contfont C\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}. Then by induction, we get {\colourfortype\Gamma,y{:}\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.M^{\prime})N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. Then, by rules $(\textit{App})$ and $(\textit{Abs})$, there exists \typecolT such that {\colourfortype\Gamma,y{:}\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt},x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and (also using Lem. 5.2) ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. But then we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda xy.M^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt by $(\textit{Abs})$, and by rule $(\textit{App})$ also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda xy.M^{\prime})N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$M=PQ$

Then there exists \typecolR such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P\,[N/x]}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q[N/x]}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Then by induction, both {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.P)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.Q)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Then by rules $(\textit{Abs})$, $(\textit{App})$, and (\mathop{{\colourfortype\mbox{{\cap}}}}) there are \typecolS, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}_{i}$, $\upsilon_{i}$, $\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}$ ($i\mathbin{\in}\underline{n}$) such that \mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}={\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\contfont C\kern 0.825pt}_{i}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon_{i}, and {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, as well as {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}_{i}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, for all $i\mathbin{\in}\underline{n}$ (notice that, as above, we can assume that $x$ is not free in $N$).

By (\mathop{{\colourfortype\mbox{{\cap}}}}) and Lem. 5.4 we have {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}{\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}{\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol R}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt as well as {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}{\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. By $(\textit{App})$ and Lem. 5.4 we get {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}{\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol PQ}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and by $(\textit{Abs})$ {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda x.PQ}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathop{{\colourfortype\mbox{{\cap}}}}{\mbox{{\cap}}}_{\underline{n}}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}_{i}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt. Then by $(\textit{App})$ we obtain {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.PQ)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$M\mathrel{\equiv}\mu\alpha.[\alpha]P$

Then there exists \typecolD such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[N/x]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt with $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and by induction {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.P)N}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt. Then by rules $(\textit{Abs})$ and $(\textit{App})$, there exists \typecolS such that {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ (we can assume that $\alpha$ is not free in $N$). Then by rule $(\mu)$, {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and by $(\textit{Abs})$ and $(\textit{App})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.\mu\alpha.[\alpha]P)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$M\mathrel{\equiv}\mu\alpha.[\beta]P$, $\alpha\not=\beta$

Then there exists $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, \typecolD such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[N/x]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt with $\mbox{\contfont{\typecol D}}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}$, and by induction {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.P)N}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt. Then by rules $(\textit{Abs})$ and $(\textit{App})$, there exists \typecolS such that {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt$ (we can assume that $\alpha$ is not free in $N$). Then by rule $(\mu^{\prime})$, {\colourfortype\Gamma,x{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt and by $(\textit{Abs})$ and $(\textit{App})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\lambda x.\mu\alpha.[\beta]P)N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta}}\hskip 1.1pt. 2. 2.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\gamma]P[Q{\cdot}\gamma/\beta]Q:\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype\Delta}$, then by rule $(\mu)$ there are $\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\contfont{\typecol D}},\upsilon$ such that A=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$ and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[Q{\cdot}\gamma/\beta]Q:\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}. Then by rule $(\textit{App})$ there exists $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}$ such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[Q{\cdot}\gamma/\beta]:\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta} and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}}\mathbin{\mid}{\colourfortype{\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt$.

By Lem. 5.5 there exists $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}$ such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Take \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{2}, then ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ by Lem. 5.2, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt by Lem. 5.4. Then \mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}, so by rule $(\mu)$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\beta.[\beta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt; then, by rule $(\textit{App})$, we get ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\mu\beta.[\beta]P)Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 3. 3.

If ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\delta]P[Q{\cdot}\gamma/\beta]:\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype\Delta}$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\mbox{\contfont{\typecol D}},\upsilon$ such that \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\Delta=\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}$, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[Q{\cdot}\gamma/\beta]:\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}. By Lem. 5.5, there exists \typecolS such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt$. By rule $(\mu)$, we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\beta.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt and we get ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol(\mu\beta.[\delta]P)Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ by rule $(\textit{App})$. 4. 4.

We distinguish the following cases (where we assume that distinct identifiers are not equal, and $N=\mu\alpha.([\delta]P)[\beta/\gamma]$ and $M=\mu\alpha.[\beta]\mu\gamma.[\delta]P$):

$N=\mu\alpha.[\alpha]P[\alpha/\gamma]$

By rule $(\mu)$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\contfont{\typecol D}},\upsilon$ such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M[\alpha/\gamma]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt, \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, and $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$. Then also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt. Then either:

$M=\mu\alpha.[\alpha]\mu\gamma.[\gamma]P$

By rule $(\mu)$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\gamma]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt, and again by rule $(\mu)$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]\mu\gamma.[\gamma]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$M=\mu\alpha.[\alpha]\mu\gamma.[\alpha]P$

By rule $(\mu^{\prime})$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta}}\hskip 1.1pt, and by rule $(\mu)$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]\mu\gamma.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt.

$N=\mu\alpha.[\alpha]P[\beta/\gamma]$

Then $M=\mu\alpha.[\beta]\mu\gamma.[\alpha]P$. By rule $(\mu)$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\mbox{\contfont{\typecol D}},\upsilon$ such that \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\Delta=\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[\beta/\gamma]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt, and $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$; then also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. Then we have {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt by rule $(\mu^{\prime})$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]\mu\gamma.[\alpha]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt again by rule $(\mu^{\prime})$.

$N=\mu\alpha.[\beta]P[\beta/\gamma]$

By rule $(\mu^{\prime})$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\mbox{\contfont{\typecol D}},\upsilon$ such that \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\Delta=\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}$, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[\beta/\gamma]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt, and $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$. Then {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt, and either:

$M=\mu\alpha.[\beta]\mu\gamma.[\gamma]P$

By rule $(\mu)$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\gamma]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt, and by rule $(\mu^{\prime})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]\mu\gamma.[\gamma]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt.

$M=\mu\alpha.[\beta]\mu\gamma.[\beta]P$

By rule $(\mu^{\prime})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\beta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt and again by rule $(\mu^{\prime})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]\mu\gamma.[\beta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt.

$N=\mu\alpha.[\delta]P[\alpha/\gamma]$

Then $M=\mu\alpha.[\alpha]\mu\gamma.[\delta]P$. By rule $(\mu^{\prime})$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\contfont{\typecol D}},\upsilon$ such that $\Delta=\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}$, \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[\alpha/\gamma]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. Then also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. We get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt by rule $(\mu^{\prime})$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]\mu\gamma.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt by rule $(\mu)$.

$N=\mu\alpha.[\delta]P[\beta/\gamma]$

Then $M=\mu\alpha.[\beta]\mu\gamma.[\delta]P$. By rule $(\mu^{\prime})$, there are $\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\mbox{\contfont{\typecol D}},\upsilon$ such that \mbox{\kern 0.275pt\typefont A\kern 0.825pt}=\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon, $\Delta=\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}$, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P[\beta/\gamma]}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}}}\hskip 1.1pt; then also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\gamma{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}}}\hskip 1.1pt. By rule $(\mu^{\prime})$ we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\gamma.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}}}\hskip 1.1pt and we get {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]\mu\gamma.[\delta]P}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\delta{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime\prime},\Delta^{\prime}}}\hskip 1.1pt again by $(\mu^{\prime})$. ∎

Thm. 5.14 below shows that the set of strongly normalisable terms is exactly the set of terms typeable in the intersection system without using the type constant $\omega$. The proof goes by induction on the leftmost outermost reduction path. First we introduce the notion of leftmost, outer-most reduction.

Definition 5.11**.**

An occurrence of a redex R in a term $M$ is called the leftmost, outermost redex of $M$ ($\textit{lor}\hskip 0.43999pt(M)$), if:

There is no redex $\mbox{{R}}^{\prime}$ in $M$ such that $\mbox{{R}}^{\prime}=\textrm{\small\sf C}\hskip 1.1pt[\hskip 1.1pt\mbox{{R}}\hskip 1.1pt]$ with $\textrm{\small\sf C}\hskip 1.1pt[\hskip 1.1pt-\hskip 1.1pt]\not=[-]$ (outer-most); 2. 2.

There is no redex $\mbox{{R}}^{\prime}$ in $M$ such that $M=\textrm{\small\sf C}_{0}\hskip 1.1pt[\hskip 1.1pt\textrm{\small\sf C}_{1}\hskip 1.1pt[\hskip 1.1pt\mbox{{R}}^{\prime}\hskip 1.1pt]\,\textrm{\small\sf C}_{2}\hskip 1.1pt[\hskip 1.1pt\mbox{{R}}\hskip 1.1pt]\hskip 1.1pt]$ (leftmost).

We write $M\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N$ is used to indicate that $M$ reduces to $N$ by contracting $\textit{lor}\hskip 0.43999pt(M)$.

The following lemma formulates a subject expansion result for $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$ with respect to left-most outer-most reduction.

Lemma 5.12**.**

Assume $M\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt; if $\textit{lor}\hskip 0.43999pt(M)=PQ$ also assume that ${\colourfortype\Gamma_{0}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta_{0}}}\hskip 1.1pt$. Then there exists $\Gamma^{\prime},\Delta^{\prime},\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$ such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt.

Proof 5.13**.**

We reason by induction on the structure of terms:

$M\mathrel{\equiv}VP_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}$

We distinguish two cases:

1. 1.

$V$* is a \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}-redex, and $N\mathrel{\equiv}V^{\prime}P_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}$, where $V^{\prime}$ is the result of contracting $V$. From the fact that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol V^{\prime}P_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}:\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\Delta}, we know there are $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1},\ldots,\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}$ such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol V^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ for all ${i}\mathbin{\in}{\underline{n}}$. Then by Lem. 5.9, {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol V}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, so also {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol VP_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}:\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\Delta}.* 2. 2.

$V\mathrel{\equiv}y$, so there exists ${j}\mathbin{\in}{\underline{n}}$ such that $\textit{lor}\hskip 0.43999pt(M)=\textit{lor}\hskip 0.43999pt(P_{j})$, $P_{j}\mathrel{\rightarrow_{\textit{\scriptsize lor}}}P_{j}^{\prime}$, and $N\mathrel{\equiv}yP_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP^{\prime}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}$. From {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol yP_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{j}^{\prime}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}:\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\Delta}, we know there are $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1},\ldots,\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}$ such that {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol y}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P_{i}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{i}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ for all $i\not=j\mathbin{\in}\underline{n}$, and ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P^{\prime}_{j}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{j}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Notice that then there exists $y{:}\mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\in}\Gamma$ such that \mbox{\kern 0.275pt\typefont{\typecol T}\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon.

Then, by induction, there are $\Gamma_{j}$, $\Delta_{j}$, and B such that ${\colourfortype\Gamma_{j}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol P_{j}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta_{j}}}\hskip 1.1pt$. Then

• {\colourfortype\Gamma\mathop{{\colourfortype\mbox{{\cap}}}}\Gamma_{j}\mathop{{\colourfortype\mbox{{\cap}}}}\{\,y{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{1}\mathord{\mbox{\typecol\typefont\times}}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mbox{\kern 0.275pt\typefont B\kern 0.825pt}\hskip 0.43999pt{\cdots}\hskip 0.43999pt\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}_{n}\mathord{\mbox{\typecol\typefont\times}}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon\,\}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol yP_{1}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{j}\hskip 0.43999pt{\cdots}\hskip 0.43999ptP_{n}:\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype\Delta_{j}}\mathop{{\colourfortype\mbox{{\cap}}}}\Delta.**

$M\mathrel{\equiv}\lambda y.M^{\prime}$

If $M\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N$, then $N=\lambda y.N^{\prime}$ and $M^{\prime}\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N^{\prime}$. Then there exists $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt},\mbox{\contfont{\typecol D}}$ such that {\colourfortype\Gamma,y{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt and \mbox{\kern 0.275pt\contfont C\kern 0.825pt}=\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}. By induction, there exists $\Gamma^{\prime}$, $\Delta^{\prime}$, $\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}^{\prime}$, and $\mbox{\contfont{\typecol D}}^{\prime}$ such that {\colourfortype\Gamma^{\prime},y{:}\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt. Then, by rule $(\textit{Abs})$, {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\lambda y.M^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont{\typecol S}\kern 0.825pt}^{\prime}\mathord{\mbox{\typecol\typefont\times}}\mbox{\contfont{\typecol D}}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt.

$M\mathrel{\equiv}\mu\alpha.[\alpha]P$

Then $N=\mu\alpha.[\alpha]Q$ and $P\mathrel{\rightarrow_{\textit{\scriptsize lor}}}Q$. Since {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\alpha]Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, there exists \typecolD such that $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\Delta_{0}}}\hskip 1.1pt. Then by induction there exist $\Gamma^{\prime}$, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, $\mbox{\contfont{\typecol D}}^{\prime}$, and $\Delta^{\prime}$ such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. By Lem. 5.4 {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}}}\hskip 1.1pt\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\contfont{\typecol D}}^{\prime},\Delta^{\prime} and then by rule $(\mu)$ we get {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt.

$M\mathrel{\equiv}\mu\alpha.[\beta]M^{\prime}$** with $\alpha\not=\beta$**

Then $N=\mu\alpha.[\beta]N^{\prime}$ and $M^{\prime}\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N^{\prime}$. Since {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]N^{\prime}}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt, there are $\Delta_{0}$, \typecolE, \typecolD such that $\Delta=\beta{:}\mbox{\contfont{\typecol E}},\Delta^{\prime}_{0}$, $\mbox{\contfont{\typecol E}}\mathbin{\leq_{\hbox{{\sc s}}}}\mbox{\contfont{\typecol D}}$, and {\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol N^{\prime}}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt},\beta{:}\mbox{\contfont{\typecol E}},\Delta_{0}}}\hskip 1.1pt. Then by induction there exist $\Gamma^{\prime}$, $\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}$, $\mbox{\contfont{\typecol E}}^{\prime}$, $\mbox{\contfont{\typecol D}}^{\prime}$, and $\Delta^{\prime}$ such that {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\contfont{\typecol D}}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\contfont{\typecol E}}^{\prime},\Delta^{\prime}}}\hskip 1.1pt. Then by Lem. 5.4 we have {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\alpha{:}\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime},\beta{:}\mbox{\contfont{\typecol E}}^{\prime}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\contfont{\typecol D}}^{\prime},\Delta^{\prime}}}\hskip 1.1pt and {\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol\mu\alpha.[\beta]Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\contfont C\kern 0.825pt}^{\prime}\mbox{\typecol\typefont\mathbin{\rightarrow}}\upsilon}\mathbin{\mid}{\colourfortype{\beta{:}\mbox{\contfont{\typecol E}}^{\prime}\mathop{{\colourfortype\mbox{{\cap}}}}\mbox{\contfont{\typecol D}}^{\prime},\Delta^{\prime}}}\hskip 1.1pt follows by rule $(\mu^{\prime})$. ∎

We can now show that all strongly normalisable terms are exactly those typeable in $\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}$.

Theorem 5.14**.**

\raise-0.25pt\hbox{\exists}\hskip 1.1pt\Gamma, $\Delta$, $\mbox{\kern 0.275pt\typefont A\kern 0.825pt}~{}[\hskip 1.1pt{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt\hskip 1.1pt]\mathrel{\hskip 1.0pt{\Leftarrow}\kern-6.60004pt{\Rightarrow}\hskip 1.0pt}M$ is strongly normalisable with respect to \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}.

• *Proof: *

$\mathrel{\Rightarrow}$

If ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$, then by Lem. 5.2(5), also ${\orangecol\hskip 1.1pt\mathcal{D}}\mathrel{::}{\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{{\sc s}}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. Then, by Thm. 2.4(4), ${\orangecol\hskip 1.1pt\mathcal{D}}$ is strongly normalisable with respect to \mathrel{\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\mbox{\scriptsize\sc Der}}}. Since ${\orangecol\hskip 1.1pt\mathcal{D}}$ contains no $\omega$, all redexes in $M$ correspond to redexes in ${\orangecol\hskip 1.1pt\mathcal{D}}$, a property that is preserved by derivation reduction (it does not introduce $\omega$). So also $M$ is strongly normalisable with respect to \mathbin{\semcolour\mbox{\typecol\typefont\mathbin{\rightarrow}}_{\beta\mu}}.

$\mathrel{\Leftarrow}$

By induction on the maximum of the lengths of reduction sequences for a strongly normalisable term $M$ to its normal form (denoted by $\#\,{M}$).

1. 1.

If $\#\,{M}=0$, then $M$ is in normal form, and by Lem. 5.6(2), there exist $\Gamma$, $\Delta$ and A such that ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$. 2. 2.

If $\#\,{M}\mathop{\geq}1$, so $M$ contains a redex, then let $M\mathrel{\rightarrow_{\textit{\scriptsize lor}}}N$ by contracting the redex $PQ$. Then $\#\,{N}<\#\,{M}$, and $\#\,{Q}<\#\,{M}$ (since $Q$ is a proper sub-term of a redex in $M$), so by induction, for some $\Gamma$, $\Gamma^{\prime}$, $\Delta$, $\Delta^{\prime}$, A, and B, we have ${\colourfortype\Gamma}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont A\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta}}\hskip 1.1pt$ and ${\colourfortype\Gamma^{\prime}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol Q}\mathbin{:}{\colourfortype\mbox{\kern 0.275pt\typefont B\kern 0.825pt}}\mathbin{\mid}{\colourfortype{\Delta^{\prime}}}\hskip 1.1pt$. Then, by Lem. 5.12, there exist $\Gamma_{1}$, $\Delta_{1}$, \typecol$C$ such that {\colourfortype\Gamma_{1}}\mathbin{{\vdash}\kern-2.20001pt_{\hbox{\scriptsize\sc sn}}}{\ltermcol M}\mathbin{:}{\colourfortype\mbox{\typecol\typefontC}}\mathbin{\mid}{\colourfortype{\Delta_{1}}}\hskip 1.1pt. If the redex is $\mu\alpha.[\beta]\mu\gamma.[\delta]P$, then $\#\,{\mu\alpha.[\beta]\mu\gamma.[\delta]P}>\#\,{\mu\alpha.([\delta]P)[\beta/\gamma]}$, so the result follows by induction. ∎

Conclusions

We have studied a strict version of the intersection type system for ${\semcolour\lambda\mu}$ of [11]. Using the fact that derivation reduction (a kind of cut-elimination) is strongly normalisable, we have shown an approximation theorem, and from that given a characterisation of head normalisation. We have also shown that the system without the type constant $\omega$ characterises the strongly normalisable terms and that we can characterise normalisation as well.