From: Enrico Tassi Date: Tue, 8 Nov 2005 08:56:32 +0000 (+0000) Subject: added some stuff on inductive types X-Git-Tag: V_0_7_2_3~109 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1b7ffcde9dce2848b36a28eeb73c5c28c4f901ad;p=helm.git added some stuff on inductive types --- diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex index 2766e16ff..9a1f4ec25 100644 --- a/helm/papers/system_T/t.tex +++ b/helm/papers/system_T/t.tex @@ -13,6 +13,7 @@ \renewcommand{\star}{\ast} \newcommand{\one}{\mathbb{1}} \renewcommand{\times}{\cdot} +\newcommand{\ind}{Ind(X)} \title{Modified Realizability and Inductive Types} \author{...} @@ -149,12 +150,13 @@ This paper is the first step in this direction. \section{Extraction} +We have to extend systeem T with inductive types (and they recursors). \begin{itemize} \item $\sem{A} = 1$ 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.P} = \N \to \sem{P}$ -\item $\sem{\exists x.P} = \N \times \sem{P}$ +\item $\sem{\forall x:T.P} = T \to \sem{P}$ +\item $\sem{\exists x:T.P} = T \times \sem{P}$ \end{itemize} definition. @@ -300,9 +302,105 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$. equal to the second number. So $$\lambda \_:\N. \lambda \_:\N. \star \R \forall x,y.x+S(y)=S(x+y)$$. - \end{itemize} +\section{Inductive types} +The notation we wwill 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 +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 +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$ + +\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...). + + +\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)$. +\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 +\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)$. +\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 +\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)$. +\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 +\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{...}$ + + + + + + \begin{thebibliography}{} \bibitem{Girard86}G.Y.Girard. The system F of variable types, fifteen years later. Theoretical Computer Science 45, 1986.