An exercise on simple reading of lambda-terms.

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