From 3c5dd9fd8a3b5f429a27f4f91537362be53848f9 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 22 Jan 2024 12:39:51 +0100
Subject: An exercise on simple reading of lambda-terms.

---
 controle-20240126.tex | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 6c40a27..b48ed48 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -107,6 +107,54 @@ Git: \input{vcline.tex}
 \pagebreak
 
 
+%
+%
+%
+
+\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}
+
+
 %
 %
 %
-- 
cgit v1.2.3