diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index d2d9bd0..d2ef3ef 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -947,6 +947,7 @@ Présentation avec les seules conclusions : \end{frame} % \begin{frame} +\label{example-predicate-proof-as-lambda-term} \frametitle{Notation des preuves par des $\lambda$-termes} On reprend la preuve donnée aux transp. précédents : @@ -1129,4 +1130,101 @@ contexte). \end{frame} % +\begin{frame} +\frametitle{Curry-Howard pour la logique du premier ordre} + +\itempoint Il faut penser Curry-Howard dans le sens +preuve $\mapsto$ programme. + +\smallskip + +{\footnotesize (Faute de description précise de règles de typage on ne + peut pas espérer mieux ici.)\par} + +\medskip + +\itempoint Curry-Howard va mélanger le monde logique avec le monde des +individus. + +\medskip + +\itempoint On convertit les propositions en types : +\begin{itemize} +\item $\Rightarrow,\land,\lor,\top,\bot$ deviennent + $\rightarrow,\times,+,1,0$ comme en calcul propositionnel, +\item $\forall,\exists$ deviennent produits et sommes $\prod,\sum$ + paramétrés par $v:I$. +\end{itemize} + +\smallskip + +\itempoint On convertit preuves en programmes selon l'interprétation +fonctionnelle des notations données au +transp. \ref{natural-deduction-rules-with-quantifiers-and-notations}. + +\medskip + +\itempoint P.ex., la preuve de $(\exists x.\forall +y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))$ donnée +transp. \ref{example-predicate-proof-as-lambda-term} : +\[ +\lambda(u:\exists x.\forall y.B(x,y)).\; +\lambda(y':I).\; +(\texttt{match~}u\texttt{~with~}\langle x,v\rangle \mapsto +\langle x,vy'\rangle) +\] +devient un programme de type +\[ +(\sum_{x:I} \prod_{y:I} \, B(x,y)) \rightarrow +(\prod_{y':I} \sum_{x':I} \, B(x',y')) +\] + +\end{frame} +% +\begin{frame} +\frametitle{L'égalité au premier ordre} + +\itempoint En général on veut travailler en logique du premier ordre +\alert{avec égalité}. C'est-à-dire qu'on introduit une relation +binaire « $=$ » (notée de façon infixe) sujette aux \alert{axiomes} +suivants : +\begin{itemize} +\item réflexivité : $\textsf{refl} : \forall x.(x=x)$ +\item substitution : $\textsf{subst}_{(\lambda s.P(s))} : \forall + x.\forall y.((x=y) \Rightarrow P(x) \Rightarrow P(y))$ pour toute + formule $P(s)$ ayant une variable d'individu libre $s$. +\end{itemize} + +\medskip + +{\footnotesize \itempoint La logique du premier ordre montre ici ses + limites : on n'a pas le droit de quantifier sur $P(s)$ ni même + d'introduire $\lambda (s:I). P(s)$. Il faut donc comprendre qu'on a + un « schéma d'axiomes » de substitution, dont chaque + $\textsf{subst}_{(\lambda s.P(s))}$ est une instance (et $\lambda + s.P(s)$ une notation \textit{ad hoc}).\par} + +\medskip + +\itempoint Exemple de preuve : la symétrie $\forall x.\forall y.((x=y) +\Rightarrow (y=x))$ est prouvée en appliquant la substitution à $P(s)$ +valant « $s=x$ », donc par le $\lambda$-terme +\[ +\lambda (x:I). \, +\lambda (y:I). \, \lambda (u:(x=y)). \, \textsf{subst}_{(\lambda + s.s=x)} \, x \, y \, u \, (\mathsf{refl}\,x) +\] + +\medskip + +\itempoint Autre exemple : la transitivité $\forall x.\forall +y.\forall z. ((x=y) \Rightarrow (y=z) \Rightarrow (x=z))$ par +\[ +\lambda (x:I). \, \lambda (y:I). \, \lambda (z:I). \, \lambda +(u:(x=y)). \, \lambda (v:(y=z)). \, \textsf{subst}_{(\lambda s.x=s)} +\, y \, z \, v \, u +\] + +\end{frame} +% \end{document} |