summaryrefslogtreecommitdiffstats
path: root/controle-20240126.tex
diff options
context:
space:
mode:
Diffstat (limited to 'controle-20240126.tex')
-rw-r--r--controle-20240126.tex28
1 files changed, 25 insertions, 3 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex
index b48ed48..343c58c 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -113,6 +113,8 @@ Git: \input{vcline.tex}
\exercice
+(Dans cet exercice, on ne demande pas de justifier les réponses.)
+
\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
@@ -127,14 +129,25 @@ $\lambda$-calcul simplement typé enrichi de types produits ?)
\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: C\land\forall x. B(x))).\,
+\lambda(x:I).\,
+\langle (\pi_1 p),\,(\pi_2 p)x\rangle
+\]
+(Ici, $C$ est une variable de relation nullaire, c'est-à-dire une
+variable propositionnelle, $B$ est une variable de relation unaire, et
+$I$ est le symbole du type des individus.)
+
+\textbf{(3)} 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.)
+variable propositionnelle, et $B$ est une variable de relation
+unaire.)
\begin{corrige}
\textbf{(1)} Dans le contexte où $p$ a type $C\land(A\Rightarrow B)$
@@ -145,7 +158,15 @@ 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
+\textbf{(2)} On se place dans le contexte où $p$ a type $C\land
+\forall x. B(x)$ et $x$ est un individu. Alors $\pi_1 p$ a type $C$
+et $\pi_2 p$ a type $\forall z. B(z)$, si bien que $(\pi_2 p)x$ a type
+$B(x)$, et $\langle (\pi_1 p),\,(\pi_2 p)x\rangle$ a type $C\land
+B(x)$, donc l'expression dans son ensemble a type $(C\land \forall
+x. B(x)) \Rightarrow \forall x. (C\land B(x))$, i.e., elle représente
+une preuve de cette affirmation.
+
+\textbf{(3)} 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
@@ -155,6 +176,7 @@ x. B(x))$, i.e., elle représente une preuve de cette affirmation.
\end{corrige}
+
%
%
%