Call-by-Value, Elementary Time and Intersection Types

Abstract

We present a type assignment system for the call-by-value $\lambda$-calculus, such that typable terms reduce to normal form in a number of steps which is elementary in the size of the term itself and in the rank of the type derivation. Types are built through non-idempotent and non-associative intersection, and the system is loosely inspired by elementary affine logic. The result is due to the fact that the lack of associativity in intersection supplies a notion of stratification of the reduction, which recalls the similar notion of stratification in light logics.

A Appendix

Proof of Lemma 3 (Substitution Lemma). The proof of Substitution Lemma uses the following lemma, which is a corollary of Lemma 2.

Lemma 5

• i. Let $\varPi {\,\triangleright \,}\varGamma \mid \varDelta \vdash \mathtt{M}: \sigma$, where $\mathtt{M}\in \mathtt{V}$ and $\sigma$ is a multiset type; then, for every $\sigma _{1},\ldots , \sigma _{n}$ such that $\sigma \cong \sqcup _{i=1}^{n} \sigma _{i}$, there are $\varPi _{i} {\,\triangleright \,}\varGamma _{i} \mid \varDelta _{i} \vdash \mathtt{M}: \sigma _{i}$, for $1 \le i \le n$, such that $\varGamma = \sqcup _{i=1}^{n} \varGamma _{i}$ and $\varDelta = \sqcup _{i=1}^{n} \varDelta _{i}$; moreover, $\mathtt{W}(\varPi ,j) = \sum _{i=1}^{n} \frac{|\sigma _{i}|}{ |\sigma | } \cdot \mathtt{W}(\varPi _{i},j)$ and $\mathtt{R}(\varPi , j) = \sum _{i=1}^{n} \mathtt{R}(\varPi _{i}, j)$ for every $j \ge 0$.

• ii. Let $\varPi {\,\triangleright \,}\varGamma \mid \varDelta \vdash \mathtt{M}: \sigma$, where $\mathtt{M}\in \mathtt{V}$ and $\sigma$ is a multiset type; then, for every $\sigma _{1},\ldots , \sigma _{n}$ such that $\sigma \cong [ \sigma _{1},\ldots , \sigma _{n} ]$, there are $\varPi _{i} {\,\triangleright \,}\varGamma _{i} \mid \varDelta _{i} \vdash \mathtt{M}: \sigma _{i}$, for $1 \le i \le n$, such that $\varDelta = \sqcup _{i=1}^{n} \varGamma _{i} \sqcup _{i=1}^{n} [ \varDelta _{i} ]$, $\mathtt{W}(\varPi ,j) = \sum _{i=1}^{n} \frac{|\sigma _{i}|}{ |\sigma | } \cdot \mathtt{W}(\varPi _{i},j-1)$ and $\mathtt{R}(\varPi , j) = \sum _{i=1}^{n}\mathtt{R}(\varPi _{i}, j-1)$ for every $j > 0$.

Proof

The proof of point i can be given by induction on $\sigma$, that of point ii by induction on $\varPi$, using Lemma 2.

Now we are able to show the proof of Substitution Lemma. Both points follow by induction on $\varPi$.

• i.  

  • Let $\varPi$ be

    

    where $n=1$, $\mathtt{M}[ \mathtt{N}/ \mathtt{x}] = \mathtt{N}$ and $\sigma = \mathtt{A}_{1}$; then $\mathcal {S}^{\varSigma _{1}}_{\varPi }$ is $\varSigma _{1} {\,\triangleright \,}\varGamma _{1} \mid \varDelta _{1} \vdash \mathtt{N}: \mathtt{A}_{1}$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1}}_{\varPi },j) = \mathtt{W}(\varSigma _{1},j) \le \mathtt{W}(\varPi ,j) + \mathtt{W}(\varSigma _{1},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1}}_{\varPi }, j) = \mathtt{R}(\varSigma _{1}, j) \le \mathtt{R}(\varPi , j) + \mathtt{R}(\varSigma _{1}, j)$ for every $j \ge 0$.

  • Let $\varPi$ end with an application of rule (w). If $\varPi$ is

    

    then the proof follows by induction. Otherwise, let $\varPi$ be

    

    for some k such that $0 \le k < n$. By inductive hypothesis $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi '} {\,\triangleright \,} \varGamma ' \sqcup _{i=1}^{k} \varGamma _{i} \mid \varDelta ' \sqcup _{i=1}^{k} \varDelta _{i} \vdash \mathtt{M}[\mathtt{N}/ \mathtt{x}]: \sigma$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi '},j) \le \mathtt{W}(\varPi ',j) + \sum _{i = 1}^{k} \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi '}, j) \le \mathtt{R}(\varPi , j) + \sum _{i=1}^{k} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$. Then $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi } {\,\triangleright \,}\varGamma \sqcup _{i=1}^{n} \varGamma _{i} \mid \varDelta \sqcup _{i=1}^{n} \varDelta _{i} \vdash \mathtt{M}[\mathtt{N}/ \mathtt{x}]: \sigma$ is obtained from $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi '}$ by applying rule (w), where $\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi },j) \le \mathtt{W}(\varPi ',j) + \sum _{i = 1}^{k} \mathtt{W}(\varSigma _{i},j) \le \mathtt{W}(\varPi ,j) + \sum _{i = 1}^{n} \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi }, j) = \mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \sum _{i=1}^{k} \mathtt{R}(\varSigma _{i}, j) \le \mathtt{R}(\varPi , j) + \sum _{i=1}^{n} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$.

  • Let $\varPi$ be

    

    where $\mathtt{M}= \lambda \mathtt{y}. \mathtt{P}$ and $\sigma = \mathtt{A}\rightarrow \mu$. By the $\alpha$-rule we may assume that $\mathtt{y}\not \in \mathtt{FV}(\mathtt{N})$. By inductive hypothesis $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi '} {\,\triangleright \,}\varGamma \sqcup _{i=1}^{n} \varGamma _{i}, \mathtt{y}: [ \mathtt{A}] \mid \varDelta \sqcup _{i=1}^{n} \varDelta _{i} \vdash \mathtt{P}[\mathtt{N}/ \mathtt{x}]: \mu$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi '},j) \le \mathtt{W}(\varPi ',j) + \sum _{i = 1}^{n} \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \sum _{i=1}^{n} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$.

    Then $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi } {\,\triangleright \,}\varGamma \sqcup _{i=1}^{n} \varGamma _{i} \mid \varDelta \sqcup _{i=1}^{n} \varDelta _{i} \vdash (\lambda \mathtt{y}. \mathtt{P})[\mathtt{N}/ \mathtt{x}]: \mathtt{A}\rightarrow \mu$ is obtained from $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi '}$ by applying rule $(\rightarrow I_{L})$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi },j) \le \mathtt{W}(\varPi ,j) + \sum _{i = 1}^{n} \mathtt{W}(\varSigma _{i},j)$ by the definition of weight and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi }, j) = \mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi '}, j) \le \mathtt{R}(\varPi , j) + \sum _{i=1}^{n} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$.

    The case of $(\rightarrow I_{M})$ is similar.

  • Let $\varPi$ end with an application of rule $(\rightarrow E)$ with premises $\varPi _{1} {\,\triangleright \,}\varGamma ', \mathtt{x}: [ \mathtt{A}_{1},\ldots , \mathtt{A}_{k} ] \mid \varDelta ' \vdash \mathtt{P}: \rho \rightarrow \sigma$ and $\varPi _{2} {\,\triangleright \,}\varGamma '', \mathtt{x}: [ \mathtt{A}_{k+1},\ldots , \mathtt{A}_{n} ] \mid \varDelta '' \vdash \mathtt{Q}: \rho$, such that $\mathtt{M}= \mathtt{P}\mathtt{Q}$. By inductive hypothesis on $\varPi _{1}$, there is a derivation ${ \mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi _{1}} {\,\triangleright \,}\varGamma ' \sqcup _{i=1}^{k} \varGamma _{i} \mid \varDelta ' \sqcup _{i=1}^{k} \varDelta _{i} \vdash \mathtt{P}[\mathtt{N}/ \mathtt{x}]: \rho \rightarrow \sigma }$, where ${\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi _{1}},j) \le \mathtt{W}(\varPi _{1},j) + \sum _{i = 1}^{k} \mathtt{W}(\varSigma _{i},j)}$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi _{1}}, j) \le \mathtt{R}(\varPi _{1}, j) + \sum _{i=1}^{k} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$. By inductive hypothesis on $\varPi _{2}$, there is a derivation $\mathcal {S}^{\varSigma _{k+1},\ldots , \varSigma _{n}}_{\varPi _{2}} {\,\triangleright \,}\varGamma '' \sqcup _{i=k+1}^{n} \varGamma _{i} \mid \varDelta '' \sqcup _{i=k+1}^{n} \varDelta _{i} \vdash \mathtt{Q}[\mathtt{N}/ \mathtt{x}]: \rho$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{k+1},\ldots , \varSigma _{n}}_{\varPi _{2}},j) \le \mathtt{W}(\varPi _{2},j) + \sum _{i = k+1}^{n} \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{k+1},\ldots , \varSigma _{n}}_{\varPi _{2}}, j) \le \mathtt{R}(\varPi _{2}, j) + \sum _{i=k+1}^{n} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$. Then $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi } {\,\triangleright \,}\varGamma ' \sqcup \varGamma '' \sqcup _{i=1}^{n} \varGamma _{i} \mid \varDelta ' \sqcup \varDelta '' \sqcup _{i=1}^{n} \varDelta _{i} \vdash (\mathtt{P}\mathtt{Q})[\mathtt{N}/ \mathtt{x}]: \sigma$ is obtained by applying rule $(\rightarrow E)$ to the premises $\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{k}}_{\varPi _{1}}$ and $\mathcal {S}^{\varSigma _{k+1},\ldots , \varSigma _{n}}_{\varPi _{2}}$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi },j) \le \mathtt{W}(\varPi ,j) + \sum _{i = 1}^{n} \mathtt{W}(\varSigma _{i},j)$ follows by the definition of weight and $\mathtt{R}(\mathcal {S}^{\varSigma _{1},\ldots , \varSigma _{n}}_{\varPi }, j) \le \mathtt{R}(\varPi _{1}, j) + \sum _{i=1}^{k} \mathtt{R}(\varSigma _{i}, j) + \mathtt{R}(\varPi _{2}, j) + \sum _{i=k+1}^{n} \mathtt{R}(\varSigma _{i}, j) \le \mathtt{R}(\varPi , j) + \sum _{i=1}^{n} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$.

  • The case of (m) is not possible.

• ii.  

  • The case of (Ax) is not possible.

  • Let $\varPi$ end with an application of rule (w). If $\varPi$ is

    

    then the proof follows by induction. Otherwise, let $\varPi$ be

    

    where $\tau \cong \tau _{1} \sqcup \tau _{2}$. Note that $|\tau |=|\tau _{1}| + |\tau _{2}|$. By Lemma 5.i there are $\varSigma _{1} {\,\triangleright \,}\varGamma _{1} \mid \varDelta _{1} \vdash \mathtt{N}: \tau _{1}$ and $\varSigma _{2} {\,\triangleright \,}\varGamma _{2} \mid \varDelta _{2} \vdash \mathtt{N}: \tau _{2}$ such that $\varGamma ' = \varGamma _{1} \sqcup \varGamma _{2}$ and $\varDelta ' = \varDelta _{1} \sqcup \varDelta _{2}$; moreover, $\mathtt{W}(\varSigma ,j) = \sum _{i=1}^{2} \frac{|\tau _{i}|}{ |\tau | } \cdot \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\varSigma , j) = \sum _{i=1}^{2} \mathtt{R}(\varSigma _{i}, j)$ for every $j \ge 0$. By inductive hypothesis ${ \mathcal {S}^{\varSigma _{1}}_{\varPi '} {\,\triangleright \,}\varGamma _{1} \sqcup \varGamma \mid \varDelta _{1} \sqcup \varDelta \vdash \mathtt{M}[\mathtt{N}/ \mathtt{x}]: \sigma }$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1}}_{\varPi '},j) \le \mathtt{W}(\varPi ',j) + |\tau _{1}| \cdot \mathtt{W}(\varSigma _{1},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1}}_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \mathtt{R}(\varSigma _{1}, j)$ for every $j \ge 0$.

    Then $\mathcal {S}^{\varSigma }_{\varPi } {\,\triangleright \,}\varGamma \sqcup \varGamma ' \mid \varDelta \sqcup \varDelta ' \vdash \mathtt{M}[\mathtt{N}/ \mathtt{x}]: \sigma$ is obtained from $\mathcal {S}^{\varSigma _{1}}_{\varPi '}$ by applying rule (w), where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },j) = \mathtt{W}(\mathcal {S}^{\varSigma _{1}}_{\varPi '},j) = \mathtt{W}(\varPi ',j) + |\tau _{1}| \cdot \mathtt{W}(\varSigma _{1},j) \le \mathtt{W}(\varPi ,j) + |\tau | \cdot \mathtt{W}(\varSigma ,j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, j) = \mathtt{R}(\mathcal {S}^{\varSigma _{1}}_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \mathtt{R}(\varSigma _{1}, j) \le \mathtt{R}(\varPi , j) + \mathtt{R}(\varSigma , j)$ for every $j \ge 0$.

  • Let $\varPi$ be

    

    where $\mathtt{M}= \lambda \mathtt{y}. \mathtt{P}$.

    By the $\alpha$-rule we may assume that $\mathtt{y}\not \in \mathtt{FV}(\mathtt{N})$. By inductive hypothesis ${ \mathcal {S}^{\varSigma }_{\varPi '} {\,\triangleright \,}\varGamma \sqcup \varGamma ', \mathtt{y}: [ \mathtt{A}] \mid \varDelta \sqcup \varDelta ' \vdash \mathtt{P}[\mathtt{N}/ \mathtt{x}]: \mu }$, where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi '},j) \le \mathtt{W}(\varPi ',j) + |\tau | \cdot \mathtt{W}(\varSigma ,j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \mathtt{R}(\varSigma , j)$ for every $j \ge 0$. Then $\mathcal {S}^{\varSigma }_{\varPi } {\,\triangleright \,}\varGamma \sqcup \varGamma ' \mid \varDelta \sqcup \varDelta ' \vdash (\lambda \mathtt{y}. \mathtt{P})[\mathtt{N}/ \mathtt{x}]: \mathtt{A}\rightarrow \mu$ is obtained from $\mathcal {S}^{\varSigma }_{\varPi '}$ by applying rule $(\rightarrow I)$, where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },j) \le \mathtt{W}(\varPi ,j) + | \tau | \cdot \mathtt{W}(\varSigma ,j)$ follows by the definition of weight and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, j) = \mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi '}, j) \le \mathtt{R}(\varPi ', j) + \mathtt{R}(\varSigma , j) = \mathtt{R}(\varPi , j) + \mathtt{R}(\varSigma , j)$ for every $j \ge 0$.

    The case of $(\rightarrow I_{M})$ is similar.

  • Let $\varPi$ end with an application of rule $(\rightarrow E)$ with premises $\varPi _{1} {\,\triangleright \,}\varGamma _{1} \mid \varDelta _{1}, \mathtt{x}: \tau _{1} \vdash \mathtt{P}: \rho \rightarrow \sigma$ and $\varPi _{2} {\,\triangleright \,}\varGamma _{2} \mid \varDelta _{2}, \mathtt{x}: \tau _{2} \vdash \mathtt{Q}: \rho$, where $\tau \cong \tau _{1} \sqcup \tau _{2}$ and $\mathtt{M}= \mathtt{P}\mathtt{Q}$. Note that $|\tau |=|\tau _{1}| + |\tau _{2}|$. By Lemma 5.i, $\varSigma {\,\triangleright \,}\varGamma ' \mid \varDelta ' \vdash \mathtt{N}: \tau$ implies there are $\varSigma _{1} {\,\triangleright \,}\varGamma '_{1} \mid \varDelta '_{1} \vdash \mathtt{N}: \tau _{1}$ and $\varSigma _{2} {\,\triangleright \,}\varGamma '_{2} \mid \varDelta '_{2} \vdash \mathtt{N}: \tau _{2}$ such that $\varGamma ' = \varGamma '_{1} \sqcup \varGamma '_{2}$ and $\varDelta ' = \varDelta '_{1} \sqcup \varDelta '_{2}$; moreover, $\mathtt{W}(\varSigma ,j) = \sum _{i=1}^{2} \frac{|\tau _{i}|}{ |\tau | } \cdot \mathtt{W}(\varSigma _{i},j)$ and $\mathtt{R}(\varSigma , j) = \sum _{i=1}^{2} \mathtt{W}(\varSigma _{i},j)$ for every $j \ge 0$. By inductive hypothesis on $\varPi _{1}$, there is a derivation ${ \mathcal {S}^{\varSigma _{1}}_{\varPi _{1}} {\,\triangleright \,}\varGamma _{1} \sqcup \varGamma '_{1} \mid \varDelta _{1} \sqcup \varDelta '_{1} \vdash \mathtt{P}[\mathtt{N}/ \mathtt{x}]: \rho \rightarrow \sigma }$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{1}}_{\varPi _{1}},j) \le \mathtt{W}(\varPi _{1},j) + |\tau _{1}| \cdot \mathtt{W}(\varSigma _{1},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{1}}_{\varPi _{1}}, j) \le \mathtt{R}(\varPi _{1}, j) + \mathtt{R}(\varSigma _{1}, j)$ for every $j \ge 0$. Similarly, by inductive hypothesis on $\varPi _{2}$ there is $\mathcal {S}^{\varSigma _{2}}_{\varPi _{2}} {\,\triangleright \,}\varGamma _{2} \sqcup \varGamma '_{2} \mid \varDelta _{2} \sqcup \varDelta '_{2} \vdash \mathtt{Q}[\mathtt{N}/ \mathtt{x}]: \rho$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{2}}_{\varPi _{2}},j) \le \mathtt{W}(\varPi _{2},j) + |\tau _{2}| \cdot \mathtt{W}(\varSigma _{2},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{2}}_{\varPi _{2}}, j) \le \mathtt{R}(\varPi _{2}, j) + \mathtt{R}(\varSigma _{2}, j)$ for every $j \ge 0$.

    Then $\mathcal {S}^{\varSigma }_{\varPi } {\,\triangleright \,}\varGamma _{1} \sqcup \varGamma _{2} \sqcup \varGamma ' \mid \varDelta _{1} \sqcup \varDelta _{2} \sqcup \varDelta ' \vdash (\mathtt{P}\mathtt{Q})[\mathtt{N}/ \mathtt{x}]: \sigma$ is obtained by applying rule $(\rightarrow E)$ to $\mathcal {S}^{\varSigma _{1}}_{\varPi _{1}}$ and $\mathcal {S}^{\varSigma _{2}}_{\varPi _{2}}$, where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },j) \le \mathtt{W}(\varPi ,j) + |\tau _{1}| \cdot \mathtt{W}(\varSigma _{1},j) + |\tau _{2}| \cdot \mathtt{W}(\varSigma _{2},j) = \mathtt{W}(\varPi ,j) + |\tau | \cdot \mathtt{W}(\varSigma ,j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, j) = \mathtt{R}(\mathcal {S}^{\varSigma _{1}}_{\varPi _{1}}, j) + \mathtt{R}(\mathcal {S}^{\varSigma _{2}}_{\varPi _{2}}, j) \le \mathtt{R}(\varPi _{1}, j) + \mathtt{R}(\varSigma _{1}, j) + \mathtt{R}(\varPi _{2}, j) + \mathtt{R}(\varSigma _{2}, j) = \mathtt{R}(\varPi , j) + \mathtt{R}(\varSigma , j)$ for every $j \ge 0$.

  • Let $\varPi$ end with an application of rule (m): there are two possible cases.

    • Let $\varPi$ be

      

      where $\tau \cong [ \mathtt{A}^{1}_{1},\ldots ,\mathtt{A}^{h_{1}}_{1},\ldots , \mathtt{A}^{1}_{p},\ldots , \mathtt{A}^{h_{p}}_{p}]$ and $\varDelta = \sqcup _{s=1}^{p} \varGamma _{s}, \sqcup _{s=1}^{p} [ \varDelta _{s} ]$. By hypothesis there is $\varSigma {\,\triangleright \,}\varGamma ' \mid \varDelta ' \vdash \mathtt{N}: \tau$. By Lemma 5.ii, there are $\varSigma _{s}^{r} {\,\triangleright \,}\varGamma _{s}^{r} \mid \varDelta _{s}^{r} \vdash \mathtt{N}: \mathtt{A}_{s}^{r}$ ($1\le s \le p, 1\le r \le h_{s}$) such that $\varDelta ' = \sqcup _{s=1}^{p} ,_{r=1}^{h_{s}} \varGamma _{s}^{r}, \sqcup _{s=1}^{p} ,_{r=1}^{h_{s}} [ \varDelta _{s}^{r} ]$; moreover $\mathtt{W}(\varSigma ,0) = \mathtt{R}(\varSigma , 0) = 0$, $\mathtt{W}(\varSigma ,j+1) = \sum _{s=1}^{p} ,_{r=1}^{h_{s}} \frac{1}{|\tau |} \cdot \mathtt{W}(\varSigma _{s}^{r},j)$ and ${ \mathtt{R}(\varSigma , j+1) = \sum _{s=1}^{p} ,_{r=1}^{h_{s}} \mathtt{R}(\varSigma _{s}^{r}, j) }$ for every $j \ge 0$. By Lemma 3.i, there are derivations $\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}} {\,\triangleright \,}\varGamma _{s} \sqcup _{r=1}^{h_{s}} \varGamma _{s}^{r} \mid \varDelta _{s} \sqcup _{r=1}^{h_{s}} \varDelta _{s}^{r} \vdash \mathtt{M}[ \mathtt{N}/ \mathtt{x}]: \sigma _{s}$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}},j) \le \mathtt{W}(\varPi _{s},j) + \sum _{r = 1}^{h_{s}} \mathtt{W}(\varSigma _{s}^{r},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}}, j) \le \mathtt{R}(\varPi _{s}, j) + \sum _{r=1}^{h_{s}} \mathtt{R}(\varSigma _{s}^{r}, j)$ for every $j \ge 0$ and $1 \le s \le p$. Then $\mathcal {S}^{\varSigma }_{\varPi } {\,\triangleright \,}\varGamma ' \mid \varDelta \sqcup \varDelta ' \vdash \mathtt{M}[ \mathtt{N}/ \mathtt{x}]: [ \sigma _{1},\ldots , \sigma _{n} ]$ is obtained by applying rule (m) to $\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}}$, for $1 \le s \le p$, followed by a (possibly empty) sequence of rule (w) adding $\varGamma '$, where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },0) = \mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, 0) = 0$, $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },j+1) = \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot \mathtt{W}(\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}},j) \le \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot ( \mathtt{W}(\varPi _{s},j) + \sum _{r = 1}^{h_{s}} \mathtt{W}(\varSigma _{s}^{r},j) ) = \mathtt{W}(\varPi ,j+1) + \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot \sum _{r = 1}^{h_{s}} \mathtt{W}(\varSigma _{s}^{r},j) \le \mathtt{W}(\varPi ,j+1) + \sum _{s=1}^{p} ,_{r = 1}^{h_{s}} \mathtt{W}(\varSigma _{s}^{r},j) \le \mathtt{W}(\varPi ,j+1) + | \tau | \cdot \mathtt{W}(\varSigma ,j+1)$ and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, j+1) = \sum _{s=1}^{p} \mathtt{R}(\mathcal {S}^{\varSigma _{s}^{1},\ldots , \varSigma _{s}^{h_{s}}}_{\varPi _{s}}, j) \le \sum _{s=1}^{p} \mathtt{R}(\varPi _{s}, j) + \sum _{s=1}^{p} ,_{r=1}^{h_{s}} \mathtt{R}(\varSigma _{s}^{r}, j) = \mathtt{R}(\varPi , j+1) + \mathtt{R}(\varSigma , j+1)$ for every $j \ge 0$.

    • Let $\varPi$ be

      

      where $\varDelta = \sqcup _{s=1}^{p} \varGamma _{s}, \sqcup _{s=1}^{p} [ \varDelta _{s} ]$ and $\tau \cong [ \tau _{1},\ldots , \tau _{s} ]$.

      By hypothesis there is $\varSigma {\,\triangleright \,}\varGamma ' \mid \varDelta ' \vdash \mathtt{N}: \tau$. By Lemma 5.ii, there are $\varSigma _{s} {\,\triangleright \,}\varGamma '_{s} \mid \varDelta '_{s} \vdash \mathtt{N}: \tau _{s}$ ($1\le s \le p$) such that $\varDelta ' = \sqcup _{s=1}^{p} \varGamma '_{s}, \sqcup _{s=1}^{p} [ \varDelta '_{s} ]$; moreover $\mathtt{W}(\varSigma ,0) = \mathtt{R}(\varSigma , 0) = 0$, $\mathtt{W}(\varSigma ,j+1) = \sum _{s=1}^{p} \frac{|\tau _{s}|}{|\tau |} \cdot \mathtt{W}(\varSigma _{s},j)$ and ${ \mathtt{R}(\varSigma , j+1) = \sum _{s=1}^{p} \mathtt{R}(\varSigma _{s}, j) }$ for every $j \ge 0$.

      By inductive hypothesis, there are $\mathcal {S}^{\varSigma _{s}}_{\varPi _{s}} {\,\triangleright \,}\varGamma _{s} \sqcup \varGamma '_{s} \mid \varDelta _{s} \sqcup \varDelta '_{s} \vdash \mathtt{M}[ \mathtt{N}/ \mathtt{x}]: \sigma _{s}$, where $\mathtt{W}(\mathcal {S}^{\varSigma _{s}}_{\varPi _{s}},j) \le \mathtt{W}(\varPi _{s},j) + |\tau _{s}| \cdot \mathtt{W}(\varSigma _{s}^{r},j)$ and $\mathtt{R}(\mathcal {S}^{\varSigma _{s}}_{\varPi _{s}}, j) \le \mathtt{R}(\varPi _{s}, j) + \mathtt{R}(\varSigma _{s}, j)$ for every $j \ge 0$ and $1 \le s \le p$.

      Then $\mathcal {S}^{\varSigma }_{\varPi } {\,\triangleright \,}\varGamma ' \mid \varDelta \sqcup \varDelta ' \vdash \mathtt{M}[ \mathtt{N}/ \mathtt{x}]: [ \sigma _{1},\ldots , \sigma _{n} ]$ is obtained by applying rule (m) to $\mathcal {S}^{\varSigma _{1}}_{\varPi _{1}},\ldots , \mathcal {S}^{\varSigma _{p}}_{\varPi _{p}}$, followed by a (possibly empty) sequence of applications of rule (w) adding $\varGamma '$, where $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },0) = \mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, 0) = 0$, $\mathtt{W}(\mathcal {S}^{\varSigma }_{\varPi },j+1) = \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot \mathtt{W}(\mathcal {S}^{\varSigma _{s}}_{\varPi _{s}},j) \le \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot ( \mathtt{W}(\varPi _{s},j) + |\tau _{s}| \cdot \mathtt{W}(\varSigma _{s},j) ) = \mathtt{W}(\varPi ,j+1) + \sum _{s=1}^{p} \frac{|\sigma _{s}|}{|\sigma |} \cdot |\tau _{s}| \cdot \mathtt{W}(\varSigma _{s},j) \le \mathtt{W}(\varPi ,j+1) + \sum _{s=1}^{p} |\tau _{s}| \cdot \mathtt{W}(\varSigma _{s},j) = \mathtt{W}(\varPi ,j+1) + | \tau | \cdot \mathtt{W}(\varSigma ,j+1)$ by Lemma 5.ii, and $\mathtt{R}(\mathcal {S}^{\varSigma }_{\varPi }, j+1) = \sum _{s=1}^{p} \mathtt{R}(\mathcal {S}^{\varSigma _{s}}_{\varPi _{s}}, j) \le \sum _{s=1}^{p} \mathtt{R}(\varPi _{s}, j) + \sum _{s=1}^{p} \mathtt{R}(\varSigma _{s}, j) = \mathtt{R}(\varPi , j+1) + \mathtt{R}(\varSigma , j+1)$ for every $j \ge 0$.