diff options
| -rw-r--r-- | controle-20240126.tex | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex index 6c40a27..b48ed48 100644 --- a/controle-20240126.tex +++ b/controle-20240126.tex @@ -113,6 +113,54 @@ Git: \input{vcline.tex} \exercice +\textbf{(1)} En calcul propositionnel intuitionniste, quelle est la +conclusion de la démonstration représentée par le $\lambda$-terme +suivant ? (Ou si on préfère : quel est le type de ce terme du +$\lambda$-calcul simplement typé enrichi de types produits ?) +\[ +\lambda(p: C\land(A\Rightarrow B)).\, +\lambda(h:A).\, +\langle (\pi_1 p),\,(\pi_2 p)h\rangle +\] +(Ici, $A,B,C$ sont des variables propositionnelles.) + +\textbf{(2)} En logique du premier ordre, quelle est la conclusion de +la démonstration représentée par le $\lambda$-terme suivant ? +\[ +\lambda(p: \exists x.(A\Rightarrow B(x))).\, +\lambda(h:A).\, +(\texttt{match~}p\texttt{~with~}\langle x,j\rangle +\mapsto \langle x,jh\rangle) +\] +(Ici, $A$ est une variable de relation nullaire, c'est-à-dire une +variable propositionnelle, $B$ est une variable de relation unaire, et +$x$ est une variable d'individu.) + +\begin{corrige} +\textbf{(1)} Dans le contexte où $p$ a type $C\land(A\Rightarrow B)$ +et $h$ a type $A$, on voit que $\pi_1 p$ a type $C$ et $\pi_2 p$ a +type $A\Rightarrow B$, si bien que $(\pi_2 p)h$ a type $B$, et le +couple $\langle (\pi_1 p),\,(\pi_2 p)h\rangle$ a type $C\land B$, donc +l'expression dans son ensemble a type $C\land(A\Rightarrow B) +\Rightarrow (A \Rightarrow C\land B)$, i.e., elle représente une +preuve de cette affirmation. + +\textbf{(2)} On se place dans le contexte où $p$ a type $\exists +x.(A\Rightarrow B(x))$ et $h$ a type $A$. Le \texttt{match} va +déstructurer $p$ en un $x$ individu et un $j$ de type $A\Rightarrow +B(x)$. Alors $jh$ a type $B(x)$, et $\langle x,jh\rangle$ a type +$\exists x.B(x)$. Donc l'expression dans son ensemble a type +$(\exists x.(A\Rightarrow B(x))) \Rightarrow (A \Rightarrow \exists +x. B(x))$, i.e., elle représente une preuve de cette affirmation. +\end{corrige} + + +% +% +% + +\exercice + En utilisant l'une quelconque (au choix) des sémantiques vues en cours pour le calcul propositionnel intuitionniste, montrer que la formule suivante n'est pas démontrable en calcul propositionnel |