\documentclass[12pt,a4paper]{article}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage{times}
\usepackage{amssymb,amsmath,stmaryrd,latexsym}
\usepackage{proof}
\usepackage{framed}

\def\solution{\leftbar\it}
\def\endsolution{\endleftbar}

\usepackage{enumitem}
\usepackage{xypic,xy}


\title{DM, $\lambda$-calcul, 2020}
\author{\relax}
\date{\`a rendre le 09 juin 2020 au plus tard}

%%%
%%% Les macros que j'utilise dans ce sujet:
%%%

\newcommand\C{\mathbf{C}}
\newcommand\B{\mathbf{B}}
\newcommand\W{\mathbf{W}}
\newcommand\K{\mathbf{K}}
\renewcommand\S{\mathbf{S}}
\newcommand\I{\mathbf{I}}

\newcommand\HA{\mathbf{HA}}
\newcommand\R{\mathbf{R}}
\newcommand\s{\mathbf{S}}

\newcommand\nat{\mathbb{N}}
% \newcommand\letkw{\mathop{\mathtt{let}}}
% \newcommand\letin[2]{\letkw{#1}\;{\mathtt{in}}\;{#2}}
% \newcommand\letrecin[2]{\mathop{\mathtt{letrec}}{#1}\mathbin{\mathtt{in}}{#2}}
% \newcommand\valu{\mathop{\mathtt{val}}}
% \newcommand\tc{\pmb{T}}
\newcommand\limp{\mathrel{\Rightarrow}}
\newcommand\eqdef{\mathrel{\buildrel\text{def}\over=}}
\newcommand\true{\mathbf{V}}
\newcommand\false{\mathbf{F}}
\newcommand\Id{\mathbf{I}}


\newcommand\jgl[1]{\marginpar{\tiny #1}}

%%% 

\begin{document}

\maketitle

\paragraph{Notes préliminaires.}  Les recommandations de clarté, de
justesse, de soin, et de concision sont les mêmes que pour le DM.

Je mettrai le source \LaTeX{} de ce sujet en ligne, et vous pourrez
écrire votre solution en donnant votre nom comme argument de la
commande \verb:\author: en tête de document, puis écrire vos réponses
entre les différentes \verb:\begin{solution}: et
  \verb:\end{solution}:.  Envoyez-moi ensuite le pdf, pas le source.

Comme promis, l'examen contient certaines suites à des questions du
DM.  Vous avez donc le droit d'utiliser des résultats du DM, sans les
(re)démontrer.  En fait, je compterai beaucoup moins de points pour
une redémonstration que pour une citation.  Je vous demande de citer
les résultats du DM que vous utiliserez par une formule telle que \og
par la question~$\langle n\rangle$ du DM\fg{}.

Finalement, les questions les plus difficiles sont bien sûr aussi
celles qui compteront pour le plus de points, où qu'elles soient dans
le sujet.

\section{Mise en bouche: le lemme de Hindley-Rosen}
\label{sec:le-lemme-de}

On étudie des critères de confluence pour des relations de réécriture
abstraites, c'est-à-dire des relations binaires sur un ensemble $A$.

Une relation binaire $R$ sur $A$ est, formellement, juste un
sous-ensemble de $A \times A$.  On notera souvent
$a \mathrel{\buildrel R \over \to} b$ au lieu de $(a, b) \in R$.

Deux relations binaires $R$ et $S$ \emph{commutent} si et
seulement si:
\[
  \xymatrix{
    \bullet \ar[r]^{R} \ar[d]_{S} & \bullet \ar@{.>}[d]^{S} \\
    \bullet \ar@{.>}[r]_{R} & \bullet
  }
\]
% explication:
% - \ar = arrow
% - optionnel: spécification de style de flèche avec @{}
%    @{.>} forme une flèche pointillée
% - entre crochets: la direction: [r]=à droite, [d]=en bas, [u]=en haut,
%    [l]=à gauche
% - ensuite, _{truc}, ^{truc}, ou |{truc}
%    pour étiqueter la flèche par truc
%    on utilise _{truc} pour mettre truc en-dessous de la flèche,
%                    ^{truc} pour le mettre au-dessus,
%                    |{truc} pour le superposer à la flèche
% - pour plus de détails, voir:
% http://texdoc.net/texmf-dist/doc/generic/xypic/xyguide.pdf
autrement dit, si pour tous $a$, $b$, $c$ tels que
$a \mathrel{\buildrel R \over \to} b$ et
$a \mathrel{\buildrel S \over \to} c$, il existe un $d$ tel que
$b \mathrel{\buildrel S \over \to} d$ et
$c \mathrel{\buildrel R \over \to} d$.

Pour toutes relations binaires $R$ et $S$, on notera $R;S$ la relation
définie par $(a, b) \in R;S$ si et seulement s'il existe $a_1$ tel que
$a \mathrel{\buildrel R\over \to} a_1 \mathrel{\buildrel S \over\to}
b$; et pour tout $n \geq 0$, $R^n$ la relation
$\underbrace{R; R; \cdots; R}_{n\text{ fois}}$ (si $n=0$, c'est par
convention la relation d'égalité: $(a, b) \in R^0$ si et seulement si
$a=b$).

On notera $R^*$ la clôture réflexive-transitive d'une relation binaire
$R$.  Autrement dit, $a \mathrel{\buildrel R^* \over \to} b$ si et
seulement s'il existe $n \geq 0$ ($0$ est autorisé) tel que
$(a, b) \in R^n$.

\begin{enumerate}[series=q,label=\textbf{Question \arabic*}]
\item Montrer que, si $R$ et $S$ sont confluentes et si $R^*$ et $S^*$
  commutent, alors:
  \begin{enumerate}
  %\item $R^*$ et $S^*$ commutent;
  \item $R^*;S^*$ est fortement confluente;
  \item $R \cup S$ est confluente.
  \end{enumerate}

  \begin{solution}
    %%% Votre solution ici:
    %%% (cherchez 'explication' dans un commentaire plus haut pour les
    %%% commandes de base de \xymatrix, si vous voulez faire de jolis diagrammes!)

  \end{solution}

\item On dit que $R$ \emph{pseudo-commute} avec $S$ si et seulement si:
  \[
    \xymatrix{
      \bullet \ar[r]^{R} \ar[d]_{S} & \bullet \ar@{.>}[d]^{S^*} \\
      \bullet \ar@{.>}[r]_{R^{\leq 1}} & \bullet
    }
  \]
  où $R^{\leq 1} = R^0 \cup R^1$.  (En général, $R^{\leq n}$ est
  définie comme l'union de $R^0$, $R^1$, \ldots, $R^n$.)  On notera
  bien que \og $R$ pseudo-commute avec $S$\fg{} n'est pas équivalent à
  \og $S$ pseudo-commute avec $R$\fg{}.  Montrer que si $R$
  pseudo-commute avec $S$, alors $R^*$ et $S^*$ commutent.

  \begin{solution}
    %%% Votre solution ici:
    %%% (cherchez 'explication' dans un commentaire plus haut pour les
    %%% commandes de base de \xymatrix, si vous voulez faire de jolis diagrammes!)

  \end{solution}
\end{enumerate}

On en déduit le \emph{lemme de Hindley-Rosen}: si $R$ et $S$ sont deux
relations confluentes, et si $R$ pseudo-commute avec $S$, alors
$R \cup S$ est confluente.  Ceci sera utile dans la partie qui suit.

\section{Entrée: le combinateur $\delta$ de Church}
\label{sec:le-combinateur-delta}

On va considérer deux extensions du $\lambda$-calcul, le
$\lambda\delta$-calcul et le $\lambda\delta_C$-calcul.  L'idée y est
de rajouter une constante $\delta$ qui implémente le test d'égalité.

Dans les deux calculs, la syntaxe est obtenue en ajoutant juste une
constante $\delta$ aux termes.  Autrement dit, les
$\lambda\delta_{(C)}$-termes sont:
\begin{align*}
  s, t, u, v, \ldots & ::= x, y, z, \ldots & \text{variables} \\
                     & \mid \delta & \text{le combinateur de Church} \\
                     & \mid uv & \text{application} \\
                     & \mid \lambda x . u & \text{abstraction}.
\end{align*}
Comme d'habitude, les termes sont considérés à $\alpha$-renommage
près.

Un $\lambda\delta$-terme est dit \emph{canonique} si et seulement s'il
est $\beta$-normal, et ne contient pas de sous-terme de la forme
$\delta s t$.  (Il peut donc contenir des sous-termes de la forme
$\delta s$, ou bien $\delta$ tout seul.)

Les règles de réduction du $\lambda\delta$-calcul sont, outre la
$\beta$-réduction, les règles suivantes appelées
\emph{$\delta$-règles}:
\begin{align*}
  \delta u v & \to \true & \text{si $u$ et $v$ sont des termes
                           canoniques identiques} \\
  \delta u v & \to \false & \text{si $u$ et $v$ sont des termes
                            canoniques distincts.}
\end{align*}
Au risque de me répéter, \og identiques\fg{} et \og distincts\fg{}
doivent être compris à $\alpha$-renommage près.

Les termes $\true \eqdef \lambda x, y . x$ et
$\false \eqdef \lambda x, y . y$ sont les booléens de Church usuels.
On notera aussi $\Id \eqdef \lambda x . x$.

On parlera de $\beta\delta$-réduction pour la notion de réduction
définie par $\beta$ et les deux règles ci-dessus.  Il est tacite
qu'elle passe au contexte.  La $\beta\delta$-convertibilité est la
plus petite relation d'équivalence contenant la $\beta\delta$-réduction.

\begin{enumerate}[resume*=q]
\item En considérant le terme
  $d_0 \eqdef (\lambda x, y \cdot \delta x y) \Id \Id$,
  \begin{enumerate}
  \item montrer que $\true$ et $\false$ sont
    $\beta\delta$-convertibles;
  \item en déduire que le $\lambda\delta$-calcul a une théorie
    triviale: \emph{tous} les $\lambda\delta$-termes sont
    $\beta\delta$-convertibles.
  \end{enumerate}

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}
\end{enumerate}

Vous devriez vous être aperçu, aussi, que le $\lambda\delta$-calcul
n'est pas confluent.  (Je ne demande pas de le démontrer.)  Pour
réparer ces défauts, on considère le $\lambda\delta_C$-calcul.  Sa
syntaxe est la même, et ses règles sont modifiées: en
$\lambda\delta_C$-calcul, les $\delta$-règles ne s'appliquent plus au
rédex $\delta u v$ que si non seulement $u$ et $v$ sont canoniques
mais aussi \emph{clos}.  On appellera cette modification les
\emph{$\delta_C$-règles}.

\begin{enumerate}[resume*=q]
\item Montrer que le $\lambda\delta_C$-calcul est
  confluent.\jgl{On n'a pas démontré un lemme qui peut servir?}

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}

\item En déduire que, contrairement au cas du $\lambda\delta$-calcul,
  le $\lambda\delta_C$-calcul a une théorie \emph{non} triviale.

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}
\end{enumerate}



\section{Plat principal: résolubilité}
\label{sec:resolubilite}

Si $\vec u$ est une suite finie de termes $u_1$, $u_2$, \ldots, $u_n$,
on notera $t \vec u$ pour $tu_1 u_2 \cdots u_n$.  (On peut avoir
$n=0$.)

Un terme clos $t$ est \emph{résoluble} si et seulement s'il existe une
suite finie $\vec u$ de termes telle que $t \vec u =_\beta \I$, où
$\I$ est par définition le terme $\lambda x \cdot x$.

Un terme $t$, non nécessairement clos, est résoluble si et seulement
si le terme $\lambda x_1, \cdots, x_m \cdot t$, où $x_1$, \ldots,
$x_m$ sont les variables libres de $t$, est résoluble.  (Le terme en
question est clos, et l'on applique donc la définition précédente de
la résolubilité.)  On appellera $\lambda x_1, \cdots, x_m \cdot t$ la
\emph{fermeture} de $t$, même si elle n'est pas unique.

\begin{enumerate}[resume*=q]
\item\label{q:resol:h} Supposons $t$ clos et résoluble.\jgl{C'est le
    moment d'utiliser des résultats du cours.}
  \begin{enumerate}
  \item Pourquoi existe-t-il une suite finie $\vec u$ de termes telle
    que $t \vec u \to^* \I$?
  \item \ldots{} et même $t \vec u \limp_s \I$?
  \item \ldots{} et même $t \vec u \to_h^* \I$?  ($\to_h$, ou $\to_t$,
    dénote la réduction de tête.)
  \end{enumerate}

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}

\item\label{q:resol:tuhn} En déduire que pour tout terme clos
  résoluble $t$, il existe une suite finie de termes $\vec u$ tel que
  $t \vec u$ est typable dans le systèmes des types intersection
  simples du DM.  \jgl{3 lignes, chez moi.}  (C'est-à-dire qu'il
  existe un contexte de typage $\Gamma$ formé de liaisons
  $x_i : \mu_i$ où les $\mu_i$ sont des multi-ensembles de types
  intersection simples, et il existe un type intersection simple
  $\tau$ tels que $\Gamma \vdash t \vec u : \tau$ soit dérivable dans
  le système de la partie~3 du DM.)
  % , un contexte de typage $\Gamma$ et un
  % type $\tau$ tels que $\Gamma \vdash t \vec u : \tau$ soit dérivable
  % dans le systèmes des types intersection simples du DM.

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}

\item\label{q:resol:hn:clos} En déduire que tout terme clos résoluble
  $t$ a une forme normale de tête.  \jgl{Pas très long non plus.}  (On
  rappelle que ceci signifie que sa réduction de tête termine.)

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}

\item\label{q:resol:hnf} Montrer enfin que tout terme résoluble a une
  forme normale de tête.\jgl{6 lignes chez moi.}

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}

  \item Exhiber un terme non résoluble, et justifier.  \jgl{2 lignes.}

    \begin{solution}
      %%% Votre solution ici:
    \end{solution}

\item\label{q:resol} Montrer que, réciproquement:
  \begin{enumerate}
  \item toute forme normale de tête close est résoluble;
  \item \ldots{} tout terme clos qui a une forme normale de tête est
    résoluble;
  \item \ldots{} enfin, tout terme qui a une forme normale de tête est
    résoluble.
  \end{enumerate}

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}
\end{enumerate}

Et donc, les trois notions suivantes sont équivalentes: (a) être
résoluble, (b) avoir une forme normale de tête, (c) être typable dans
le système des types intersection simples.

\section{Un dessert copieux: le système des types F-intersection}
\label{sec:les-systeme-des}

On considère les \emph{type F-intersection} définis par la grammaire:
\begin{align*}
  \sigma, \tau, \ldots & ::= \alpha & \text{variables de types} \\
                       & \mid [\sigma_1, \cdots, \sigma_n] \to \tau \\
                       & \mid \forall \alpha . \tau &
                                                      \text{quantification
                                                      de types.}
\end{align*}
On a donc juste rajouté la quantification du système F au système des
types intersection simples du DM.  On abrégera encore commodément un
multi-ensemble de types $[\sigma_1, \cdots, \sigma_n]$ par la simple
lettre $\mu$.

Les règles de typage sont (normalement sans surprise):
\[
\begin{array}{c}
  \begin{prooftree}
    \justifies
    \Gamma, x : [\sigma_1, \cdots, \sigma_n] \vdash x : \sigma_i
    \using (Var) \quad\text{(où $1\leq i\leq n$)}
  \end{prooftree}
  \\ \\
  \begin{prooftree}
    \Gamma \vdash u : [\sigma_1, \cdots, \sigma_n] \to \tau \quad
    \Gamma \vdash v : \sigma_1 \quad \ldots \quad
    \Gamma \vdash v : \sigma_n
    \justifies
    \Gamma \vdash uv : \tau
    \using (App)
  \end{prooftree}
  \quad
  \begin{prooftree}
    \Gamma, x : \mu \vdash u : \tau
    \justifies
    \Gamma \vdash \lambda x \cdot u : \mu \to \tau
    \using (Abs)
  \end{prooftree}
  \\ \\
  \begin{prooftree}
    \Gamma \vdash u : \forall \alpha . \tau
    \justifies
    \Gamma \vdash u : \tau [\alpha:=\sigma]
    \using (\forall^2 E)
  \end{prooftree}
  \quad
  \begin{prooftree}
    \Gamma \vdash u : \tau
    \justifies
    \Gamma \vdash u : \forall \alpha . \tau
    \using (\forall^2 I)^*
  \end{prooftree}
\end{array}
\]
\begin{flushright}
  $^*$ si $\alpha$ n'est libre dans aucun type de $\Gamma$.  
\end{flushright}

\begin{enumerate}[resume*=q]
\item Montrer que tout $\lambda$-terme typable dans le systèmes des
  types F-intersection a une forme normale de tête.  \jgl{Quasiment
    une question de cours.  Deux pages chez moi: n'en écrivez pas
    plus, s'il-vous-plaît!}

  Je ne demande pas, et même surtout pas, une démonstration dans tous
  les détails.  Je rappelle la recommandation de concision énoncée au
  début de ce sujet.  Je veux, en premier lieu, un plan clair de la
  démonstration, avec les définitions précises que vous utilisez.  Si
  un lemme se démontre comme un autre que vous avez vu ailleurs,
  dites-le et citez le résultat, en marquant clairement les
  différences; mais ne m'écrivez pas de longues vérifications
  laborieuses, et donc difficiles à lire.

  \begin{solution}
    %%% Votre solution ici:

  \end{solution}
\end{enumerate}



\end{document}
