\documentclass[a4paper]{article}
\pagestyle{headings}
%\usepackage{graphicx}
-\usepackage{amssymb,amsmath,mathrsfs}
+\usepackage{amssymb,amsmath,mathrsfs,stmaryrd,amsthm}
%\usepackage{hyperref}
%\usepackage{picins}
-\newcommand{\sem}[1]{[\![ #1 ]\!]}
+\newcommand{\semT}[1]{\ensuremath{\llbracket #1 \rrbracket}}
+\newcommand{\sem}[1]{\llbracket \ensuremath{#1} \rrbracket}
\newcommand{\R}{\;\mathscr{R}\;}
\newcommand{\N}{\,\mathbb{N}\,}
\newcommand{\NT}{\,\mathbb{N}\,}
\newcommand{\NH}{\,\mathbb{N}\,}
\renewcommand{\star}{\ast}
-\newcommand{\one}{\mathbb{1}}
-\renewcommand{\times}{\cdot}
+\renewcommand{\vec}{\overrightarrow}
+\newcommand{\one}{\mathscr{1}}
+\newcommand{\mult}{\cdot}
\newcommand{\ind}{Ind(X)}
+\newcommand{\Xind}{\ensuremath{X_{ind}}}
+\renewcommand{\|}{\ensuremath{\quad | \quad}}
+\newcommand{\triUP}{\ensuremath{\Delta}}
+\newcommand{\triDOWN}{\ensuremath{\nabla}}
+\newcommand{\Rx}{\ensuremath{R_X}}
+
+\newtheorem{thm}{Theorem}[subsection]
+
\title{Modified Realizability and Inductive Types}
\author{...}
...
\end{abstract}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
The characterization of the provable recursive functions of
Peano Arithmetic as the terms of system T is a well known
prove that the Induction Principle is realized by the recursor $R$
of system $T$ you catch a sudden gleam of understanding in the
students eyes; usually, the same does not happen when you show, say,
-that the ``forgetful'' intrepretation of the higher order predicate defining
+that the ``forgetful'' interpretation of the higher order predicate defining
the natural numbers is the system $F$ encoding
$\forall X.(X\to X) \to X \to X$ of $\N$.
Moreover, after a first period of enthusiasm, the impredicative
substantially prevent a really neat theoretical exposition (at present,
it does not
even exists a truly complete consistency proofs covering all aspects
-of such systems); moreover, not eveybody may be interested in all the features
+of such systems); moreover, not everybody may be interested in all the features
offered by these frameworks, from polymorphism to types depending on
proofs. Our program is to restart the analysis of logical systems with
primitive inductive types in a smooth way, starting form first order
logic and adding little by little small bits of logical power.
This paper is the first step in this direction.
-
-
-
-
-
-
-
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Heyting's arithmetics}
{\bf Axioms}
\begin{itemize}
-
\item $nat\_ind: P(0) \to (\forall x.P(x) \to P(S(x))) \to \forall x.P(x)$
\item $ex\_ind: (\forall x.P(x) \to Q) \to \exists x.P(x) \to Q$
\item $ex\_intro: \forall x.(P \to \exists x.P)$
\item $injS: \forall x,y.S(x) = S(y) \to x=y$
\item $plus\_O:\forall x.x+0=x$
\item $plus\_S:\forall x,y.x+S(y)=S(x+y)$
-\item $times\_O:\forall x.x\times0=0$
-\item $times\_S:\forall x,y.x\times S(y)=x+(x\times y)$
+\item $times\_O:\forall x.x\mult0=0$
+\item $times\_S:\forall x,y.x\mult S(y)=x+(x\mult y)$
\end{itemize}
\noindent
{\bf Inference Rules}
+say that ax:AX refers to the previous Axioms list...
+
+\[
+ (Proj)\hspace{0.2cm} \Gamma, x:A, \Delta \vdash x:A
+ \hspace{2cm}
+ (Const)\hspace{0.2cm} \Gamma \vdash ax : AX
+\]
+
\[
- (\to_i)\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
- (\to_e)\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
+ (\to_i)\hspace{0.2cm}\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} \hspace{2cm}
+ (\to_e)\hspace{0.2cm}\frac{\Gamma \vdash M: A \to Q \hspace{1cm}\Gamma \vdash N: A}
{\Gamma \vdash M N: Q}
\]
%\]
\[
- (\forall_i)\frac{\Gamma \vdash M:P}{\Gamma \vdash
+ (\forall_i)\hspace{0.2cm}\frac{\Gamma \vdash M:P}{\Gamma \vdash
\lambda x:\N.M: \forall x.P}(*) \hspace{2cm}
- (\forall_e)\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+ (\forall_e)\hspace{0.2cm}\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
\]
\section{Extraction}
-We have to extend systeem T with inductive types (and they recursors).
-\begin{itemize}
-\item $\sem{A} = 1$ if A is atomic
+The formulae to types translation function
+$\sem{\cdot}$ takes in input formulae in HA and returns types in T.
+
+\begin{enumerate}
+\item $\sem{A} = \one$ if A is atomic
\item $\sem{A \land B} = \sem{A}\times \sem{B}$
\item $\sem{A \to B} = \sem{A}\to \sem{B}$
-\item $\sem{\forall x:T.P} = T \to \sem{P}$
-\item $\sem{\exists x:T.P} = T \times \sem{P}$
-\end{itemize}
+\item $\sem{\forall x:\N.P} = \N \to \sem{P}$
+\item $\sem{\exists x:\N.P} = \N \times \sem{P}$
+\end{enumerate}
definition.
-For any type T of system T $\bot_T: 1 \to T$ is inuctively defined as follows:
+For any type T of system T $\bot_T: \one \to T$ is inductively defined as follows:
\begin{enumerate}
-\item $\bot_1 = \lambda x:1.x$
-\item $\bot_N = \lambda x:1.0$
-\item $\bot_{U\times V} = \lambda x:1.<\bot_{U} x,\bot_{V} x>$
-\item $\bot_{U\to V} = \lambda x:1.\lambda \_:U. \bot_{V} x$
+\item $\bot_\one = \lambda x:\one.x$
+\item $\bot_N = \lambda x:\one.0$
+\item $\bot_{U\times V} = \lambda x:\one.<\bot_{U} x,\bot_{V} x>$
+\item $\bot_{U\to V} = \lambda x:\one.\lambda \_:U. \bot_{V} x$
\end{enumerate}
\begin{itemize}
\item $\sem{snd} = \pi_2$
\item $\sem{conj} = \lambda x:\sem{P}.\lambda y:\sem{Q}.<x,y>$
\item $\sem{false\_ind} = \bot_{\sem{Q}}$
-\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:1.\star$
-\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:1.\star$
+\item $\sem{discriminate} = \lambda \_:\N.\lambda \_:\one.\star$
+\item $\sem{injS}= \lambda \_:\N. \lambda \_:\N.\lambda \_:\one.\star$
\item $\sem{plus\_O} = \sem{times\_O} = \lambda \_:\N.\star$
\item $\sem{plus\_S} = \sem{times_S} = \lambda \_:\N. \lambda \_:\N.\star$
\end{itemize}
In the case of structured proofs:
\begin{itemize}
-\item $\sem{M N} = \sem{M} \sem{N}$
-\item $\sem{\lambda x:A.M} = \lambda x:\sem{A}.\sem{M}$
-\item $\sem{\lambda x:\N.M} = \lambda x:\N.\sem{M}$
-\item $\sem{M t} = \sem{M} \sem{t}$
+\item $\semT{M N} = \semT{M} \semT{N}$
+\item $\semT{\lambda x:A.M} = \lambda x:\sem{A}.\semT{M}$
+\item $\semT{\lambda x:\N.M} = \lambda x:\N.\semT{M}$
+\item $\semT{M t} = \semT{M} \semT{t}$
\end{itemize}
\section{Realizability}
-The realizability relation is a relation $f \R P$ where $f: \sem{P}$.
+The realizability relation is a relation $f \R P$ where $f: \sem{P}$, and
+$P$ is a closed formula.
In particular:
\begin{itemize}
\item $\neg (\star \R \bot)$
\item $f \R (\forall x.P)$ iff for any natural number $n$ $(f n) \R P[\underline{n}/x]$
\item $<n,g> \R (\exists x.P)$ iff $g \R P[\underline{n}/x]$
\end{itemize}
+%We need to generalize the notion of realizability to sequents.
+%Given a sequent $B_1, \ldots, B_n \vdash A$ with free variables in
+%$\vec{x} = x_1,\ldots, x_m$, we say that $f \R B1, \ldots, B_n \vdash A$ iff
+%forall natural numbers $n_1, \ldots, n_m$,
+%if forall $i \in {1,\ldots,n}$
+%$m_i \R B_i[\vec{\underline{n}}/\vec{x}]$ then
+%$$f <m_1, \ldots, m_n> \R A[\vec{\underline{n}}/\vec{x}]$$.
+%
+\noindent
+We need to generalize the notion of realizability to sequents.\\
+Let $\vec{x} = FV_{\N}( B_1, \ldots, B_n, P)$ a vector of variables of type
+$\N$ that occur free in $B_1, \ldots, B_n, P$. Let $\vec{b:B}$ the vector
+$b_1:B_1, \ldots, b_n:B_n$.\\
+We say that $f \R B_1, \ldots, B_n \vdash A:P$ iff
+$$\lambda \vec{x:\N}. \lambda \vec{b:B}.f \R
+\forall \vec{x}. B_1 \to \ldots \to B_n \to P$$
+Note that $\forall \vec{x}. B_1 \to \ldots \to B_n \to P$ is a closed formula,
+so we can use the previous definition of realizability on it.
\noindent
We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
$f$ is a function such that forall $n$ and for all $m \R P[\underline{n}/x]$
then $f~n~m \R Q$ (note that $x$ is not free in $Q$ so $[\underline{n}/x]$
affects only $P$).\\
- Exapanding the definition of $\underline{ex\_ind}$, $fst$
+ Expanding the definition of $\underline{ex\_ind}$, $fst$
and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
since $g_p \R P[\underline{n_p}/x]$.
\item $ex\_intro$.
We must prove that
$$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
- that leads to prove that foreach n
+ that leads to prove that for each n
$\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
Evaluating the substitution we have
$\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
$<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
\item $fst$.
- Wehave to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
+ We have to prove that $\pi_1 \R P \land Q \to P$, that is equal to proving
that for each $m \R P \land Q$ then $\pi_1~m \R P$ .
$m$ must be a couple $<f_m,g_m>$ such that $f_m \R P$ and $g_m \R Q$.
So we conclude that $\pi_1~m$ reduces to $f_m$ that is in relation $\R$
We have to prove that
$$\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y> \R P \to Q \to P \land Q$$
Following the definition of $\R$ we have to show that
- foreach $m \R P$ and foreach $n \R Q$ then
+ for each $m \R P$ and for each $n \R Q$ then
$(\lambda x:\sem{P}. \lambda y:\sem{Q}.<x,y>)~m~n \R P \land Q$.\\
This is the same of $<m,n> \R P \land Q$ that is verified since
$m \R P$ and $n \R Q$.
\item $injS$.
We have to prove that for each $n_1$ and $n_2$\\
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R
+ $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2 \R
(S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
We assume that $m \R S(n_1)=S(n_2)$ and we have to show that
- $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2~m$ that reduces to
+ $\lambda \_:\N. \lambda \_:\N.\lambda \_:\one.*~n_1~n_2~m$ that reduces to
$*$ is in relation $\R$ with $n_1=n_2$. Since in the standard model of
natural numbers $S(n_1)=S(n_2)$ implies $n_1=n_2$ we have that
$* \R n_1=n_2$.
\item $times\_O$.
Since in the standard model for natural numbers $0$ is the absorbing element
- for multiplication $\lambda \_:\N.\star \R \forall x.x \times 0 = x$.
+ for multiplication $\lambda \_:\N.\star \R \forall x.x \mult 0 = 0$.
\item $times\_S$.
In the standard model of natural numbers the multiplications of two
\end{itemize}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Inductive types}
-The notation we wwill use is similar to the one used in
+The notation we will use is similar to the one used in
\cite{Werner} and \cite{Paulin89} but we prefer
-giving a label to each contructor and use that label instead of the
+giving a label to each constructor and use that label instead of the
longer $Constr(n,\ind\{\ldots\})$ to indicate the $n^{th}$ constructor.
We adopt the vector notation to make things more readable.
-$\overrightarrow{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
-be equal to 0 (we use $m_1~\overrightarrow{m}$ when we want to give a
+$\vec{m}$ has to be intended as $m_1~\ldots~m_n$ where $n$ may
+be equal to 0 (we use $m_1~\vec{m}$ when we want to give a
name to the first $m$ and assert $n>0$). If the vector notation is
used inside an arrow type it has a slightly different meaning,
-$A \to \overrightarrow{B} \to C$ is a shortcut for
-$A \to B_1 \to \ldots \to B_n \to C$
+$A \to \vec{B} \to C$ is a shortcut for
+$A \to B_1 \to \ldots \to B_n \to C$.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Extensions to the logic framework}
+To talk about arbitrary inductive types (and not hard coded natural numbers) we
+have to extend a bit our framework.
+
+First we admit quantification over inductive types $T$, thus $\forall x:T.A$
+and $\exists x:T.A$ are allowed. Then rules 4 and 5 of the $\sem{\cdot}$
+definition are replaced by $\sem{\forall x:T.P} = T \to \sem{P}$ and
+$\sem{\exists x:T.P} = T \times \sem{P}$.
+
+For each inductive type we will describe the formation rules and the
+corresponding induction principle schema.
+
+Symmetrically we have to extend System T with arbitrary inductive types and
+we will see how theyr recursors are defined in the following sections.
+
+The definition of $\R$ is modified substituting each occurrence of $\N$ with
+a generic inductive type $T$.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Type definition}
$$\ind\{c_1:C(X); \ldots ; c_n:C(X)\}$$
-$$C(X) ::=
-X \quad | \quad
-\forall m:T.C(X) \quad | \quad
-t \to C(X)$$
-In the second case we need $(X \notin FV(T))$, while in the third we
-need that POS(X,t) holds.
-POS(X,t) is true iff t = X (POS has a meaning only for Higher Order...).
-
+$$C(X) ::= X \| T \to C(X) \| X \to C(X)$$
+In the second case we mean $T \neq X$.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Induction principle}
The induction principle for an inductive type $X$ and a predicate $Q$
is a constant with the following type
-$$X_{ind}:\overrightarrow{\vartriangle\{C(X), c\}} \to \forall t:X.Q(x)$$
-$\vartriangle$ takes a constructor type and the is defined by recursion on $C(X)$.
+$$\Xind:\vec{\triUP\{C(X), c\}} \to \forall t:X.Q(x)$$
+$\triUP$ takes a constructor type $C(X)$ and a term $c$ (initially $c$ is a
+constructor of X, and $c:C(X)$) and is defined by recursion as follows:
\begin{eqnarray}
-\vartriangle\{C(X), c\} & = & Q(c) \nonumber\\
-\vartriangle\{\forall t:T.C(X), c\} & = &
- \forall m:T.\vartriangle\{C(X),c~m\} \nonumber\\
-\vartriangle\{t \to C(X), c\} & = &
- \forall t:X.Q(t) \to \vartriangle\{C(X), c~t\} \nonumber
+\triUP\{X, c\} & = & Q(c) \nonumber\\
+\triUP\{T \to C(X), c\} & = &
+ \forall m:T.\triUP\{C(X),c~m\} \nonumber\\
+\triUP\{X \to C(X), c\} & = &
+ \forall t:X.Q(t) \to \triUP\{C(X), c~t\} \nonumber
\end{eqnarray}
-
+%%%%%%%%%%%%%%%%%%%%%
\subsection{Recursor}
\subsubsection{Type}
-The type of the recursor $R_X$ on an inductive type $X$ is
-$$R_X : \overrightarrow{\square\{C(X)\}} \to X \to \alpha$$
-$\square$ is defined by recursion on the contructor type $C(X)$.
+The type of the recursor $\Rx$ on an inductive type $X$ is
+$$\Rx : \vec{\square\{C(X)\}} \to X \to \alpha$$
+$\square$ is defined by recursion on the constructor type $C(X)$.
\begin{eqnarray}
\square\{X\} & = & \alpha \nonumber \\
-\square\{\forall m:T.C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
-\square\{t \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
+\square\{T \to C(X)\} & = & T \to \square\{C(X)\}\nonumber \\
+\square\{X \to C(X)\} & = & X \to \alpha \to \square\{C(X)\}\nonumber
\end{eqnarray}
\subsubsection{Reduction rules}
We say that
-$$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m}) \leadsto
-\triangledown\{C(X)_i, f_i, \overrightarrow{m}\}$$
-$\triangledown$ is defined by recursion on the constructor type $C(X)$.
+$$\Rx~\vec{f}~(c_i~\vec{m}) \leadsto
+\triDOWN\{C(X)_i, f_i, \vec{m}\}$$
+$\triDOWN$ takes a constructor type $C(X)$, a term $f$
+(of type $\square\{C(X)\}$) and is defined by recursion as follows:
\begin{eqnarray}
-\triangledown\{X, f, \overrightarrow{m}\} & = & f\nonumber \\
-\triangledown\{\forall m:T.C(X), f, m_1~\overrightarrow{m}\} & = &
- \triangledown\{C(X), f~m_1, \overrightarrow{m}\}\nonumber \\
-\triangledown\{t \to C(X), f, m_1~\overrightarrow{m}\} & = &
- \triangledown\{C(X), f~m_1~(R_X~\overrightarrow{f}~m_1),
- \overrightarrow{m}\}\nonumber
+\triDOWN\{X, f, \} & = & f\nonumber \\
+\triDOWN\{T \to C(X), f, m_1~\vec{m}\} & = &
+ \triDOWN\{C(X), f~m_1, \vec{m}\}\nonumber \\
+\triDOWN\{X \to C(X), f, m_1~\vec{m}\} & = &
+ \triDOWN\{C(X), f~m_1~(\Rx~\vec{f}~m_1),
+ \vec{m}\}\nonumber
\end{eqnarray}
-
-\subsection{$R_X : \sem{X_{ind}}$ and $R_X\R X_{ind}$}
-We have to compare the definition of $\square$ and $\vartriangle$
-since thay play the same role in constructing respectively $R_X$ and
-$X_{ind}$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem$
-function to each righ side of the $\vartriangle$ definition we obtain
-exactly $\square$. The last two elements of the arrows $R_X$ and
-$X_{ind}$ are again the same up to $\sem$.
-
-questa non va bene, il caso base e' se il tipo del costruttore usa
-solo le prime 2 regole di delta, quello induttivo se usa ANCHE la
-terza...
-
-To prove that $R_X\R X_{ind}$ we must assume that for each $i$ index
-of a constructor of $X$, $f_i \R \vartriangle\{C(X)_i, c_i\}$ and we
-have to proove that for each $t:X$
-$$R_X~\overrightarrow{f}~t \R Q(t)$$.
-We proceede by induction on the type of the head constructor $c_i$ in $t$.
-The first base case is $c_i=X$ that, according to $\triangledown$,
-reduces in one
-step to $f_i$ and by hypothesis we have $f_i \R \vartriangle\{X,
-c_i\}$. Unfolding $\vartriangle$ we have $f_i \R Q(c_i)$. The second
-base case is $c_i=\overrightarrow{\forall t:T}.X$ and is analoug to
-the first case.\\
-The inductive step is when we have one or more recursive aruments in
-$c_i$ and the induction hypothesis is that for each recursve argument
-$m$, $R_X~\overrightarrow{f}~m \R X \to Q$. Since $f_i \R
-\vartriangle\{C(X)_i, c_i\}$ and
-$R_X~\overrightarrow{f}~(c_i~\overrightarrow{m})$ reduces to
-$f_i~\overrightarrow{...}$
-
-
-
-
-
-
+We assume $\Rx~\vec{f}~(c_i~\vec{m})$ is well typed, so in the first case we
+can omit $\vec{m}$ since it is an empty sequence.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Realizability of the induction principle}
+Once we have inductive types and their induction principle we want to show that
+the recursor $\Rx$ realizes $\Xind$, that is that $\Rx$ has type
+$\sem{\Xind}$ and is in relation $\R$ with $\Xind$.
+
+\begin{thm}$\Rx : \sem{\Xind}$\end{thm}
+\begin{proof}
+We have to compare the definition of $\square$ and $\triUP$
+since they play the same role in constructing respectively the types of
+$\Rx$ and
+$\Xind$. If we assume $\alpha = \sem{Q}$ and we apply the $\sem{\cdot}$
+function to each right side of the $\triUP$ definition we obtain
+exactly $\square$. The last two elements of the arrows $\Rx$ and
+$\Xind$ are again the same up to $\sem{\cdot}$.
+\end{proof}
+
+\begin{thm}$\Rx\R \Xind$\end{thm}
+\begin{proof}
+To prove that $\Rx\R \Xind$ we must assume that for each $i$ index
+of a constructor of $X$, $f_i \R \triUP\{C(X)_i, c_i\}$ and we
+have to prove that for each $t:X$
+$$\Rx~\vec{f}~t \R Q(t)$$
+\noindent
+We proceed by induction on the structure of $t$.
+\\
+The base case is when the
+type of the head constructor of $t$ has no recursive arguments (i.e. the type
+is generated using only the first two rules $C(X)$), so
+$(\Rx~\vec{f}~(c_i~\vec{m}))$ reduces in one step to $(f_i~\vec{m})$. $f_i$
+realizes $\triUP\{C(X)_i, c_i\}$ by assumption and since we are in the base
+case $\triUP\{C(X)_i, c_i\}$ is of the form $\vec{\forall t:T}.Q(c_i~\vec{t})$.
+Thus $f_i~\vec{m} \R Q(c_i~\vec{m})$.
+\\
+In the induction step we have as induction hypothesis that each recursive
+argument $t_i$ of the head constructor $c_i$ is realized by $r_i\equiv
+\Rx~\vec{f}~t_i$. By the third rule of $\triDOWN$ we obtain the reduct
+$f_i~\vec{m}~\vec{t~r}$ (here we write first all the non recursive arguments,
+then all the recursive one. In general they can be mixed and the proof is
+exactly the same but the notation is really heavier). We know by hypothesis
+that $f_i \R \triUP\{C(X)_i, c_i\} \equiv \vec{\forall m:T}.\vec{\forall
+t:X.Q(t)} \to Q(c_i~\vec{m}~\vec{t})$, thus $f_i~\vec{m}~\vec{t~r} \R
+Q(c_i~\vec{m}~\vec{t})$.
+\end{proof}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thebibliography}{}
\bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen
years later. Theoretical Computer Science 45, 1986.
projects / helm.git / commitdiff