\documentclass[draft]{article} \input linear \input theorem \input prooftree \title{Proof Irrelevance with Hereditary Substitution} \author{Jason Reed} \def\rtype{\mathop{\mathrm{type}}} \def\rkind{\mathop{\mathrm{kind}}} \def\rctx{\mathop{\mathrm{ctx}}} \def\rsgn{\mathop{\mathrm{sgn}}} \def\tcheck{\mathrel{\Leftarrow}} \def\tsynth{\mathrel{\Rightarrow}} \def\bullet{o} \def\imp{\supset} \def\D{\mathcal D} \def\lstar{} %\def\lstar{^\star} \begin{document} \maketitle \section{Language} \begin{tabular}{lrcl} Relevance&$\star,\ast$&$::=$&${:} \celse {\div}$\\ Normal Terms&$M, N$&$::=$&$\lambda x\lstar. M \celse R$\\ Atomic Terms&$R$&$::=$&$H \cdot S $ \\ Heads&$H$&$::=$&$x \celse c$\\ Spines&$S$&$::=$&$() \celse (M^\star ; S)$\\ Types&$A, B$&$::=$&$a\cdot S \celse \Pi x \star A . B$\\ Kinds&$K, L$&$::=$&$\rtype \celse \Pi x \star A . K$\\ Classifiers&$V, W$&$::=$&$A \celse K$\\ Contexts&$\Gamma$&$::=$&$\cdot \celse \Gamma, x \star A$\\ Signatures&$\Sigma$&$::=$&$\cdot \celse \Sigma, c : A \celse \Sigma, a : K$\\ Simple Types&$\tau$&$::=$&$\bullet \celse \tau_1 \to \tau_2$\\ %TOSTAR Type Skeletons&$\tau$&$::=$&$\bullet \celse \tau_1 \to^\star \tau_2$\\ \end{tabular} \section{Syntactic Operations} \subsection{Simplification} $$(a\cdot S)^- = \bullet$$ $$(\Pi x\star A . B)^- = (A)^- \to (B)^-$$ %TOSTAR $$(\Pi x\star A . B)^- = (A)^- \to^\star (B)^-$$ \subsection{Substitution and Reduction} Definitions adapted from [CLF paper {\em XXX cite}]. Substitution is a partial function $[M/x]^\tau N$ on two terms and a simple type; it is the substitution of the term $M$ for the variable $x$ at simple type $\tau$ in the term $N$, which may be undefined. The definition of substitution is mutually recursive with that of {\em reduction} $[M|S]^\tau$, which operates on a term $M$ and list of arguments (a `spine') $S$ at simple type $\tau$, and produces the term that is the result of applying the head $M$ (presumed to be of simple type $\tau$) to arguments $S$. The important case of the definition of substitution is when we reach the variable, and invoke reduction (see below). $$[M/x]^\tau (x \cdot S) = [M| [M/x]^\tau S]^\tau$$ The remainder of the definition consists of simple congruences. Let $\sigma$ abbreviate $[M/x]^\tau$. $$\begin{tabular}{r@{$\ =\ $}l} $\sigma (\lambda y\lstar . N) $&$ \lambda y\lstar . \sigma N $\\ $\sigma (y \cdot S) $&$ y \cdot (\sigma S)\qquad (y\ne x)$\\ $\sigma (c \cdot S) $&$ c \cdot( \sigma S )$\\ %$\sigma \bot $&$ \bot$\\ $\sigma () $&$ ()$\\ $\sigma (N^\star ; S) $&$ ((\sigma N)^\star; \sigma S)$\\ $\sigma (a \cdot S) $&$ a \cdot( \sigma S )$\\ $\sigma (\Pi y \star A . B) $&$ \Pi y \star (\sigma A) . (\sigma B)$\\ $\sigma \rtype $&$ \rtype$\\ $\sigma (\Pi y \star A . K) $&$ \Pi y \star (\sigma A) . (\sigma K)$\\ $\sigma \cdot $&$ \cdot$\\ $\sigma (\Gamma, x\star A) $&$ (\sigma\Gamma), x \star (\sigma A)$\\ \end{tabular}$$ \subsection{Reduction} Here we recursively use the definition of substitution, but only at strictly smaller simple types. $$[\lambda x\lstar . M|(N^\star;S)]^{\tau_1\to\tau_2} = [[N/x]^{\tau_1}M| S]^{\tau_2}$$ $$[R|()]^\bullet = R$$ Any other reduction $[M|S]^\tau$ that doesn't match these two patterns is undefined. \subsection{Promotion} Promotion is an operation on contexts; written as $\Gamma^\star$, it outputs a context. $$\cdot^\div = \cdot$$ $$(\Gamma, x\star A)^\div = \Gamma^\div, x : A$$ $$\Gamma^: = \Gamma$$ The purpose of promotion is to allow irrelevant arguments to functions to refer to irrelevant hypotheses. When irrelevant arguments are type-checked, they are checked in the `promoted' context where all irrelevant hypotheses have been converted to genuine ones. \subsection{Equivalence} We tacitly identify all $\alpha$-equivalent terms. If a metavariable is repeated, it implies a requirement of strict syntactic identity (up to $\alpha$-equivalence). We write this same notion of syntactic identity as $=$. The definition of equivalence $\equiv$ is nearly the same as $=$, except that we accept as equal all terms $M$ found at positions of the form $(M^\div; S)$. In other words the term identity of terms `at irrelevant position' does not matter. A program that checks equivalence does strictly a subset of the work an ordinary syntactic equality check would have performed. In this way we have unique canonical forms {\em up to} the choice of irrelevant representatives. $$\begin{prooftree} M_1 \equiv M_2 \justifies \lambda x\lstar . M_1 \equiv \lambda x\lstar . M_2 \end{prooftree}$$ $$\begin{prooftree} S_1 \equiv S_2 \justifies H \cdot S_1 \equiv H \cdot S_2 \end{prooftree}$$ %$$\begin{prooftree} %\using ??? \justifies %\bot \equiv \bot %\end{prooftree}$$ $$\begin{prooftree} \justifies () \equiv () \end{prooftree}$$ $$\begin{prooftree} M_1 \equiv M_2 \qquad S_1 \equiv S_2 \justifies (M_1^:; S_1) \equiv (M_2^:; S_2) \end{prooftree} \qquad \begin{prooftree} S_1 \equiv S_2 \justifies (M_1^\div; S_1) \equiv (M_2^\div; S_2) \end{prooftree} $$ $$\begin{prooftree} S_1 \equiv S_2 \justifies a \cdot S_1 \equiv a \cdot S_2 \end{prooftree}$$ $$\begin{prooftree} A_1 \equiv A_2 \qquad V_1 \equiv V_2 \justifies \Pi x\star A_1 . V_1 \equiv \Pi x\star A_2 . V_2 \end{prooftree}$$ $$\begin{prooftree} \justifies \rtype \equiv \rtype \end{prooftree}$$ \section{Typing} We begin with signature validity --- it is, however, mutually recursive with all the remaining typing rules. These are the only ones on which we explicitly index the judgement by a signature. All turnstiles that follow these three rules carry an implicit $\Sigma$ subscript. \subsection{Signature Validity} $$\begin{prooftree} \justifies \prov \cdot : \rsgn \end{prooftree}$$ $$\begin{prooftree} \cdot \prov_\Sigma A : \rtype \qquad\prov \Sigma:\rsgn \justifies \prov (\Sigma, c : A) : \rsgn \end{prooftree}$$ $$\begin{prooftree} \cdot \prov_\Sigma K : \rkind \qquad\prov \Sigma:\rsgn \justifies \prov (\Sigma, a : K) : \rsgn \end{prooftree}$$ Term typing is divided naturally into checking and synthesis. \subsection{Term Checking} $$\begin{prooftree} \Gamma, x \star A \prov M \tcheck B \justifies \Gamma \prov \lambda x\lstar . M \tcheck \Pi x \star A . B \end{prooftree}$$ In the following rule, the boundary between synthesis and checking, we check that the synthesized type is equal to the type the term is checked against, up to the choice of irrelevant representatives. $$\begin{prooftree} \Gamma\prov R \tsynth A' \qquad A \equiv A' \justifies \Gamma \prov R \tcheck A \end{prooftree}$$ \subsection{Term Synthesis} $$\begin{prooftree} c : A \in \Sigma \qquad \Gamma\prov S : A > B \justifies \Gamma \prov c \cdot S \tsynth B \end{prooftree}$$ $$\begin{prooftree} x : A \in \Gamma \qquad \Gamma\prov S : A > B \justifies \Gamma \prov x \cdot S \tsynth B \end{prooftree}$$ \subsection{Spine Synthesis} In $\Gamma \prov S : V > W$, the inputs are $\Gamma, S, V$, and $W$ is output. $$\begin{prooftree} \justifies \Gamma \prov () : a\cdot S > a\cdot S \end{prooftree}$$ $$\begin{prooftree} \justifies \Gamma \prov () : \rtype > \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M \tcheck^\star A \qquad \Gamma \prov S : [M/x]^{A^-} V > W \justifies \Gamma \prov (M^\star; S) : \Pi x \star A . V > W \end{prooftree}$$ \subsection{Promotion} $$\begin{prooftree} \Gamma^\star \prov M \tcheck B \justifies \Gamma \prov M \tcheck^\star B \end{prooftree}$$ \subsection{Type Validity} $$\begin{prooftree} a : K \in \Sigma \qquad \Gamma\prov S : K > \rtype \justifies \Gamma \prov a \cdot S : \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A : \rtype\qquad \Gamma, x \star A \prov B : \rtype \justifies \Gamma \prov \Pi x\star A . B :\rtype \end{prooftree}$$ \subsection{Kind Validity} $$\begin{prooftree} \justifies \Gamma \prov \rtype : \rkind \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A : \rtype\qquad \Gamma, x \star A \prov K:\rkind \justifies \Gamma \prov \Pi x\star A . K : \rkind \end{prooftree}$$ \subsection{Context Validity} $$\begin{prooftree} \justifies \prov \cdot :\rctx \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A : \rtype \qquad\prov \Gamma:\rctx \justifies \prov (\Gamma, x \star A) :\rctx \end{prooftree}$$ \section{Properties} \begin{lemma} \label{atomic.term.atomic.type} If $\Gamma \prov R \tsynth A$, then $A$ is of the form $a \cdot S$. \end{lemma} \begin{proof} By induction on the structure of the typing derivation. \cqed \end{proof} A note on the fact that substitution is partial: when we say two expressions are syntactically identical without any further qualification, (i.e. $M = N$) we mean that either both are undefined, or both are defined and syntactically identical. \begin{lemma} \label{div.subst.commute} $([M/x]^\tau \Gamma)^\div =[M/x]^\tau (\Gamma^\div)$. \end{lemma} \begin{proof} By induction on the structure of $\Gamma$. \cqed \end{proof} \begin{definition} Defining $\Gamma \preceq \Gamma'$, ``$\Gamma$ is weaker than $\Gamma'$''. $$\begin{prooftree}\justifies \cdot \preceq \cdot\end{prooftree}\qquad \begin{prooftree}\Gamma \preceq \Gamma' \justifies \Gamma, x\star A \preceq \Gamma, x \star A\end{prooftree}\qquad \begin{prooftree}\Gamma \preceq \Gamma' \justifies \Gamma, x\div A \preceq \Gamma, x :A\end{prooftree}$$ \end{definition} \begin{lemma} Suppose $\Gamma \preceq \Gamma'$. If $\Gamma \prov J$ then $\Gamma' \prov J$, for any typing judgment $J$. %% \begin{enumerate} %% \item If $\Gamma \prov M \tcheck^\star A$, then $\Gamma' \prov M \tcheck^\star A$. %% \item If $\Gamma \prov M \tcheck A$, then $\Gamma' \prov M \tcheck A$. %% \item If $\Gamma \prov R \tsynth A$, then $\Gamma' \prov R \tsynth A$. %% \item If $\Gamma \prov S : V > W$, then $\Gamma' \prov S : V > W$. %% \end{enumerate} \end{lemma} \begin{proof} By induction on the structure of the typing derivation. Most cases are trivial. The only interesting cases are those that treat rules that significantly manipulate the context. \begin{itemize} \item[Case:] $$\D = \begin{prooftree} \[\D' \djust \Gamma, x \star A_0 \prov M_0 \tcheck B\] \justifies \Gamma \prov \lambda x\lstar . M_0 \tcheck \Pi x \star A_0 . B \end{prooftree}$$ Observe that since $\Gamma \preceq\Gamma'$, also $\Gamma, x \star A_0 \preceq \Gamma', x\star A_0$. Use the induction hypothesis on this fact and the derivation $\D'$ to obtain $\Gamma', x\star A_0 \prov M_0 \tcheck B$. Rule application gives $\Gamma' \prov \lambda x\lstar . M_0 \tcheck \Pi x \star A_0 .B$ as required. \item[Case:] $$\D = \begin{prooftree} x : A \in \Gamma \qquad \[\D' \djust \Gamma\prov S : A > B\] \justifies \Gamma \prov x \cdot S \tsynth B \end{prooftree}$$ Use the induction hypothesis on $\D'$ to get $\Gamma' \prov S : A>B$. It follows from the definition of $\preceq$ that if $x : A \in \Gamma$ and $\Gamma \preceq \Gamma'$, then $x : A \in \Gamma'$. So by rule application we see $\Gamma' \prov x \cdot S \tsynth B$ as required. \item[Case:] $$\D = \begin{prooftree} \[\D' \djust \Gamma^\star \prov M \tcheck B\] \justifies \Gamma \prov M \tcheck^\star B \end{prooftree}$$ It is easy to see from the definitions of $\preceq$ and promotion that if $\Gamma \preceq \Gamma'$, then $\Gamma^\star \preceq (\Gamma')^\star$ for either possible value of $\star$. Therefore use the induction hypothesis on $\D'$ to obtain $(\Gamma')^\star \prov M \tcheck B$ and apply the rule to get $\Gamma' \prov M \tcheck^\star B$ as required. \end{itemize} \cqed \end{proof} \begin{corollary} \label{promotion.weakening} If $\Gamma \prov M \tcheck^\star A$, then $\Gamma^\div \prov M \tcheck A$. \end{corollary} \begin{proof} If $\star$ is $:$, then apply the lemma to $\Gamma \prov M \tcheck A$ (which we know by inversion) and the fact that $\Gamma \preceq \Gamma^\div$. If $\star$ is $\div$ then the result is immediate from inversion.\cqed \end{proof} \begin{lemma} \label{skeletal.ignore.subst} If $[M/x]^\tau A$ is well-defined, then $([M/x]^\tau A)^- = A^-$. \end{lemma} \begin{proof} By induction on the structure of $A$. \cqed \end{proof} \begin{lemma}[Weakening] \label{weakening} If $\Gamma, \Gamma' \prov J$ then $\Gamma, x\star A, \Gamma' \prov J$. \end{lemma} \begin{proof} By induction on the derivation of $\Gamma \prov J$. \cqed \end{proof} \begin{lemma} \label{strengthening} If $X$ contains no free occurrence of $x$, then $[M/x]^\tau X = X$. \end{lemma} \begin{proof} By induction on the structure of $X$. \cqed \end{proof} \begin{lemma} \label{equiv.stability} If $X \equiv X'$ and both $[M/x]^\tau X$ and $[M/x]^\tau X'$ are defined, then $[M/x]^\tau X \equiv [M/x]^\tau X'$. \end{lemma} \begin{proof} By induction over $\D :: X \equiv X'$. The only interesting case is when $$\D = \begin{prooftree} \[ \D' \djust S_1 \equiv S_2\] \justifies (M_1^\div; S_1) \equiv (M_2^\div; S_2)\end{prooftree}$$ Here the induction hypothesis on $\D'$ gives us that $[M/x]^\tau S_1 \equiv [M/x]^\tau S_2$. By rule application we get $ (([M/x]^\tau M_1)^\div; [M/x]^\tau S_1) \equiv (([M/x]^\tau M_2)^\div; [M/x]^\tau S_2)$ as required. \cqed \end{proof} \begin{lemma} Make the following abbreviations: $\sigma_B = [N/z]^{B^-}$, $\sigma_A = [M/x]^{A^-}$, and $\sigma_A' = [\sigma_B M/x]^{A^-}$. \label{subst.commute} \begin{itemize} \item[1.] Suppose $\sigma_A V$, $\sigma_B V$, and $\sigma_B M$ are defined. Suppose $x$ does not occur free in $N$. Then $\sigma_B \sigma_A V$ and $\sigma_A'\sigma_B V$ are both defined, and $\sigma_B \sigma_A V=\sigma_A'\sigma_B V$. \item[2.] Suppose $[M| S]^{C^-}$, $\sigma_B M$, and $\sigma_B S$ are defined. Then $\sigma_B [M| S]^{C^-}$ and $[\sigma_B M | \sigma_B S]^{C^-}$ are both defined, and $\sigma_B [M| S]^{C^-}=[\sigma_B M | \sigma_B S]^{C^-}$. \end{itemize} \end{lemma} \begin{proof} By lexicographic induction first on the simple type (either the larger of $(A^-, B^-)$ in case 1 or $C^-$ in case 2), and subsequently on the structure of the expression $V$. \begin{itemize} \item[1.] \item[Case:] $V = z\cdot S$. $$\sigma_A'\sigma_B (z\cdot S) = \sigma_A' [N|\sigma_B S]^{B^-}$$ $$\sigma_B\sigma_A (z\cdot S) = [\sigma_A' N|\sigma_B\sigma_A S]^{B^-}$$ We know that $\sigma_A' N$ is defined because $x$ does not occur in $N$. By the induction hypothesis part 1, we know that $\sigma_A'\sigma_B S$ and $\sigma_B\sigma_A S$ are defined and identical. From the induction hypothesis part 2 on $N$, $\sigma_B S$, $B^-$, and $\sigma_A'$, we get $\sigma_A' [N|\sigma_B S]^{B^-} = [\sigma_A' N|\sigma'_A\sigma_B S]^{B^-}$. It follows from the identity above that the latter is the same as $[\sigma_A' N|\sigma_B\sigma_A S]^{B^-}$, as required. \item[Case:] $V = x\cdot S$. $$\sigma_A'\sigma_B (x\cdot S) = [\sigma_B M|\sigma_A'\sigma_B S]^{A^-}$$ $$\sigma_B\sigma_A (x\cdot S) = \sigma_B [M|\sigma_A S]^{A^-}$$ We know that $\sigma_B M$ is defined by assumption. The remained of this case is symmetric to the previous one. \item[2.] \item[Case:] $M = \lambda w . M'$, $S = ((M'')^\star; S')$, and $C^- = C_1^- \to C_2^-$. Then by definition of reduction $$\sigma_B[M|S]^{C^-} = \sigma_B[[M''/w]^{C_1^-}M' | S']^{C_2^-}\eqno(*)$$ $$[\sigma_B M|\sigma_B S]^{C^-} = [[\sigma_B M''/w]^{C_1^-}\sigma_B M' | \sigma_B S']^{C_2^-}\eqno(**)$$ We can see from the induction hypothesis (part 1, at a smaller type) that $$\sigma_B [ M''/w]^{C_1^-}M' = [\sigma_B M''/w]^{C_1^-}\sigma_B M' $$ and both are well-defined, since $w$ can't appear in $N$. Thus we can use the induction hypothesis (part two, at $C^-_2$) to conclude the right-hand sides of $(*)$ and $(**)$ are equal, as required. \end{itemize} \cqed \end{proof} \def\bigg{\Gamma, z\ast B, \Gamma'} \def\postg{\Gamma, \sigma\Gamma'} \begin{lemma}[Substitution] Suppose $\Gamma \prov N \tcheck^\ast B$. Let $\sigma$ be an abbreviation for $[N/z]^{B^-}$, with $z$ being a variable that does not occur free in $\Gamma$ or $B$. For cases 2-5, suppose $\sigma \Gamma'$ is well-defined. \begin{enumerate} \item If $\Gamma \prov S : B > A$ and $\Gamma \prov M \tcheck B$ then $\Gamma \prov [M | S]^{B^-} \tsynth A$. \label{reduction.case} \item If $ \bigg \prov M \tcheck^\star A$ and $\sigma A$ is defined, then $\postg\prov \sigma M \tcheck^\star \sigma A$. \label{checkstar.case} \item If $ \bigg \prov M \tcheck A$ and $\sigma A$ is defined, then $\postg\prov \sigma M \tcheck \sigma A$. \label{check.case} \item If $ \bigg \prov R \tsynth A$, then $\postg\prov \sigma R \tsynth \sigma A$. \item If $ \bigg \prov S : V > W$ and $\sigma V$ is defined, then $\postg\prov \sigma S : \sigma V > \sigma W$. \label{spine.case} \end{enumerate} \end{lemma} \begin{proof} By lexicographic induction on first the simple type $B^-$, next on the case (where case 1 is ordered less than all the remaining cases), and finally (for cases 2-5) on the structure of the typing derivation. \begin{itemize} \item[1.] \item[Case:] $M$ is of the form $\lambda x\lstar . M_0$. Then the typing derivation of $M$ must be of the form $$\begin{prooftree} \[\D_1 \djust \Gamma, x \star B_1 \prov M_0 \tcheck B_2\] \justifies \Gamma \prov \lambda x\lstar . M_0 \tcheck \Pi x \star B_1 . B_2 \end{prooftree}$$ Since we know that $B$ is $\Pi x \star B_1 . B_2$, the typing derivation of $S$ must look like $$\begin{prooftree} \[\D_2\djust \Gamma \prov M_1 \tcheck^\star B_1\] \[\D_3\djust\Gamma \prov S_1 : [M_1/x]^{B_1^-} B_2 > A\] \justifies \Gamma \prov (M_1^\star; S_1) : \Pi x \star B_1 . B_2 > A \end{prooftree}$$ with $S$ being $(M_1^\star; S_1)$. By the induction hypothesis (part~\ref{check.case}) on the smaller simple type $B_1^-$ and the derivations $\D_1$ and $\D_2$, (knowing that $[M_1/x]^{B_1^-} B_2$ is defined because we have $\D_3$ in our hands) we find that $$\Gamma \prov [M_1/x]^{B_1^-} M_0 \tcheck [M_1/x]^{B_1^-} B_2 \eqno(*)$$ Observe that by Lemma~\ref{skeletal.ignore.subst} we know $( [M_1/x]^{B_1^-} B_2)^- = B_2^-$, and therefore (since $B_2^-$ is a smaller simple type) we can apply the induction hypothesis (part~\ref{reduction.case}) to $(*)$ and the derivation $\D_3$ to infer first that $$\Gamma \prov [[M_1 / x]^{B_1^-} M_0 |S_1]^{([M_1/x]^{B_1^-}B_2)^-} \tcheck A$$ and subsequently by the syntactic identity we just noted $$\Gamma \prov [[M_1 / x]^{B_1^-} M_0 |S_1]^{B_2^-} \tcheck A$$ But by definition of reduction we can read off that $$[M | S]^{B^-} = [(\lambda x\lstar . M_0) | (M_1^\star; S_1)]^{B_1^- \to B_2^-} =[[M_1 / x]^{B_1^-} M_0 |S_1]^{B_2^-}$$ so we are done. \item[Case:] $M$ is atomic, i.e. of the form $R$. By inversion and Lemma~\ref{atomic.term.atomic.type} we have a typing derivation $$\Gamma \prov R \tcheck a\cdot S_0 \eqno(*)$$ That is, $B$ is $a \cdot S_0$, and so $B^- = \bullet$. The only typing rule that would conclude $S : B > A$ is $$\begin{prooftree} \justifies \Gamma \prov () : a\cdot S_0 > a\cdot S_0 \end{prooftree}$$ so $S$ must be empty, and $A$ is also $a\cdot S_0$. Therefore $$[M | S]^{B^-} = [R | ()]^{\bullet} = R$$ but we already have a derivation that $\Gamma \prov R \tcheck a \cdot S_0$, namely $(*)$. \item[2.] \item[Case:] $$\D = \begin{prooftree} \[\D' \djust \bigg \prov M \tcheck A\] \justifies \bigg \prov M \tcheck^: A\end{prooftree}$$ By the induction hypothesis on $\D'$ we obtain $\postg \prov \sigma M \tcheck \sigma A$. By rule application we have $\postg \prov \sigma M \tcheck^: \sigma A$ as required. \item[Case:] $$\D = \begin{prooftree} \[\D' \djust (\bigg)^{\div} \prov M \tcheck A\] \justifies \bigg \prov M \tcheck^\div A \end{prooftree}$$ By Corollary~\ref{promotion.weakening} we know $\Gamma^\div \prov N \tcheck B$, so we can apply the induction hypothesis to $\D'$ (which, unwinding the definition of promotion, is a derivation of $\Gamma^\div, z : B, (\Gamma')^\div \prov M \tcheck A$) to obtain $ \Gamma^\div, \sigma((\Gamma')^\div) \prov \sigma M \tcheck \sigma A$. This is the same as $(\postg)^\div \prov \sigma M \tcheck \sigma A$ by Lemma~\ref{div.subst.commute}. By rule application we have $\postg \prov \sigma M \tcheck^\div \sigma A$ as required. \item[3.] \item[Case:] $$\D = \begin{prooftree} \[\D' \djust \bigg, x \star A_0 \prov M_0 \tcheck B_0\] \justifies \bigg \prov \lambda x\lstar . M_0 \tcheck \Pi x \star A_0 . B_0 \end{prooftree} $$ By the induction hypothesis on $\D'$ we know $\postg, x \star \sigma A_0 \prov \sigma M_0 \tcheck \sigma B_0$. By rule application we obtain $\postg \prov \lambda x\lstar . \sigma M_0 \tcheck \Pi x \star \sigma A_0 . \sigma B_0$ as required. \item[Case:] $$\D = \begin{prooftree} \[\D'\djust \bigg\prov R \tsynth A'\] \qquad A \equiv A' \justifies \bigg \prov R \tcheck A \end{prooftree}$$ By the induction hypothesis on $\D'$ we obtain $\postg \prov \sigma R \tsynth \sigma A'$. Since $A \equiv A'$, so too $\sigma A \equiv \sigma A'$ by Lemma~\ref{equiv.stability}. By rule application we obtain $\postg \prov \sigma R \tcheck \sigma A$ as required. \item[4.] \item[Case:] $$\D = \begin{prooftree} c : A_0 \in \Sigma \qquad \[\D'\djust \bigg\prov S : A_0 > A\] \justifies \bigg \prov c \cdot S \tsynth A \end{prooftree}$$ By the induction hypothesis on $\D'$ we obtain $\postg \prov \sigma S : \sigma A_0 > \sigma A$. But $A_0$ can have no free occurrence of $z$, so $\sigma A_0 = A_0$ by Lemma~\ref{strengthening}. By rule application we get $\postg \prov c \cdot \sigma S \tsynth \sigma A$ as required. \item[Case:] $$\D = \begin{prooftree} x : A_0 \in \bigg \qquad \[\D'\djust \bigg\prov S : A_0 > A\] \justifies \bigg \prov x \cdot S \tsynth A \end{prooftree}$$ We split on three subcases depending on the location of $x\in\bigg$. \item[Subcase:] $x \in \Gamma$. In this case $z$ can have no occurrence in the type $A_0$ of $x$. Thus $\sigma A_0$ is syntactically equal to $A_0$ by Lemma~\ref{strengthening}. By the induction hypothesis (part~\ref{spine.case}) on $\D'$ we obtain $\postg \prov \sigma S : A_0 > \sigma A$. By rule application we get $\postg \prov x \cdot \sigma S \tsynth \sigma A$ as required. \item[Subcase:] $x$ is in fact $z$. In this case $A_0$ and $B$ are syntactically identical, the relevancy variable $\ast$ must be $:$, and the term $\sigma (x \cdot S)$ we aim to type is $[N|\sigma S]^{B^-}$. We know $\Gamma \prov N \tcheck B$, and by using Lemma~\ref{weakening} repeatedly we can obtain $\postg \prov N \tcheck B$. By Lemma~\ref{strengthening} and the induction hypothesis (part~\ref{spine.case}), we know $\postg \prov \sigma S : B > \sigma A$. Use the induction hypothesis (part \ref{reduction.case}: this is licensed because it is ordered as less than the other cases, and the simple type $B^-$ has remained the same) to obtain the required derivation of $\postg \prov [N| \sigma S]^{B^-} \tsynth \sigma A$. %$x$ is in fact $z$. In this case $A_0$ and $B$ are syntactically identical, the relevancy variable $\ast$ must be $:$, %and $\sigma (x \cdot S)$ is $[N|\sigma S]^{B^-}$. %We know $\Gamma \prov N \tcheck B$ (and by using Lemma~\ref{weakening} repeatedly and Lemma~\ref{strengthening} we can obtain %$\postg \prov N \tcheck \sigma B$) and %$\postg \prov \sigma S : \sigma B > \sigma A$ and we %must show that $$\postg \prov [N| \sigma S]^{B^-} \tsynth \sigma A \eqno(*)$$ %Use the induction hypothesis (part \ref{reduction.case}) to infer %$\postg \prov [N| \sigma S]^{(\sigma B)^-} \tsynth \sigma A$, which is nearly what we need. %This use of the induction hypothesis is licensed by the fact that $B^-$ is syntactically identical to $(\sigma B)^-$, %(by Lemma~\ref{skeletal.ignore.subst}). So the simple type has stayed the same, and the case of the lemma has gotten smaller, %so the induction is well-founded. %Finally use Lemma~\ref{skeletal.ignore.subst} again to reconcile the $(\sigma B)^-$ in the result of using the induction hypothesis % with the $B^-$ in $(*)$. \item[Subcase:] $x \in \Gamma'$. By assumption on $\Gamma'$, we have that $\sigma A_0$ is defined. By the induction hypothesis (part~\ref{spine.case}) $\postg \prov \sigma S : \sigma A_0 > \sigma A$. Clearly $x : \sigma A_0 \in \Gamma, \sigma\Gamma'$ so it follows by rule application that $\postg \prov x \cdot \sigma S \tsynth \sigma A$. \item[5.] \item[Case:] $$\D =\begin{prooftree} \justifies \bigg \prov () : a\cdot S > a\cdot S \end{prooftree}$$ Since we know $a\cdot \sigma S$ is defined, by rule application we immediately have $\postg \prov () :a\cdot\sigma S > a\cdot \sigma S$. \item[Case:] $$\D =\begin{prooftree} \justifies \bigg \prov () : \rtype > \rtype \end{prooftree}$$ By rule application, we immediately have $\postg \prov () :\rtype > \rtype$. \item[Case:] $$\D = \begin{prooftree} \[\D_1\djust \bigg \prov M \tcheck^\star A \] \[\D_2 \djust \bigg \prov S : [M/x]^{A^-} V > W\] \justifies \bigg \prov (M^\star; S) : \Pi x \star A . V > W \end{prooftree}$$ By the induction hypothesis (part~\ref{checkstar.case}) we know $\postg\prov \sigma M \tcheck^\star \sigma A$. Observe that $M$ has no free occurrence of $z$, by assumption $\sigma V$ is well-defined, and from the existence of $\D_2$ we know that $[M/x]^{A^-} V$ is well-defined. Therefore we can use Lemma~\ref{subst.commute} to infer that both $[\sigma M/x]^{A^-} \sigma V$ and $\sigma [M/x]^{A^-} V$ are defined, and that they are syntatically identical. By the induction hypothesis (part~\ref{spine.case}) we know $\postg\prov \sigma S : \sigma [M/x]^{A^-} V > \sigma W$, which is the same thing as $\postg\prov \sigma S : [\sigma M/x]^{A^-} \sigma V > \sigma W$. By rule application we obtain $\postg \prov (\sigma M^\star;\sigma S):\Pi x \star \sigma A . \sigma V > \sigma W$. \end{itemize} \cqed \end{proof} \begin{lemma}[Validity] Suppose $\Gamma$ is well-formed. \begin{enumerate} \item If $\Gamma \prov R \tsynth A$ then $\Gamma \prov A : \rtype$. \item If $\Gamma \prov S : A > B$ and $\Gamma \prov A : \rtype$, then $\Gamma \prov B : \rtype$. \end{enumerate} \end{lemma} \begin{proof} By induction on the structure of the derivation. Requires the fact that if $\Gamma$ valid, then $\Gamma^\div$ valid, which requires Corollary~\ref{promotion.weakening}. \cqed \end{proof} \end{document} \section{Erasure} We write hereafter just % $\lambda$ for $\lambda^:$ and $\Pi$ for $\Pi^:$ and $(M;S)$ for $(M^:;S)$. Replace the term checking rules with $$\begin{prooftree} \Gamma, x : A \prov^\psi M \tcheck B \justifies \Gamma \prov^\psi \lambda x . M \tcheck \Pi x : A . B \end{prooftree}$$ $$\begin{prooftree} \Gamma, x \div A \prov^\psi M \tcheck B \qquad x\hbox{ not free in }$M,B$ \justifies \Gamma \prov^\psi M \tcheck A \imp B \end{prooftree}$$ $$\begin{prooftree} \Gamma\prov R \tsynth A \justifies \Gamma \prov R \tcheck A \end{prooftree}$$ Replace the spine cons rule with: $$\begin{prooftree} \Gamma \prov^\psi M \tcheck A \qquad \Gamma \prov S : [M/x]^{A^-} V > W \justifies \Gamma \prov^\psi (M; S) : \Pi x : A . V > W \end{prooftree}$$ $$\begin{prooftree} \Gamma^\div \prov^\psi M \tcheck A \qquad \Gamma \prov S : V > W \justifies \Gamma \prov^\psi S : A \imp V > W \end{prooftree}$$ Pi typing rule with $$\begin{prooftree} \Gamma \prov^\psi A : \rtype\qquad \Gamma, x : A \prov^\psi B : \rtype \justifies \Gamma \prov^\psi \Pi x : A . B :\rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov^\psi A : \rtype \qquad \Gamma, x \div A \prov^\psi B : \rtype \qquad x\hbox{ not free in }$B$ \justifies \Gamma \prov^\psi A \imp B :\rtype \end{prooftree}$$ Simplification for $\imp$ works like $(A \imp B)^- = B^-$, substitution like $$\sigma (A \imp B) = (\sigma A) \imp (\sigma B)$$ \subsection{Translation} $$(\lambda x^: . M)^\psi = \lambda x . (M^\psi)$$ $$(\lambda x^\div . M)^\psi = M^\psi$$ $$(M^:; S)^\psi = (M^\psi; S^\psi)$$ $$(M^\div ; S)^\psi = S^\psi$$ $$(\Pi x : A . B)^\psi = \Pi x : (A^\psi) . (B^\psi)$$ $$(\Pi x \div A . B)^\psi = (A^\psi) \imp (B^\psi)$$ $$(\Gamma, x \star A)^\psi = (\Gamma^\psi), x \star A^\psi$$ (remainder are just congruences) We use $=$ for syntactic identity up to $\alpha$-equivalence. \begin{lemma} \label{in.absentia} Suppose $x\div B\in\Gamma$ and that the variable $x$ does not occur free in any type in $\Gamma$. \begin{enumerate} \item If $\Gamma \prov^\psi M \tcheck A$, and $x$ does not occur free in $A$, then $x$ does not occur free in $M$. \item If $\Gamma \prov^\psi R \tsynth A$, then $x$ does not occur free in $R$. \item If $\Gamma \prov^\psi S : A > C$ and $x$ does not occur free in $A$, then $x$ does not occur free in $C$. \item If $\Gamma \prov^\psi A : \rtype$, then $x$ does not occur free in $A$. \end{enumerate} \end{lemma} \begin{proof} By induction on the context $\Gamma$, case, and the derivation. The difference between the $\prov^\psi$ and $\prov$ rules is that the former only use promotion to typecheck the `guessed' term and then throw it away, so there are no valid uses of irrelevant variables that can survive to a well-typed term. \cqed \end{proof} \begin{lemma} \label{equiv.equal} If $X \equiv X'$ then $X^\psi = (X')^\psi$. \end{lemma} \begin{proof} By induction. \cqed \end{proof} \begin{lemma} Let $\sigma$ abbreviate $[N/y]^{B^-}$ and $\sigma^\psi$ abbreviate $[N^\psi/y]^{(B^\psi)^-}$. Suppose $\prov \Gamma : \rctx$. \begin{itemize} \item If $\Gamma \prov M \tcheck A$ and $\Gamma \prov A : \rtype$, then $(\sigma M)^\psi = \sigma^\psi M^\psi$ \item If $\Gamma \prov R \tsynth A$, then $(\sigma R)^\psi = \sigma^\psi R^\psi$ \item If $\Gamma \prov S : A > C$ and $\Gamma \prov A : \rtype$, then $(\sigma S)^\psi = \sigma^\psi S^\psi$ \item If $\Gamma \prov N \tcheck A$ and $\Gamma \prov S : A > C$, then $([N | S]^{\tau})^\psi = [N^\psi | S^\psi]^{\tau}$ \end{itemize} \end{lemma} \begin{proof} Induction on the simple type $B^-$ and the structure of $X$ and $S$. We show some representative cases. \begin{itemize} \item[Case:] $$[\lambda x\lstar . M|(N^\star;S)]^{B_1^-\to B^-_2} = [[N/x]^{B^-_1}M| S]^{B^-_2}$$ with typing derivations of $\lambda x\lstar . M \tcheck \Pi x\star B_1 . B_2$ and $S : \Pi x \star B_1 . B_2 > C$. If we hit this with $\psi$ ``on the outside'' we get $([[N/x]^{B^-_1}M| S]^{B^-_2})^\psi$ which by two applications of the i.h. is equal to $([[N^\psi/x]^{(B_1^\psi)^-}M^\psi| S^\psi]^{(B_2^\psi)^-})$. If $\star$ is $:$, then this is transparently equal to applying $\psi$ ``on the inside'' and computing $$[(\lambda x^: . M)^\psi|(N^:;S)^\psi]^{(B_1^\psi)^-\to (B_2^\psi)^-} = [[N^\psi/x]^{(B_1^\psi)^-}M^\psi| S^\psi]^{(B_2^\psi)^-}$$ Otherwise $\star$ is $\div$, and $(N^\div;S)^\psi = S^\psi$. In this case we compute $$[(\lambda x^\div . M)^\psi|(N^\div;S)^\psi]^{((\Pi x \star B_1 . B_2)^\psi)^-} = [ M^\psi|S^\psi]^{(B_2^\psi)^-}$$ But we know $M$ is well-typed in $\Gamma, x\div B_1$, and so by Lemma~\ref{in.absentia} $x$ does not actually occur in $M$, thus by Lemma~\ref{strengthening} we have $[ M^\psi|S^\psi]^{(B_2^\psi)^-} = ([[N^\psi/x]^{(B_1^\psi)^-}M^\psi| S^\psi]^{(B_2^\psi)^-})$. $$[R|()]^\bullet = R$$ \end{itemize} \cqed \end{proof} \begin{lemma} Suppose $\prov \Gamma :\rctx$. \begin{enumerate} \item $\prov^\psi \Gamma^\psi :\rctx$. \item If $\Gamma \prov M \tcheck A$ and $\Gamma \prov A : \rtype$ then $\Gamma^\psi \prov^\psi M^\psi \tcheck A^\psi$. \item If $\Gamma \prov R \tsynth A$ then $\Gamma^\psi \prov^\psi R^\psi \tsynth A^\psi$. \item If $\Gamma \prov S : V > W$ and ($\Gamma \prov V : \rtype$ or $\Gamma \prov V : \rkind$) then $\Gamma^\psi \prov^\psi S^\psi : V^\psi > W^\psi$. \item If $\Gamma \prov A : \rtype$ then $\Gamma^\psi \prov^\psi A^\psi \rtype$. \label{type.case} \end{enumerate} \end{lemma} \begin{proof} By induction. Call $\D_\Gamma$ the derivation of $\prov \Gamma :\rctx$. \begin{itemize} \item[1.] If $\Gamma$ is empty, we are immediately done. Otherwise $\Gamma$ is of the form $\Gamma, x \star A$ and $$\begin{prooftree} \[\D_1 \djust \prov \Gamma :\rctx\] \[\D_2 \djust \Gamma \prov A : \rtype\] \justifies \prov \Gamma, x \star A :\rctx \end{prooftree}$$ Apply the i.h. to $\D_1$ to find $\prov^\psi \Gamma^\psi :\rctx$ and the i.h. part \ref{type.case} to $\D_2$ to obtain $\Gamma^\psi\prov^\psi A^\psi:\rtype$. The required fact that $\prov^\psi \Gamma^\psi, x \star A^\psi$ then follows by rule application. \item[2.] \item[Case:] $$\begin{prooftree} \[\D_1 \djust \Gamma, x \star A \prov M \tcheck B\] \justifies \Gamma \prov \lambda x\lstar . M \tcheck \Pi x \star A . B \end{prooftree}$$ $$\begin{prooftree} \[\D_2 \djust \Gamma \prov A : \rtype \]\[\D_3 \djust \Gamma, x \star A \prov B : \rtype\] \justifies \Gamma \prov \Pi x \star A . B : \rtype \end{prooftree}$$ By i.h. on $\D_\Gamma$ we can get $\D_\Gamma^\psi :: \prov^\psi \Gamma^\psi :\rctx$. By i.h. on $\D_\Gamma,\D_2$ we can get $\D_2^\psi :: \Gamma^\psi \prov^\psi A^\psi : \rtype$. By rule application on $\D_\Gamma^\psi,\D_2^\psi$ we can get $\D_{\Gamma x}^\psi :: \prov^\psi \Gamma^\psi, x \star A^\psi :\rctx$. By rule application on $\D_\Gamma, \D_2$ we can get $\D_{\Gamma x} :: \prov \Gamma, x \star A :\rctx$. By i.h. on $\D_{\Gamma x}, \D_1$, we get $\D_1^\psi :: \Gamma^\psi, x \star A^\psi \prov M^\psi \tcheck B$. If $\star$ is $:$, then we get by rule application that $\Gamma^\psi \prov^\psi \lambda x . M^\psi \tcheck \Pi x : A^\psi . B^\psi$ as required. Otherwise $\star$ is $\div$ and, what we know is specifically $\Gamma^\psi, x \div A^\psi \prov^\psi M^\psi \tcheck B^\psi$. The obstacle is that to apply the other lambda rule, $x$ must not appear in $M^\psi$ or $B^\psi$. In fact it is quite possible that $x$ appears in $M$ and $B$ --- we need to be sure that the translation erases all occurrences. Indeed we can use Lemma~\ref{in.absentia} on $\D_{\Gamma x}^\psi, \D^\psi_1$ to see that $x$ doesn't occur in $M^\psi$. Use the i.h. on $\D_{\Gamma x}, \D_3$ to get $\D_3^\psi :: \Gamma^\psi, x \div A^\psi \prov B^\psi : \rtype$ and subsequently use the same lemma on $\D_{\Gamma x}^\psi, \D_3^\psi$ to see that $x$ doesn't occur in $B^\psi$. So we are licensed to apply the rule to see that $\Gamma^\psi \prov M^\psi \tcheck A^\psi \imp B^\psi$ as required. \item[Case:] $$\begin{prooftree} \[\D_1 \djust \Gamma\prov R \tsynth A'\] \qquad A \equiv A' \justifies \Gamma \prov R \tcheck A \end{prooftree}$$ i.h. on $\D_\Gamma, \D_1$ gives $\Gamma^\psi \prov^\psi R^\psi \tsynth (A')^\psi$. Because of Lemma~\ref{equiv.equal}, we can use the rule to conclude $\Gamma^\psi \prov^\psi R^\psi \tcheck A^\psi$. \item[3.] \item[Case:] $$\begin{prooftree} x : A \in \Gamma \qquad \[D_1\djust \Gamma\prov S : A > B\] \justifies \Gamma \prov x \cdot S \tsynth B \end{prooftree}$$ Since $\Gamma$ is assumed valid, we know $\Gamma \prov A : \rtype$, so we can use the induction hypothesis on $\D_\Gamma, \D_1$ to get $\Gamma^\psi \prov^\psi S : A^\psi > B^\psi$. Rule application (since $x:A^\psi \in \Gamma^\psi$) yields $\Gamma^\psi \prov x \cdot S^\psi \tsynth B^\psi$. The constant case works similarly with the signature instead of the context. \item[4.] \item[Case:] $$\begin{prooftree} \justifies \Gamma \prov () : a\cdot S > a\cdot S \end{prooftree}$$ Immediate. \item[Case:] $$\begin{prooftree} \justifies \Gamma \prov () : \rtype > \rtype \end{prooftree}$$ Immediate. \item[Case:] $$\begin{prooftree} \[\[D_1 \djust \Gamma \prov M \tcheck A \]\justifies \Gamma \prov M \tcheck^: A\] \[\D_2 \djust \Gamma \prov S : [M/x]^{A^-} B > C\] \justifies \Gamma \prov (M^:; S) : \Pi x : A . B > C \end{prooftree}$$ $$\begin{prooftree} \[\D_3 \djust \Gamma \prov A : \rtype \]\[\D_4 \djust \Gamma, x : A \prov B : \rtype\] \justifies \Gamma \prov \Pi x : A . B : \rtype \end{prooftree}$$ To show $\Gamma^\psi \prov^\psi (M^\psi; S^\psi) : \Pi x : A^\psi : B^\psi > C^\psi$. By i.h. on $\D_\Gamma,\D_1,\D_3$ we get $\Gamma^\psi \prov^\psi M^\psi \tcheck A^\psi$. By substitution on $\D_1,\D_4$ we get $\D_5 :: \Gamma\prov [M/x]^{A^-}B : \rtype$. By i.h. on $\D_\Gamma, \D_2, \D_5$ (prioritize in the lexicographic order the derivation that the spine is well-formed before the derivation that the head type is a valid type) we get $\Gamma^\psi \prov^\psi S^\psi : ([M/x]^{A^-}B)^\psi > C^\psi$. By a lemma I haven't proven XXX this is the same as $\Gamma^\psi \prov^\psi S^\psi : [M^\psi/x]^{(A^\psi)^-}B^\psi > C^\psi$. Rule application finishes the case. \item[Case:] $$\begin{prooftree} \[\[D_1 \djust \Gamma^\div \prov M \tcheck A \]\justifies \Gamma \prov M \tcheck^\div A\] \[\D_2 \djust \Gamma \prov S : [M/x]^{A^-} B > C\] \justifies \Gamma \prov (M^\div; S) : \Pi x \div A . B > C \end{prooftree}$$ $$\begin{prooftree} \[\D_3 \djust \Gamma \prov A : \rtype \]\[\D_4 \djust \Gamma, x \div A \prov B : \rtype\] \justifies \Gamma \prov \Pi x \div A . B : \rtype \end{prooftree}$$ To show $\Gamma^\psi \prov^\psi S^\psi : A^\psi \imp B^\psi > C^\psi$. In order to get this it suffices to show $(\Gamma^\psi)^\div \prov^\psi M^\psi \tcheck A^\psi$ and $\Gamma^\psi \prov^\psi S : B^\psi> C^\psi$. The first of these is satisfied by applying i.h. to $\D_\Gamma, \D_1,\D_3$ and showing XXX that $\dash^\psi$ and $\dash^\div$ commute. Use substitution on $\D_1$ plus the subsequent rule and $\D_4$ to find a derivation $\D_5 :: \Gamma \prov [M/x]^{A^-} B : \rtype$. The second requirement follows shortly after using the i.h. on $\D_\Gamma,\D_2,\D_5$. Examining $\D_4$ we realize by Lemma~\ref{in.absentia} that $x$ has no occurrence in $B^\psi$, so that $([M/x]^{A^-} B)^\psi = [M^\psi/x]^{(A^\psi)^-} B^\psi = B^\psi$. XXX need to show this commutativity result. Thus rule application finishes the case. \cqed \end{itemize} \end{proof} \begin{theorem} \begin{enumerate} \item If $\Gamma \prov^\psi M\tcheck A$ then there exists $\Gamma_0,M_0,A_0$ such that $\Gamma_0 \prov M_0 \tcheck A_0$ and $X_0^\psi = X$ for $X\in \{\Gamma, M, A\}$. %\item Moreover, these $\dash^\psi$-preimages $M,A$ are unique up to $\equiv$ in the following sense. \item If $\Gamma \prov M_1 \tcheck A$ and $\Gamma \prov M_2 \tcheck A$ and $M_1^\psi = M_2^\psi$, then $M_1 \equiv M_2$. \item If $\Gamma \prov R_1 \tsynth A_1$ and $\Gamma \prov R_2 \tsynth A_2$ and $R_1^\psi = R_2^\psi$, then $R_1 \equiv R_2$ and $A_1 \equiv A_2$. \end{enumerate} \end{theorem} \begin{proof} By induction on... stuff. For 3, case analysis on the type. \begin{itemize} \item[Case:] $$\begin{prooftree} \Gamma, x \div A \prov M_{11} \tcheck B \justifies \Gamma \prov \lambda x^\div . M_{11} \tcheck \Pi x \div A . B \end{prooftree}\qquad \begin{prooftree} \Gamma, x \div A \prov M_{21} \tcheck B \justifies \Gamma \prov \lambda x^\div . M_{21} \tcheck \Pi x \div A . B \end{prooftree}$$ \end{itemize} \cqed \end{proof} \hrule \vskip 1in $$[\lambda x^\div . M|(N^\div;S)]^{\tau_1\to\tau_2} = [[N/x]^{\tau_1}M| S]^{\tau_2}$$ Trying to define a translation that commutes with this reduction $$ [[N/x]^{\tau_1}M| S]^{\tau_2} = [(\lambda x^\div . M)^\psi | (N^\div; S)^\psi ]^{\tau_1\to\tau_2}$$ SHIT \end{document}