Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\section{Further details on Dfn.~\ref{dfn:translation-of-proofs}, Sect.~\ref{sect:wfm}}

\label{sect:app-wfm}

%\paragraph*{Further details on Dfn.~\ref{dfn:translation-of-proofs}}

			The initial steps of $\arith$ are translated as follows,

			\[

			\begin{array}{ccc}

%			\vlinf{\word_\epsilon}{}{\seqar \word (\epsilon)}{}

%			& : &

%			\epsilon

%			\\

			\vlinf{\genzer}{}{\word(t) \seqar \word(\succ_0 t)}{}

			& \quad :\quad  &

			\succ_0 ( ;x)

			\\

			\vlinf{\genone}{}{\word(t) \seqar \word(\succ_1 t)}{}

			& \quad : \quad &

			\succ_1 (; x)

			\\

%			\vlinf{\epsilon^0}{}{ \word (t)  , \epsilon = \succ_0 t \seqar }{}

%			& : &

%			\epsilon

%			\\

%			\vlinf{\epsilon^1}{}{ \word (t)  , \epsilon = \succ_1 t \seqar }{}

%			& : &

%			\epsilon

%			\\

%			\vlinf{\succ_0}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}

%			& : &

%			\epsilon

%			\\

%			\vlinf{\succ_1}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}

%			& : &

%			\epsilon

%			\\

%			\vlinf{\inj}{}{\word(t), \succ_0 t = \succ_1 t \seqar}{}

%			& : &

%			\epsilon

%			\\

			\vlinf{\surj}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word. t = \succ_1 y }{}

			&\quad : \quad  &

			( \epsilon , \pred (  ;x) , \pred (;x ) )

			\\

				\vlinf{\wordcntr}{}{\word(t) \seqar \word(t) \land \word(t) }{}

				& \quad  : \quad &

				( \id (;x) , \id (;x) )

			\end{array}

			\]

			and the remaining initial steps are translated to $\epsilon$.

					Suppose $\pi$ ends with a $\rigrul{\land}$ step:

						\[

						\vlderivation{

							\vliin{\land}{}{ \Gamma, \Sigma \seqar \Delta, \Pi, A\land B }{

								\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

							}{

							\vltr{\pi_2}{ \Sigma \seqar \Pi, B }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

						}

					}

					\]

					By the inductive hypothesis let us suppose we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y)$ from $\pi_1$ and $\pi_2$ respectively, where $\type\left( \bigotimes\Gamma \right) = (\vec u; \vec x)$ and $\type \left( \bigotimes \Sigma \right) = (\vec v ; \vec y)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ and $\vec h = (\vec h^\Pi , \vec h^B)$, to denote the $\Delta$ and $A$ parts of $\vec g$ and the $\Pi$ and $B$ parts of $\vec h$.

					%	So we have $\vec f^{1} (\vec x ; \vec a)$ and $\vec f^2 (\vec y ; \vec b)$ for $\pi_1 $ and $\pi_2$ respectively, by the inductive hypothesis.

					We construct $\vec f^\pi$ by simply rearranging these tuples of functions:

					\[

					\vec f^\pi (\vec u , \vec v ; \vec x , \vec y)

					\quad := \quad

					\left(

					\vec g^\Delta (\vec u ; \vec x) , \vec h^\Pi (\vec v ; \vec y)  , \vec g^A (\vec u ; \vec x) , \vec h^B (\vec v ; \vec y)

					\right)

					\]

						If $\pi$ ends with a $\lefrul{\exists}$ step,

									\[

									\vlderivation{

										\vlin{\lefrul{\exists}}{}{ \Gamma, \exists x^\word . A(x) \seqar \Delta }{

											\vltr{\pi'}{ \Gamma , A(a),  \word(a) \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

										}

									}

									\]

									then $\vec f^{\pi}$ is exactly the same as $\vec f^{\pi'}$.

											Suppose $\pi$ ends with a $\cut$ step:

											\[

											\vlderivation{

												\vliin{\cut}{}{\Gamma , \Sigma \seqar \Delta , \Pi}{

													\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

												}{

												\vltr{\pi_2}{\Sigma , A \seqar \Pi}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

											}

										}

										\]

										We have two cases. First, if $A$ is free of modalities, then $\type (A)$ consists of only safe inputs. Therefore we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y, \vec z)$ from $\pi_1$ and $\pi_2 $ respectively, such that $\type(\Gamma) = (\vec u ; \vec x)$, $\type(\Sigma) = (\vec v ; \vec y )$ and $\type (A) = (;\vec z)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ as before, and we define $\vec f^\pi$ as follows:

										\[

										\vec f^\pi ( \vec u , \vec v ; \vec x, \vec y)

										\quad := \quad

										\left(

										\vec g^\Delta (\vec u ; \vec x)

										,

										\vec h ( \vec v ; \vec y , \vec g^A ( \vec u ; \vec x ) )

										\right)

										\]

										Notice that all safe inputs on the left occur hereditarily safe on the right, and so these expressions are definable in BC by Prop.~\ref{prop:bc-properties}.

											Suppose $\pi$ ends with a $\lefrul{\cntr}$ step,

												\[

												\vlderivation{

													\vlin{\lefrul{\cntr}}{}{ !A , \Gamma \seqar \Delta }{

														\vltr{\pi'}{  !A, !A , \Gamma \seqar \Delta}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

													}

												}

												\]

												so we have functions $\vec f' ( \vec u^1, \vec u^2 , \vec v ; \vec x)$, with $\vec u^1$ and $\vec u^2$ corresponding to the two copies of $!A$ in the conclusion of $\pi'$ and $\type (\Gamma) = (\vec v; \vec x)$.

										%		(Recall that the typing corresponding to $!$ means that all inputs for each $!A$ are normal).

												We define $\vec f^\pi$ by duplicating the arguments for $!A$:

												\[

												\vec f^\pi (\vec u , \vec v ; \vec x)

												\quad := \quad

												\vec f' (\vec u, \vec u , \vec v ; \vec x)

												\]

%														\begin{proof}

%															[Proof of Thm.~\ref{thm:main-result}]

%															%		[Proof sketch]

%															By Thm.~\ref{thm:free-cut-elim} and Lemma~\ref{lemma:spec-norm-form} we have a free-cut free proof $\pi$ in $\closure{\eqspec} \cup \arith$ of $!\word (\vec x ) \seqar \word (f (\vec x))$. By Lemma~\ref{lemma:witness-invariant} above this means that $\vec a = \vec x \cimp f^\pi (\vec a) = f(\vec x)$ is true in any model of $\qfindth$ satisfying $\eqspec$ and $\eqspec^\pi$.

%															%		Since some model must exist by coherence (cf.\ Prop.~\ref{prop:eq-spec-model}), we have that

%															Using the fact that $\eqspec \cup \eqspec^\pi$ is coherent we can construct such a model, similarly to Prop.~\ref{prop:eq-spec-model}, which will contain $\Word$ as an initial segment, in which we must have $f^\pi (\vec x) = f (\vec x)$ for every $\vec x \in \Word$, as required.\todo{polish}

%														\end{proof}