diff options
| -rw-r--r-- | controle-20240126.tex | 126 |
1 files changed, 120 insertions, 6 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex index 0e3c269..fa0ed60 100644 --- a/controle-20240126.tex +++ b/controle-20240126.tex @@ -106,7 +106,7 @@ et $3$ points par exercice et environ $0.75$ points par question du problème. \ifcorrige -Ce corrigé comporte \textcolor{red}{à remplir} pages (page de garde incluse). +Ce corrigé comporte 13 pages (page de garde incluse). \else Cet énoncé comporte 7 pages (page de garde incluse). \fi @@ -202,11 +202,50 @@ que programme (i.e., le comportement du programme associé à la preuve par la correspondance de Curry-Howard). \begin{corrige} -\textcolor{red}{Corrigé de cet exercice à écrire. Ce qui suit est un - résumé.} Le $\lambda$-terme est $\lambda(x:A).\, -\lambda(k:A\Rightarrow B).\, k x$, et le programme transforme $x$ en -la fonction qui applique une fonction $k$ à $x$, ou, ce qui revient au -même, il prend successivement $x$ et $k$ et applique $k$ à $x$. +Voici une preuve complète écrite dans le style « drapeau » : +\bgroup\normalsize +\begin{footnotesize} +\begin{flagderiv}[exercice-2-proof] +\assume{hypa}{A}{} +\assume{hypaib}{A\Rightarrow B}{} +\step{concb}{B}{$\Rightarrow$Élim sur \ref{hypaib} et \ref{hypa}} +\conclude{subconc}{(A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{concb}} +\conclude{mainconc}{A\Rightarrow (A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{subconc}} +\end{flagderiv} +\end{footnotesize} +\egroup + +La voici écrite sous forme d'arbre de preuve : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{A,\; A\Rightarrow B \vdash A\Rightarrow B}\\ +\inferrule*[Right={Ax}]{ }{A,\; A\Rightarrow B \vdash A} +}{A, A\Rightarrow B \vdash B} +}{A \vdash (A\Rightarrow B) \Rightarrow B} +}{\vdash A\Rightarrow (A\Rightarrow B) \Rightarrow B} +\] +\end{footnotesize} +ou, si on veut donner des noms aux hypothèses et marquer tous les +termes de preuve intermédiaires : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; k:A\Rightarrow B}\\ +\inferrule*[Right={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; x:A} +}{x:A,\; k:A\Rightarrow B\; \vdash\; kx:B} +}{x:A \; \vdash \; \lambda(k:A\Rightarrow B).\,kx\; :\; (A\Rightarrow B) \Rightarrow B} +}{\vdash\; \lambda(x:A).\, \lambda(k:A\Rightarrow B).\,kx\; :\; A\Rightarrow (A\Rightarrow B) \Rightarrow B} +\] +\end{footnotesize} +Le $\lambda$-terme est donc $\lambda(x:A).\, \lambda(k:A\Rightarrow +B).\, k x$, et le programme transforme $x$ en la fonction qui applique +une fonction $k$ à $x$, ou, ce qui revient au même, il prend +successivement $x$ et $k$ et applique $k$ à $x$. \end{corrige} @@ -442,6 +481,81 @@ formule proposée avait été démontrable, on aurait trouvé tout $\mathbb{R}^2$ (par \emph{correction} de la sémantique des ouverts) : ce n'est pas le cas, donc la formule n'est pas démontrable. +\begin{center} +\lineskip=1explus5ex +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $U$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $V$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (1.5,0) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $W$ +\end{tabular} +\penalty-1000 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (1.5,0) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg U$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (-0.866,1.5) -- (1.5,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg V$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- (-1.5,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg W$ +\end{tabular} +\end{center} + \emph{Sémantique de la réalisabilité :} Supposons qu'il existe un \emph{même} programme $e$ qui réalise la formule qu'on considère quelles que soient les parties $P,Q,R \subseteq \mathbb{N}$ mises à la |