diff options
Diffstat (limited to 'controle-20240126.tex')
| -rw-r--r-- | controle-20240126.tex | 28 |
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} + % % % |