diff options
| -rw-r--r-- | controle-20240126.tex | 71 |
1 files changed, 50 insertions, 21 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex index 0441add..740aaa1 100644 --- a/controle-20240126.tex +++ b/controle-20240126.tex @@ -81,9 +81,9 @@ feuille entre deux exercices). Les questions du problème dépendent les unes des autres, mais ont été rédigées de manière à ce que chacune donne toutes les informations -nécessaires pour passer à la suite. Mais comme les questions (du -problème) présentent une gradation approximative de difficulté, il est -recommandé de les traiter dans l'ordre. +nécessaires pour passer à la suite. Mais comme elles (les questions +du problème) présentent une gradation approximative de difficulté, il +est recommandé de les traiter dans l'ordre. La longueur du sujet ne doit pas effrayer : l'énoncé du problème est très long parce que des rappels ont été faits et que les questions ont @@ -101,13 +101,14 @@ L'usage des appareils électroniques est interdit. Durée : 3h -Barème \emph{approximatif} et \emph{indicatif} : $2.5$ points par -exercice et $0.75$ points par question du problème. +Barème \emph{approximatif} et \emph{indicatif} (sur $20$) : entre $2$ +et $3$ points par exercice et environ $0.75$ points par question du +problème. \ifcorrige -Ce corrigé comporte 12 pages (page de garde incluse). +Ce corrigé comporte \textcolor{red}{à remplir} pages (page de garde incluse). \else -Cet énoncé comporte 6 pages (page de garde incluse). +Cet énoncé comporte 7 pages (page de garde incluse). \fi \vfill @@ -189,13 +190,39 @@ pour terminer la démonstration). \exercice +Donner une démonstration en calcul propositionnel intuitionniste de la +formule suivante : +\[ +(A\Rightarrow B\Rightarrow C) \Rightarrow (B\Rightarrow A\Rightarrow C) +\] +On donnera la démonstration sous la forme qu'on préfère (arbre de +preuve, style drapeau, ou même simplement précisément écrite en +français), puis on donnera aussi un $\lambda$-terme de preuve. On +décrira ensuite brièvement ce que fait ce terme vu en tant que +programme (i.e., le comportement du programme associé à la preuve par +la correspondance de Curry-Howard). + +\begin{corrige} +\textcolor{red}{Corrigé de cet exercice à écrire. Ce qui suit est un + résumé.} Le $\lambda$-terme est $\lambda(f:A\Rightarrow +B\Rightarrow C).\, \lambda(y:B).\, \lambda(x:A).\, f x y$ et il +échange les deux arguments d'une fonction de deux variables donnée +sous forme curryfiée. +\end{corrige} + + +% +% +% + +\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 de -preuve suivant ? (Ou si on préfère : quel est le type de ce terme du -$\lambda$-calcul simplement typé enrichi de types produits, qu'on a -écrit en notations logiques ?) +\textbf{(1)} En calcul propositionnel intuitionniste, quel est +l'énoncé prouvé par le $\lambda$-terme de preuve suivant ? (Ou si on +préfère : quel est le type de ce terme du $\lambda$-calcul simplement +typé enrichi de types produits, qu'on a écrit en notations logiques ?) \[ \lambda(p: C\land(A\Rightarrow B)).\, \lambda(h:A).\, @@ -203,9 +230,8 @@ $\lambda$-calcul simplement typé enrichi de types produits, qu'on a \] (Ici, $A,B,C$ sont des variables propositionnelles.) -\textbf{(2)} En logique du premier ordre intuitionniste, quelle est la -conclusion de la démonstration représentée par le $\lambda$-terme de -preuve suivant ? +\textbf{(2)} En logique du premier ordre intuitionniste, quel est +l'énoncé prouvé par le $\lambda$-terme de preuve suivant ? \[ \lambda(p: C\land\forall x. B(x)).\, \lambda(x:I).\, @@ -215,9 +241,8 @@ preuve suivant ? 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 intuitionniste, quelle est la -conclusion de la démonstration représentée par le $\lambda$-terme de -preuve suivant ? +\textbf{(3)} En logique du premier ordre intuitionniste, quel est +l'énoncé prouvé par le $\lambda$-terme de preuve suivant ? \[ \lambda(p: \exists x.(A\Rightarrow B(x))).\, \lambda(h:A).\, @@ -271,6 +296,9 @@ $\lambda$-calcul non typé : syntaxe OCaml). Quel théorème du calcul propositionnel intuitionniste obtient-on de ceci par Curry-Howard ? +(Une réponse qui ne suit pas l'algorithme de Hindley-Milner mais qui +est néanmoins correcte vaudra une partie des points.) + \begin{corrige} Dans une première phase, on collecte les types et contraintes suivants : $f:\eta_1$, $z:\eta_2$, $fz : \eta_3$ avec $\eta_1 = @@ -349,8 +377,9 @@ la promesse qu'au moins deux d'entre elles sont vides : pour la réalisabilité, on pourra considérer une des parties valant $\mathbb{N}$ et les deux autres valant $\varnothing$ et constater qu'on ne peut pas réaliser les trois affectations à la fois, tandis -que pour la sémantique des problèmes finis, on pourra trois problèmes -ayant un seul candidat chacun mais un seul ayant une solution.) +que pour la sémantique des problèmes finis, on pourra considérer trois +problèmes ayant un seul candidat chacun mais un seul ayant une +solution.) \begin{corrige} On donne quatre solutions possibles, une pour chaque sémantique vue en @@ -581,7 +610,7 @@ rien d'essentiel). \smallskip -On fait donc les définitions suivantes : +On introduit donc les définitions suivantes : \begin{itemize} \item Un \textbf{dyadique} est un rationnel de la forme $\frac{k}{2^n}$ avec $k\in\mathbb{Z}$ et $n\in \mathbb{N}$ (i.e., |