diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 57 |
1 files changed, 53 insertions, 4 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 5083da9..7e4c691 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1342,6 +1342,38 @@ hypothèses $P_1,\ldots,P_r$, on a $Q$ ». \end{frame} % \begin{frame} +\frametitle{Le calcul propositionnel intuitionniste : connecteurs} + +\itempoint Chaque connecteur logique a des règles +d'\textbf{introduction} permettant de \alert{démontrer} ce connecteur, +et des règles d'\textbf{élimination} permettant de l'\alert{utiliser}. + +\bigskip + +En français, et un peu informellement : +\begin{itemize} +\item pour introduire $\Rightarrow$ : on démontre $Q$ \alert{sous + l'hypothèse} $P$, ce qui donne $P\Rightarrow Q$ (hypothèse + déchargée) ; +\item pour éliminer $\Rightarrow$ : si on a $P\Rightarrow Q$ et $P$, + on a $Q$ (\textit{modus ponens}) ; +\item pour introduire $\land$ : on démontre $Q_1$ et $Q_2$, ce qui + donne $Q_1\land Q_2$ ; pour l'éliminer : si on a $Q_1 \land Q_2$ on + en tire $Q_1$ resp. $Q_2$ ; +\item pour introduire $\lor$ : on démontre $Q_1$ et $Q_2$, ce qui + donne $Q_1\land Q_2$ ; +\item pour éliminer $\lor$ : si on a $P_1 \lor P_2$, on démontre $Q$ + successivement sous les hypothèses $P_1$ et $P_2$, ce qui donne $Q$ + (hypothèses déchargées) ; +\item pour introduire $\top$, c'est trivial, et on ne peut pas + l'éliminer ; +\item pour éliminer $\bot$, on tire la conclusion qu'on veut + (\textit{ex falso quodlibet}), et on ne peut pas l'introduire. +\end{itemize} + +\end{frame} +% +\begin{frame} \frametitle{Le calcul propositionnel intuitionniste : règles} Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$. @@ -1387,6 +1419,13 @@ $\bot$ \label{example-propositional-proofs} \frametitle{Exemples de démonstrations} +Indiquant à côté de chaque barre une abréviation de la règle utilisée +(« $\Rightarrow$Int » pour introduction de $\Rightarrow$, +« $\land$Élim$_2$ » pour la 2\textsuperscript{e} règle d'élimination +de $\land$, etc.) : + +\bigskip + {\footnotesize \[ \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{ @@ -1429,11 +1468,11 @@ $\bot$ \frametitle{Présentation différente} On peut aussi n'écrire que les conclusions (partie droite du -signe $\vdash$), à condition d'indiquer pour chaque hypothèse +signe « $\vdash$ »), à condition d'indiquer pour chaque hypothèse déchargée à quel endroit elle l'a été (ceci sacrifie de la lisibilité pour un gain de place) : -\bigskip +\medskip {\footnotesize \[ @@ -1451,7 +1490,7 @@ pour un gain de place) : \] \par} -\bigskip +\medskip {\footnotesize \[ @@ -1471,6 +1510,12 @@ pour un gain de place) : \] \par} +\medskip + +{\footnotesize\textbf{N.B.} : une même hypothèse \emph{peut} être + déchargée à plusieurs endroits ($u$ dans le 1\textsuperscript{er} + exemple).\par} + \end{frame} % \begin{frame} @@ -1511,7 +1556,7 @@ Présentation « drapeau », plus proche de l'écriture naturelle, commode \frametitle{Quelques tautologies du calcul propositionnel intuitionniste} \itempoint Lorsque $\vdash P$ (sans hypothèse), on dit que $P$ est -\textbf{valide} dans le calcul propositionnel intuitionniste, ou est +\textbf{valable} dans le calcul propositionnel intuitionniste, ou est une \textbf{tautologie} de celui-ci. \medskip @@ -2312,8 +2357,12 @@ $\Rightarrow$Int de (1) dans (5). » \end{frame} % % TODO: +% - discussion de la négation et double négation % - substitution des variables propositionnelles par des formules % - substitution d'équivalences +% - présentation en calcul des séquents +% - élimination des coupures % - Kripke +% - inférence de type de Hindley-Milner % \end{document} |