\documentclass[12pt,a4paper]{article}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage{times}
\usepackage{amssymb,amsmath,stmaryrd,latexsym,graphicx,url}
\usepackage[all]{xy}
\usepackage{xcolor}
\usepackage{framed}

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

\usepackage{enumitem}


\title{DM, $\lambda$-calcul, 2025}
\author{
  \begin{tabular}{l}
    \emph{Votre nom}:
    \hskip10cm\strut % cette ligne à supprimer après avoir écrit votre nom
    \\
    \hline
  \end{tabular}
  }
\date{\`a rendre le 08 avril 2025
  au plus tard, à \url{jgl@lmf.cnrs.fr}}

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

\newcommand\votresolutionici{\textsf{Votre solution ici.}}

\newcommand\limp{\mathrel{\Rightarrow}}
\newcommand\fv{\mathop{\mathrm{fv}}}
\newcommand\bv{\mathop{\mathrm{bv}}}
\newcommand\vdal[1]{\Longrightarrow_{#1}}
\newcommand\eqdef{\mathrel{\buildrel \text{def}\over=}}
\newcommand\nat{\mathbb{N}}
\newcommand\true{\mathbf{V}}
\newcommand\false{\mathbf{F}}
\newcommand\pow{\mathbb{P}}
\newcommand\fin{{\text{fin}}}
\newcommand\Pfin{\pow_\fin}
\newcommand\Eval[1]{\llbracket {#1} \rrbracket}
\newcommand\code[1]{\ulcorner {#1} \urcorner}
\newcommand\asr{\mathbf{asr}}
\newcommand\asrhelper{\mathbf{asr\_helper}}
\newcommand\couple{\mathbf{cpl}}
\newcommand\decpl{\mathbf{decpl}}
\newcommand\proj{\mathbf{p}}
\newcommand\num{\mathbf{num}}
\newcommand\kwote{\mathbf{kwote}}
\newcommand\kwotehelper{\mathbf{kwote\_helper}}
\newcommand\kwoteiter{\mathbf{kwote\_iterator}}
\newcommand\diag{\mathbf{diag}}
\newcommand\coh{\mathrel{{\relax}^{\smash{\frown}}_{\smash{\smile}}}}
\newcommand\p{{\mathrm{p}}}

\newtheorem{fact}{Fait}
\newtheorem{lemma}[fact]{Lemme}

\newcommand\proof{\emph{Démonstration.}}
\newcommand\qed{\hfill$\Box$}
\newcommand\identity[1]{\mathrm{id}_{#1}}

\newcommand\V{{\mathtt V}}
\newcommand\callcc{\mathtt{callcc}}
\newcommand\CC{\mathbf{C}}
\newcommand\tete{\to_{\mathrm{t}}}
\newcommand\tf{\to_{\mathrm{tf}}}
\newcommand\std{\limp_{\mathrm{s}}}
\newcommand\I{\mathbf I}

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

\newcommand\blackrect{\raisebox{-2pt}{\rule{4pt}{8.5pt}}}
\newcommand\whiterect{\raisebox{1.5pt}{\framebox{\rule{-3pt}{1.5pt}}}}
\newcommand\trivial{\whiterect\,\whiterect\,\whiterect\,\whiterect\,\whiterect}
\newcommand\veryeasy{\blackrect\,\whiterect\,\whiterect\,\whiterect\,\whiterect}
\newcommand\easy{\blackrect\,\blackrect\,\whiterect\,\whiterect\,\whiterect}
\newcommand\medium{\blackrect\,\blackrect\,\blackrect\,\whiterect\,\whiterect}
\newcommand\hard{\blackrect\,\blackrect\,\blackrect\,\blackrect\,\whiterect}
\newcommand\veryhard{\blackrect\,\blackrect\,\blackrect\,\blackrect\,\blackrect}

%%% 

\begin{document}

\maketitle

\paragraph{Notes préliminaires.} Les réponses doivent être claires;
une réponse juste mais pas claire ne vaut pas mieux qu'une réponse
incorrecte.

Toute affirmation doit être justifiée, par une preuve ou par une
référence au cours.  Aucune référence en avant n'est autorisée.
N'oubliez pas de vérifier les hypothèses des résultats que vous
utilisez.  \og Par récurrence\fg{} ne veut rien dire si vous ne dites
pas sur quoi vous faites la récurrence, et au besoin le long de quel
ordre bien fondé.

Ceci est un devoir à la maison.  Vous avez donc le temps de vous
relire: pas de faute d'orthographe, pas de rature, pas de question
dans le désordre, notamment.

N'inventez pas vos propres notations, et utilisez celles de l'énoncé,
ou du cours.

La correction sera effectuée question par question.  Toute réponse à
une question doit donc être lisible indépendamment des autres réponses
aux questions.  Toute référence à un lemme auxiliaire, à une
construction ou à une définition que vous auriez faite dans une autre
question sera ignorée.

Si vous le souhaitez, 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.

Annotations: \trivial{} trivial, \veryeasy{} très facile et court,
\easy{} facile, moyennement long, \medium{} assez long ou difficile,
\hard{} difficile ou long, \veryhard{} très difficile et long.  (Notes
en conséquence.)

La section~\ref{sec:beta-eta} est indépendante des suivantes.  Les
sections~\ref{sec:le-theoreme-danti} et~\ref{sec:une-fonction-qui} ne
sont pas indépendantes.

L'examen contiendra peut-être une suite à ce DM.

\section{Confluence de la $\beta\eta$-réduction}
\label{sec:beta-eta}


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\easy{} Montrer que, si $R$ et $S$ sont confluentes et si $R^*$
  et $S^*$ commutent, alors:
  \begin{enumerate}
  \item $R^*;S^*$ est fortement confluente;
  \item $R \cup S$ et $R^*; S^*$ ont la même clôture réflexive-transitive;
  \item $R \cup S$ est confluente.
  \end{enumerate}

  \begin{solution}
    \votresolutionici
  \end{solution}

\end{enumerate}

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{}.

\begin{enumerate}[resume*=q]
\item\medium{} Montrer que si $R$ pseudo-commute avec $S$, alors $R^*$
  et $S^*$ commutent.


  \begin{solution}
    \votresolutionici
  \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.

On considère les relations:
\begin{align*}
  (\beta) \quad (\lambda x . u) v & \to u [x:=v] \\
  (\eta) \qquad \lambda x . ux & \to u
                                    & \text{si }x \not\in \fv (u).
\end{align*}
Par convention, elles passent au contexte, et tous les termes sont
compris à $\alpha$-équivalence près.  On écrira $s \to_\beta t$ si $s$
se réécrit en $t$ par $(\beta)$, $s \to_\eta t$ si $s$ se réécrit en
$t$ par $(\eta)$, $s \to_{\beta\eta} t$ si $s \to_\beta t$ ou
$s \to_\eta t$.  La relation $\to_{\beta\eta}$ est la
\emph{$\beta\eta$-réduction}.

On pourra utiliser sans preuve que si $u \to_{\beta\eta} u'$ alors
$\fv (u') \subseteq \fv (u)$.


\begin{enumerate}[resume*=q]
\item\label{q:eta}\easy{} Montrer que $\to_\eta$ est fortement
  confluente.

  \begin{solution}
    \votresolutionici
  \end{solution}
  
\item\label{q:eta:comm}\hard{} Montrer que:
  \begin{enumerate}[label=(\alph*)]
  \item si $u \to_\eta u'$ alors $u [x:=v] \to_\eta u' [x:=v]$;
  \item si $v \to_\eta v'$ alors $u [x:=v] \to^*_\eta u [x:=v']$;
  \item $\to_\beta$ pseudo-commute avec $\to_\eta$.
  \end{enumerate}

  \begin{solution}
    \votresolutionici
  \end{solution}
\item\trivial{} En déduire que la $\beta\eta$-réduction est confluente.
  % Citez bien tous les résultats et questions que vous utilisez.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

\section{Le théorème d'anti-standardisation}
\label{sec:le-theoreme-danti}

On revient au $\lambda$-calcul avec $\beta$-réduction.

Pour tout $\lambda$-terme $u$, on définit $\nu (u)$ comme la longueur
de la plus longue réduction partant de $u$ si $u \in SN$ (l'ensemble
des termes fortement normalisants), comme $\infty$ sinon. On notera
que $\nu (u)=\infty$ si et seulement s'il y a une réduction infinie
partant de $u$.  On notera aussi que $\nat \cup \{\infty\}$ est bien
fondé, et l'on peut donc effectuer des récurrences sur $\nu (u)$.
On fera aussi attention que: dans $\nat \cup \{\infty\}$, on n'a
\emph{pas} $n < n+1$\ldots{} uniquement si $n < \infty$;
$u \to v$ n'entraîne \emph{pas} $\nu (u) > \nu (v)$ (seulement $\nu
(u) \geq \nu (v)$), sauf si $u$ est fortement normalisable.

On note $|u|$ la taille d'un $\lambda$-terme $u$.

\begin{enumerate}[resume*=q]
\item\label{q:fund:max}\medium{} Pour tous $\lambda$-termes $s$,
  $u_1$, \ldots, $u_m$, avec $m \geq 1$, montrer que:
  \begin{align*}
    \nu ((\lambda x . s) u_1 \cdots u_m)
    & = \left\{
      \begin{array}{ll}
        \nu (s [x:=u_1] u_2 \cdots u_m) + 1
        & \text{si }x \in \fv (s) \\
        \nu (s u_2 \cdots u_m) + \nu (u_1) + 1
        & \text{sinon.}
      \end{array}
          \right.
  \end{align*}
  Il est fortement conseillé de procéder par doubles inégalités.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

La \emph{stratégie perpétuelle} sélectionne le redex le plus à gauche
$(\lambda x . u) v$ tel que $x$ soit libre dans $u$ ou que $v$ soit
normal, le cas échéant (sinon, la réduction s'arrête). Soit $\to_\p$
la $\beta$-réduction selon la stratégie perpétuelle. Explicitement,
$u \to_\p u'$ est défini par récurrence sur la taille de $u$ comme
suit.
\begin{enumerate}[label=(\Alph*)]
\item si $u$ est en forme normale de tête
  $\lambda x_1, \cdots, x_n . x u_1 \cdots u_m$, si $u_1$, \ldots,
  $u_{i-1}$ sont en forme normale, et si $u_i \to_\p u'_i$
  ($1 \leq i\leq m$), alors\\
  $u \to_\p \lambda x_1, \cdots, x_n . x u_1 \cdots u_{i-1} u'_i
  u_{i+1} \cdots u_m$;
\item si
  $u = \lambda x_1, \cdots, x_n . (\lambda x \cdot s) u_1 u_2 \cdots
  u_m$ avec $m \geq 1$,
  \begin{enumerate}
  \item
    $u \to_\p \lambda x_1, \cdots, x_n . s [x:=u_1] u_2 \cdots u_m$ si
    $x \in \fv (s)$ ou $u_1$ est normal;
  \item
    $u \to_\p \lambda x_1, \cdots, x_n . (\lambda x \cdot s) u'_1 u_2
    \cdots u_m$ si $u_1 \to_\p u'_1$ et $x \not\in \fv (s)$.
  \end{enumerate}
\end{enumerate}
Attention, $\to_\p$ n'est \emph{pas} destinée à passer aux contextes:
la description ci-dessus est la description complète de $\to_\p$.

On notera que pour tout $\lambda$-terme $u$, soit $u$ est en forme
normale (pour la $\beta$-réduction ordinaire), soit $u$ a un unique
$\to_\p$-redex.  En particulier, la stratégie perpétuelle est
déterministe.  De plus, un $\lambda$-terme a un $\to_\p$-réduit en une
étape si et seulement s'il n'est pas normal.

Pour tout terme $u$, soit $\nu_\p (u)$ la longueur de l'unique
$\to _\p$-réduction partant de $u$ (éventuellement $\infty$).  Il est
clair que $\nu_\p (u) \leq \nu (u)$, puisque toute $\to_\p$-réduction
est une $\to$-réduction.

On note $SN$ l'ensemble des $\lambda$-termes fortement normalisables.

\begin{enumerate}[resume*=q]
\item\label{q:elim}\trivial{} Montrer que
  $\nu (\lambda x_1, \cdots, x_n \cdot t) = \nu (t)$ et que
  $\nu_\p (\lambda x_1, \cdots, x_n \cdot t) = \nu_\p (t)$, pour tout
  $n \in \nat$, toutes variables $x_1$, \ldots, $x_n$ et tout
  $\lambda$-terme $t$.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

\begin{enumerate}[resume*=q]
\item\label{q:nu=nup:aux}\veryhard{} Soit $u$ un $\lambda$-terme et
  $k \in \nat$ (donc $k \neq \infty$), avec $(k, |u|)$ minimal dans
  l'ordre lexicographique tel que $\nu_\p (u) < k \leq \nu (u)$.
  Montrer que:
  \begin{itemize}
  \item (A) si $u$ est sous forme normale de tête
    $\lambda x_1, \cdots, x_n . x u_1 . u_m$, c'est impossible.
  \item (B) si $u$ a pour forme de tête
    $\lambda x_1, \cdots, x_n . (\lambda x . s) u_1 \cdots u_m$ avec
    $m \geq 1$:
    \begin{itemize}
    \item (a) si $x \in \fv (s)$, ou $u_1$ est normal, c'est
      impossible;
    \item (b) si $x \not\in \fv (s)$ et $u_1$ n'est pas normal, alors
      $u_1 \to_\p u'_1$ pour un certain $\lambda$-terme $u'_1$, et en
      posant $j \eqdef \nu (s u_2 \cdots u_m)$, montrer que
      $j + \nu (u'_1) < k-2$, donc que $j < \infty$, puis que
      $\nu (u_1) \geq k-1-j$, mais que la double inégalité
      $\nu_\p (u_1) < k-1-j \leq \nu (u_1)$ est impossible; en déduire
      une contradiction dans ce cas aussi.
    \end{itemize}
    Donc, pour tout $\lambda$-terme $u$, pour tout $k \in \nat$, il
    est impossible que $\nu_\p (u) < k \leq \nu (u)$.
  \end{itemize}

  \begin{solution}
    \votresolutionici
  \end{solution}
  
\item\label{q:nu=nup}\veryeasy{} En déduire que $\nu_\p (u) = \nu (u)$
  pour tout $\lambda$-terme $u$.

  \begin{solution}
    \votresolutionici
  \end{solution}
  
\item\label{q:anti}\trivial{} Montrer le \emph{théorème
    d'anti-standardisation}: si $u$ n'est pas fortement normalisable,
  alors la $\to_\p$-réduction à partir de $u$ est infinie.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

\section{Une fonction qui dépasse toutes les fonctions calculables}
\label{sec:une-fonction-qui}


Pour tout $u \in SN$, on définit $h (u)$ comme suit:
\begin{align}
  \label{eq:h:hnf}
  h (\lambda x_1, \cdots, x_n . x u_1 \cdots u_m)
  & \eqdef \sum_{i=1}^m h (u_i) \\
  \label{eq:h:hred:a}
  h (\lambda x_1, \cdots, x_n . (\lambda x . s) u_1 \cdots
  u_m)
  & \eqdef h (s [x:=u_1] u_2 \cdots u_m)+1 \\
  \nonumber
  & \qquad\text{si $m \geq 1$,} \\
  \nonumber
  & \qquad\text{et $x \in \fv (s)$  ou $u_1$ est normal} \\
  \label{eq:h:hred:b}
  h (\lambda x_1, \cdots, x_n . (\lambda x . s) u_1 \cdots
  u_m)
  & \eqdef h (s u_2 \cdots u_m) + h (u_1)+1 \\
  \nonumber
  & \qquad\text{si $m \geq 1$,} \\
  \nonumber
  & \qquad\text{$x \not\in \fv (s)$, et $u_1$ n'est pas normal.}
\end{align}
Ceci ressemble à une définition de $h (u)$ par récurrence sur la taille de la
forme de tête de $u$, mais n'en est pas une: dans (\ref{eq:h:hred:a}),
le terme sur lequel $h$ s'applique à droite n'est pas nécessairement
plus petit que le terme de gauche.

\begin{enumerate}[resume*=q]
\item\label{q:h}\medium{} Montrer que $h (u)$ est bien défini pour
  tout $u \in SN$.  Un point important de la question est: sur quoi
  faire porter la récurrence?

  \begin{solution}
    \votresolutionici
  \end{solution}
\item\medium{} Montrer que $h (u) = \nu_\p (u)$ pour tout $u \in SN$.
  La~\ref{q:h} a montré qu'il existe une unique fonction
  $h \colon SN \to \nat$ satisfaisant aux équations (\ref{eq:h:hnf}),
  (\ref{eq:h:hred:a}) et (\ref{eq:h:hred:b}).  Il suffit donc de
  vérifier que $\nu_\p$ est bien définie sur tout $SN$ et que $\nu_\p$
  satisfait aux mêmes équations que $h$.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

On cherche à estimer la vitesse de croissance de la fonction $h$ en
fonction de son argument.

On représente les $\lambda$-termes sous forme de chaînes de caractères
de façon évidente.  On admettra que le problème suivant, noté
\textbf{SN}, est indécidable:\\
\textbf{Entrée:} un $\lambda$-terme $u$;\\
\textbf{Question:} $u \in SN$?

On note $\p$ la fonction qui prend en entrée un
$\lambda$-terme $u$ et retourne en sortie l'unique réduit en une étape
de $u$ par $\to_\p$ si $u$ n'est pas normal, et un symbole spécial
$\checkmark$, différent de tous les $\lambda$-termes, si $u$ est
normal.  On admettra que $\p$ est calculable, autrement dit, qu'il
existe une machine de Turing qui termine toujours et retourne $\p (u)$
sur tout $\lambda$-terme $u$ en entrée.

\`A partir de $\p$, on définit une fonction $F$ qui à tout couple
$(u, k)$ d'un $\lambda$-terme $u$ et d'un entier $k \in \nat$ associe
la forme normale $u \downarrow$ de $u$ si l'on a
$u \to_\p^* u \downarrow$ en $k$ étapes ou moins, et sinon l'unique
réduit de $u$ par $\to_\p$ en exactement $k$ étapes; autrement dit,
$F (u, 0) \eqdef u$, $F (u, n+1)$ vaut $u$ si $\p (u) = \checkmark$,
$F (\p (u), n)$ sinon.  Il est clair que $F$ est calculable.

\begin{enumerate}[resume*=q]
\item\label{q:indec}\veryeasy{} Supposons une fonction (totale) calculable
  $\ell$ prenant un $\lambda$-terme $u$ en entrée et retournant un
  entier $\ell (u)$, telle que $h (u) \leq \ell (u)$ pour tout
  $u \in SN$.  La fonction $c$ qui à tout $\lambda$-terme $u$ associe
  $0$ si $\p (F (u, \ell (u)) = \checkmark$, $1$ sinon, est
  calculable.  Montrer que, sous ces hypothèses, \textbf{SN} serait
  décidable, et en conclure que la fonction $h$ n'est en fait majorée
  (sur $SN$) par aucune fonction calculable définie sur tous les
  $\lambda$-termes.

  \begin{solution}
    \votresolutionici
  \end{solution}
\end{enumerate}

Une remarque pour finir.  On peut utiliser la construction de
la~\ref{q:h} pour montrer que $h$ est une fonction qui est non
seulement bien définie sur $SN$, mais même calculable sur $SN$, au
sens suivant: il existe une machine de Turing $\mathcal M$ qui, si on
lui donne un $\lambda$-terme $u \in SN$ en entrée, termine en
produisant en sortie la valeur de $h (u)$.  Si on lui donne un
$\lambda$-terme $u$ non fortement normalisant en entrée, rien n'est
demandé de $\mathcal M$, et elle peut parfaitement ne pas terminer sur
$u$.  La~\ref{q:indec} montre en particulier qu'on ne peut pas étendre
$h$ à une fonction qui serait calculable sur tous les
$\lambda$-termes, et qu'il n'y a même pas de fonction calculable
$\ell$ sur les $\lambda$-termes qui pourrait fournir une approximation
supérieure $\ell (u)$ de $h (u)$ pour chaque $u \in SN$.

Tout ceci repose sur le fait que \textbf{SN} est indécidable, que nous
avons admis.  Une des démonstrations les plus simples de ce fait se
trouve dans: Pawe\l{} Urzyczyn, \emph{A simple proof of the
  undecidability of strong normalization}, Mathematical Structures in
Computer Science 13(2003), pages 5--13.

\end{document}
