\documentclass{book}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Définition du style

\usepackage[french]{babel}
\usepackage[T1]{fontenc}
%\usepackage{fullpage}
\usepackage{palatcm}
\usepackage{lettrine}

\usepackage{fancyheadings}
\lhead[\rm\thepage]{\sl\rightmark}
\rhead[\sl\leftmark]{\rm\thepage}
\cfoot[]{}
\pagestyle{fancy}

\renewcommand{\chaptermark}[1]{\markboth{#1}{}}
\renewcommand{\sectionmark}[1]{\markright{\thesection. #1}}
\makeatletter
\renewcommand{\subsection}{\@startsection
  {subsection}
  {2}
  {0pt}
  {2ex}
  {2ex}
  {\centering\normalfont\large\scshape}}
\renewcommand{\paragraph}{\@startsection
  {paragraph}
  {4}
  {0pt}
  {1ex}
  {-\fontdimen2\font plus -\fontdimen3\font minus -\fontdimen4\font}
  {\normalfont\normalsize\itshape}}
\makeatother

\usepackage{amsmath,amssymb,stmaryrd}
\usepackage{theorem}

\newtheorem{theo}{Théorème}[section]
\newtheorem{coro}[theo]{Corollaire}
\theorembodyfont{\rmfamily}
\newtheorem{lemme}[theo]{Lemme}

\newcommand{\aere}{\par\medskip}
\newcommand{\qed}{
  \ifmmode % if math mode, assume display: omit penalty etc.
  \else \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill
  \fi
  \quad\hbox{$\Box$}}

\newenvironment{rem}{\aere\noindent\textsc{Remarque~: }}{\aere}
\newenvironment{proof}{\aere\noindent\emph{Preuve~: }}{\qed\aere}

\addtolength{\textwidth}{2cm}
\addtolength{\textheight}{4cm}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Macros

\newcommand{\ie}{\emph{i.e.}}
\newcommand{\ssi}{\text{ ssi }}

\newcommand{\PR}[1]{\textbf{PR#1}}
\newcommand{\R}[1]{\textbf{R#1}}

\newcommand{\Proj}{\Pi}
\newcommand{\Term}[1]{\underline{#1}}
\newcommand{\Zero}{\mathord{\Term 0}}\newcommand{\Succ}{\mathop{\Term S}}
\newcommand{\Plus}{\mathop{\Term +}}\newcommand{\Mult}{\mathop{\Term .}}
\newcommand{\Val}[1]{|#1|}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Dom}{\mathop{\mathrm{dom}}}
\newcommand{\Def}[1]{#1\mathord{\downarrow}}
\newcommand{\Undef}[1]{#1\mathord{\uparrow}}
\newcommand{\fleche}{\rightarrow}
\newcommand{\car}[1]{{\chi}_{#1}}
\newcommand{\carp}[1]{\chi^p_{#1}}
\newcommand{\Abs}[2]{\lambda#1.\,#2}
\newcommand{\Prem}[2]{\mu#1.\,(#2)}
\newcommand{\Premb}[2]{\Prem{#1\mathop{<}#2}}
\newcommand{\existsb}[2]{\exists#1\mathop{<}#2.}
\newcommand{\forallb}[2]{\forall#1\mathop{<}#2.}
\newcommand{\et}{\wedge}\newcommand{\ou}{\vee}
\newcommand{\Equiv}{\leftrightarrow}
\newcommand{\Clot}[1]{\overline{#1}}
\newcommand{\Moins}{\stackrel{\cdot}{\smash{-}}}
\newcommand{\Mod}{\mathop{\%}}
\newcommand{\Couple}[2]{\langle#1,#2\rangle}
\newcommand{\Seq}[2]{\langle#2\rangle_{#1}}
\newcommand{\Div}{\mathrel|}
\renewcommand{\P}[2]{(#1)_{#2}}
\newcommand{\Tail}{\mathop{\mathtt{Suite}}}
\newcommand{\Seqp}{\mathop{\mathtt{Seq}}}
\newcommand{\Length}{\mathop{\mathtt{Lg}}}
\newcommand{\Restr}[2]{#1{\upharpoonright_#2}}
\newcommand{\Concat}[2]{#1\ast#2}
\newcommand{\Godel}[1]{\ulcorner#1\urcorner}
\newcommand{\VarP}{\mathop{\mathtt{Var}}}
\newcommand{\TermP}{\mathop{\mathtt{Term}}}
\newcommand{\Num}{\mathop{\mathtt{Num}}}
\newcommand{\AtomP}{\mathop{\mathtt{Atom}}}
\newcommand{\FormP}{\mathop{\mathtt{Form}}}
\newcommand{\FunP}{\mathop{\mathtt{Fun}}}
\newcommand{\PredP}{\mathop{\mathtt{Pred}}}
\newcommand{\LibresP}{\mathop{\mathtt{VarLibres}}}
\newcommand{\LibreP}{\mathop{\mathtt{Libre}}}
\newcommand{\LibresF}{\mathop{\mathtt{VL}}}
\newcommand{\ClosP}{\mathop{\mathtt{Clos}}}
\newcommand{\ClotF}{\mathop{\mathtt{Clot}}}
\newcommand{\Sub}{\mathop{\mathtt{Sub}}}
\newcommand{\Neg}{\mathop{\mathtt{Neg}}}
\newcommand{\Index}{\mathop{\mathtt{I}}}
\newcommand{\ParSub}{\mathop{\mathtt{ParSub}}}
\newcommand{\QBP}{\mathop{\mathtt{QuantBorn}}}
\newcommand{\ValF}{\mathop{\mathtt{Val}}}
\newcommand{\TrueP}{\mathop{\mathtt{Vr}}}
\newcommand{\Coh}{\mathop{\mathtt{Coh}}}
\newcommand{\KApp}[2]{\{#1\}(#2)}
\newcommand{\Ax}{\mathop{\mathtt{Ax}}\nolimits}
\newcommand{\Proof}{\mathop{\mathtt{Pr}}\nolimits}
\newcommand{\Thm}{\mathop{\mathtt{Thm}}\nolimits}
\newcommand{\EA}{\text{\bfseries EA}}
\newcommand{\LK}{\text{\bfseries LK}}
\newcommand{\PA}{\text{\bfseries PA}}

\newcommand{\App}[2]{(#1)#2}
\newcommand{\AppT}[2]{\langle #1,#2\rangle}
\newcommand{\Lam}[2]{\lambda#1\,#2}
\newcommand{\ST}[1]{\mathtt{ST}#1)}
\newcommand{\VL}[1]{\mathtt{VL}(#1)}
\newcommand{\Subst}[2]{#1[#2]}
\newcommand{\Implies}{\rightarrow}
\newcommand{\Bun}{\mathrel{\beta_0}}
\newcommand{\Btr}{\mathrel{\beta}}
\newcommand{\Beq}{\mathrel{=_\beta}}
\newcommand{\Bpar}{\mathrel{\rho}}
\newcommand{\BTun}{\mathrel{\beta_0^t}}
\newcommand{\BTtr}{\mathrel{\beta^t}}
\newcommand{\BGun}{\mathrel{\beta^g_0}}
\newcommand{\BGtr}{\mathrel{\beta^g}}

\newcommand{\Rep}[1]{\underline{#1}}
\newcommand{\Paire}[2]{\langle#1,#2\rangle}

\newcommand{\RightLeft}{\mathop{{\renewcommand{\arraystretch}{0}
      \begin{array}{c}
        \longrightarrow\\
        \longleftarrow
      \end{array}}}\limits}
\newcommand{\D}{\mathcal{D}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\N}{\mathcal{N}}
\newcommand{\Power}[1]{\mathcal{P}(#1)}
\newcommand{\PowerFin}[1]{\mathcal{P}_{\mathrm{fin}}(#1)}
\newcommand{\Sup}{\bigcup}
\newcommand{\subsetFin}{\subset_{\mathrm{fin}}}
\newcommand{\Trace}{\mathop{\mathrm{Tr}}\nolimits}
\newcommand{\Fun}{\mathop{\mathrm{Fun}}\nolimits}
\newcommand{\Interp}[1]{\llbracket#1\rrbracket}
\newcommand{\Real}[1]{|#1|}

%\def\newpar#1#2\fin{\lettrine{#1}{#2}}
%\renewcommand{\paragraph}[1]{\newpar#1\fin}

\author{}\title{Notes de cours <<~Preuves et Types~>>, DEA MDFI\\
  \normalsize Version préliminaire}

\setcounter{secnumdepth}{1}
\FrenchItemizeSpacingfalse

\begin{document}

\maketitle
\tableofcontents

\chapter{Théorèmes de Gödel}
\lettrine{C}{e chapitre} reproduit pour l'essentiel le premier chapitre du
livre de Girard~\cite{Girard87a} dont il suit grosso modo le plan. Le lecteur
pourra aussi se reporter au Shoenfield~\cite{Shoenfield67} pour élucider ou
compléter l'exposé.


\section{Le langage de l'arithmétique.}

Le langage de l'arithmétique est défini par
\begin{itemize}
\item les symboles de fonctions $\Zero$ (symbole de constante, \ie, fonction
  d'arité $0$), $\Succ$ (symbole de fonction unaire), $\Plus$ et $\Mult$
  (symboles de fonction binaire)~;
\item les symboles de prédicats $=$ et $<$.
\end{itemize}

En toute rigueur les termes et les formules de l'arithmétique sont construits
en utilisant la notation \emph{polonaise préfixée} (c'est à dire que la formule
qui exprime que $x$ est égale à $y$ s'écrit ${=}xy$). En pratique on utilisera
des parenthèses et les symboles binaires en notation infixe.

\paragraph{Vérité, équivalence de formules.}
On dira que deux formules $A$ et $B$ sont \emph{logiquement équivalentes} si le
séquent $\vdash A\Equiv B$ est prouvable dans $\LK$ (le calcul des séquents).
On dira qu'une formule $A$ de l'arithmétique est vraie, ou simplement que l'on
a $A$ si $A$ est vraie dans les entiers. En particulier on dira que deux
énoncés $A$ et $B$ traitant des entiers sont équivalents s'ils sont équivalents
dans les entiers.

\paragraph{Formules $\Delta$, $\Sigma$ et $\Pi$.}
Les formules $\Delta$ sont définies par récurrence~:
\begin{itemize}
\item les formules atomiques sont $\Delta$~;
\item si $A$ et $B$ sont $\Delta$ alors $\neg A$, $A\et B$, $A\ou B$ sont
  $\Delta$~;
\item si $A$ est $\Delta$ et si $t$ est un terme ne contenant pas $x$ alors
  $\forall x(x<t\fleche A)$ (que l'on notera $\forallb xt\,A$) et $\exists
  x(x< t\et A)$ (que l'on notera $\existsb xt\,A$) sont $\Delta$.
\end{itemize}

\begin{rem}
  Les quantificateurs $\forallb xt$ et $\existsb xt$ sont appelés
  \emph{quantificateurs bornés}. Une formule $\Delta$ est donc une formule dans
  laquelle tous les quantificateurs sont bornés.
\end{rem}

Les formules $\Sigma$ sont données par~:
\begin{itemize}
\item les formules atomiques et leurs négations sont $\Sigma$~;
\item si $A$ et $B$ sont $\Sigma$ alors $A\et B$ et $A\ou B$ sont
  $\Sigma$~;
\item si $A$ est $\Sigma$ et si $t$ est un terme ne contenant pas $x$ alors
  $\forallb xt\,A$ est $\Sigma$~;
\item si $A$ est $\Sigma$ alors $\exists xA$ est $\Sigma$.
\end{itemize}

Une formule $\Pi$ est la négation d'une formule $\Sigma$.

\begin{rem}
  L'ensemble des formules $\Delta$ est inclus dans l'ensemble des formules
  $\Sigma$. L'inclusion est bien entendu stricte, mais il y a tout de même une
  <<~réciproque~>> au sens du lemme suivant.
\end{rem}

\begin{lemme}
  Si $A$ est $\Sigma$ alors il existe une formule $A_0$ qui est $\Delta$ et
  telle que $A$ est équivalente à $\exists xA_0$.
\end{lemme}
Ce lemme très utile, sera souvent utilisé sans référence dans la suite.

\begin{proof}
  On choisit une variable $x$ qui n'apparait pas dans $A$ (ni libre, ni liée)
  et on remplace chaque quantificateur non borné $\exists y$ de $A$ par
  $\exists y<x$. On obtient ainsi une formule $A_0$ qui est $\Delta$ et on voit
  facilement que $A$ est équivalente à $\exists x\,A_0$.
\end{proof}

\paragraph{Notations diverses.}
Soit $A$ une formule. On écrira $A[x_1, \dots, x_k]$ (ou $A[\vec x])$ pour dire
que $x_1$, \dots, $x_k$ sont des variables libres de $A$ et dans ce cas on
écrira $A[t_1,\dots,t_k]$ (ou $A[\vec t]$) pour désigner la formule $A$ dans
laquelle chaque variable $x_i$ est remplacée par le terme $t_i$, \ie, $A[\vec
t] = A[t_1/x_1,\dots,t_k/x_k]$. A ce propos on rappelle que la notation
$A[t_1/x_1,\dots,t_n/x_n]$ désigne la substitution \emph{sans capture de
  variable}. On se reportera au premier chapitre du Krivine~\cite{Krivine90b}
pour une définition rigoureuse d'ycelle.

\aere
Soit $a$ un entier, on note $\Term a$ le terme définie par récurrence par~:
\begin{itemize}
\item si $a = 0$ alors $\Term a$ est $\Zero$~;
\item si $a = b + 1$ alors $\Term a$ est $\Succ\Term b$.
\end{itemize}

\aere
Soit $t$ un terme clos. On note $\Val t$ la \emph{valeur} de $t$ définie par
récurrence par~:
\begin{itemize}
\item si $t$ est $\Zero$ alors $\Val t = 0$~;
\item si $t$ est $\Succ u$ alors $\Val t = \Val u + 1$~;
\item si $t$ est $u\Plus v$ alors $\Val t = \Val u + \Val v$~;
\item si $t$ est $u\Mult v$ alors $\Val t = \Val u\Val v$.
\end{itemize}

On voit donc que $\Val{\Term a} = a$ pour tout entier $a$.


\section{Fonctions (primitive) récursives}

\paragraph{Notations.}
Soient $x_1$, \dots, $x_k$ des objets. Lorsque le contexte est clair on écrira
$\vec x$ en lieu et place de $x_1,\dots,x_k$~; par exemple le $l$-uplet
$(a_1,\dots,a_l)$ s'écrira simplement $(\vec a)$. On utilisera les lettres $a$,
$b$, $c$, $k$, $l$, $n$, $m$ pour désigner des entiers, $t$, $u$, $v$ pour les
termes, $x$, $y$, $z$ pour les variables, $F$, $G$, $H$ pour les fonctions,
$P$, $Q$, $R$ pour les prédicats.

Si $e$ est une expression entière dépendant (ou pas) des variables $x_1$,
\dots, $x_k$ (par exemple $e = x_1+x_2$) on notera $\Abs{\vec x}e$ la
fonction qui à tout $k$-uplet d'entiers $(\vec a)$ associe $e(\vec a)$. En
particulier si $n$ est un entier, $\Abs xn$ représente la fonction
constante de valeur $n$.

\paragraph{Prédicats.}
On appelle \emph{prédicat} d'arité $k$ toute relation $k$-aire entre entiers où
équivalemment, tout sous-ensemble de $\Nat^k$. Si $P$ est un prédicat $k$-aire
on notera indifféremment $(\vec a) \in P$ ou $P(\vec a)$.  La \emph{fonction
  caractéristique} de $P$ est $\car P:\Nat^k\fleche\Nat$ définie par $\car
P(\vec a) = 0$ si $P(\vec a)$ (\ie, si $\vec a\in P$), $\car P(\vec a) = 1$
sinon. Remarquons que l'on prend ici une convention qui semble peu naturelle à
savoir que $0$ représente la valeur vraie et $1$ la valeur faux~; ce choix
s'explique pour des raisons techniques que l'on verra apparaître un peu plus
bas.

\paragraph{Fonctions partielles.}
Une fonction \emph{partielle} $F$ (d'arité $k$) de $\Nat^k\fleche\Nat$ est
donnée par une partie $\Dom F$ de $\Nat^k$ appelée le \emph{domaine} de $F$ et
une fonction de $\Dom F\fleche\Nat$. Si $\Dom F=\Nat^k$ on dit que $F$ est
\emph{totale}. On notera $\Def{F(\vec a)}$ (resp.  $\Undef{F(\vec a)}$) pour
$(\vec a)\in\Dom F$ (resp. $(\vec a)\not\in\Dom F$).

Si $F$ est partielle d'arité $k$ et $G$ est partielle d'arité $l$, $F(\vec a) =
G(\vec b)$ signifie que soit $\Undef{F(\vec a)}$ et $\Undef{G(\vec b)}$, soit
$\Def{F(\vec a)}$ et $\Def{G(\vec b)}$ et $F(\vec a) = G(\vec b)$.

\subsection{Fonctions récursives}

Une fonction partielle d'arité $k$ de $\Nat^k\fleche\Nat$ est \emph{récursive}
si on peut la définir en appliquant un nombre fini de fois les schémas
suivant~:
\begin{description}
\item[\R1] les projections $\Proj^k_i: (\vec a)\fleche a_i$ sont récursives
  totales (d'arité $k$)~; l'addition, la multiplication et la fonction
  caractéristique $\car<$ sont récursives totales (d'arité 2)~;
\item[\R2 (schéma de composition)] Si $H$ est récursive (d'arité $n$) et $G_1$,
  \dots, $G_n$ sont récursives (d'arité $k$) alors la \emph{composée} $F$~:
  \begin{displaymath}
    F(\vec a) \fleche H(G_1(\vec a), \dots, G_n(\vec a))
  \end{displaymath}
  est récursive. Son domaine est défini par~;
  \begin{displaymath}
    \Def{F(\vec a)}\quad\ssi\quad\Def{G_i(\vec a)}\text{ pour $i=1$, \dots, $n$ et }\Def{H(G_1(\vec a), \dots, G_n(\vec a))}
  \end{displaymath}
\item[\R3 (schéma de minimisation)] Si $G$ est récursive d'arité $k+1$ alors la
  fonction $F$~: 
  \begin{displaymath}
    F(\vec a) = \Prem x{G(x,\vec a) = 0}
  \end{displaymath}
  dont la valeur (si elle est définie) est le plus petit $x$ tel que $G(x,\vec
  a)=0$ et le domaine est donné par~:
  \begin{displaymath}
    \Def{F(\vec a)}\quad\ssi\quad
    \begin{cases}
      \forall b<a,\,\Def{G(b,\vec a)}\text{ et }G(b,\vec a)>0\\
      \Def{G(a,\vec a)}\text{ et }G(a,\vec a)=0
    \end{cases}
  \end{displaymath}
\end{description}

\begin{rem}
  Le schéma de minimisation est le seul qui peut produire des fonctions non
  totales. Par exemple la fonction $F(a)=\Prem x{\car<(x, 0) = 0}$ ($F(a)$ est
  le premier entier strictement plus petit que $0$) est nulle part définie ce
  qui ne l'empêche pas d'être récursive.
\end{rem}

\paragraph{Prédicats récursifs, récursivement énumérables.}
Un prédicat est récursif si sa fonction caractéristique est récursive totale.
Un prédicat $P$ est \emph{récursivement énumérable} s'il est le domaine d'une
fonction récursive, c'est à dire s'il existe $F$ récursive telle que $P(\vec
a)$ ssi $\Def{F(\vec a)}$ pour tout $k$-uplet $(\vec a)$.  On utilise
communément l'abbréviation \emph{r.e.} pour <<~récursivement énumérable~>>.

\begin{rem}
  Un prédicat récursif est récursivement énumérable~: soit $F$ définie par
  $F(a) = \Prem x{a = 0}$. Alors $F$ est récursive (pourquoi~?) et on a
  $\Def{F(a)}$ ssi $a=0$. Par conséquent $\Def{F(\car P(\vec a))}$ ssi $P(\vec
  a)$. Comme $\car P$ est récursive $F\circ\car P$ l'est par schéma de
  composition et donc $P$ est récursivement énumérable.
\end{rem}

\subsection{Définissabilité des fonctions récursives}

\begin{theo}[Définissabilité]
  \label{theo:definissabilite}
  \emph{(i)} Si $F$ est une fonction récursive d'arité $k$ alors il existe une
  formule $A[\vec x, y]$ qui est $\Sigma$ et qui \emph{définit} $F$, c'est à
  dire que~:
  \begin{displaymath}
    F(\vec a) = b \ssi A[\vec{\Term a}, \Term b]
  \end{displaymath}
  
  \emph{(ii)} Si $P$ est un prédicat r.e. d'arité $k$ alors il existe une
  formule $A[\vec x]$ qui est $\Sigma$ et qui \emph{définit} $P$, c'est à
  dire que~:
  \begin{displaymath}
    P(\vec a) \ssi A[\vec{\Term a}]
  \end{displaymath}
\end{theo}

\begin{proof}
  La deuxième partie du théorème se déduit de la première~: si $P$ est r.e.
  alors il y a une fonction récursive $F$ telle que $P(\vec a)$ ssi
  $\Def{F(\vec a)}$, c'est à dire ssi $\exists y\,y = F(\vec a)$.  D'après
  \emph{(i)} il y a une formule $A[\vec x, y]$ qui définit $F$ et qui est
  $\Sigma$~; mais alors $B=\exists yA[\vec x,y]$ définit $P$ et comme $A$
  est $\Sigma$, $B$ l'est aussi.
  
  La première partie se démontre par récurrence sur la construction de $F$. Si
  $F$ est la projection $\Proj_i^k$ alors $F$ est définie par $y=x_i$~;
  l'addition est définie par $y = x_1 \Plus x_2$ et la multiplication par
  $y = x_1\Mult x_2$. Enfin $\car <$ se définit par $(x_1 < x_2 \et y =
  \Zero) \ou (x_1 \not< x_2 \et y = \Succ\Zero)$ ($x_1\not< x_2$ est une
  abbréviation pour $\neg(x_1<x_2)$). Remarquons que pour l'instant toutes ces
  formules sont $\Delta$.
  
  Si $F(\vec a) = H(\vec G(\vec a))$ où les $G_i$ et $H$ sont récursives alors
  par hypothèse de récurrence il y a des formules $B_i[\vec x,y_i]$ pour
  $i=1,\dots,n$ et $C[\vec y, y]$ qui sont $\Sigma$ et qui définissent
  respectivement les $G_i$ et $H$. On pose
  \begin{displaymath}
    A = \exists y_1\dots\exists y_n\,B_1[\vec x,y_1]\et\dots\et B_n[\vec
    x,y_n]\et C[\vec y,y]
  \end{displaymath}
  Clairement $A$ est $\Sigma$ et définit $F$.
  
  Enfin si $F(\vec a) = \Prem x{G(x,\vec a) = 0}$ où $G$ est récursive alors
  par hypothèse de récurrence il y a une formule $B[x,\vec x, y]$ qui est
  $\Sigma$ et qui définit $G$. On pose
  \begin{displaymath}
    A = \forallb {y'}y\exists z\,B[y', \vec x, \Succ z]\et B[y,\vec x, \Zero]
  \end{displaymath}
\end{proof}
(Question~: pourquoi n'a-t-on pas défini $A=\forallb {y'}y\,\neg B[y', \vec x,
0]\et B[y,\vec x, \Zero]$~?)

\subsection{Fonctions primitives récursives}

Il est bien clair que parmi les fonctions récursives on est plus intéressé par
celles qui sont totales~: du point de vue informatique la totalité correspond à
la notion de \emph{correction} de programme, c'est à dire que lorsqu'on écrit
$\Undef{F(\vec a)}$ cela correspond à un programme qui <<~bugge~>> sur
l'entrée $\vec a$ (typiquement en entrant dans une boucle infinie).

Toutefois l'ensemble des fonctions récursives totales n'a pas de bonnes
propriétés, par exemple bien qu'il soit visiblement dénombrable, il n'est pas
récursivement énumérable.%
\footnote{On le démontre par \emph{diagonalisation}~: on verra un peu plus loin
  qu'un ensemble $X$ est r.e. ssi il existe une fonction récursive totale $F$
  qui \emph{énumère} $X$, c'est à dire telle que $X$ est l'image de $F$. Soit
  $T_1$ l'ensemble des fonctions récursive totales unaires et $\varphi$ une
  fonction de $\Nat^2$ dans $\Nat$ qui énumère $T_1$, c'est à dire telle que
  pour toute $F$ dans $T_1$ il existe un $e_F$ tel que $F(a) = \varphi(e_F, a)$
  pour tout $a$.  On va voir que $\varphi$ ne peut être récursive. Définissons
  $G$ par $G(a) = \varphi(a, a) + 1$~; alors $G$ est clairement totale et
  unaire mais elle ne peut être récursive, sinon elle est dans $T_1$ et il y a
  un $e_G$ tel que $G(a) = \varphi(e_G, a)$ pour tout $a$ donc en particulier
  pour $a =e_G$, $G(e_G) = \varphi(e_G, e_G)$ contredisant la définition de
  $G$.  Donc $\varphi$ n'est pas récursive, sinon $G$ le serait également.}
%
C'est pourquoi on est amené à introduire des classes de fonctions récursives
totales bénificiant de meilleures propriétés.  On verra plus tard dans le cours
les fonctions représentables par des lambda-termes typés mais tout de suite on
va introduire les \emph{fonctions primitives récursives}.

Une fonction de $\Nat^k\fleche\Nat$ est primitive récursive (p.r.) si on peut
l'obtenir en appliquant un nombre fini de fois les schémas suivant~:
\begin{description}
\item[\PR1] Les projections $\Proj^k_i$, l'addition, la multiplication, la
  fonction caractéristique de $<$ \emph{et les fonctions constantes} $\Abs{\vec
    x}n$ sont primitives récursives~;
\item[\PR2 (schéma de composition)] idem que pour les fonctions récursives~;
\item[\PR3 (schéma de récurrence)] si $G$ est primitive récursive d'arité $k$
  et $H$ est primitive récursive d'arité $k+2$ alors $F$ définie par~:
  \begin{displaymath}
    F(a, \vec a) = 
    \begin{cases}
      G(\vec a) &\text{si } a = 0\\
      H(F(a-1,\vec a), a, \vec a) &\text{si } a>0
    \end{cases}
  \end{displaymath}
  est primitive récursive d'arité $k+1$.
\end{description}

\paragraph{Prédicat récursif primitif.}
Un prédicat est primitif récursif si sa fonction caractéristique l'est.

\begin{theo}\label{theo:recprim}
  Si $F$ est une fonction primitive récursive alors $F$ est récursive
  (totale). Si $P$ est un prédicat primitif récursif alors $P$ est récursif.
\end{theo}

\begin{proof}
  La démonstration qui suit est initialement due à Gödel~; c'est une variante
  de celles que l'on trouvera dans le Shoenfield~\cite{Shoenfield67} et/ou le
  Cori-Lascar~\cite{CoriLascar93}.  Remarquons tout d'abord que la partie
  traitant des prédicats est conséquence immédiate de celle sur les fonctions.
  
  On va montrer que chacun des schémas \PR1, \PR2 et \PR3 peut se
  <<~programmer~>> à l'aide des schémas \R1, \R2 et \R3. Pour \PR1 il faut
  juste voir que les fonctions constantes sont programmables. La fonction
  $C_0=\Abs{\vec x}0$ est donnée par $C_0(\vec a)=\Prem x\Proj_1^{k+1}(x,\vec
  a) = 0$~; la fonction $C_1=\Abs{\vec x}1$ par $C_1(\vec x) = \Prem x\car<(0,
  x) = 0$.  Remarquons que c'est cette définition qui justifie le choix
  technique et peu naturel de prendre $0$ pour valeur vraie des fonctions
  caractéristiques. La fonction $C_2=\Abs{\vec x}2$ est donnée par $C_2(\vec x)
  = C_1(\vec x)+C_1(\vec x)$, et plus généralement on définit $C_{n+1}$ par
  $C_{n+1}(\vec x) = C_n(\vec x)+C_1(\vec x)$.
  
  Le schéma \PR2 est le même que le schéma \R2~; reste donc à voir le schéma de
  récurrence primitive \PR3 et c'est là qu'il va falloir travailler un peu. On
  commence par dériver de \R1, \R2 et \R3 des schémas supplémentaires pour
  programmer des fonctions récursives.
  
  Soit $P(x,\vec x)$ un prédicat récursif. Alors la fonction définie par
  $F(\vec a) = \Prem x{P(x,\vec a)}$ est récursive~; en effet comme $P$ est
  récursif $\car P$ est récursive (totale), et donc $F$ est obtenue par $\R3$
  (ici aussi on se sert du choix $\car P(a,\vec a) = 0$ ssi $P(a,\vec a)$).  Si
  de plus pour tout $\vec a$ il y a un $a$ tel que $P(a,\vec a)$ alors $F$ est
  totale.

  La fonction $\Abs {xy}{x\Moins y}$ est récursive (totale)~: on l'obtient par
  $a\Moins b = \Prem x{x+b+1>a}$.

  Soient $P$ et $Q$ des prédicats récursifs~; alors $\neg P$, $P\ou Q$, $P\et
  Q$ sont récursifs. En effet leurs fonctions caractéristiques s'obtiennent au
  moyen de celles de $P$ et $Q$ par les opérations arithmétiques $+$, $.$ et
  $\Moins$ qui sont tous récursifs totals. Remarquons que si on suppose $P$
  seulement r.e. alors $\neg P$ n'est pas r.e. en général (pourquoi~?).
  
  Soit $P(x,\vec x)$ un prédicat récursif et $F(\vec x)$ une fonction récursive
  totale~; alors la fonction $G(\vec x)$ définie par $G(\vec a) = \Premb
  x{F(\vec a)}P(x,\vec a)$ (le premier $x<F(\vec a)$ tel que $P(x,\vec a)$ s'il
  en existe, $F(\vec a)$ sinon), est récursive totale. En effet $G(\vec a)$ est
  égal à $\Prem x{(x<F(\vec a)\et P(x,\vec a))\ou x=F(\vec a)}$. En particulier
  le prédicat $\existsb x{F(\vec a)}{P(x,\vec a)}$ est récursif puisqu'il est
  équivalent à $(\Premb x{F(\vec a)}{P(x,\vec a)})<F(\vec a)$.  Par négation le
  prédicat $\forallb x{F(\vec a)}{P(x,\vec a)}$ est également récursif.

  \begin{lemme}
    Il existe une fonction $\beta$ récursive totale vérifiant~: pour tout $n$
    et tous $a_0$, \dots, $a_n$, il existe $c$ tel que pour $i=0,\dots,n$ on a
    $\beta(i, c) = a_i$.
  \end{lemme}
  On ne va pas démontrer ce lemme ici et l'on renvoie le lecteur aux références
  sus-citées~; Lascar-Cori le dérive du lemme chinois et Shoenfield le prouve
  in extenso au moyen de simples récurrences.
  
  On note $\P ci=\beta(i, c)$.  Muni du lemme on va pouvoir démontrer que le
  schéma de récurrence primitive \PR3 est récursif.
  
  Soit $G(\vec x)$ et $H(x,y,\vec x)$ des fonctions récursives totales. On
  définit $\bar F(x,\vec x)$ par~:
  \begin{displaymath}
    \bar F(a,\vec a) = \Prem x{\Bigl(\P x0 = G(\vec a)\et \forallb ya{
        \bigl(\P x{y+1}= H(\P xy, y+1, \vec a)\bigr)}\Bigr)}.
  \end{displaymath}
  La fonction $\bar F$ est clairement récursive et on peut facilement se
  convaincre par récurrence sur $n$ qu'elle est totale. Soit maintenant $F$
  donnée par $F(a,\vec a)=\P{\bar F(a,\vec a)}a$~; alors $F$ est également
  récursive totale et on peut vérifier par récurrence sur $a$ que l'on a
  $F(0,\vec a)=G(\vec a)$ et $F(a+1,\vec a)=H(F(a,\vec a), a, \vec a)$ pour
  tout $a$, soit que $F$ est définie par récurrence primitive à partir de $G$
  et $H$.
\end{proof}

\subsection{Programmation de fonctions primitives récursives.}
On va maintenant se donner un certain nombre d'autres schémas pour définir des
fonctions et prédicats p.r.

\paragraph{Itération.}
Si $G$ est p.r. d'arité $k+1$ alors la fonction $F$ définie par~:
\begin{displaymath}
  F(a,b,\vec a) = G^a(b,\vec a)
\end{displaymath}
est p.r. d'arité $k+2$. En fait c'est une reformulation du schéma de récursion
primitive. Clairement $F$ est donnée par $F(0, b, \vec a) = b$ et $F(a+1, b,
\vec a) = G(F(a, b, \vec a), \vec a)$.

\paragraph{Soustraction.}
On définit $a\Moins 1$ par~: $0\Moins 1 = 0$ et $(a+1)\Moins 1 = a$. 
On définit $a\Moins b$ par $a\Moins 0 = a$ et $a\Moins (b+1) = (a\Moins
b)\Moins 1$. La fonction binaire $\Moins$ est clairement p.r.

\paragraph{Variante de la récursion primitive.}
Soient $G_0$ une fonction p.r. d'arité $k$, $H$ p.r. d'arité $k+2$ et
$G_1$,\dots, $G_k$ des fonctions p.r. d'arité $k+1$ . Alors la fonction $F$
définie par
\begin{align*}
  F(0,\vec a) &= G_0(\vec a)\\
  F(a+1,\vec a) &= H(F(a, \vec G(a,\vec a)),a,\vec a)
\end{align*}
est p.r. Remarquons qu'il s'agit presque du schéma de récurrence p.r. On va le
montrer pour $k=1$, le cas général s'en déduit immédiatement en utilisant des
séquences.

Supposons donc que $F$ est définie par 
\begin{align*}
  F(0,b) &= G_0(b)\\
  F(a+1, b) &= H(F(a,G_1(a,b)),a,b)
\end{align*}
On se donne $g$~:
\begin{align*}
  g(0, b, a) &= b\\
  g(i+1, b, a) &= G_1(a\Moins (i+1), g(i, b, a))
\end{align*}
et $h$~:
\begin{align*}
  h(0, b, a) &= G_0(g(a,b,a))\\
  h(i+1, b, a) &= H(h(i, b, a), i, g(a\Moins (i+1), b, a))
\end{align*}
Il est clair que $g$ et $h$ sont toutes les deux p.r. On va montrer que pour
tout $b$~:
\begin{equation}\label{eq:1}
  F(a,b) = h(a,b,a)
\end{equation}
Comme $h$ est p.r. on en déduira que $F$ l'est.

On vérifie aisément par récurrence sur $i$ que pour tout $a\geq i$ on a
\begin{equation}\label{eq:2}
  g(i+1, b, a+1) = g(i, G_1(a,b), a)
\end{equation}
puis que
\begin{equation}\label{eq:3}
  h(i,b,a+1) = h(i,G_1(a,b),a)
\end{equation}

On montre \eqref{eq:1} par récurrence sur $a$. Pour $a=0$ on a
$h(0,b,0)=G_0(g(0,b,0))=G_0(b)=F(0,b)$. Supposons que $F(a,b)=h(a,b,a)$. Alors
{\def\t#1{\qquad\text{#1}}
\begin{alignat*}{2}
  h(a+1,b,a+1) &= H(h(a,b,a+1), a, g(0, b, a+1)) &&\t{par définition de $h$}\\
               &= H(h(a,b,a+1), a, b)            &&\t{par définition de $g$}\\
               &= H(h(a,G_1(a,b),a), a, b) &&\t{par l'équation~\eqref{eq:3}}\\
               &= H(F(a,G_1(a,b)), a, b)   &&\t{par hypothèse de récurrence}\\
               &= F(a+1, b)                &&\t{par définition de $F$}
\end{alignat*}}

\paragraph{Opérations booléennes.}
Si $P$ et $Q$ sont p.r. d'arité $k$ alors $\neg P$, $P\ou Q$, $P\et Q$ sont
p.r.~: $\car{\neg P}(\vec a) = 1\Moins \car P(\vec a)$, $\car{P\ou Q}(\vec a) =
\car P(\vec a)\car Q(\vec a)$, $\car{P\et Q}(\vec a) = 1\Moins(1\Moins\car
P(\vec a))(1\Moins\car Q(\vec a))$.

\paragraph{Définitions par cas.}
Si $P$ est un prédicat p.r. d'arité $k$, $G$ et $H$ sont p.r. d'arité $k$ alors
$F$ définie par~:
\begin{displaymath}
  F(\vec a) =
  \begin{cases}
    G(\vec a) &\text{si } P(\vec a)\\
    H(\vec a) &\text{sinon}
  \end{cases}
\end{displaymath}
est p.r.~: on l'obtient par $F(\vec a) = (1\Moins\car P(\vec a))G(\vec a) +
\car P(\vec a)H(\vec a)$. Plus généralement si $P_1$, \dots, $P_n$ sont
p.r. et $G_1$, \dots, $G_{n+1}$ sont p.r. alors
\begin{displaymath}
  F(\vec a) =
  \begin{cases}
    G_1(\vec a) &\text{si }P_1(\vec a)\\
    \quad\vdots\\
    G_n(\vec a) &\text{si }\neg(P_1(\vec a)\ou\dots\ou P_{n-1}(\vec a))\et
                           P_n(\vec a)\\
    G_{n+1}(\vec a) &\text{sinon}
  \end{cases}
\end{displaymath}
est p.r.

\paragraph{Quelques prédicats p.r.}
Par définition $<$ est p.r. C'est également le cas de $\not<$, $=$,
$\not=$, $\leq$, $\not\leq$, $>$, $\not>$, $\geq$, $\not\geq$~: par exemple
$\car{\not<}(a,b)=1\Moins\car<(a,b)$,
$\car==\car{\not<\et\not>}$, \dots

\paragraph{Minimisation bornée.}
Si $P$ est p.r. alors $F$ donnée par $F(a,\vec a)=\Premb xa{P(x,\vec a)}$ dont
la valeur est le premier $b<a$ tel que $P(b,\vec a)$ s'il en existe, $a$ sinon,
est p.r. On la définit par $F(a,\vec a) = G(a\Moins 1, a, \vec a)$ où $G$ est
donnée par~:
\begin{alignat*}{2}
  G(0, b, \vec a) &= 0 &\quad&\text{si $P(0,\vec a)$}\\
  G(0, b, \vec a) &= b &&\text{si $\neg P(0,\vec a)$}\\
  G(a+1, b, \vec a) &= G(a, a+1, \vec a)&&\text{si } P(a+1,\vec a)\\
  G(a+1, b, \vec a) &= G(a, b, \vec a)&&\text{sinon}
\end{alignat*}


\paragraph{Quantificateurs bornés.}
Si $P$ est un prédicat p.r. d'arité $k+1$ alors $\forallb xa\,P(x,\vec a)$ et
$\existsb xa\,P(x,\vec a)$ sont p.r.~: le second est défini par~: $\existsb
xa\,P(x,\vec a)$ ssi $\Premb xa{P(x,\vec a)}<a$ (\ie, $\car{\existsb
  xa\,P}(\vec a) = \car<(\Premb xa{P(x,\vec a)},a)$), le premier par $\forallb
xa\,P$ ssi $\neg\existsb xa\,\neg P(x,\vec a)$ (\ie, $\car{\forallb
  xa\,P}=1\Moins\car{\existsb xa\,\neg P}$).

\paragraph{Arithmétique.}
Les fonctions binaires $\Abs{xy}{x/y}$ (quotient de $x$ par $y$ ) et $\Abs
{xy}{x\%y}$ (reste de $x$ modulo $y$) sont p.r.~: la première est donnée par
$a/b = (\Premb x{a+1}{a<xb})\Moins 1$ et la seconde par $a\%b = a\Moins(a/b)b$.
Le prédicat $a\Div b$ ($a$ divise $b$) se définit par $a\%b=0$ et est donc
p.r.

\paragraph{Suites d'entiers.}
On définit la fonction $\Abs{xy}{\Couple xy}$ par
\begin{displaymath}
  \Couple ab = ((a+b)(a+b+1))/2+a
\end{displaymath}
Il est clair qu'elle est p.r.
\aere
On définit $\pi_1$ et $\pi_2$ par~:
\begin{gather*}
  \pi_1c = \Premb x{c+1}{\existsb y{c+1}\,\Couple xy = c}\\
  \pi_2c = \Premb y{c+1}{\existsb x{c+1}\,\Couple xy = c}
\end{gather*}
$\pi_1$ et $\pi_2$ sont donc p.r. et, comme $\Abs{xy}{\Couple xy}$ est
bijective on a $\Couple{\pi_1 a}{\pi_2a} = a$ pour tout $a$.

Pour chaque $k$ on pose~:
\begin{displaymath}
  \Seq k{a_1\dots, a_k} = \Couple k{\Couple{a_1}{\dots\Couple{a_{k-1}}{a_k}\dots}}
\end{displaymath}
Plus précisément les fonction $\Abs{\vec x}\Seq k{\vec x}$ sont définies par~:
\begin{align*}
  \Seq 0{} &= 0\\
  \Seq{k+1}{a_0, \vec a} &= \Couple{k+1}{\Couple{a_0}{\pi_2\Seq k{\vec a}}}
\end{align*}
On voit donc (par récurrence sur $k$) que chacune d'elles est p.r.
\begin{itemize}
\item L'ensemble des (codes de) suites est caractérisé par le prédicat
  $\Seqp$~: $\Seqp(a)$ ssi $\pi_1a\not= 0 \ou a = 0$.
  
\item La longueur d'une suite est $\Length a = \pi_1 a$.
  
\item Le $i$-ème élément de la suite $a$ est $\P ai = \pi_1\pi_2^ia$ si
  $i<\Length a$, $\pi_2^{\Length a}a$ sinon.

La concaténation $\Concat ab$ des suites $a$ et $b$ est donnée par
$\Concat ab = \Couple{\Length a +\Length b}{F(\Length a, \pi_2a, \pi_2b)}$ où
$F$ est définie par $F(0, a, b) = b$, $F(1,a,b)=\Couple ab$ et $F(l+1, a, b) =
\Couple{\pi_1a}{F(l, \pi_2a, b)}$.

\item La suite d'une liste est donnée par $\Tail a =0$ si $\Length a = 0$,
  $\Tail a = \Premb xa{\Concat{\Seq1{\P a1}}x=a}$ sinon. Donc on a
  \begin{displaymath}
    \Tail\Seq n{a_1,\dots,a_n}=\Seq{n-1}{a_2,\dots,a_n}
  \end{displaymath}
En particulier si $\Length a >0$ alors $\Tail a<a$. Ceci nous permettra de
définir des fonctions par récurrence sur des listes d'entiers.
\end{itemize}

\begin{rem}
  A cause de la bijectivité de $\Abs{xy}{\Couple xy}$, si $a$ et $b$ sont deux
  (codes de) suites telles que  $\Length a = \Length b$ et pour tout
  $i\leq\Length a$, $\P ai = \P bi$ alors $a=b$.
\end{rem}

Toutes ces fonctions (et prédicats) sont clairement p.r.


\paragraph{Récurrence générale.}
Soit $F$ une fonction p.r. d'arité $k+1$. On note $\bar F$ la fonction donnée
par~:
\begin{displaymath}
  \bar F(a,\vec a) = \Seq {a}{F(0,\vec a),\dots, F(a-1,\vec a)}
\end{displaymath}
Alors $\Bar F$ est p.r. En effet on l'obtient par~: $\bar F(0, \vec a) = \Seq
0{}$ et $\bar F(a+1,\vec a) = \Concat{\bar F(a, \vec a)}{\Seq 1{F(a)}}$.

Soit maintenant $G$ une fonction p.r. d'arité $k+1$. Alors la fonction $F$
définie par (récurrence généralisée)~:
\begin{displaymath}
  F(a, \vec a) = G(\bar F(a, \vec a), \vec a)
\end{displaymath}
est p.r. Soit $H$ donnée par $H(0, \vec a) = \Seq 0{}$ et $H(a+1, \vec a) =
\Concat{H(a,\vec a)}\Seq 1{G(H(a,\vec a), \vec a)}$ qui est donc p.r.  On
montre facilement par récurrence sur $a$ que $H(a,\vec a) =\bar F(a,\vec a)$
d'où l'on déduit que $F$ est p.r. en considérant que $F(a,\vec a) =
\P{\bar F(a+1,\vec a)}{a+1}$.

\paragraph{Une autre récurrence.}
Soit $G_1$, \dots, $G_n$ des fonctions p.r. d'arité $k+1$ telles que
$G_i(a,\vec a)<a$ dès que $a>0$, $H_0$ une fonction p.r. d'arité $k$ et $H_1$
une fonction p.r. d'arité $n+k+2$. Alors la fonction $F$ donnée par~:
\begin{displaymath}
  F(a,\vec a) =
  \begin{cases}
    H_0(\vec a) &\text{si $a=0$}\\
    H_1(F(G_1(a,\vec a),\vec a), \dots, F(G_n(a,\vec a),\vec a), a, \vec a)
      &\text{sinon}
  \end{cases}
\end{displaymath}
est p.r. On définit $H$ par
\begin{displaymath}
  H(b, a, \vec a) =
  \begin{cases}
    H_0(\vec a) &\text{si $a=0$}\\
    H_1(\P b{G_1(a,\vec a)}, \dots, \P b{G_n(a,\vec a)}, a, \vec a)
    &\text{sinon}
  \end{cases}
\end{displaymath}
La fonction $H$ est clairement p.r., d'arité $k+2$ et $F$ est obtenue par
récurrence généralisée sur $H$~:
\begin{displaymath}
  F(a,\vec a) = H(\Bar F(a,\vec a), a, \vec a)
\end{displaymath}

\section{Codage de Gödel}

\lettrine{O}{n va maintenant} utiliser le petit <<~langage de programmation~>>
des fonctions p.r. pour représenter le formalisme du calcul des prédicats dans
les entiers.  A chaque objet $X$ du formalisme (variable, terme, formule,
démonstration) on va associer un entier unique $\Godel X$ appelé son \emph{code
  de Gödel}. On construit ensuite un ensemble de fonctions p.r. qui agissent
sur les codes de Gödel et implémentent toutes les transformations syntaxiques
standard, typiquement la substitution d'un ensemble de termes à un ensemble de
variable dans une formule ou un terme.

\subsection{Codage du formalisme}
Soit $L$ un langage, c'est à dire que $L$ est déterminé par sa signature
$\Sigma_L = (F_L, P_L)$ où $F_L$ est l'ensemble (au plus dénombrable) des
symboles de fonctions de $L$ et $P_L$ est l'ensemble (au plus dénombrable) des
symboles de prédicats. On suppose que $L$ contient le langage de l'arithmétique
c'est à dire que $\Zero$, $\Succ$, $\Plus$ et $\Mult$ sont dans $F_L$ et que
$=$ et $<$ sont dans $P_L$.

\paragraph{Représentation des symboles.}
Comme $F_L$ et $P_L$ sont au plus dénombrables on peut les énumérer par des
suites $(f_i)_{i<\sigma_L}$ et $(P_i)_{i<\tau_L}$ où $\sigma_L$ et $\tau_L$
sont les cardinaux respectifs (possiblement infinis) de $F_L$ et $P_L$. De même
comme l'ensemble des (noms de) variables du calcul des prédicats est
dénombrable on peut supposer que celui-ci est complètement énuméré par la suite
$(x_i)_{i\in\Nat}$.  Si $s$ est un symbole ou une variable, on définit alors
\begin{displaymath}
  \Godel s = 
  \begin{cases}
    \Seq 4{0,0,i,0} &\text{si $s=x_i$}\\
    \Seq 4{0,1,i,n} &\text{si $s=f_i$ et $f_i$ est d'arité $n$}\\
    \Seq 4{0,2,i,n} &\text{si $s=P_i$ et $P_i$ est d'arité $n$}\\
  \end{cases}
\end{displaymath}

\paragraph{Représentation des termes.}
Soit $t$ un terme du langage $L$~; on définit $\Godel t$ par~:
\begin{displaymath}
  \Godel t = 
  \begin{cases}
    \Seq4{1, 0, \Godel x, 0} &\text{si $t$ est la variable $x$}\\
    \Seq4{1, 1, \Godel f, \Seq n{\Godel{t_1},\dots,\Godel{t_n}}} &
      \text{si $t = f(t_1,\dots, t_n)$}
  \end{cases}
\end{displaymath}

\paragraph{Représentation des formules.}
Soit $A$ une formule du langage $L$. On définit $\Godel A$ par~:
\begin{displaymath}
  \Godel A =
  \begin{cases}
    \Seq4{2, 0, \Godel P, \Seq n{\Godel{t_1},\dots, \Godel{t_n}}} &
      \text{si $A$ est la formule atomique $P(t_1,\dots, t_n)$}\\
    \Seq4{2, 1, \Godel{A'}, 0} & \text{si $A=\neg A'$}\\
    \Seq4{2, 2, \Godel{A'},\Godel{A''}} &\text{si $A = A'\et A''$}\\
    \Seq4{2, 3, \Godel{A'},\Godel{A''}} &\text{si $A = A'\ou A''$}\\
    \Seq4{2, 4, \Godel{A'},\Godel{A''}} &\text{si $A = A'\fleche A''$}\\
    \Seq4{2, 5, \Godel x,\Godel{A'}} &\text{si $A = \forall x A'$}\\
    \Seq4{2, 6, \Godel x,\Godel{A'}} &\text{si $A = \exists x A'$}
  \end{cases}
\end{displaymath}

\begin{lemme}
  Soit $X$ un objet du langage (terme ou formule) et $Y$ un
  sous-objet de $X$~: par exemple $X$ est la formule $\Succ x<\Zero$ et $Y$ est
  la variable $x$. Alors $\Godel Y < \Godel X$.
\end{lemme}

La preuve est immédiate par récurrence sur $X$ et en considérant pour tout
$(a,b)\neq(0,0),(0,1)$ on a $a,b<\Couple ab$. Ce lemme servira dans ce qui
suit à définir des fonctions ou prédicats sur les (codes d') objets du
formalisme par récurrence sur leurs (codes) de sous-objets.

\paragraph{Prédicats de la signature.}
On définit les prédicats p.r.  $\VarP(a)$~: <<~$a$ est le code d'une
variable~>>, $\FunP(a, n)$~: <<~$a$ est le code d'un symbole de fonction
d'arité $n$~>>, $\PredP(a,n)$~: <<~$a$ est le code d'un symbole de prédicat
d'arité $n$~>> par~:
\begin{align*}
  \VarP(a) &\ssi\Length a = 4\et \P a1 = 0\et \P a2 = 0\\
  \FunP(a, n) &\ssi\Length a = 4 \et \P a1 = 0 \et \P a2 = 1 \et \P a4 = n\\
  \PredP(a, n) &\ssi \Length a = 4 \et \P a1 = 0 \et \P a2 = 2 \et \P a4 =
  n\\
\end{align*}

\paragraph{Objets du langage.}
On définit $\TermP(a)$~: <<~$a$ est le code d'un terme~>>, $\AtomP(A)$~: \og
$a$ est le code d'une formule atomique~>> et $\FormP(a)$~: <<~$a$ est le code
d'une formule~>> par~:
\begin{align*}
  \TermP(a) &\ssi\Length a = 4\et \P a1 = 1\et 
  \begin{cases}
    \P a2 = 0 \et \VarP(\P a3)\quad\text{ou}\\
    \P a2 = 1 \et \FunP(\P a3, \Length \P a4) \et\forallb i{\Length \P a4}\,
    \TermP(\P {\P a4}{i+1}
  \end{cases}\\
  \AtomP(a) &\ssi  \Length a = 4\et \P a1 = 2\et \P a2 = 0 \et \PredP(\P a3,
      \Length \P a4) \et \forallb i{\Length \P a4}\, \TermP(\P{\P a4}{i+1})\\
  \FormP(a) &\ssi\Length a = 4\et \P a1 = 2\et 
  \def\suite{&\text{ou}\\}
  \begin{cases}
    \AtomP(a)\suite
    \P a2 = 1 \et \P a4 = 0 \et \FormP\P a3\suite
    \P a2 = 2 \et \FormP \P a3 \et \FormP \P a4\suite
    \P a2 = 3 \et \FormP \P a3 \et \FormP \P a4\suite
    \P a2 = 4 \et \FormP \P a3 \et \FormP \P a4\suite
    \P a2 = 5 \et \VarP \P a3 \et \FormP \P a4\suite
    \P a2 = 6 \et \VarP \P a3 \et \FormP \P a4
  \end{cases}
\end{align*}


\subsection{Fonctions et prédicats manipulant le formalisme}

On définit une fonction $\Num$ par
\begin{align*}
  \Num(0) &= \Godel\Zero\\
  \Num(a+1) &= \Seq4{1,1,\Godel\Succ,\Seq1{\Num(a)}}
\end{align*}
$\Num$ est clairement p.r. et vérifie~:
\begin{displaymath}
  \Num(a) = \Godel{\Term a}
\end{displaymath}
pour tout entier $a$.

\paragraph{Variables libres.}
On définit le prédicat p.r. $\LibresP(a, b)$~: <<~$a$ est une séquence de
variables contenant toutes les variables libres de l'objet codé par $b$~>>,
par~:
{\def\suite{&\text{ou}\\}
\begin{multline*}
  \LibresP(a, b)\ssi\forallb i{\Length a}\, \VarP(\P a{i+1}) \et\\
  \begin{cases}
    \TermP(b) \et \P b2 = 0 \et \existsb i{\Length a}\, \P b3 = \P
    a{i+1}\suite
    \TermP(b) \et \P b2 = 1 \et \forallb i{\Length \P b4}\, \LibresP(a, \P{\P
      b4}{i+1})\suite
    \FormP(b) \et \P b2 = 0 \et \forallb i{\Length \P b4}\, \LibresP(a, \P{\P
      b4}{i+1})\suite
    \FormP(b) \et \P b2 = 1 \et \LibresP(a, \P b3)\suite
    \FormP(b) \et \P b2 = 2, 3\text{ ou } 4 \et (\LibresP(a, \P
    b3)\et\LibresP(a, \P b4))\suite
    \FormP(b) \et \P b2 = 5\text{ ou } 6 \et \LibresP(\Concat a{\Seq1{\P
        b3}}, \P b4)
  \end{cases}
\end{multline*}}

\begin{rem}
  La dernière clause concerne une formule de la forme $A=Qx\, B$ où $Q$ est
  l'un des quantificateurs~; dans ce cas on dit que $X$ est l'ensemble des
  variables libres de $A$ si $X\cup \{x\}$ est l'ensemble des variables libres
  de $B$.
\end{rem}

On définit la fonction p.r. $\LibresF(a)$ par~:
\begin{displaymath}
  \LibresF(a) = 
  \begin{cases}
    0 &\text{si $\neg\TermP(a)\ou\neg\FormP(a)$}\\
    \Premb x{\Seq a{a,\dots,a}}{\LibresP(x,a)} &\text{sinon}
  \end{cases}
\end{displaymath}
On a donc pour tout objet $X$
\begin{displaymath}
  \LibresF(\Godel X) = \Seq n{\Godel{x_1},\dots,\Godel{x_n}}
\end{displaymath}
où $x_1$, \dots, $x_n$ sont toutes les variables libres de $X$.

On définit le prédicat p.r. $\LibreP(a, b)$ (<<~$a$ est le code d'une
variable libre dans l'objet codé par $b$~>>)
par~:
\begin{displaymath}
  \def\suite{&\text{ou}\\}
  \LibreP(a, b)\ssi \VarP(a) \et
  \begin{cases}
    \TermP(b) \et \P b2 = 0 \et a = \P b3\suite
    \TermP(b) \et \P b2 = 1 \et \existsb i{\Length \P b4}\, \LibreP(a, \P{\P
      b4}{i+1})\suite
    \FormP(b) \et \P b2 = 0 \et \existsb i{\Length \P b4}\, \LibreP(a, \P{\P
      b4}{i+1})\suite
    \FormP(b) \et \P b2 = 1 \et \LibreP(a, \P b3)\suite
    \FormP(b) \et \P b2 = 2, 3\text{ ou } 4 \et (\LibreP(a, \P b3)\ou\LibreP(a,
      \P b4))\suite
    \FormP(b) \et \P b2 = 5\text{ ou } 6 \et a\neq \P b3\et \LibreP(a, \P b4)
  \end{cases}
\end{displaymath}

\paragraph{Objets clos.}
On définit $\ClosP(a)$ (<<~$a$ est le code d'un objet clos~>>) par 
\begin{displaymath}
  \ClosP(a) \ssi \LibresP(\Seq 0{}, a)
\end{displaymath}

\paragraph{Clôture universelle d'une formule.}
Soit $A$ une formule. La \emph{clôture universelle} $\Clot A$ de $A$ est la
formule $\forall x_1\dots\forall x_n\,A$ où $x_1$, \dots $x_n$ sont toutes les
variables libres de $A$.  On définit $\ClotF(a) = F(\LibresF(a), a)$ où $F$ est
donnée par
\begin{displaymath}
  F(l, a) = 
  \begin{cases}
    a &\text{si $\Length l = 0$}\\
    \Seq4{2,5,\P l1,\ClotF(\Tail l, a)} &\text{sinon}
  \end{cases}
\end{displaymath}
Clairement $\ClotF$ est p.r. vérifie
\begin{displaymath}
  \ClotF(\Godel A) = \Godel{\Clot A}
\end{displaymath}
pour toute formule $A$.

\paragraph{Substitution.}
On va maintenant définir la fonction p.r. $\Sub$ telle que~:
\begin{displaymath}
  \Sub(\Godel X, \Godel x, \Godel t) = \Godel{X[t/x]}
\end{displaymath}
pour tout terme ou formule $X$, et toute variable $x$ et terme $t$. Toutefois,
pour résoudre le problème de <<~capture de variable~>>, on va passer par une
fonction légèrement plus générale $\ParSub$ qui prend en argument (le code d')
un objet $X$ et (le code d') une séquence de (code de) couples $(x_i, t_i)$ et
qui effectue la substitution \emph{en parallèle} de chaque $x_i$ par $t_i$ dans
$X$. L'idée est, dans le cas où l'on substitue la variable $x$ par le terme $t$
dans une formule quantifiée, par exemple $Qy\, A$, d'exploiter le fait
que~:
\begin{displaymath}
  (Qy\, A)[t/x] \Equiv Qz\, A[z/y, t/x]
\end{displaymath}
où $z$ est une variable qui n'est pas libre dans $t$.

On définit $\Index$ par $\Index(a, b)=\Premb i{\Length b+1}{(i>0\et\pi_1\P bi =
  a)}$~; donc si $b = \Seq n{\Couple{a_1}{b_1},\dots,\Couple{a_n}{b_n}}$ alors
$\Index(a,b)$ est le premier $i$ tel que $a_i = a$, ou $n+1$ s'il n'existe
aucun tel $i$.

On définit $\ParSub$ par~:
\begin{displaymath}
  \begin{array}{ll}
    \qquad\ParSub(a, b) =\\
    0 &\text{si $\neg((\TermP(a)\ou\FormP(a))\et{}$}\\
      &\qquad\forallb i{\Length b}\,(\VarP(\pi_1\P bi)\et\TermP(\pi_2\P
      bi)))\\[1ex]
    \pi_2\P b{\Index(a, b)} &\text{si $\TermP(a)\et\P a2 =
      0\et\Index(a,b)\leq\Length b$}\\
    a &\text{si $\TermP(a)\et\P a2 = 0 \et\Index(a,b)>\Length b$}\\[1ex]
    \Seq4{1,1,\P a3, \Seq n{a_1,\dots, a_n}} &\text{si $\TermP(a)\et\P a2 =
      1\et n=\Length\P a4\et{}$}\\&\qquad \forallb i{n+1}\,(i= 0\ou
                                           a_i=\ParSub(\P {\P a4}i,b))\\[1ex]
    \Seq4{2,0,\P a3, \Seq n{a_1,\dots, a_n}} &\text{si $\FormP(a)\et\P a2 =
      0\et n=\Length\P a4\et{}$}\\&\qquad \forallb i{n+1}\,(i= 0\ou
                                          a_i=\ParSub(\P {\P a4}i,b))\\[1ex]
    \Seq4{2,1, \ParSub(\P a3, b),0} &\text{si $\FormP(a) \et\P a2 = 1$}\\
    \Seq4{2,\P a2, \ParSub(\P a3, b), \ParSub(\P a4, b)} &\text{si
      $\FormP(a)\et\P a2 = 3,4$ ou $5$}\\
    \Seq4{2,\P a2, V(a,b), \ParSub(\P a4, \Concat{\Seq1{\Couple{\P
            a3}{V(a,b)}}}b)} &\text{si $\FormP(a)\et \P a2 = 5$ ou $6$}
  \end{array}
\end{displaymath}
où $V(a,b) =\Seq4{0, 0, ab, 0}$ est le code de la variable de numéro $ab$. On
s'assure ainsi que cette variable n'apparait ni dans la formule codée par $a$,
ni dans aucun des termes dont les codes sont listés dans $b$. Remarquons que
l'on a en particulier~:
\begin{displaymath}
  \ParSub(\Godel{Qx\,A}, \Seq1{\Couple{\Godel x}{\Godel t}}) =
  \Godel{Qv\,\ParSub(\Godel A, \Seq2{\Couple{\Godel x}{\Godel v},\Couple{\Godel
        x}{\Godel t}})}
\end{displaymath}
si bien que la variable $x$ est substituée par la nouvelle variable $v$ dans
$A$, et non par $t$, ce qui est conforme à la définition de la substitution.

\begin{rem}
  Le prédicat $\ParSub$ est p.r. car il utilise essentiellement (dans la
  dernière clause) le schéma intitulé <<~variante de la récursion primitive~>>.
\end{rem}

On définit finalement $\Sub$ par~:
\begin{displaymath}
  \Sub(a,b,c) = \ParSub(a, \Seq1{\Couple bc})
\end{displaymath}

\paragraph{Quantificateurs bornés.}
On définit le prédicat $\QBP(a)$ (<<~$a$ est le code d'une formule $\forallb
xt\,A$ ou $\existsb xt\,A$~>>) par~:
\begin{displaymath}
  \QBP(a)\ssi \FormP(a) \et
  \begin{cases}
    \P a2 = 5 \et P(\P a4, 4, \P a3)\quad\text{ou}\\
    \P a2 = 6 \et P(\P a4, 2, \P a3)
  \end{cases}
\end{displaymath}
où $P(a,b,c)$ est le prédicat <<~$a$ est le code d'une formule
$x<t\mathop{\alpha}A'$ où $\alpha = {\fleche}$ si $b=4$, $\alpha = {\et}$ si
$b=2$ et où $x$ est la variable de code $c$ et $t$ est un terme ne contenant
pas $x$~>> défini par~:
\begin{displaymath}
  P(a,b,c)\ssi \FormP(a)\et \P a2 = b\et \P{\P a3}2 = 0 \et \P{\P a3}3 =
  \Godel< \et \P{\P{\P a3}4}1 = c\et \neg\LibreP(c, \P{\P{\P a3}4}2)
\end{displaymath}

\begin{theo}
  \label{theo:truep}
  Il existe une fonction p.r. $\ValF$ telle que pour tout terme clos $t$ de
  l'arithmétique
  \begin{displaymath}
    \ValF(\Godel t) = \Val t
  \end{displaymath}
  Il existe un prédicat p.r. $\TrueP$ telle que pour toute formule $A$ de
  l'arithmétique, $\Delta$ et close
  \begin{displaymath}
    \TrueP(\Godel A) \ssi A
  \end{displaymath}
\end{theo}

\begin{proof}
  La fonction $\ValF$ est définie par~:
  \begin{displaymath}
    \ValF(a) = 
    \begin{cases}
      0 &\text{si $\P a3 = \Godel{\Zero}$}\\
      \ValF(\P{\P a4}1)+1 &\text{si $\P a3 = \Godel{\Succ}$}\\
      \ValF(\P{\P a4}1)+\ValF(\P{\P a4}2) &\text{si $\P a3 = \Godel{\Plus}$}\\
      \ValF(\P{\P a4}1)\ValF(\P{\P a4}2) &\text{si $\P a3 = \Godel{\Mult}$}\\
      0 & \text{sinon}
    \end{cases}
  \end{displaymath}

  Le prédicat $\TrueP$ est défini par~:
  \begin{displaymath}
    \TrueP(a) \ssi \FormP(a)\et\ClosP(a)\et
    \begin{cases}
      \ValF(\P{\P a4}1)=\ValF(\P{\P a4}2) &\text{si $\P a2 = 0$ et $\P a3 =
        \Godel=$}\\
      \ValF(\P{\P a4}1)<\ValF(\P{\P a4}2) &\text{si $\P a2 = 0$ et $\P a3 =
        \Godel<$}\\
      \neg\TrueP(\P a3) &\text{si $\P a2 = 1$}\\
      \TrueP(\P a3)\et\TrueP(\P a4) &\text{si $\P a2 = 2$}\\
      \TrueP(\P a3)\ou\TrueP(\P a4) &\text{si $\P a2 = 3$}\\
      \neg\TrueP(\P a3)\ou\TrueP(\P a4) &\text{si $\P a2 = 4$}\\
      \forallb i{\ValF(\P{\P{\P{\P a4}3}4}2)}\,\TrueP(\Sub(\P{\P a4}4,\P a3,
        \Num(i))) &\text{si $\QBP(a) \et \P a2 = 5$}\\
      \existsb i{\ValF(\P{\P{\P{\P a4}3}4}2)}\,\TrueP(\Sub(\P{\P a4}4,\P a3,
        \Num(i))) &\text{si $\QBP(a) \et \P a2 = 6$}
    \end{cases}
  \end{displaymath}
  La condition $x$ n'est pas variable libre de $t$ dans la définition des
  quantificateurs bornés nous assure d'une part que $t$ est clos, si bien que
  l'on est fondé à appliquer $\ValF$ à son code, et d'autre part que
  $\Sub(\P{\P a4}4,\P a3, \Num(i))$ est bien le code d'une formule
  close.
\end{proof}

\begin{rem}
  La définition de $\TrueP$ n'entre pas exactement dans le cadre des schémas de
  définitions de prédicats p.r. vus dans la section précédente. Le problème est
  que dans les deux derniers cas (correspondant aux quantificateurs bornés), on
  définit $\TrueP(\Godel{\forallb xt\,A})$ en fonction de $\TrueP(\Sub(\Godel
  A,\Godel x, \Num(i))$. Or pour que ceci soit vraiment p.r. il faudrait que
  $\Sub(\Godel A,\Godel x, \Num(i))<\Godel{\forallb xt\,A}$ ce qui est en
  général faux. En fait il faut définit un prédicat $V(a,b)$ à deux paramètres
  en utilisant la variante de la récursion primitive récursive~: le paramètre
  $a$ est le code de la formule sur laquelle on récurre, mais il ne s'agit pas
  d'une formule close~; le paramètre $b$ est (le code d') un ensemble de
  substitutions qui remplace toutes les variables libres de $A$ par des termes
  clos. Par exemple, l'avant-dernière clause ci-dessus devient alors~:
  $V(\Godel{\forallb xt\,A}, b)$ ssi
  \begin{displaymath}
      \forallb i{\ValF{\Godel t}}\,V(\Godel A, b::[\Num(i)/x])
  \end{displaymath}
  où $b::[\Num(i)/x]$ représente (le code de) la substitution $b$ augmentée de
  la substitution $\Num(i)/x$.
\end{rem}

\subsection{Résultats élémentaires sur les fonctions récursives}

Les fonctions de codage vont nous permettre d'établir quelques résultats de
base en théorie des fonctions récursives. L'idée fondamentale est d'associer un
\emph{programme}, c'est à dire un objet formel identifié par un entier, à une
fonction récursive. Le programme d'une fonction récursive $F$ sera ici une
formule $A$ de l'arithmétique définissant la fonction et le calcul de $F(\vec
a)$ revient à rechercher un $b$ tel que $A[\vec{\Term a},b]$.

\begin{theo}[Forme normale de Kleene]
  Pour tout $k$ il existe un prédicat p.r. $T_k$ d'arité $k+2$ tel que si $F$
  est une fonction récursive d'arité $k$ alors il existe un entier $e$ appelé
  \emph{l'indice} de $F$ tel que
  \begin{equation}
    \label{eq:kleeneFN}
    F(\vec a) = \pi_1\Prem x{T_k(e, \vec a, x)}
  \end{equation}
\end{theo}
\begin{rem}
  C'est un théorème de factorisation du schéma de minimisation.
\end{rem}
\begin{proof}
  Soit donc $F$ une fonction récursive d'arité $k$. D'après le
  théorème~\ref{theo:definissabilite} il y a une formule $A[\vec x,y,z]$ de
  l'arithmétique qui est $\Delta$ et telle que~:
  \begin{displaymath}
    b = F(\vec a) \ssi \exists z\,A[\vec{\Term a}, \Term b, z]
  \end{displaymath}
  Mais d'après le théorème~\ref{theo:truep} de la partie précédente, pour tout
  entier $c$, comme $A[\vec{\Term a}, \Term b, \Term c]$ est une formule close,
  on a $A[\vec{\Term a}, \Term b, \Term c]\ssi\TrueP(\Godel{A[\vec{\Term a},
    \Term b, \Term c]})$. Par définition de la fonction $\ParSub$ on obtient
  donc
  \begin{displaymath}
    A[\vec{\Term a}, \Term b, \Term c]\ssi
    \TrueP(\ParSub(\Godel A, \Seq{k+2}{
      \Couple{\Godel{x_1}}{\Num(a_1)},\dots,
      \Couple{\Godel{x_k}}{\Num(a_k)},
      \Couple{\Godel y}{\Num(b)},
      \Couple{\Godel z}{\Num(c)}}))
  \end{displaymath}
  On définit
  \begin{displaymath}
    T_k(e, \vec a, a) \ssi \TrueP(\ParSub(e, \Seq{k+2}{
      \Couple{\Godel{x_1}}{\Num(a_1)},\dots,
      \Couple{\Godel{x_k}}{\Num(a_k)},
      \Couple{\Godel y}{\Num(\pi_1a)},
      \Couple{\Godel z}{\Num(\pi_2a)}}))
  \end{displaymath}
  Le prédicat $T_k$ est clairement p.r. et vérifie $T_k(\Godel A, \vec a, a)$
  ssi $A[\vec{\Term a}, \Term{\pi_1 a}, \Term{\pi_2 a}]$. Supposons qu'il y a
  un $b$ tel que $b=F(\vec a)$. Donc par définition de $A$ il y a un $c$ tel
  que $A[\vec{\Term a},\Term b, \Term c]$.  Si on prend $a=\Couple bc$ on a
  montré l'existence d'un $a$ tel que $T_k(\Godel A, \vec a, a)$.
  Réciproquement, si il existe un tel $a$, alors on a $A[\vec{\Term
    a},\Term{\pi_1 a}, \Term{\pi_2a}]$ et donc par définition de $A$ on a
  $\pi_1 a=F(\vec a)$. Donc le théorème est démontré avec $e=\Godel A$ où $A$
  est une formule qui définit $F$.
\end{proof}

\begin{theo}
  \label{theo:rec-re}
  Un prédicat $P$ est récursif ssi $P$ et $\neg P$ sont tous deux récursivement
  énumérables.
\end{theo}
\begin{proof}
  On a déja vu que si $P$ est récursif alors il est r.e. Si $P$ est récursif
  alors $\neg P$ est aussi récursif et donc $\neg P$ est également r.e.
  Réciproquement supposons que $P$ et $\neg P$ sont tous deux r.e. Soient $F_1$
  et $F_2$ deux fonctions récursives telles que $P(\vec a)$ ssi $\Def{F_1(\vec
    a)}$ et $\neg P(\vec a)$ ssi $\Def{F_2(\vec a)}$ et soient $e_1$ et $e_2$
  des indices pour $F_1$ et $F_2$. On a donc $F_i(\vec a) = \pi_1\Prem
  x{T_k(e_i,\vec a, x)}$ et en particulier $\Def{F_i(\vec a)}$ ssi il existe un
  $a$ tel que $T_k(e_i,\vec a, a)$. Donc
  \begin{displaymath}
    \car P(\vec a) = \pi_1\Prem x{(T_k(e_1, \vec a, \pi_2 x)\et\pi_1 x = 0)\ou
                                  (T_k(e_2, \vec a, \pi_2 x)\et\pi_1 x = 1)}
  \end{displaymath}
  Comme pour tout $\vec a$ on a  $\Def{F_i(\vec a)}$ pour exactement un $i$ on
  déduit que la fonction $\car P$ est totale.
\end{proof}

\begin{theo}
  Soit $P(\vec a)$ un prédicat r.e. d'arité $1$ et non vide (il y a un
  $a\in\Nat$ tel que $P(a)$). Alors il existe une fonction récursive
  \emph{totale} $G$ telle que $P$ est l'image de $G$, c'est à dire~:
  \begin{displaymath}
    P(a)\ssi\exists n,\, a=F(n)
  \end{displaymath}
\end{theo}
\begin{proof}
  Par définition de r.e. il y a une fonction récursive $F$ dont $P$ est le
  domaine c'est à dire~: $P(a)$ ssi $\Def{F(a)}$. Soit $e$ un indice de $F$.
  Par le théorème de Kleene on a donc~:
  \begin{displaymath}
    P(a)\ssi\exists x\,T_1(e, a, x)
  \end{displaymath}
  Soit $G$ la fonction définie par~:
  \begin{displaymath}
    G(c) =
    \begin{cases}
      \pi_1c &\text{si $T_1(e, \pi_1c, \pi_2c)$}\\
      \pi_1\Prem x{T_1(e,\pi_1 x, \pi_2 x)} &\text{sinon}
    \end{cases}
  \end{displaymath}
  La fonction $G$ est alors récursive et comme on a supposé $P$ non vide elle
  est totale. De plus, par construction $P$ est l'image de $G$.
\end{proof}

\paragraph{Accolades de Kleene (Kleene's brackets).}
Soit $e$ un entier. On définit
\begin{displaymath}
  \KApp e{\vec a} = \pi_1\Prem x{T_k(e, \vec a, x)}
\end{displaymath}
\begin{rem}
  La fonction $\Abs{e\vec a}{\KApp e{\vec a}}$ est donc récursive d'arité
  $k+1$. Si $F$ est $k$-récursive et $e$ est un indice pour $F$ alors 
  \begin{displaymath}
    F(\vec a) = \KApp e{\vec a}
  \end{displaymath}
\end{rem}
\begin{theo}[Théorème $S_m^n$]
  Pout tous entiers $m$ et $n$, il existe une fonction p.r. $S_m^n$ d'arité
  $m+1$ telle que
  \begin{displaymath}
    \KApp e{a_1,\dots,a_{m+n}} = \KApp{S_m^n(e, a_{n+1},\dots,
      a_{m+n})}{a_1,\dots,a_n}
    \end{displaymath}
\end{theo}
\begin{proof}
  On ne traite que le cas $m=1$, le reste s'en déduit par récurrence sur $m$.
  On définit $S^n$ par~:
  \begin{displaymath}
    S^n(e,a) = \Sub(e, \Godel{x_{n+1}}, \Num(a))
  \end{displaymath}
  On voit immédiatement par définition des accolades de Kleene et du prédicat
  $T_n$ que l'on a le résultat attendu~: $\KApp e{a_1,\dots, a_{n+1}} =
    \KApp{S^n(e, a_{n+1})}{a_1,\dots, a_n}$.
\end{proof}

Nous terminerons cette partie avec une conséquence importante du théorème
$S_m^n$.
\begin{theo}[Théorème de récursivité de Kleene]
  Soit $F$ une fonction récursive d'arité $k+1$. Il existe un entier $e$ tel
  que
  \begin{displaymath}
    \KApp e{\vec a} = F(\vec a,e)
  \end{displaymath}
\end{theo}
C'est ce théorème qui permet de montrer que toute fonction définie par un
système d'équations récursives (au sens informatique) est récursive. Un exemple
notable est la fonction d'Ackermann définie par~:
\begin{align*}
  A(0, p) &= p+1\\
  A(n+1, 0) &= A(n, 1)\\
  A(n+1, p+1) &= A(n, A(n+1, p))
\end{align*}
Pour montrer qu'elle est récursive on considère la fonction $H$ définie par
\begin{displaymath}
  H(n, p, a) = 
  \begin{cases}
    p+1 &\text{si $n = 0$}\\
    \KApp a{n\Moins 1,1} &\text{si $n>0$ et $p=0$}\\
    \KApp a{n\Moins 1, \KApp a{n, p\Moins 1}} &\text{sinon}
  \end{cases}
\end{displaymath}
Alors $H$ est récursive et en applicant le théorème de récursivité de Kleene,
on déduit l'existence d'un $a$ tel que $\KApp a{n,p} = H(n,p,a)$. Un tel $a$
est un indice pour la fonction $A$.

\begin{proof}
  Soit $G$ la fonction récursive définie par $G(\vec a, a) = F(\vec a, S^k(a,
  a))$ et soit $f$ un indice pour $G$. Alors on a $\KApp f{\vec a,a} = F(\vec
  a, S^k(a, a))$~; mais par le théorème $S_m^n$ on en déduit que
  $\KApp{S^k(f,a)}{\vec a} = F(\vec a, S^k(a, a))$. Si on prend $a=f$ on
  obtient le résultat souhaité avec $e=S^k(f,f)$.
\end{proof}


\section{Le prédicat de prouvabilité}

\paragraph{Codage des séquents}
On rappelle qu'un séquent n'est rien d'autre qu'un couple de deux suites finies
de formules~; soit $S=A_1,\dots,A_m\vdash B_1,\dots,B_n$ un séquent. Le code de
$S$ est~:
\begin{displaymath}
  \Godel S = \Seq4{3, 0, \Seq m{\Godel{A_1},\dots,\Godel{A_m}},
                         \Seq n{\Godel{B_1},\dots, \Godel{B_n}}}
\end{displaymath}


\paragraph{Théorie.}
Une théorie $T$ est un ensemble de formules closes appelées les \emph{axiomes
  de $T$}, dans un langages $L$ donné. Une formule $A$ \emph{prouvable dans la
  théorie $T$} si il existe un sous-ensemble fini $T_0$ de $T$ tel que le
séquent $T_0\vdash A$ est prouvable. On dit alors que $A$ est \emph{un théorème
  de $T$} ce que l'on note $T\vdash A$.

Une théorie est \emph{cohérente} si le séquent vide n'y est pas démontrable,
c'est à dire si pour tout sous-ensemble fini $T_0$ de $T$ le séquent
$T_0\vdash$ n'est pas prouvable. Une théorie est \emph{primitive récursive} si
le prédicat
\begin{displaymath}
  \Ax_T(a) \ssi\text{$a$ est le code d'un axiome de $T$}
\end{displaymath}
est primitif récursif. 

On dit qu'une théorie $T'$ \emph{étend} une théorie $T$ si le langage $L'$ de
$T'$ contient le langage $L$ de $T$ et si $T'$ contient $T$. On dit de plus que
$T'$ est une \emph{extension primitive récursive} de $T$ si $T$ et $T'$ sont
primitive récursives

\paragraph{Codage des preuves.}
On se donne maintenant une numérotation des règles du calcul des séquents~: 0
pour la règle axiome, 1 pour la règle de coupure, 2 et 3 pour les règles
d'échanges gauche et droite, 4 et 5 pour les règles d'affaiblissement gauche et
droite, \dots\ On définit le code d'une démonstration $\pi$ du calcul des
séquents dans la théorie p.r. $T$ par~:
\begin{displaymath}
  \Godel\pi =
  \begin{cases}
    \Seq4{4, 0, \Godel A,0} &\text{si $\pi$ est la démonstration réduite au
      seul séquent $A\vdash A$}\\
    \Seq4{4, i, \Godel{\pi_0},0} &\text{si $\pi$ est obtenue en appliquant la
      règle unaire de numéro $i$ à la preuve $\pi_0$}\\
    \Seq4{4, i, \Godel{\pi_1}, \Godel{\pi_2}} &\text{si $\pi$ est obtenue en
      appliquant la règle binaire de numéro $i$ à $\pi_1$ et $\pi_2$}
  \end{cases}
\end{displaymath}

\begin{theo}
  Soit $T$ une théorie p.r. Il existe un prédicat p.r. $\Proof_T$ tel que~:
  \begin{displaymath}
    \Proof_T(a, p) \ssi\text{$p=\Godel\pi$ et $a=\Godel A$ où $\pi$ est une
    démonstration de $T_0\vdash A$ pour un sous-ensemble fini $T_0$ de $T$}
  \end{displaymath}
\end{theo}

Essentiellement le théorème établit que l'on peut vérifier de manière
calculatoire (et même par une fonction primitive récursive ce qui est à peine
plus fort) la correction d'une preuve.  Il serait trop fastidieux de le
démontrer ici. Il s'agit encore une fois de programmer tout un ensemble de
fonctions et prédicats p.r.

\paragraph{Le prédicat de prouvabilité.}
On note $\Thm_T$ le prédicat de prouvabilité de la théorie $T$, c'est à dire
que $\Thm_T$ est défini par~:
\begin{displaymath}
  \Thm_T(a) \ssi\text{$a$ est le code d'un théorème de $T$}
\end{displaymath}
Comme on a $\Thm_T(a)\ssi \exists b\,\Proof_T(a, b)$ on voit que $\Thm_T$ est
r.e. (dès que $T$ est p.r.).

\paragraph{Théories complètes, décidables.}
Une théorie $T$ est \emph{complète} si pour toute formule $A$ close on a soit
$T\vdash A$, soit $T\vdash\neg A$. Une théorie $T$ est \emph{décidable} si
$\Thm_T$ est un prédicat récursif.

\begin{theo}
  \label{theo:complt-dcid}
  Si $T$ est une théorie p.r. cohérente et complète alors $T$ est décidable.
\end{theo}
\begin{proof}
  Remarquons que pour toute formule $A$ on a $T\vdash A$ ssi $T\vdash \Clot A$.
  Par conséquent si $T$ est cohérente et complète alors $T\not\vdash A$ ssi
  $T\vdash \neg\Clot A$. Donc on a $\neg\Thm_T(a)$ ssi soit $a$ n'est pas le
  code d'une formule, soit $\Thm_T(\Neg(\ClotF(a)))$. Comme la fonction $\Abs
  x{\Neg(\ClotF(x))}$ est p.r. et comme $\Thm_T$ est r.e. on voit que
  $\neg\Thm_T$ est r.e. d'où l'on déduit par le théorème~\ref{theo:rec-re} que
  $\Thm_T$ est récursif.
\end{proof}

\subsection{L'arithmétique élémentaire}
L'arithmétique élémentaire (\EA) est l'ensemble fini (des clôtures
universelles) des axiomes suivants (dans le langage de l'arithmétique~:
\begin{enumerate}
\item Axiomes d'égalité~:
  \begin{enumerate}
  \item $x = x$~;;
  \item $x = x' \et y = y' \et x = y \Implies x' = y'$~;
  \item $x = x'\Implies S(x) = S(x')$~;
  \item $x = x' \et y = y' \Implies x+x' = y+y'$~:
  \item $x = x' \et y = y' \Implies x\cdot x' = y\cdot y'$~;
  \item $x = x' \et y = y' \et x < y \Implies x' < y'$~;
  \end{enumerate}
\item Axiomes de définitions~:
  \begin{enumerate}
  \item $\neg S(x) = 0$~;
  \item $S(x) = S(y) \Implies x = y$~;
  \item $x + 0 = x$~;
  \item $x + S(y) = S(x + y)$~;
  \item $x \cdot 0 = 0$~;
  \item $x \cdot S(y) = x \cdot y + x$~;
  \item $\neg x < 0$~;
  \item $x < S(y) \Equiv x < y \ou x = y$~;
  \item $x < y \ou x = y \ou y < x$~;
  \end{enumerate}
\end{enumerate}

\begin{lemme}
  L'arithmétique élémentaire est une théorie primitive récursive.
\end{lemme}

On note $\Proof_0$ le prédicat $\Proof_{\EA}$ et $\Thm_0$ le prédicat
$\Thm_{\EA}$.

\begin{theo}
  \label{theo:sigma}
  Si $A$ est une formule de l'arithmétique qui est $\Delta$ et close alors~:
  \begin{align*}
    A &\fleche \EA\vdash A\\
    \neg A &\fleche \EA\vdash\neg A
  \end{align*}
  Si $A$ est $\Sigma$ et close alors~:
  \begin{displaymath}
    A\fleche \EA\vdash A
  \end{displaymath}
\end{theo}

\begin{proof}
  Le cas d'une formule $\Delta$ se déduit du lemme suivant~:
  \begin{lemme}
    Pour tous entiers $n$ et $m$ et tout terme $t$ du langage de l'arithmétique
    on a
    \begin{align*}
      &\EA\vdash \Term n\Plus\Term m =\Term{m+n}\\
      &\EA\vdash \Term n\Mult\Term m =\Term{mn}\\
      \Val t = n\fleche{}&\EA\vdash t = \Term n\\
      n = m \fleche{}&\EA\vdash\Term n = \Term m\\
      n\neq m\fleche{}&\EA\vdash\neg(\Term n = \Term m)\\
      n < m \fleche{}&\EA\vdash\Term n<\Term m\\
      n \not< m \fleche{}&\EA\vdash\neg(\Term n<\Term m)\\
      &\EA\vdash x<\Term n \Equiv x=\Zero\ou\dots\ou x=\Term{n-1}
    \end{align*}
  \end{lemme}
  
  Chaque clause du lemme se démontre par récurrence sur $n$ et/ou $m$ et/ou
  $t$.  Pour fixer les idées on va montrer la dernière clause~: $\EA\vdash
  x<\Term n\Equiv x=\Zero\ou\dots\ou x=\Term{n-1}$. Si $n=0$ cette équivalence
  est conséquence de l'axiome $x<0\vdash$ de \EA~: en effet la disjonction est
  alors vide donc fausse donc équivalente à $x<0$ puisque cette formule est
  supposée fausse dans $\EA$. Supposons le résultat démontré pour $n$. On a
  $\EA\vdash x<\Term{n+1}\Equiv x<\Term n\ou x=\Term n$ comme conséquence des
  axiomes de \EA\ et du fait que $\EA\vdash \Succ\Term n=\Term{n+1}$. Or par
  récurrence sur $n$ on a $\EA\vdash x<\Term n\Equiv x=\Zero\ou\dots\ou
  x=\Term{n-1}$~; on en déduit immédiatement le résultat, \ie, $\EA\vdash
  x<\Term{n+1}\Equiv x=\Zero\ou\dots\ou x=\Term n$.
  
  \aere
  Le théorème se déduit du lemme par induction sur la formule $A$. Le cas d'une
  formule atomique est traitée presqu'entièrement par le lemme. Le seul cas
  compliqué est est en fait celui des formules à quantificateur borné.
  Supposons donc  que $A=\forallb xt\,B$. Comme $A$ est close, $t$ est clos et
  $B=B[x]$ a $x$ pour seule variable libre.
  
  Si $A$ est vraie alors pour tout $a$ inférieur à $\Val t$, $B[\Term a]$ est
  vraie. Par hypothèse d'induction on en déduit que $\EA\vdash B[\Term a]$ pour
  tout $a<\Val t$. Donc $\EA\vdash x = \Term a\fleche B$ pour tout $a<\Val t$.
  Notons $n=\Val t$. On a $\EA\vdash x<\Term n\Equiv x=\Zero\ou\dots\ou
  x=\Term{n-1}$.  Donc $\EA\vdash x<\Term n\fleche B$. Comme $\EA\vdash t=\Term
  n$ (puisque $n=\Val t$) on obtient finalement le résultat souhaité~:
  $\EA\vdash x<t\fleche B$.
  
  Si $A$ est fausse alors il y a un $a<\Val t$ tel que $B[\Term a]$ est fausse.
  Par hypothèse d'induction on a $\EA\vdash \neg B[\Term a]$, mais comme
  $a<\Val t$ on a également $\EA\vdash \Term a<t$ d'où l'on déduit finalement
  $\EA\vdash\existsb xt\,\neg B$. Mais cette dernière formule est logiquement
  équivalente à $\neg A$.

  Le cas d'un $\exists$ borné se déduit de la remarque que $\EA\vdash
  \neg\forallb xt\,B\Equiv \existsb xt\,\neg B$ (cette équivalence est
  d'ailleurs prouvable dans le calcul des séquents sans axiome) et du cas d'un
  $\forall$ borné.

  \aere
  Si maintenant $A$ est une formule $\Sigma$ close et que $A$ est vraie on
  démontre que $\EA\vdash A$ par induction sur $A$. Le seul cas intéressant de
  l'induction est $A=\exists x\,B$ où $B=B[x]$ a comme seule variable libre
  $x$. Comme $A$ est vraie il existe un $a$ tel que $B[\Term a]$ est vraie,
  donc par induction $\EA\vdash B[\Term n]$ d'où l'on déduit immédiatement que
  $\EA\vdash A$.
\end{proof}

\paragraph{Fonctions et prédicats représentables dans \EA.}
Soit $F$ une fonction d'arité $k$. On dit que $F$ est \emph{représentable} si
il existe une formule $A[\vec x, y]$ de l'arithmétique et telle que~:
\begin{displaymath}
  b = F(\vec a) \fleche \EA\vdash A[\vec{\Term a}, y] \Equiv y = \Term b
\end{displaymath}

Soit $P$ un prédicat d'arité $k$. On dit que $P$ est \emph{représentable} si il
existe une formule $A[\vec x]$ telle que~:
\begin{align*}
  P(\vec a) &\ssi \EA\vdash A[\vec{\Term a}]\\
  \neg P(\vec a)&\ssi\EA\vdash \neg A[\vec{\Term a}]
\end{align*}

\begin{theo}[Représentabilité]
  \label{theo:repr}
  Si $F$ est est une fonction récursive alors $F$ est représentable. Si $P$ est
  un prédicat récursif alors $P$ est représentable.
\end{theo}
\begin{proof}
  Le cas d'un prédicat récursif est conséquence de celui d'une fonction. Si $P$
  est récursif alors $\car P$ est récursive totale, donc il y a une formule
  $A[\vec x, y]$ qui représente $\car P$. Mais alors la formule $B[\vec x] =
  A[\vec x, \Zero]$ représente $P$.  Supposons que $P(\vec a)$, c'est à dire
  que $\car P(\vec a) = 0$.  Alors on a $\EA\vdash A[\vec{\Term a},y]\Equiv
  y=\Zero$ d'où l'on déduit aisément en appliquant les axiomes d'égalité que
  $\EA\vdash B[\vec{\Term a}]$. Si au contraire on a $\neg P(\vec a)$ c'est à
  dire $\car P(\vec a) = 1$ alors $\EA\vdash A[\vec{\Term a}, y]\Equiv
  y=\Succ\Zero$. En particulier $\EA\vdash A[\vec{\Term a}, \Zero] \Equiv
  \Zero=\Succ\Zero$. Comme $\EA\vdash\neg(\Zero=\Succ\Zero)$ on voit que
  $\EA\vdash\neg B[\vec{\Term a}]$.
  
  \aere On montre maintenant le cas d'une fonction récursive. C'est une
  conséquence de~:
  \begin{lemme}
    Si $F$ est récursive alors il existe une formule $A[\vec x, y]$ qui est
    $\Sigma$, qui définit $F$ et telle que
    \begin{displaymath}
      \EA\vdash A[\vec x, y]\et A[\vec x, y'] \fleche y = y'
    \end{displaymath}
  \end{lemme}
  Commençons par finir le théorème. Supposons $b=F(\vec a)$. Comme la formule
  $A$ du lemme définit $F$ on a $A[\vec{\Term a},\Term b]$~; comme elle est
  $\Sigma$, par le théorème~\ref{theo:sigma} on déduit que $\EA\vdash
  A[\vec{\Term a},\Term b]$. En utilisant les axiomes d'égalité on voit
  immédiatement qu'alors $\EA\vdash y=\Term b\fleche A[\vec{\Term a},y]$. Par
  ailleurs, d'après le lemme on a que $\EA\vdash A[\vec{\Term a}, y]\et
  A[\vec{\Term a}, \Term b] \fleche y = \Term b$. Mais comme $\EA\vdash
  A[\vec{\Term a},\Term b]$, on voit que $ \EA\vdash A[\vec{\Term a},
  y]\fleche y=\Term b$.
  
  \aere
  Démontrons maintenant le lemme. Soit $A$ une formule $\Sigma$ qui définit
  $F$. On va construire une formule $D[\vec x, y]$ qui est $\Sigma$,
  équivalente à $A$ (donc qui définit $F$) et telle que $\EA\vdash D[\vec
  x,y]\et D[\vec x, y']\fleche y = y'$. Comme $A$ est $\Sigma$ on sait qu'il
  existe une formule $A_0[\vec x, y, z]$ qui est $\Delta$ et telle que
  \begin{displaymath}
    A \Equiv\exists z\,A_0
  \end{displaymath}
  On note $x\leq y$ pour $x<\Succ y$. On définit $B_0[\vec x, y, z] = \exists w
  \leq z\,(y\leq z\et z = y\Plus w\et A_0[\vec x, y, w])$. Clairement $B_0$ est
  $\Delta$ et $\exists z\,B_0$ est équivalente à $A$. Mais en plus on a
  \begin{displaymath}
    \EA\vdash B_0[\vec x,y,z]\fleche y\leq z
  \end{displaymath}
  Soit maintenant $C_0=B_0\et \forall z'<z\,\forall y'\leq z'\,\neg B_0[\vec x,
  y', z']$. Alors $C_0$ est $\Delta$ et on a encore $\exists z\,C_0$
  équivalente à $A$. Mais en plus on a
  \begin{displaymath}
    \EA\vdash C_0[\vec x, y, z]\et C_0[\vec x, y', z']\fleche z = z'
  \end{displaymath}
  On raisonne dans $\EA$~: soient $z$, $z'$ et $y$, $y'$ tels que $C_0[\vec x,
  y, z]$ et $C_0[\vec x, y', z']$. Supposons que $z<z'$. Comme $C_0[\vec x, y',
  z']$ on a $\forall u<z'\,\forall v\leq u\,\neg B_0[\vec x, v, u]$ donc en
  particulier pour $u=z$, $\forall v\leq z\,\neg B_0[\vec x, v, z]$. Mais
  comme $C_0[\vec x, y, z]$ on a $B_0[\vec x, y, z]$ et donc $y\leq z$. En
  prenant $v=y$ on obtient une contradiction. Donc $\neg(z<z')$. Similairement
  $\neg(z'<z)$ et les axiomes de \EA\ entrainent alors que $z=z'$.
  
  Soit finalement $D_0=C_0\et\forall y'<y\,\neg C_0[\vec x, y', z]$. Alors
  $D=\exists z\,D_0$ a les propriétés requises par le lemme. En effet $D_0$ est
  $\Delta$ et clairement $D$ est équivalente à $A$ donc définit $F$. Supposons
  que $y$ et $y'$ sont tels que $D[\vec x,y]$ et $D[\vec x, y']$. On raisonne
  dans \EA. Comme $D[\vec x, y]$ il y a un $z$ tel que $D_0[\vec x, y, z]$
  donc en particulier tel que $C_0[\vec x, y, z]$. De même, comme $D[\vec x,
  y']$, il y a un $z'$ tel que $C_0[\vec x, y', z']$. Mais alors $z=z'$ et donc
  $D_0[\vec x, y, z]\et D_0[\vec x, y', z]$. Mais comme précédemment on voit
  que l'on ne peut alors avoir $y<y'$, ni $y'<y$ d'où $y=y'$ comme annoncé.
\end{proof}


\section{Théorèmes d'indécidabilité et d'incomplètude}
\label{sec-theo}

\begin{theo}[Church]
  Soit $T$ une extension p.r. de \EA. Si $T$ est cohérente alors $T$ est
  indécidable.
\end{theo}

\begin{proof}
  On définit un prédicat $Q$ par~:
  \begin{displaymath}
    Q(a)\ssi\neg\Thm_T(\Sub(a, \Godel x, \Num(a))
  \end{displaymath}
  Supposons que $Q$ est récursif. Par le théorème de représentation il y a une
  formule $A[x]$ qui représente $Q$.  Posons $a=\Godel A$.
  
  Si $Q(a)$ est vrai, alors $\EA\vdash A[\Term a]$, donc comme $T$ est une
  extension de $\EA$, $T\vdash A[\Term a]$. Mais alors $\Thm_T(\Godel{A[\Term
    a]})$ est vrai, \ie, $\Thm_T(\Sub(\Godel A,\Godel x, \Num(a)))$,
  \ie, $\neg Q(a)$ puisque $a=\Godel A$.
  
  Donc $Q(a)$ est faux, c'est à dire que $\Thm_T(\Sub(a, \Godel x, \Num(a)))$
  est vrai donc, comme $a=\Godel A$, que $T\vdash A[\Term a]$. Mais si
  $Q(a)$ est faux, comme $A$ représente $Q$ on a $EA\vdash \neg A[\Term a]$,
  donc $T\vdash\neg A[\Term a]$ ce qui contredit la cohérence de $T$.
  
  Par conséquent $Q$ ne peut être récursif. Comme $\Sub$ et $\Num$ sont toutes
  les deux p.r., c'est que $\Thm_T$ n'est pas récursif.
\end{proof}

\begin{coro}
  Le calcul des prédicats est indécidable.
\end{coro}
\begin{proof}
  On note $\mathcal{N}$ la suite (finie) des formules de l'arithmétique
  suivantes~:
  \begin{description}
  \item[Égalité] $x = x$, $x=y\fleche\Succ x=\Succ y$, $x=x'\et y=y'\fleche
    x\Plus y = x'\Plus y'$, $x=x'\et y=y'\fleche
    x\Mult y = x'\Mult y'$, $x=x'\et y=y'\fleche x=y\fleche x'=y'$, $x=x'\et
    y=y'\fleche x<y\fleche x'<y'$~;
  \item[Arithmétique élémentaire] $x\Plus\Zero =x$, $x\Plus\Succ y=\Succ(x\Plus
    y)$, $x\Mult \Zero=\Zero$, $x\Mult\Succ y=x\Mult y\Plus x$, $\neg (x<0)$,
    $x<\Succ y\Equiv x<y\ou x=y$, $\neg(\Succ x=0)$, $\Succ x=\Succ y\fleche
    x=y$, $x<y\ou x=u\ou y<x$.
  \end{description}

  On a alors
  \begin{lemme}
    Soit $A$ une formule de l'arithmétique. Alors
    \begin{displaymath}
      \EA\vdash A \ssi \text{le séquent $\mathcal{N}\vdash A$ est prouvable
      dans le calcul des séquents}
    \end{displaymath}
  \end{lemme}
  La preuve de ce lemme est un (comme d'autres) trop fastidieuse pour être
  explicitée ici. On la laisse au lecteur.
  
  Soit $\Thm_{\LK}$ le prédicat de prouvabilité du calcul des séquents défini
  par $\Thm_{\LK}(a)$ ssi $a$ est le code d'un séquent $S$ et $S$ est prouvable
  dans $\LK$.  D'après le lemme pour toute formule $A$, $\Thm_{\EA}(\Godel A)$
  est équivalent à $\Thm_{\LK}(\Godel{\mathcal{N}\vdash A})$, donc d'après le
  théorème de Church, $\Thm_{\LK}$ n'est pas récursif.
\end{proof}

\begin{coro}[Incomplétude]
  Soit $T$ une extension p.r. de \EA. Si $T$ est cohérente alors $T$ est
  incomplète.
\end{coro}
\begin{proof}
  On a vu qu'une théorie cohérente et complète est décidable.
\end{proof}


\section{Le second théorème de Gödel}
\begin{theo}
  \label{theo:weak-godel}
  Soit $T$ une extension primitive récursive cohérente de $\EA$. Il existe une
  formule $\Pi$ close $G_T$ telle que~: $G_T$ est vraie mais $G_T$ n'est pas
  prouvable dans $T$.
\end{theo}

\begin{proof}
  On va commencer par énoncer le lemme suivant
  \begin{lemme}
    Soit $Q$ un prédicat unaire. Si $Q$ est r.e. (resp. si $\neg Q$ est
    r.e.\footnote{On dit que $Q$ est co-r.e.}) alors il existe une formule
    close $A$ de l'arithmétique qui est $\Sigma$ (resp. $\Pi$) telle que~:
    \begin{displaymath}
      Q(\Godel A)\ssi A
    \end{displaymath}
  \end{lemme}

  Supposons le lemme démontré et prenons $Q(a)$ ssi $\neg\Thm_T(a)$. Alors $Q$
  est co-r.e. donc, d'après le lemme, il existe une formule close $G_T$ qui est
  $\Pi$ et telle que ~:
  \begin{displaymath}
    G_T \ssi \neg\Thm_T(\Godel{G_T})
  \end{displaymath}
  Si $G_T$ est fausse on a donc $\Thm_T(\Godel G_T)$, donc $T\vdash G_T$. Mais
  si $G_T$ est fausse, $\neg G_T$ est vraie et comme elle est (équivalente à
  une formule) $\Sigma$, on a $\EA\vdash \neg G_T$ par le
  théorème~\ref{theo:sigma}. Comme $T$ est une extension de $\EA$ on a
  également $T\vdash\neg G_T$, ce qui contredit la cohérence de $T$. Par
  conséquent $G_T$ est vraie et donc n'est pas prouvable dans $T$.
  
  \aere Démontrons maintenant le lemme. Supposons que $Q$ est r.e. (resp.
  co-r.e.) et soit $P$ le prédicat binaire défini par $P(a, b)$ ssi $Q(\Sub(a,
  \Godel x, \Num(b)))$ (resp. ssi $\neg Q(\Sub(a, \Godel x, \Num(b)))$. Comme
  $\Sub$ et $\Num$ sont p.r. $P$ est r.e.  Donc il existe une formule de
  l'arithmétique $B[x,y]$ qui est $\Sigma$ et telle que
  \begin{displaymath}
    P(a,b) \ssi B[\Term a,\Term b]
  \end{displaymath}
  Posons $A[x] = B[x, x]$ (resp. $A[x] = \neg B[x,x]$) et soit $a=\Godel A$.
  Remarquons que $A$ est $\Sigma$ (resp. $\Pi$) et que $A[\Term a]$ est close.
  On a~: $A[\Term a]$ est équivalente à $P(a, a)$ (resp. à $\neg P(a,a)$),
  c'est à dire à $Q(\Sub(a, \Godel x, \Num(a)))$. Mais par définition de $\Sub$
  on a $\Sub(a, \Godel x, \Num(a)) = \Godel{A[\Term a]}$, donc finalement
  $A[\Term a]$ est équivalente à $Q(\Godel{A[\Term a]})$.
\end{proof}

\begin{rem}
  Quand bien même $G_T$ est vraie, il se pourrait que $\neg G_T$ soit prouvable
  dans $T$. Il n'a jamais été dit, et c'est d'ailleurs faux, qu'une extension
  quelconque de $\EA$ ne démontre que des formules vraies. Typiquement si $A$
  est une formule qui exprime la cohérence de $\PA$ alors $\PA + \neg A$ est
  cohérente (en vertu du second théorème de Gödel ci-dessous) et démontre $\neg
  A$ qui est visiblement fausse (nul ne doute que $\PA$ est cohérente~!). On
  n'a donc pas démontré ici l'incomplètude de $T$ mais un résultat un peu plus
  faible. C'est assez normal si on considère que l'on n'a utilisé ici que la
  définissabilité du prédicat $\Thm_T$ alors que pour démontrer l'incomplètude
  on s'est servi de la représentabilité de $\Thm_T$.
\end{rem}


\paragraph{Arithmétique de Peano.}
L'arithmétique de Peano $\PA$ est la théorie constituée des séquents de $\EA$
auxquels on ajoute le \emph{principe de récurrence}, \ie, tous les séquents de
la forme
\begin{displaymath}
  A[\Zero], \forall x\,(A[x]\fleche A[\Succ x])\vdash A[x]
\end{displaymath}
où $A[x]$ est une formule quelconque.

\begin{lemme}
  $\PA$ est une théorie p.r.
\end{lemme}

Remarquons que toutes les preuves que nous avons faites jusqu'à maintenant
(ainsi d'ailleurs que celles que nous n'avons pas faites) n'utilise comme
principe le plus évolué que le principe de récurrence. C'est en particulier le
cas du théorème ci-dessus ainsi que des deux faits que l'on a utilisés pour le
montrer~:
\begin{enumerate}
\item le fait que $\Thm_T$ est définissable par une formule $\Sigma$~;
\item le théorème~\ref{theo:sigma} (une formule $\Sigma$ vraie est prouvable
  dans $\EA$).
\end{enumerate}

Autrement dit on a le lemme suivant
\begin{lemme}
  Le théorème~\ref{theo:weak-godel} est entièrement formalisable dans $\PA$,
  c'est à dire que, si $T$ est une extension p.r. de $\EA$ alors~:
  \begin{displaymath}
    \PA\vdash \Coh(T)\fleche G_T\et\neg\Thm_T(\Godel{G_T})
  \end{displaymath}
\end{lemme}
Encore une démonstration fastidieuse que l'on ommet ici. 

\begin{theo}[Gödel]
  Soit $T$ une extension cohérente p.r. de $\PA$. Alors $T$ ne démontre pas sa
  propre cohérence.
\end{theo}
\begin{proof}
  Comme $T$ étend $\PA$ on a $\PA\vdash \Coh(T)\fleche
  G_T\et\neg\Thm_T(\Godel{G_T})$ donc en particulier $T\vdash \Coh(T)\fleche
  G_T$. Donc si $T\vdash \Coh(T)$ alors $T\vdash G_T$ et d'après le
  théorème\ref{theo:weak-godel}, $T$ n'est pas cohérente.
\end{proof}


\chapter{Lambda-calcul}

\lettrine{O}{n va procéder} ici à une rapide introduction au lambda-calcul.
Pour plus ample information, le lecteur est invité à se reporter au livre de
Krivine~\cite{Krivine90b} duquel sont empruntés les concepts et résultats
exposés ici.

\section{Le lambda-calcul pur}

\lettrine{L}{e lambda-calcul} peut être décrit comme une théorie générale des fonctions. Il
fournit des notations pour les deux opérations sur les fonctions~:

\begin{itemize}
\item application d'une fonction à un argument
\item définition d'une fonction à partir d'un terme, comme lorsqu'on
  parle de la fonction qui à $x$ associe $x+3$. Observer que cela
  nécessite aussi la présence de \emph{variables} (comme <<~$x$~>> dans
  l'exemple précédent).
\end{itemize}

Ce qui peut sembler étrange au premier abord, c'est que la syntaxe du
lambda-calcul ne possède que ces deux opérations~: il n'y a pas d'objets <<~de
base~>> (comme les entiers) sur lesquels calculer, ni d'opérations prédéfinies
(addition, etc.). Il se trouve que ces objets peuvent être définis dans le
lambda-calcul, comme on aura l'occasion de le voir.

On se donne un ensemble infini dénombrable $V$ de \emph{variables}. L'ensemble
des lambda-termes $\Lambda$ (ou $\Lambda(V)$ lorsqu'il est nécessaire de
préciser les variables) est donné par~:

\begin{itemize}
\item Si $x\in V$, alors $x\in\Lambda$.
\item Si $t,u\in\Lambda$, alors $\App tu\in\Lambda$ (application de la
  <<~fonction~>> $t$ à l'<<~argument~>> $u$).
\item Si $t\in\Lambda$ et $x\in V$, alors $\Lam xt\in\Lambda$. Ce terme
  représente la fonction qui à $x$ associe $t$ (dans lequel $x$
  figure en général).
\end{itemize}

Il faut voir un (lambda-)terme comme un arbre possédant trois types de noeuds~:
\begin{itemize}
\item Des feuilles, qui sont étiquetées par des variables.
\item Des noeuds \emph{application}, qui ont deux descendants (la fonction
  et l'argument).
\item Des noeuds lambda ou \emph{abstraction}, qui sont étiquetés par une
  variable et ont un descendant (le corps de la fonction).
\end{itemize}

Voici deux conventions typographiques très utiles et très répandues
dans la littérature sur le sujet~:
\begin{itemize}
\item Au lieu d'écrire $\App{\dots\App{t}{t_1}\dots}{t_n}$, on écrit
  $\App t{t_1\dots t_n}$.
\item Au lieu d'écrire $\Lam{x_1}{\dots\Lam{x_n}t}$, on écrit
  $\Lam{x_1\dots x_n}t$.
\end{itemize}


\paragraph{Sous-termes.}
Un \emph{sous-terme} d'un terme $t$ est un terme apparaissant sous un noeud de
$t$.  Un même sous-terme de $t$ peut apparaître à plusieurs endroits différents
de $t$~: il a alors plusieurs \emph{occurrences} dans $t$. Par exemple, le
terme $\Lam x{\App yx}$ a deux occurrences différentes dans le terme suivant~:
\begin{displaymath}
  \App{\Lam x{\App yx}}{\Lam z{\App z{\Lam x{\App yx}}}}  
\end{displaymath}


\paragraph{{Variables libres, liées.}}
Une variable apparaissant dans un terme est \emph{liée} s'il y a au-dessus
d'elle, dans l'arbre, un noeud lambda étiqueté par la même variable. Une
variable qui n'est pas liée est \emph{libre}. Par exemple, dans
\begin{displaymath}
  t_1=\Lam x{\App yx} ,
\end{displaymath}
la variable $x$ est liée, et la variable $y$ est libre.

Plus précisément, on peut définir par récurrence sur la taille
des lambda-termes l'ensemble $\VL t$ des variables libres d'un
terme $t$~:
\begin{displaymath}
  \VL t=
  \begin{cases}
    \{x\} &\text{si $t=x$}\\
    \VL u\cup \VL v &\text{si $t=\App uv$}\\
    \VL u\setminus\{x\} &\text{si $t = \Lam xu$}
  \end{cases}
\end{displaymath}

Il est clair que le nom d'une variable liée n'a aucune importance~:
le terme $t_1$ précédent doit être identifié au terme
\begin{displaymath}
  \Lam z{\App yz}
\end{displaymath}
Toutefois, lorsqu'on renomme en $y$ la variable liée $x$, dans une occurrence
d'un sous-terme $\Lam xu$ d'un terme $t$, il faut prendre garde à ce que la
nouvelle variable $y$ que l'on veut utiliser ne soit pas déjà libre dans $u$~:
dans le terme $t_1$, on ne peut pas renommer $x$ en $y$. On obtiendrait le
terme $\Lam y{\App yy}$, qui n'a pas la même signification que $t$.


\paragraph{Alpha-équivalence.}
Deux termes sont dits \emph{$\alpha$-équivalents} (ou simplement
\emph{équivalents}) si on peut obtenir le second à partir du premier en
renommant des variables liées (en respectant bien sûr les précautions ci-dessus
concernant la capture des variables libres). Il s'agit d'une relation
d'équivalence. 

\begin{quote}
  A partir de maintenant, on considérera les lambda-termes à
  $\alpha$-équivalence près, c'est à dire que l'on écrira $t=u$ pour <<~$t$ est
  $\alpha$-équivalent à $u$~>>, ou  <<~$t$ et $u$ ne diffèrent que par les noms
  de leur variables liées~>>.
\end{quote}

\paragraph{Substitution.}
Une opération très importante sur les lambda-termes est la \emph{substitution}
d'une suite de termes $u_1,\dots,u_n$ à la suite de variables libres
$x_1,\dots,x_n $ d'un terme $t$, ce qu'on note $\Subst
t{u_1/x_1,\dots,u_n/x_n}$ (ou lorsque ce n'est pas ambigu $\Subst t{\vec
  u/\vec x}$), et qu'on définit par récurrence sur la taille de
$t$~:
\begin{displaymath}
  \Subst t{\vec u/\vec x}=
  \begin{cases}
    t & \text{si $x_i\not\in\VL t$ pour $i=1,\dots,n$}\\
    u_i & \text{si $t=x_i$}\\
    \App{\Subst{t_1}{\vec u/\vec x}}{\Subst{t_2}{\vec u/\vec x}} &
      \text{si $t=\App{t_1}{t_2}$}\\
    \Lam z{\Subst s{z/y,\vec u/\vec x\setminus y}} & 
      \text{si $t=\Lam ys$ et $z$ est une variable \emph{fraîche}}
  \end{cases}
\end{displaymath}
Par <<~$z$ est une variable fraîche~>> on entend~: $z\not\in\VL{u_i}$ pour
$i=1,\dots,n$~; par $\vec u/\vec x\setminus y$ on entend la suite
$u_1/x_1,\dots,u_n/x_n$ amputée de $u_i/x_i$ si $y=x_i$.

Par exemple, si on veut substituer $y$ à $x$ et $t$ à $y$ dans le terme $t=\Lam
y{\App yx}$ on obtient~:
\begin{align*}
  \Subst{(\Lam y{\App yx})}{y/x,t/y} 
    &= \Lam z\Subst{(\App yx)}{z/y,y/x}\\
    &= \Lam z\App{\Subst y{z/y,y/x}}{\Subst x{z/y,y/x}}\\
    &= \Lam z\App zy
\end{align*}

\begin{rem}
Quand on écrit $\Subst t{t_1/x_1,\dots,t_n/x_n}$, les $n$
substitutions sont faites simultanément, et non l'une après l'autre si bien que
\begin{displaymath}\def\s{\sigma}
  \Subst t{t_1/x_1,\dots,t_n/x_n} = \Subst t{t_{\s1}/x_{\s1},\dots,t_{\s
  n}/x_{\s n}}
\end{displaymath}
pour toute permutation $\sigma$ de $\{1,\dots,n\}$.
\end{rem}

\begin{lemme}\label{lemme:subst-iteree}
Soit $t$, $t_1,\dots,t_n$, $u_1,\dots,u_m$ des termes.
On a 
\begin{displaymath}
  \Subst {\Subst t{\vec t/\vec x}}{\vec u/\vec y} =
  \Subst t{\Subst{\vec t}{\vec u/\vec y}/\vec x,\vec u/\vec y}
\end{displaymath}
\end{lemme}
La preuve de ce lemme est laissée en exercice (simple récurrence sur la
taille de $t$).

\subsection{Généralités sur les relations}
Soit $E$ un ensemble. Pour nous, une relation sur $E$ est un
sous-ensemble de $E\times E$ (on ne considère ici que des relations
binaires). Soit $R$ une relation sur $E$. On écrit souvent
$a\mathrel Rb$ au lieu de $(a,b)\in R$.

On dit que $R$ est réflexive si
\begin{displaymath}
  \forall a\in E\quad a\mathrel Ra\ .
\end{displaymath}
On dit que $R$ est symétrique si
\begin{displaymath}
\forall a,b\in E\quad a\mathrel Rb\Implies b\mathrel Ra\ .
\end{displaymath}
On dit que $R$ est transitive si
\begin{displaymath}
\forall a,b,c\in E\quad a\mathrel Rb\et b\mathrel Rc\Implies a\mathrel Rc\ .
\end{displaymath}
On dit que $R$ est une relation d'équivalence si elle a ces trois
propriétés.


\paragraph{Clôtures symétrique et transitive.}
La \emph{clôture symétrique} de $R$ est la plus petite (pour l'inclusion)
relation $S$ sur $E$ qui contient $R$ et qui est symétrique. On vérifie
facilement que
\begin{displaymath}
  a\mathrel Sb\Equiv a\mathrel Rb\ou b\mathrel Ra\ .
\end{displaymath}

La \emph{clôture transitive} de $R$ est la plus petite relation $T$ sur $E$ qui
contient $R$ et qui est réflexive et transitive. On vérifie facilement que
$a\mathrel Tb$ si et seulement s'il existe une suite $a_1,\dots a_n$ telle que
$a_1=a$, $a_n=b$ et, pour chaque $i=1,\dots,n-1$, on a $a_i\mathrel Ra_{i+1}$.

La clôture symétrique transitive de $R$ est la plus petite relation
d'équivalence sur $E$ qui contienne $R$. On vérifie facilement que c'est la
clôture transitive de la clôture symétrique de $R$.%
\footnote{et non pas la clôture symétrique de la clôture transitive de $R$
  (cette dernière relation n'a d'ailleurs aucune raison d'être une relation
  d'équivalence).}

\paragraph{Confluence.}
La relation $R$ est dite \emph{confluente} si, pour tous $a,a_1,a_2\in E$
tels que $a\mathrel Ra_1$ et $a\mathrel Ra_2$, il existe $b\in E$ tel que
$a_1\mathrel Rb$ et $a_2\mathrel Rb$.

\begin{lemme}
\label{lemme:confl-trans}
La clôture transitive d'une relation confluente est confluente.
\end{lemme}
La preuve est laissée en exercice.


\paragraph{Congruences.}
Soit $R$ une relation sur $\Lambda$. On dit que $R$ est une \emph{congruence}
ou que $R$ \emph{passe au contexte} si $R$ est réflexive et vérifie

\begin{itemize}
\item $\App uv\mathrel R\App{u'}{v'}$ dès que $u\mathrel Ru'$ et $v\mathrel
  Rv'$~;
\item $\Lam xu\mathrel R\Lam x{u'}$ dès que $u\mathrel Ru'$.
\end{itemize}

\subsection{La $\beta$-réduction}

Un \emph{rédex} est un lambda-terme de la forme
\begin{displaymath}
  \App{\Lam xt}u
\end{displaymath}
La $\beta$-réduction (la seule règle de calcul du lambda-calcul, pour nous
du moins) exprime qu'un tel rédex, où qu'il se trouve dans un terme, peut être
\emph{contracté} en
\begin{displaymath}
\Subst t{u/x}
\end{displaymath}
ce qui se justifie bien, si l'on a présent à l'esprit que l'expression
$\App{\Lam xt}u$ représente l'application à $u$ de la fonction qui à $x$
associe $t$ (dans lequel $x$ figure libre en général).

\paragraph{Beta-réduction.}
Un terme $t$ se $\beta$-réduit en une étape en un terme $t'$ si $t'$ s'obtient
à partir de $t$ en sélectionnant dans $t$ \emph{exactement un} rédex
(c'est-à-dire une occurrence de sous-terme de $t$ qui est un rédex) et en
contractant ce rédex. Plus précisément, on définit la relation $\Bun$ par
récurrence sur son premier argument~:

\begin{itemize}
\item $x\Bun u$ n'est jamais vrai quand $x\in V$~;
\item $\App{\Lam xu}v\Bun \Subst u{v/x}$~;
\item $\App uv\Bun \App{u'}v$ si $u\Bun u'$~;
\item $\App uv\Bun \App u{v'}$ si $v\Bun v'$~;
\item $\Lam xu\Bun\Lam x{u'}$ si $u\Bun u'$.
\end{itemize}

\paragraph{Forme normale.}
Un terme $t$ est dit \emph{normal} s'il ne contient aucun rédex,
autrement dit, s'il n'existe aucun terme $u$ tel que $t\Bun u$. Par
exemple, le terme
\begin{displaymath}
\Lam f{\App{f}{\Lam x{\App{f}{\Lam dx}}}}
\end{displaymath}
est normal.

On note $\Btr$ la clôture transitive de $\Bun$ et $\Beq$ la clôture
symétrique et transitive de $\Bun$. Deux termes qui sont reliés par cette
relation d'équivalence sont dits \emph{$\beta$-équivalents}.

\begin{lemme}
Les relations $\Btr$ et $\Beq$ passent au contexte.
\end{lemme}

\begin{rem}
  En fait la relation $\Btr$ (resp. $\Beq$) est la plus petite relation qui (i)
  passe au contexte, (ii) est transitive (resp. est une relation d'équivalence)
  et (iii) relate $\App{\Lam xu}v$ et $\Subst u{v/x}$.
\end{rem}

\paragraph{Termes (fortement) normalisables.}
Un terme $t$ est \emph{normalisable} s'il existe un terme normal $u$ tel que
$t\Btr u$, et alors on dit que $u$ est une \emph{forme normale} de $t$. On dit
que $t$ est \emph{fortement normalisable} s'il n'y a pas de suite infinie de
terme $(t_i)_{i=1,2,\dots}$ telle que $t_1=t$ et $t_i\Bun t_{i+1}$ pour tout
$i$.

Clairement, tout terme fortement normalisable est normalisable.

Voici quelques exemples. Soit $\Delta=\Lam x{\App xx}$.
Le terme $\App\Delta\Delta$ n'est pas normalisable, puisqu'il se réduit
en une étape en $\App\Delta\Delta$. Le terme
\begin{displaymath}
t=\App{\Lam dz}{\App\Delta\Delta}
\end{displaymath}
est normalisable, mais non fortement normalisable.


\subsection{Le théorème de Church-Rosser}

\paragraph{Confluence.}
Un même terme peut contenir plusieurs rédex, et donc il y a plusieurs façons de
le réduire en général. Par exemple, dans le terme $t$ ci-dessus, la réduction
du rédex le plus extérieur aboutit en une étape à une forme normale, alors que
la réduction de l'autre rédex aboutit à un terme égal à $t$.

On peut donc se demander si, en réduisant un terme de deux façons différentes,
on peut aboutir à deux formes normales distinctes. Ce n'est pas le cas, grâce
au théorème de Church-Rosser~:

\begin{theo}[Church-Rosser]
\label{th:CR}
La relation $\Btr$ sur $\Lambda$ est confluente.
\end{theo}

Admettons ce théorème pour un moment.  Soient $t$ un terme et $t_1$, $t_2$ deux
termes normaux tels que $t\Btr t_1$ et $t\Btr t_2$. Par le théorème, il existe
un terme $t'$ tel que $t_1\Btr t'$ et $t_2\Btr t'$. Comme $t_1$ est normal,
$t_1=t'$, et de même, $t_2=t'$. Donc $t_1=t_2$ et on vient de montrer le

\begin{coro}
Un terme normalisable du lambda-calcul a une unique forme normale.
\end{coro}

Une autre conséquence intéressante (et tout aussi immédiate) est
\begin{coro}\label{coro:CR-zigzag}
  Soient $t$ et $u$ deux termes. On a $t\Beq u$ ssi il existe $v$ tel que
  $t\Btr v$ et $u\Btr v$.
\end{coro}
En particulier deux termes normalisables sont $\beta$-équivalent ssi ils ont la
même forme normale.

Le théorème~\ref{th:CR} serait immédiat (grâce au
lemme~\ref{lemme:confl-trans}) si la relation $\Bun$ elle-même était
confluente. Ce n'est malheureusement pas le cas, comme le montre l'exemple
suivant.

Soit $I=\Lam xx$ (l'identité). Soit
\begin{displaymath}
  t=\App\Delta{\App {I_1}{I_2}}
\end{displaymath}
où l'on a indicé les deux occurrences de $I$ pour les distinguer.  Ce terme
contient deux rédex. Selon que l'on réduit l'un ou l'autre on obtient~:
\begin{displaymath}
  t_1=\App{\App{I_1}{I_2}}{\App {I_1}{I_2}}\qquad\text{ou}\qquad
  t_2=\App\Delta{I_2}
\end{displaymath}
Comme $t_2$ n'a qu'un redex, il y a un unique $t_3$ tel que $t_2\Bun t_3$, à
savoir~:
\begin{displaymath}
  t_3=\App{I_2}{I_2}
\end{displaymath}
Par contre $t_1$ contient deux rédex, mais la réduction d'aucun de ces deux
rédex ne permet (en une étape) d'obtenir $t_3$ à partir de $t_1$. Donc la
relation $\Bun$ n'est pas confluente.

Cet exemple explicite la raison pour laquelle $\Bun$ n'est pas confluente~: le
terme $t$ contient deux rédex, et la réduction du rédex le plus extérieur ($t$
lui-même) a pour effet de \emph{dupliquer} l'autre rédex (le terme
$\App{I_1}{I_2}$).  Du coup, il faut faire deux étapes de $\Bun$ pour passer de
$t_1$ à $t_3$ et refermer le diagramme de confluence.  Observer toutefois que,
pour refermer ce diagramme, on ne réduit que des rédex qui étaient
\emph{initialement présents} dans $t$~; le terme $t_3$ est un rédex qui n'était
pas initialement présent dans $t$, mais sa réduction n'est pas utile pour
refermer le diagramme de confluence.


\paragraph{Création de redex.}
L'exemple illustre un autre phénomène très important en lambda-calcul, la
\emph{création de redex}. Comme $I=\Lam xx$, le terme $t_3$ contient un redex
qui, comme on l'a déja dit, \emph{n'est pas initialement présent dans $t$},
donc a été créé par la réduction. Le fait qu'une étape de réduction en général
crée de nouveaux redex est la clef de la complexité calculatoire du
lambda-calcul. C'est en particulier la raison pour laquelle il existe des
termes non normalisables~: par exemple si l'on fait une étape de réduction sur
$\App\Delta\Delta$ alors on crée un nouveau redex qui se trouve être le terme
de départ. Pour se convaincre qu'il y a vraiment création de redex, indicer les
deux occurrences de $\Delta$, et faire la réduction.

\paragraph{Réduction parallèle.}
Nous allons montrer le théorème de Church-Rosser en définissant une relation
$\Bpar$ (appelé parfois \emph{réduction parallèle}), qui contient $\Bun$, est
confluente, et dont la clôture transitive est $\Btr$. L'idée est de supprimer
la restriction de $\Bun$ (\emph{exactement un} redex) qui est comme on vient de
le voir, la raison pour laquelle $\Bun$ n'est pas confluente. Intuitivement on
aura donc $t\Bpar t'$ si il existe un ensemble (possiblement vide) de redex de
$t$ tel que lorsqu'on les réduit tous (en parallèle), on obtient $t'$~; ou
encore si $t$ se réduit en $t'$ sans qu'aucune des étapes de réductions ne
choisisse un redex \emph{créé} par les étapes précédentes.


On défini $t\Bpar u$ pour tout $u$ par récurrence sur la longueur de $t$~:

\begin{itemize}
\item $t\Bpar t$ pour tout $t$~;
\item $\App{\Lam xu}v\Bpar \Subst{u'}{v'/x}$ si $u\Bpar u'$ et $v\Bpar b'$~;
\item $\App uv\Bpar\App{u'}{v'}$ si $u\Bpar u'$ et $v\Bpar b'$~;
\item $\Lam xu\Bpar\Lam x{u'}$ si $u\Bpar u'$.
\end{itemize}

\begin{lemme}
  La relation $\Bpar$ est la plus petite relation qui passe au contexte et
  telle que si $u\Bpar u'$ et $v\Bpar v'$ alors $\App{\Lam xu}v\Bpar
  \Subst{u'}{v'/x}$.
\end{lemme}
La démonstration est immédiate.

\begin{lemme}
  \begin{displaymath}
    {\Bun}\subseteq{\Bpar}\subseteq{\Btr}
  \end{displaymath}
\end{lemme}

\begin{proof}
  Clairement $\Bpar$ contient $\Bun$. Et comme $\Btr$ est une (la plus petite
  en fait) relation transitive passant au contexte et vérifiant la condition de
  clôture de $\Bpar$, $\Btr$ contient $\Bpar$.
\end{proof}

On en déduit le
\begin{lemme}
La clôture transitive de $\Bpar$ est $\Btr$.
\end{lemme}

\begin{lemme}\label{lemme:par-subst}
Soient $t,t',u,u'\in\Lambda$ tels que $t\Bpar t'$ et $u\Bpar u'$, et soit $x\in
V$. On a $\Subst t{u/x}\Bpar\Subst{t'}{u'/x}$.
\end{lemme}
\begin{proof}
Par récurrence sur la taille de $t$.

Si $t$ est une variable $y$, alors $t'=y$ et on conclut immédiatement, que
$y$ soit ou non égal à $x$.

Si $t=\App sr$ et $t'=\App{s'}{r'}$ avec $s\Bpar s'$ et $r\Bpar r'$, on a, par
hypothèse de récurrence, $\Subst s{u/x}\Bpar \Subst{s'}{u'/x}$ et
$\Subst r{u/x}\Bpar \Subst{r'}{u'/x}$, donc
\begin{displaymath}
  \App{\Subst s{u/x}}{\Subst r{u/x}}\Bpar 
  \App{\Subst{s'}{u'/x}}{\Subst{r'}{u'/x}}
\end{displaymath}
c'est-à-dire (par définition de la substitution),
$\Subst t{u/x}\Bpar\Subst{t'}{u'/x}$.

Si $t=\App{\Lam ys}r$ et $t'=\Subst{s'}{r'/y}$, avec $s\Bpar s'$ et $r\Bpar
r'$, observer d'abord qu'on peut supposer $y\not=x$ (quitte à renommer la
variable liée $y$). Par hypothèse de récurrence, on a 
\begin{displaymath}
  \Subst s{u/x}\Bpar \Subst{s'}{u'/x}
  \quad\text{et}\quad
  \Subst r{u/x}\Bpar \Subst{r'}{u'/x}
\end{displaymath}
et donc, par définition de $\Bpar$,
\begin{displaymath}
  \App{\Lam y{\Subst s{u/x}}}{\Subst r{u/x}}\Bpar
  \Subst{\Subst{s'}{u'/x}}{\Subst{r'}{u'/x}/y}\ ,
\end{displaymath}
or par définition de la substitution (vu que $y\not=x$, et qu'on peut
supposer que $y\notin\VL{u}$), on a 
$\App{\Lam y{\Subst s{u/x}}}{\Subst r{u/x}}=\Subst t{u/x}$, et par le
lemme~\ref{lemme:subst-iteree}, on a 
\begin{displaymath}
  \Subst{\Subst{s'}{r'/y}}{u'/x}=\Subst{s'}{u'/x,\Subst{r'}{u'/x}/y}\ ,
\end{displaymath}
et comme on peut supposer que $y\notin\VL{u'}$,
\begin{displaymath}
  \Subst{s'}{u'/x,\Subst{r'}{u'/x}/y}=
  \Subst{\Subst{s'}{u'/x}}{\Subst{r'}{u'/x}/y}
\end{displaymath}
et on conclut que
\begin{displaymath}
  \App{\Lam y{\Subst s{u/x}}}{\Subst r{u/x}}\Bpar
  \Subst{\Subst{s'}{r'/y}}{u'/x}\ ,
\end{displaymath}
ce qu'il fallait prouver.

Le cas où $t=\Lam ys$ et $t'=\Lam y{s'}$ (encore une fois, on peut supposer
$y\not=x$) est laissé au lecteur en exercice.
\end{proof}

On conclut la preuve du théorème~\ref{th:CR} au moyen du lemme suivant.
\begin{lemme}
La relation $\Bpar$ est confluente sur $\Lambda$.
\end{lemme}
\begin{proof}
  Soient $t,t_1,t_2\in\Lambda$ tels que $t\Bpar t_1$ et $t\Bpar t_2$. On
  prouve par induction sur la longueur de $t$ qu'il existe $u\in\Lambda$ tel
  que $t_i\Bpar u$ pour $i=1,2$.

  Si $t=x\in V$, alors $t_1=t_2=x$ et on peut prendre $u=x$.

  Si $t=\App uv$ et $t_i=\App{u_i}{v_i}$ avec $u\Bpar u_i$, $v\Bpar v_i$ alors
  par hypothèse de récurrence sur il existe des termes $u'$ et $v'$ tels que
  $u_i\Bpar u'$ et $v_i\Bpar v'$ pour $i=1,2$. Mais si on prend
  $t'=\App{u'}{v'}$, comme $\Bpar$ passe au contexte on voit que $t_i\Bpar t'$
  pour $i=1,2$.

  Si $t=\App{\Lam xu}v$ alors il y a deux cas à considérer~:
  \begin{itemize}
  \item $t_1=\App{\Lam x{u_1}}v_1$ et $t_2=\Subst{u_2}{v_2/x}$ où $u\Bpar u_i$
    et $v\Bpar v_i$ pour $i=1,2$. Par hypothése de récurrence on a alors $u'$
    et $v'$ tels que $u_i\Bpar u'$ et $v_i\Bpar v'$ pour $i=1,2$. Par
    définition de $\Bpar$ on a donc $t_1\Bpar\Subst{u'}{v'/x}$ et par le lemme
    de substitution ci-dessus $t_2\Bpar\Subst{u'}{v'/x}$, soit le résultat
    cherché avec $t'=\Subst{u'}{v'/x}$.
  \item $t_i=\Subst{u_i}{v_i/x}$ où $u\Bpar u_i$ et $v\Bpar v_i$ pour $i=1,2$.
    On obtient à nouveau le résultat avec $t'=\Subst{u'}{v'/x}$ en appliquant
    deux fois le lemme de substitution.
  \end{itemize}
\end{proof}

\subsection{Réduction de tête et réduction gauche}

Le résultat suivant est une observation très simple, mais très importante, sur
la forme générale d'un lambda-terme.
\begin{lemme}
  Soit $t\in\Lambda$. Il existe une unique famille de variable $x_1,\dots,x_n$
  (avec $n\geq 0$), une unique famille de termes $u_1,\dots,u_k\in\Lambda$
  (avec $k\geq 0$), et un unique terme $u\in\Lambda$ qui est \emph{soit une
    variable, soit un rédex}, tels que
  \begin{displaymath}
    t=\Lam{x_1\dots x_n}{\App u{u_1\dots u_k}}\ .
  \end{displaymath}
\end{lemme}
L'écriture du terme $t$ fournie par ce résultat sera appelée écriture
\emph{canonique} de $t$.

\paragraph{Forme normale de tête, variable de tête.}
Avec les notations du lemme, si $u$ est un rédex, on dit que c'est le
\emph{rédex de tête} de $t$. Si $u$ est une variable, on dit que c'est la
\emph{variable de tête} de $t$, et que $t$ est en \emph{forme normale de tête}
ou est une \emph{forme normale de tête}.

Un terme en forme normale est évidemment aussi en forme normale de tête,
mais la réciproque est fausse. Par exemple, le terme
\begin{displaymath}
  \Lam x{\App x{\App\Delta\Delta}}
\end{displaymath}
est en forme normale de tête, mais il n'est pas en forme normale.

\paragraph{Réduction de tête.}
Soient $t$ et $t'$ deux termes et $\Lam{\vec x}{\App {t_0}{\vec t}}$ l'écriture
canonique de $t$. On dit que $t$ \emph{se réduit de tête} en $t'$ en une étape,
et on écrit $t\BTun t'$ si $t_0$ est un rédex $\App{\Lam xu}v$ et
\begin{displaymath}
  t'=\Lam{\vec x}{\App {\Subst u{v/x}}{\vec t}}\,.
\end{displaymath}

La réduction de tête est la clôture transitive de la réduction de tête en une
étape. Elle sera notée $\BTtr$. Il est clair que ${\BTun}\subseteq{\Bun}$ et
que ${\BTtr}\subseteq{\Btr}$ (exercice~: montrer par des contre-exemples que
ces inclusions sont strictes).

Remarquer que dans un terme, il y a au plus un rédex de tête, donc
contrairement à la $\beta$-réduction, la $\beta$-réduction de tête est une
stratégie de réduction (à chaque étape, on n'a qu'une seule possibilité pour
continuer).

Sur un terme en forme normale de tête, il est bien sûr impossible d'exécuter
une réduction de tête.

\paragraph{Formes normales de tête et beta-équivalence.}
Observer qu'un terme peut avoir plusieurs formes normales de tête. Toutefois,
si deux termes $t$ et $t'$, tous deux en forme normale de tête, sont
$\beta$-équivalents, disons~:
\begin{displaymath}
  t=\Lam{x_1\dots x_n}{\App y{u_1\dots u_k}}\quad\text{et}\quad
  t'=\Lam{x'_1\dots x'_{n'}}{\App {y'}{u'_1\dots u'_{k'}}}\ ,
\end{displaymath}
il faut qu'on ait $n'=n$, $k'=k$ et (au renommage près des variables liées),
$x'_1=x_1$,\dots, $x'_n=x_n$, $y'=y$ et $u'_1\Beq u_1$,\dots $u_k\Beq u'_k$,
comme le montre le corollaire~\ref{coro:CR-zigzag}.  En effet, les seules
$\beta$-réductions que l'on peut effectuer sur $t$ sont à l'intérieur des
$u_i$, et elle ne peuvent pas affecter l'ossature de $t$ (les $\lambda$
extérieurs $\lambda x_1\dots x_n$, la variable de tête et le nombre de ses
arguments).

\paragraph{Normalisation de tête}
On dira qu'un terme $t$ est \emph{normalisable de tête} si sa réduction de
tête termine, autrement dit s'il n'y a pas de suite infinie de terme
$t_1,t_2,\dots$ telle que $t_i\BTun t_{i+1}$ pour tout $i$. Dans ce cas, le
dernier élément de la suite des réduits de tête de $t$ est évidemment
une forme normale de tête.

Voici un petit lemme utile sur la normalisabilité de tête.
\begin{lemme}\label{lemme:norm-tete}
  Soient $t$, $u_1$,\dots, $u_n$, $v_1$, \dots, $v_m$ des termes. Si
  $\App{\Subst t{\vec u/\vec x}}{\vec v}$ est normalisable de tête alors $t$
  l'est.
\end{lemme}
\begin{proof}
  Par récurrence sur la longueur de la réduction de tête de $t'=\App{\Subst
    t{\vec u/\vec z}}{\vec v}$. Si $t'$ est en forme normale de tête alors $t$
  l'est~; sinon on a
  \begin{displaymath}
    t=\Abs{\vec y}\App{\App{\Abs y{t_0}}{t_1}}{\vec w}
  \end{displaymath}
  d'où
  \begin{displaymath}
    t'= \App{\Abs{\vec y}\App{\App{\Abs y{\Subst{t_0}{\vec u/\vec x}}}
        {\Subst{t_1} {\vec u/\vec x}}}
        {\expandafter\vec\Subst w{\vec u/\vec x}}}{\vec v}
  \end{displaymath}
  et $t'$ n'est clairement pas en forme normale de tête.
  
  Si $t'$ n'est pas en forme normale de tête on raisonne par cas sur $t$. Si
  $t$ est en forme normale de tête il n'y a rien à dire. Si $t=\App r{\vec w}$
  où $r$ est un redex alors $t'=\App{\Subst r{\vec u/\vec x}}{\Subst{\vec
      w}{\vec u/\vec x}\vec v}$ donc $t'\BTun t''=\App{\Subst {r'}{\vec u/\vec
      x}}{\Subst{\vec w}{\vec u/\vec x}\vec v}$ où $r'$ est le contracté de
  $r$. Mais $t\BTun t'''=\App{r'}\vec w$ et $\App{\Subst{t'''}{\vec u/\vec
      x}}\vec v=t''$~; par récurrence sur la longueur de la réduction de tête
  de $t''$ on a que la réduction de tête de $t'''$ termine et donc celle de $t$
  puisque $t'''$ est son réduit de tête à une étape.
  
  Enfin si $t=\Abs x{t_0}$ alors $t'=\App{\Abs x{\Subst{t_0}{\vec u/\vec
        x}}}{\vec v}$ donc $t'\BTun t''=\App{\Subst{t_0}{\vec u/\vec
      x,v_1/x}}v_2\dots v_n$. Par récurrence sur la longueur de la réduction de
  tête de $t''$ on a que la réduction de tête de $t_0$ termine, et donc celle
  de $t$ par définition de la réduction de tête.
\end{proof}

\paragraph{Le théorème de normalisation de tête.}
Il s'agit de l'un des résultats de base de la théorie du lambda-calcul, au même
titre que le théorème de Church-Rosser. On l'énonce ici mais on le démontrera
en~\ref{sec-engeler}.

\begin{theo}\label{th:norm-tete}
  Un terme est normalisable de tête si et seulement s'il est $\beta$-équivalent
  à un terme en forme normale de tête.
\end{theo}
Autrement dit, la réduction de tête est une stratégie qui aboutit toujours à
une forme normale de tête, dès lors qu'on l'applique à un terme
$\beta$-équivalent à un terme en forme normale de tête. 

\paragraph{Réduction gauche.}
Soient $t$ et $t'$ deux termes. On dit que $t$ \emph{se réduit à gauche} en
$t'$ en une étape, et on écrit $t\BGun t'$ si, soit $t$ a un redex de tête et
$t'$ est obtenu par contraction d'ycelui, soit $t=\Abs{\vec x}\App x{t_1\dots
  t_n}$ est en forme normale de tête et $t'=\Abs{\vec x}\App x{t_1\dots
  t_{i-1}t'_it_{i+1}\dots t_n}$ où $t'_i$ est un réduit gauche à une étape de
$t_i$ pour un $i$. Autrement dit la réduction gauche est l'extension de la
réduction de tête aux arguments de la variable de tête. On note $\BGtr$ la
clôture transitive de $\BGun$.

Remarquons que la réduction gauche, contrairement à la réduction de tête, n'est
pas une stratégie car elle ne détermine pas un unique redex dans le cas où $t$
n'est pas en forme normale de tête. On pourrait et c'est d'ailleurs souvent
ainsi qu'elle est présentée dans la littérature, la déterminiser complètement
en demandant que l'on ne réduit dans $t_i$ que si $t_1$,\dots, $t_{i-1}$ sont
normaux. On peut aussi considérer que les redex de chaque $t_i$ sont
indépendants et que la réduction gauche les réduit tous en parallèle.

La réduction gauche admet une propriété du même genre que la réduction de
tête~:
\begin{theo}
  Un terme est normalisable si et seulement si l'une des ses réductions gauche
  termine.
\end{theo}
\begin{rem}
  Il est relativement facile de voir que si l'une des réductions gauche termine
  alors toutes terminent.
\end{rem}

On ne démontrera pas ce théorème dans ces notes. Le lecteur pourra exercer sa
compréhension de la méthode de réductibilité exposée en~\ref{sec-engeler} en
tâchant d'adapter la preuve du théorème précédent. Une autre méthode consiste à
utiliser le théorème précédent et le fait que la réduction gauche est une
itération de la réduction de tête.

\section{Représentation des fonctions récursives}

\paragraph{Entiers de Church.}
Soit $n$ un entier. On note $\Rep n$ le lambda-terme
\begin{displaymath}
  \Rep n = \Abs f{\Abs x{\underbrace{(f)\dots(f)}_{n\,\times}x}}
\end{displaymath}
Les lambda-termes de la forme $\Rep n$ sont appelés les \emph{entiers de
  Church}. Remarquons qu'ils ont une interprétation fonctionnelle très simple~:
ce sont des itérateurs.

\paragraph{Représentation des fonctions.}
Soit $F:\Nat^k\fleche\Nat$ une fonction partielle. On dira que le lambda-terme
$\Rep F$ \emph{représente} $F$ si pour tous entiers $n_1$, \dots, $n_k$ on a~:
\begin{itemize}
\item si $\Undef{F(\vec n)}$ alors le terme $\App{\Rep F}{\Rep{\vec n}}$ n'a
  pas de forme normale de tête~;
\item si $F(\vec n) = m$ alors $\App{\Rep F}{\Rep{\vec n}}\Beq\Rep m$
\end{itemize}
\begin{rem}
  D'après le théorème~\ref{th:norm-tete}, la première condition est équivalente
  à~: si $\Undef{F(\vec n)}$ alors la réduction de tête de $\App{\Rep
  F}{\Rep{\vec n}}$ ne termine pas.
\end{rem}

\paragraph{Fonctions de base sur les entiers.}
On a en particulier $\Rep 0=\Abs f{\Abs xx}$. On voit facilement que le terme
\begin{displaymath}
  \Rep S=\Abs n{\Abs f{\Abs x{\App f{\App{\App nf}x}}}}
\end{displaymath}
représente la fonction successeur au sens où $\App{\Rep S}{\Rep
  n}\Beq\Rep{n+1}$. De même les termes
\begin{displaymath}
  \mathtt{Add}=\Abs n{\Abs m{\Abs f{\Abs x{\App{\App nf}{\App{\App
  mf}x}}}}}
\end{displaymath}
et
\begin{displaymath}
  \mathtt{Mult}=\Abs n{\Abs m{\Abs f{\Abs x{\App{\App n{\App mf}}x}}}}
\end{displaymath}
représente respectivement l'addition et la multiplication

Enfin le terme
\begin{displaymath}
  \mathtt{Inf}=\Abs n{\Abs m{\App{\App{\App{\App{\Rep S}n}{\varphi}}{\Abs
            d{\Rep 0}}}{\App{\App m\varphi}{\Abs d{\Rep 1}}}}}
\end{displaymath}
où $\varphi=\Abs f{\Abs g{\App gf}}$ représente la fonction caractéristique de
$<$.


\paragraph{Un terme de mise en mémoire.}
On note $T$ le terme
\begin{displaymath}
  T=\Abs f{\Abs n{\App{\App{\App n{\Abs h{\Abs x{\App h{\App{\Rep S}x}}}}}f}
      {\Rep 0}}}
\end{displaymath}
\begin{lemme}
  Soit $t$ et $u$ deux termes.
  \begin{itemize}
  \item Si il existe un entier $n$ tel que $u\Beq \Rep n$ alors $\App T{tu}\Beq
    \App t{\Rep n}$~;
  \item Si $u$ n'a pas de forme normale de tête alors $\App T{tu}$ non plus.
  \end{itemize}
\end{lemme}
\begin{proof}
  Commençons à effectuer la réduction de tête de $\App T{tu}$. Pour alléger le
  calcul on note $\varphi$ le terme $\Abs h{\Abs x{\App h{\App{\Rep S}x}}}$.
  \begin{align*}
    \App T{tu} &\BTun\Abs n{\App{\App{\App n\varphi}t} {\Rep 0}}\\
               &\BTun\App{\App{\App u\varphi}t} {\Rep 0}
  \end{align*}
  Si $u$ n'a pas de forme normale de tête alors sa réduction de tête est
  infinie et, par le lemme~\ref{lemme:norm-tete}, celle de $\App{\App{\App
      u\varphi}t}{\Rep 0}$ aussi. Par le théorème~\ref{th:norm-tete} on en
  déduit que $\App T{tu}$ n'a pas de forme normale de tête.

  Si $u\Beq\Rep n$ alors on voit facilement qu'il existe des termes $u'$,
  $u_0$, $u_1$, \dots, $u_n$ tels que~:
  \begin{align*}
    u &\BTtr\Abs f{u'}\\
    u'&\BTtr\Abs x{u_0}\\
    u_0&\BTtr\App f{u_1}\\
    &\vdots\\
    u_{n-1}&\BTtr \App f{u_n}\\
    u_n&\BTtr x
  \end{align*}
  Alors la réduction de tête de $\App T{tu}$ se continue ainsi~:
  \begin{align*}
    \App{\App{\App u\varphi}t} {\Rep 0}
    &\BTtr\App{\App{\App {\Abs f{u'}}\varphi}t} {\Rep 0}\\
    &\BTun\App{\App{\Subst{u'}{\varphi/f}}t} {\Rep 0}\\
    &\BTtr\App{\App{\Abs x{u'_0}}t}{\Rep 0}\\
    &\BTun\App{u''_0}{\Rep 0}\\
    &\BTtr\App{\App\varphi{u''_1}}{\Rep 0}\\
    &\BTun\App{\Abs x{\App{u''_1}{\App{\Rep S}x}}}{\Rep 0}\\
    &\BTun\App{u''_1}{\App{\Rep S}{\Rep 0}}\\
    &\vdots\\
    &\BTtr\App{u''_n}{\App{\Rep S}{\dots\App{\Rep S}{\Rep 0}}}\\
    &\BTtr\App t{\App{\Rep S}{\dots\App{\Rep S}{\Rep 0}}}\\
  \end{align*}
  où $u'_0=\Subst{u_0}{\varphi/f}$ et $u''_i=\Subst{u_i}{\varphi/f,t/x}$. Mais
  comme $\App{\Rep S}{\dots\App{\Rep S}{\Rep 0}}\Beq\Rep n$, le dernier terme
  est clairement beta-équivalent à $\App t{\Rep n}$, comme annoncé.
\end{proof}
\begin{rem}
  Le terme $T$ fait partie de la classe des \emph{termes de mise en mémoire}.
  Ce sont des termes qui ont la propriété que l'on vient de voir, à savoir que
  pour tout $n$, il existe un terme $\theta_n$ (ici $\theta_n=\App{\Rep
    S}{\dots\App{\Rep S}{\Rep 0}}$) tel que $\App T{tu}\BTtr\App t{\theta_n}$
  dès que $u\Beq\Rep n$. Le terme $T$ applique donc $t$ à $u$ mais après avoir
  effectué la normalisation complète de $u$ et donc calculé sa valeur
  $\theta_n$. Si on pense que la réduction de tête est une stratégie
  \emph{paresseuse}, selon la terminologie des langages fonctionnels, c'est à
  dire une stratégie qui ne calcule la valeur des arguments que lorsque c'est
  strictement nécessaire, alors le terme $T$ permet de faire de \emph{l'appel
    par valeur}, c'est à dire de calculer l'argument avant de le passer à la
  fonction.
\end{rem}


\paragraph{Le schéma de composition.}
Soit $F$ la fonction définie par~:
\begin{displaymath}
  F(a)=\Prem x{x=0}
\end{displaymath}
Clairement $F$ est représentée par $\Rep F=\Abs d{\Rep 0}$. Soit maintenant $G$
donnée par
\begin{displaymath}
  G(a) =\Prem x{x+1 = 0}
\end{displaymath}
Tout aussi clairement $G$ est représentée par $\Rep G=\Abs
d{\App\Delta\Delta}$.  Finalement soit $H$ définie par
\begin{displaymath}
 H(a) = F(G(a)) 
\end{displaymath}
Alors par définition du schéma de composition, $H$ est, comme $G$, la fonction
nulle part définie. On voit donc que l'on ne peut pas représenter $H$ par le
terme $h=\Abs x{\App{\Rep F}{\App{\Rep G}a}}$. En effet pour tout $n$ on a
\begin{displaymath}
  \App h{\Rep n}\Beq\Rep 0
\end{displaymath}
est donc normalisable, en contradiction avec la définition de représentation
d'une fonction. Par contre, grâce au lemme de mise en mémoire, on voit que
\begin{displaymath}
  \Rep H=\Abs a{\App{\App T{\Rep F}}{\App{\Rep G}a}}
\end{displaymath}
représente $H$ correctement. On va maintenant généraliser un peu cette idée de
manière à coder le schéma de composition complet en utilisant $T$.

Soient $t$, $u_1$, \dots, $u_n$ des termes. On note $\AppT t{u_1,\dots, u_n}$
ou $\AppT t{\vec u}$ le terme défini par récurrence sur $n$~:
\begin{align*}
  \AppT t{u_1} &=\App{\App Tt}{u_1}\\
  \AppT t{u_1,\dots, u_{n+1}}&=\App{\App T{\AppT t{u_1,\dots, u_n}}}{u_{n+1}}
\end{align*}

On voit immédiatement par récurrence sur $n$ que
\begin{itemize}
\item si l'un des $u_i$ n'a pas de forme normale de tête alors $\App t{\vec u}$
  non plus~;
\item si il existe $m_1$, \dots, $m_n$ tels que $u_i=\Rep m_i$ pour $i=1,\dots,
  n$ alors $\AppT t{\vec u}\Beq\App t{\Rep m_1,\dots,\Rep m_n}$.
\end{itemize}
D'où l'on déduit le
\begin{lemme}[Composition]
  Soient $F$ une fonction partielle d'arité $n$ et $G_1$, \dots, $G_k$ des
  fonctions partielles d'arité $k$ telles qu'il existe des termes $\Rep F$,
  $\Rep G_1$, \dots, $\Rep G_n$ les représentant. Alors le terme
  \begin{displaymath}
    \Abs {x_1}{\dots\Abs{x_k}
      \AppT{\Rep F}{\App{\Rep G_1}{\vec a},\dots,\App{\Rep G_n}{\vec a}}}
  \end{displaymath}
  représente la fonction composée $F(G_1(\vec a), \dots, G_n(\vec a))$.  
\end{lemme}

\paragraph{Schéma de minimisation.}
On note $Y$ le terme
\begin{displaymath}
  Y = \App{\Abs x{\Abs f{\App f{\App{\App xx}f}}}}{\Abs x{\Abs f{\App
  f{\App{\App xx}f}}}}
\end{displaymath}

\begin{lemme}[Point fixe]
  Pour tout terme $t$ on a
  \begin{displaymath}
    \App Yt\BTtr \App t{\App Yt}
  \end{displaymath}
\end{lemme}

Soit maintenant $\varphi$ et $U$ les termes
\begin{align*}
  \varphi &=\Abs u{\Abs n{\App{\App{\App fn}{\Abs d{\App u{\App{\Rep
  S}n}}}}n}}\\
  U &=\Abs f{\App{\App Y\varphi}{\Rep 0}}
\end{align*}

\begin{lemme}
  Soit $t$ un terme et $n$ un entier tel que pour tout $i<n$, il existe $m_i>0$
  tel que  $\App t{\Rep i}\Beq\Rep m_i$. Alors on a
  \begin{itemize}
  \item si $\App t{\Rep n}$ n'a pas de forme normale de tête alors $\App Ut$
    non plus~;
  \item si $\App t{\Rep n}\Beq\Rep 0$ alors $\App Ut\Beq\Rep n$.
  \end{itemize}
\end{lemme}
\begin{proof}
  On note $\varphi'$ le terme $\Subst\varphi{t/f}$ et $U_n$ le terme $\App{\App
    Y{\varphi'}}{\App{\Rep S}{\dots\App{\Rep S}{\Rep 0}}}$ où $\Rep S$ occure
  $n$ fois.  On a alors
  \begin{align*}
    \App Ut &\BTun U_0\\
            &\BTtr\App{\App{\varphi'}{\App Y{\varphi'}}}{\Rep 0}\\
            &\BTtr\App{\App{\App t{\Rep 0}}{\Abs d{\App {\App
                    Y{\varphi'}}{\App{\Rep S}{\Rep 0}}}}}{\Rep 0}=
            \App{\App{\App t{\Rep 0}}{\Abs d{U_1}}}{\Rep 0}\\
            &\Btr\App{\App{\Rep m_0}{\Abs d{U_1}}}{\Rep 0}\\
            &\BTtr U_1\\
            &\vdots\\
            &\BTtr U_n\\
            &\Btr\App{\App{\App t{\Rep n}}{\Abs d{U_{n+1}}}}{\Rep n}
  \end{align*}
  Si $\App t{\Rep n}$ n'a pas de forme normale de tête alors par le
  lemme~\ref{lemme:norm-tete} et le théorème~\ref{th:norm-tete}, $\App Ut$ non
  plus. Si $\App t{\Rep n}\Beq\Rep 0$ alors $\App Ut\Beq\App{\App{\Rep 0}{\Abs
  d{U_{n+1}}}}{\Rep n}\BTtr \Rep n$ comme annoncé.
\end{proof}

Avec ce dernier lemme on a achevé de démontrer le
\begin{theo}
  Si $F$ est une fonction récursive alors il existe un terme $\Rep F$ qui
  représente $F$.
\end{theo}


\paragraph{Récursion primitive.}
Puisque le lambda-calcul représente les fonctions récursives, d'après le
théorème~\ref{theo:recprim} il représente également les fonctions primitive
récursives. On va donner une preuve directe de ce fait.

Si $u_1$ et $u_2$ sont des termes on note $\Paire{u_1}{u_2}$ le terme
\begin{displaymath}
  \Paire{u_1}{u_2}=\Abs x{\App x{u_1u_2}}
\end{displaymath}
Si $c$ est un terme et $i=1$ ou $2$, on note $\pi_ic$ le terme
\begin{displaymath}
  \pi_ic=\App c{\Abs x_1{\Abs x_2{x_i}}}
\end{displaymath}
On vérifie immédiatement que l'on a
\begin{displaymath}
  \pi_i\Paire{u_1}{u_2}\BTtr u_i
\end{displaymath}

On note $\varphi$ et $R$ les termes
\begin{align*}
  \varphi &= \Abs c{\Paire{\App{\Rep S}{\pi_1c}}{\App{\App f{\pi_1c}}{\pi_2
  c}}}\\
  R &= \Abs f{\Abs b{\Abs n{\pi_2\App{\App n\varphi}{\Paire{\Rep 0}b}}}}
\end{align*}

\begin{lemme}
  Pour tous termes $t$ et $u$ on a~:
  \begin{align*}
    \App R{tu\Rep 0} &\Beq u\\
    \App R{tu\,\Rep{n+1}} &\Beq \App{\App t{\Rep n}}{\App R{tu\,\Rep n}} \\
    \end{align*}
    pour tout entier $n$.
\end{lemme}
La preuve est laissé en exercice au lecteur. Soient maintenant $G$ une fonction
d'arité $k$ et $H$ une fonction d'arité $k+2$ représentées respectivement par
les termes $\Rep G$ et $\Rep H$. On vérifie facilement que si on définit
\begin{align*}
  \varphi &= \Abs a{\Abs v{\App{\Rep H}va{\vec a}}}\\
  \psi &= \App{\Rep G}{\vec a}\\
  \Rep F &= \Abs a{\Abs{\vec a}{
      {\App{\App{\App R\varphi}{\psi}} a}}}
\end{align*}
alors le terme $\Rep F$ représente la fonction $F$ définie par récursion
primitive à partir de $G$ et $H$.

\section{Le modèle de Engeler}
\label{sec-engeler}

\lettrine{L}{e modèle} $\E(\A)$ de Engeler est un cas particulier de domaine de
Scott tel qu'il existe deux fonctions~:
\begin{displaymath}
  \E(\A)\RightLeft^\phi_\psi \E(\A)\fleche\E(\A)
\end{displaymath}
vérifiant $\phi\circ\psi = \mathrm{Id}$. Toutefois nous allons en donner ici
une présentation plus concrète que nous utiliserons ensuite pour démontrer le
théorème~\ref{th:norm-tete} selon la méthode classique de \emph{réductibilité}.

\subsection{Fonctions continues}

\paragraph{Notations et conventions.}
Soit $X$ un ensemble. On note $\Power X$ l'ensemble des parties de $X$. On
utilisera $a$, $b$ et $c$ pour dénoter les éléments de $X$, $x$ et $y$ pour
dénoter les parties de $X$ (les éléments de $\Power X$) et $A$, $B$ pour
dénoter les parties de $\Power X$ (les ensembles de parties de $X$). Si $A$ est
un ensemble de parties de $X$ on note $\Sup A$ la réunion des éléments de
$A$. Si $f$ est une fonction de $I\fleche\Power X$, on note $\Sup_{i\in I}f(i)$
la réunion des $f(i)$.


\paragraph{Familles filtrantes.}
Soit $A$ un ensemble d'ensembles. On note $\Sup A$ ou $\Sup_{x\in A}x$ la
réunion des éléments de $A$. On dira que $A$ est \emph{filtrant} si $A$ est
non vide et pour tous $x_1$, $x_2$ dans $A$, il existe un $y$ tel que
$x_i\subset y$ pour $i=1,2$.  L'exemple typique de famille filtrante est
l'ensemble des parties \emph{finies} d'un ensemble $X$, que l'on notera
$\PowerFin X$. Si $x$ est un ensemble, on écrira $x_0\subsetFin x$ pour \og
$x_0$ est une partie \emph{finie} de $x$~>>.


\paragraph{Fonctions continues.}
Soient $X$ et $Y$ deux ensembles. Une fonction $F:\Power X\fleche\Power Y$ est
dite \emph{continue} si elle est croissante (pour l'inclusion) et pour tout
ensemble filtrant $A\subset\Power X$ on a~:
\begin{displaymath}
  F(\Sup A) = \Sup_{x\in A} F(x)
\end{displaymath}

\begin{rem}
  L'une des inclusions est réalisée dès que $F$ est croissante, à savoir
  $\Sup_{x\in A} F(x)\subset F(\Sup A)$.
\end{rem}

\begin{lemme}[Finitude]
  Soit $F:\Power X\fleche\Power Y$ une fonction croissante. Alors $F$ est
  continue ssi pour tout $b\in  Y$ et tout $x\subset X$ on a la \emph{condition
  de finitude}~:
  \begin{displaymath}
    \text{si }b\in F(x)\text{ alors }\exists x_0\subsetFin x\text{ tel que }
    b\in F(x_0)
  \end{displaymath}
\end{lemme}

Cette condition exprime une propriété fondamentale des programmes~: pour
pouvoir donner un résultat fini, même partiel, tel le $b$ qui appartient à
$F(x)$, la fonction $F$ qui représente un programme n'a besoin que d'utiliser
un nombre \emph{fini} d'informations sur son entrée. Clairement un programme
qui utiliserait $x$ en entier pour pouvoir répondre que $b$ est un élément du
résultat, calculerait en temps infini dès que $x$ l'est. C'est l'un des buts de
la \emph{sémantique dénotationnelle} que de trouver des propriétés abstraites
des programmes, telles que la condition de finitude, qui permettent de définir
des classes de fonctions représentant les programmes.

\begin{proof}
  Supposons pour commencer que $F$ est continue et soit $b\in F(x)$. On
  considère la famille $\PowerFin x$ qui est filtrante~; comme
  $x=\Sup\PowerFin x$ on a par continuité de $F$
  \begin{displaymath}
    F(x) = \Sup_{x_0\in\PowerFin x}F(x_0)
  \end{displaymath}
  Comme $b\in F(x)$ on voit qu'il y a un $x_0\subsetFin x$ tel que $b\in
  F(x_0)$.
  
  Réciproquement supposons que $F$ est croissante et vérifie la condition de
  finitude. Soit $A$ un ensemble filtrant inclus dans $\Power X$. On sait déja,
  par croissance de $F$ que $\Sup_{x\in A}F(x)\subset F(\Sup A)$. Soit $b\in
  F(\Sup A)$. Par condition de finitude, on sait qu'il existe un $x_0\subsetFin
  \Sup A$ tel que $b\in F(x_0)$~; notons $a_1$, \dots, $a_n$ les éléments de
  $x_0$. Comme les $a_i$ sont des éléments de $\Sup A$, il existe $x_1$, \dots,
  $x_n$ appartenant à $A$ tels que $a\in x_i$ pour $i=1,\dots, n$. Mais comme
  $A$ est filtrant, on voit facilement (par récurrence sur $n$) qu'il existe un
  $x$ appartenant à $A$ et tel que $x_i\subset x$ pour $i=1,\dots, n$. Donc
  $x_0\subset x$ et par croissance de $F$ on obtient $b\in
  F(x)\subset\Sup_{x\in A}F(x)$.
\end{proof}


\paragraph{Trace d'une fonction continue.}
Soit $F$ une fonction continue de $\Power X$ dans $\Power Y$. On appelle
\emph{trace de $F$} et on note $\Trace F$ l'ensemble inclus dans $\PowerFin
X\times Y$ des couples~:
\begin{displaymath}
  \Trace F = \{(x_0, b),\, x_0\subsetFin X\text{ et } b\in F(x_0)\}
\end{displaymath}

Le lemme de finitude nous assure que $\Trace F$ contient toute l'information
nécessaire pour calculer $F(x)$. Plus précisément, si $f$ est une
partie de $\PowerFin X\times Y$, notons $\Fun f$ la fonction de $\Power
X\fleche\Power Y$ définie par~:
\begin{displaymath}
  \Fun f(x)=\{b\in Y,\, \exists x_0\subsetFin x\text{ tel que }(x_0,b)\in f\}
\end{displaymath}
Alors on a
\begin{lemme}\label{lemme:trace-fun}
  La fonction $\Fun f$ est continue de $\Power X$ dans $\Power Y$.
  Réciproquement, si $F$ est une fonction continue de $\Power X$ dans $\Power
  Y$ alors
  \begin{displaymath}
    \Fun\Trace F=F
  \end{displaymath}
\end{lemme}

Tout le propos de la théorie des \emph{domaines} est de généraliser les
définitions ci-dessus de façon à les appliquer à une classe d'ordre plus
générale que les simples $\Power X$ que l'on considère ici. On parvient alors à
munir l'ensemble des fonctions continues d'une structure de domaine et on
obtient que les fonctions $\Trace$ et $\Fun$ sont elles même continues. Mais
c'est une autre histoire\dots


\paragraph{Fonctions à plusieurs variables.}
Soient $X_1$, \dots, $X_n$ et $Y$ des ensembles. Une fonction
$F:\Power{X_1}\times\cdots\times\Power{X_n}\fleche \Power Y$ est continue si
elle l'est séparément sur chacun de ses paramètres. Cette définition est
cohérente avec la remarque que  $\Power{X_1}\times\cdots\times\Power{X_n}$ est
isomorphe à $\Power{X_1+\cdots+X_n}$ (où $X_1+X_2$ représente l'union disjointe
de $X_1$ et $X_2$).

Soit maintenant $F:\Power{X_1}\times\cdots\times\Power{X_{n+1}}\fleche \Power
Y$ une fonction continue. On note $\Trace_n F$ la fonction de
$\Power{X_1}\times\cdots\times\Power{X_n}\fleche
\Power{\PowerFin{X_{n+1}}\times Y}$ définie par~:
\begin{displaymath}
  \Trace_n F(x_1,\dots, x_n) = \Trace F_{x_1,\dots,x_n}
\end{displaymath}
où $F_{x_1,\dots,x_n}:\Power{X_{n+1}}\fleche \Power Y$ est la fonction~:
$F_{x_1,\dots,x_n}(x)= F(x_1,\dots,x_n,x)$ (Exercice~: montrer que $\Trace_n
F$est continue).

Réciproquement si $F:\Power{X_1}\times\cdots\times\Power{X_n}\fleche
\Power{\PowerFin{X_{n+1}}\times Y}$ est continue, on note $\Fun_n
F:\Power{X_1}\times\cdots\times\Power{X_{n+1}}\fleche \Power Y$ la fonction
définie par~:
\begin{displaymath}
  \Fun_n F(x_1,\dots, x_{n+1}) = \Fun(F(x_1,\dots,x_n))(x_{n+1})
\end{displaymath}
(Exercice~: montrer que $\Fun_n F$ est continue). Comme pour le
lemme~~\ref{lemme:trace-fun} on a pour $F: \Power{X_1} \times\cdots\times
\Power{X_{n+1}}\fleche \Power Y$
\begin{displaymath}
  \Fun_n\Trace_n F= F
\end{displaymath}

\subsection{Modèle de Engeler}


\paragraph{Construction du modèle.}
Soit $\A$ un ensemble dénombrables dont les éléments seront appelés les
\emph{atomes}. On se donne une suite d'ensembles $(D_n)$ définie par récurrence
par~:
\begin{align*}
  D_0 &= \A\\
  D_{n+1} &= D_n\cup\{(x_0,a),\,x_0\subsetFin D_n\text{ et }a\in D_n\}
\end{align*}
On note $\D(\A)$ la réunion de tous les $D_n$. Par construction $\D(\A)$ est
le plus petit ensemble $D$ tel que $\A\subset D$ et $\PowerFin D\times D\subset
D$.

On note $\E(\A)$ l'ensemble $\Power{\D(\A)}$. Si $F:\E(\A)\fleche \E(\A)$ est
continue alors comme $\Trace F\subset\PowerFin{\D(\A)}\times\D(\A)$ on a
$\Trace F\in\E(\A)$. Réciproquement si $f\in\E(\A)$ on écrira $\Fun f$ pour
$\Fun(f/\A)$ qui est donc une fonction continue de $\E(A)\fleche\E(\A)$. Comme
$\Fun\Trace F=F$ pour toute fonction continue $F$ sur $\D(A)$ on voit que, en
notant $\D(\A)\fleche\D(\A)$ l'espace des fonctions continues sur $\D(\A)$, on
a~:
\begin{displaymath}
  \E(\A)\RightLeft^{\Fun}_{\Trace} \E(\A)\fleche\E(\A)
\end{displaymath}
si bien que $\Fun$ et $\Trace$ réalisent le programme annoncé dans
l'introduction (p.~\pageref{sec-engeler}).
 
\paragraph{Interprétation des termes.}
Dans toute cette partie, afin d'éviter les confusions on n'utilisera que la
lettre $z$ pour dénoter les variables du lambda-calcul. Soient
$\ell=(z_1,\dots, z_n)$ une suite finie de variables et $t$ un terme dont
les variables libres sont parmi les éléments de $\ell$. On va associer à $t$
une fonction continue $\Interp t_\ell : \E(A)\times\dots\times\E(\A) \fleche
\E(\A)$ d'arité $n$ définie par récurrence sur $t$~:

\smallskip
\begin{itemize}
\item si $t=z_i$ alors $\Interp t_\ell(\vec x)=x_i$~;
\item si $t=\App uv$ alors $\Interp t_\ell(\vec x) = \Fun_n\Interp u_\ell(\vec
  x, \Interp v_\ell(\vec x))$~;
\item si $t=\Abs zu$ alors $\Interp t_\ell(\vec x)=\Trace_n\Interp
  u_{\ell.z}(\vec x)$ où $\ell.z$ est la suite $(z_1,\dots,z_n,z)$.
\end{itemize}


\paragraph{Le modèle de Engeler vu comme système de typage.}
Si on applique les définitions de $\Fun$ et $\Trace$ on a que
\begin{itemize}
\item si $t=\App uv$ alors $\Interp t_\ell(\vec x) =\{a,\, \exists
  x_0\subsetFin \Interp v_\ell(\vec x)\text{ tel que }(x_0, a)\in\Interp
  u_\ell(\vec x)\}$.
\item si $t=\Abs zu$ alors $\Interp t_\ell(\vec x)=\{(x_0, a),\, x_0\subsetFin\D(\A)\text{ et
    }a\in\Interp u_{\ell.z}(\vec x,x_0)\}$
\end{itemize}

Notons $z_1:x_1,\dots,z_n:x_n\vdash t:a$ le fait que $a\in\Interp t_\ell(\vec
x)$ et notons $x_0\fleche a$ le couple $(x_0,a)$. Alors les clauses ci-dessus
deviennent~:
\begin{itemize}
\item $\vec z:\vec x\vdash z_i:a_i$ si $a_i\in x_i$~;
\item $\vec z:\vec x\vdash \App uv:a$ si il existe $x_0$ fini tel que pour
  tout $b$ dans $x_0$ on ait $\vec z:\vec x\vdash v:b$ et tel que $\vec z:\vec
  x\vdash u:x_0\fleche a$~;
\item $\vec z:\vec x\vdash t:x_0\fleche a$ si $\vec z:\vec x, z:x_0\vdash
  u:a$.
\end{itemize}

En fait cette façon de représenter le modèle de Engeler comme système de
typage existe sous le nom de \emph{types avec intersections} ou \emph{système
  $D$} (voir \cite{Krivine90b}).

\begin{theo}[Correction du modèle de Engeler]
  L'interprétation $\Interp t_\ell$ est \emph{dénotationnelle} c'est à dire que
  si $t$ et $t'$ sont deux termes et $\ell$ est une suite de variables
  contenant toutes les variables libres de $t$ et $t'$ alors
  \begin{displaymath}
    \text{si }t\Beq t'\text{ alors }\Interp t_\ell = \Interp {t'}_\ell
  \end{displaymath}
\end{theo}

\begin{proof}
  Il suffit de démontrer le théorème dans le cas où $t\Bun t'$. On raisonne par
  récurrence sur $t$. On suppose que $\ell=(z_1,\dots,z_n)$ contient toutes les
  variables libres de $t$. Les cas $t=z_i$, $t=\App uv$ et $t'=\App {u'}v$,
  $t=\App uv$ et $t'=\App u{v'}$, $t=\Abs zu$ et $t'=\Abs z{u'}$ sont immédiats
  par hypothèse de récurrence. Ce qui nous amène au seul cas intéressant~:
  $t=\App{\Abs zu}v$ et $t'=\Subst u{v/z}$. Il résulte du lemme suivant
  \begin{lemme}[Substitution]
    Pour tous termes $u$ et $v$ et toute suite $\ell=(z_1,\dots,z_n)$ contenant
    toutes les variables libres de $t$ et $u$ distinctes de $z$ on a
    \begin{displaymath}
      \Interp{\Subst u{v/z}}_\ell(\vec x) = \Interp u_{\ell.z}(\vec x,\Interp
      v_\ell(\vec x))
    \end{displaymath}
  \end{lemme}
  Supposons le lemme de substitution démontré.  On a
  \begin{alignat*}{2}
    \Interp t_\ell(\vec x) &= \Fun_n\Trace_n\Interp u_{\ell.z}(\vec x,
    \Interp v_\ell(\vec x)) &\quad&\text{par définition de l'interprétation}\\
    &= \Interp u_{\ell.z}(\vec x, \Interp v_\ell(\vec x)) &&\text{par le
      lemme~\ref{lemme:trace-fun}}\\
    &= \Interp{\Subst u{v/z}}_\ell(\vec x)&&\text{par le lemme de
    substitution}\\
    &= \Interp {t'}_\ell(\vec x)
  \end{alignat*}
  
  On démontre le lemme de substitution par\dots\ récurrence sur $u$. Si $u=z_i$
  alors $\Subst u{v/z}=u$ et le résultat est immédiat. Si $u=z$ alors $\Subst
  u{v/z}=v$~; par définition $\Interp u_{\ell.z}(\vec x,x)=x$ d'où l'on déduit
  le résultat en prenant $x=\Interp v_\ell(\vec x)$.
  
  Si $u=\App{u_1}{u_2}$ alors $\Subst u{v/z} = \App{\Subst{u_1}{v/z}}
  {\Subst{u_2}{v/z}}$ et l'on a
  \begin{alignat*}{2}
    \Interp{\Subst u{v/z}}_\ell(\vec x) &= 
      \Fun_n\Interp{\Subst{u_1}{v/z}}_\ell(\vec
      x,\Interp{\Subst{u_2}{v/z}}_\ell(\vec x)) &\quad&
      \text{par définition de l'interprétation}\\
      &= \Fun(\Interp{\Subst{u_1}{v/z}}_\ell(\vec
      x))(\Interp{\Subst{u_2}{v/z}}_\ell(\vec x))&&\text{par définition de
        $\Fun_n$}\\
      &=\Fun(\Interp{u_1}_{\ell.z}(\vec x,\Interp v_\ell(\vec x)))(\Interp
      {u_2}_{\ell.z}(\vec x,\Interp v_\ell(\vec x)))&&\text{par récurrence sur
        $u_1$ et $u_2$}\\
      &=\Fun_{n+1}\Interp{u_1}_{\ell.z}(\vec x,\Interp v_\ell(\vec x),\Interp
      {u_2}_{\ell.z}(\vec x,\Interp v_\ell(\vec x)))&&\text{par définition de
      $\Fun_{n+1}$}\\
      &=\Interp u_{\ell.z}(\vec x,\Interp v_\ell(\vec x))&&\text{par définition
      de l'interprétation}
  \end{alignat*}
  
  Si $u=\Abs z{u_0}$ alors $\Subst u{v/z}=u$ et le résultat est immédiat. Si
  $u=\Abs{z_{n+1}}{u_0}$ où $z_{n+1}\neq z$ et $z_{n+1}$ n'apparaît pas dans
  $v$ (ce que l'on peut toujours supposer à $\alpha$-conversion près) alors
  $\Subst u{v/z}=\Abs{z_{n+1}}{\Subst{u_0}{v/z}}$ et le résultat vient par un
  raisonnement analogue au cas de l'application.
\end{proof}

\subsection{Une application du modèle de Engeler}

On va maintenant utiliser le résultat précédent pour démontrer le théorème de
réduction de tête~\ref{th:norm-tete}. Pour ce faire on va associer à chaque
élément $a$ de $\E(\A)$ un ensemble $\Real a$ de lambda-termes inclus dans
l'ensemble des lambda-termes dont la réduction de tête termine. Puis on
démontrera le \emph{lemme d'appartenance} qui stipule que si $a\in\Interp
t_\ell$ alors $t\in\Real a$. On conclut en montrant que si $t$ est en forme
normale de tête alors $\Interp t_\ell$ est non vide. Donc si $t\Beq t_0$ et
$t_0$ est en forme normale de tête alors par le théorème de correction du
modèle de Engeler on a que $\Interp t_\ell$ est non vide donc par le lemme
d'appartenance que sa réduction de tête termine.


\paragraph{Réalisabilité.} Soit $X$ et $Y$ deux ensembles de lambda-termes. On
note $X\fleche Y$ l'ensemble
\begin{displaymath}
  X\fleche Y=\{u\text{ tel que }\forall v\in X,\,\App uv\in Y\}
\end{displaymath}
Remarquons que dans le cas particulier où $X$ est vide, alors $X\fleche
Y=\Lambda$, l'ensemble de tous les lambda-termes (à $\alpha$-conversion près).


\paragraph{Saturation.}
On dit qu'une partie $X$ de $\Lambda$ est \emph{saturée} si pour tous $u$,
$v$, $v_1$, \dots, $v_n$ on a
\begin{displaymath}
  \text{si }\App{\Subst u{v/z}}{\vec v}\in X\text{ alors }\App{\Abs zu}{v\vec
  v}\in X
\end{displaymath}

\begin{lemme}\label{lemme:Saturation}
  Soient $X$ et $Y$ deux parties de $\Lambda$. Si $Y$ est saturée alors
  $X\fleche Y$ est saturée. Si de plus $X$ est saturée alors $X\cap Y$ est
  saturée.
\end{lemme}
\begin{proof}
  Supposons que $\App{\Subst u{v/z}}{\vec v}$ est un élément de $X\fleche Y$ et
  soit $w\in X$. Par définition de $X\fleche Y$ on a $\App{\Subst u{v/z}}{\vec
    vw} \in Y$ et comme $Y$ est saturée, $\App{\Abs zu}{v\vec vw}\in Y$. Comme
  $w$ est quelconque on vient de montrer que $\App{\Abs zu}{v\vec v}$
  appartient à $X\fleche Y$.

  Le cas de l'intersection est immédiat.
\end{proof}


\paragraph{Termes normalisables de têtes.}
On note $\N$ l'ensemble des termes dont la réduction de tête termine et $\N_0$
l'ensemble des termes de la forme $\App z{\vec v}$ où $z$ est une variable et
$v_1$, \dots, $v_n$ des termes quelconques. En particulier $\N_0$ contient
toutes les variables.

\begin{lemme}\label{lemme:couple-adapte}
  Soient $X$ et $Y$  deux parties de $\Lambda$. 
  \begin{itemize}
  \item si $\N_0\subset Y$ alors $\N_0\subset X\fleche Y$~;
  \item si $\N_0\subset X$ et $Y\subset\N$ alors $X\fleche Y\subset\N$~:
  \item si $X$ et $Y$ contiennent $\N_0$ et/ou sont contenues dans $\N$ alors
    il en de même de $X\cap Y$.
  \end{itemize}
\end{lemme}
En particulier, et c'est sous cette forme que l'on utilisera le lemme, si $X$
et $Y$ contiennent tous deux $\N_0$ et sont tous deux contenus dans $\N$ alors
il en de même de $X\cap Y$ et $X\fleche Y$.
\begin{proof}
  Le cas de l'intersection est immédiat. Supposons que $\N_0\subset Y$ et soit
  $u=\App z{\vec v}$ une élément de $\N_0$ et $v$ un élément de $X$. Alors
  $\App uv=\App z{\vec vv}\in\N_0$ dont $\App uv\in Y$. Comme $v$ est un
  élément quelconque de $X$ on vient de montrer que $u\in X\fleche Y$, donc que
  $\N_0\subset X\fleche Y$.
  
  Supposons maintenant que $\N_0\subset X$ et $Y\subset\N$ et soit $u\in
  X\fleche Y$. Prenons un $v$ dans $X$~; alors $\App uv\in Y$ et comme
  $Y\subset\N$ la réduction de tête de $\App uv$ termine. Par le
  lemme~\ref{lemme:norm-tete} on a que la réduction de tête de $u$ termine,
  c'est à dire que $u\in\N$.
\end{proof}

\paragraph{Interprétation par réalisabilité.}
On va maintenant associer à chaque point de $\D(\A)$ une partie saturée
contenant $\N_0$ et contenue dans $\N$. L'intuition est que les points de
$\D(\A)$ sont des \emph{types} (un point de la forme $(x_0,a)$ représente le
type $x_0\fleche a$), c'est à dire des spécifications formelles de programmes,
et que l'on associe à un point l'ensemble des termes qui \emph{réalisent} ce
type, c'est à dire qui respectent la spécification.

On appelle \emph{valuation} une fonction $\rho:\A\fleche\Power\Lambda$ qui
associe à tout atome $\alpha$ un ensemble $\rho(\alpha)$ saturé, contenant
$\N_0$ et contenu dans $\N$. Étant donnée une valuation $\rho$, on définit
l'ensemble $\Real a_\rho$ des \emph{réalisateurs} d'un élément $a$ de $\D(\A)$
par récurrence sur $a$ (ou plus précisément par récurrence sur le plus petit
$n$ tel que $a\in D_n$)~:
\begin{itemize}
\item si $a\in\A$ alors $\Real a_\rho=\rho(a)$~;
\item si $a=(x_0,b)$ alors 
  \begin{displaymath}
    \Real a_\rho=\Real{x_0}_\rho\fleche\Real b_\rho
  \end{displaymath}
  où $\Real{x_0}_\rho$ est $\bigcap_{c\in x_0}\Real c_\rho$. En particulier si
  $x_0$ est vide alors $\Real{x_0}_\rho$ est $\Lambda$.
\end{itemize}

Grâce aux lemmes~\ref{lemme:Saturation} et \ref{lemme:couple-adapte} on a bien
que pour tout $a\in\D(\A)$ et toute valuation $\rho$, $\Real a_\rho$ est une
partie de $\Lambda$ saturée contenant $\N_0$ et contenue dans $\N$.


\paragraph{Le lemme d'appartenance.}
C'est le lemme fondamental de toute interprétation par réalisabilité. On le
retrouve dans la preuve de forte normalisation du système $F$ mais aussi dans
d'autres contexte comme la définition du collapse extensionnel d'un modèle
dénotationnel\dots

\begin{lemme}[Appartenance]
  Soient $t$ un terme dont toutes les variables libres appartiennent à la liste
  $\ell=(z_1,\dots,z_n)$, $x_1$, \dots, $x_n$ des éléments de $\E(\A)$ (des
  parties de $\D(\A)$) et $\rho$ une valuation. Alors pour tout $a\in\D(\A)$ et
  tous termes $u_1$, \dots, $u_n$ on a
  \begin{displaymath}
    \text{si }
    \begin{cases}
      a\in\Interp t_\ell(\vec x)\text{ et}\\
      u_i\in\Real{x_i}_\rho\text{ pour $i=1,\dots,n$}
    \end{cases}
    \text{ alors } \Subst t{\vec u/\vec z}\in\Real a_\rho
  \end{displaymath}
  où $\Real{x_i}_\rho$ est $\bigcap_{b\in x_i}\Real b_\rho$.
\end{lemme}

\begin{proof}
  Le lemme d'appartenance se démontre par récurrence sur $t$. Si $t=z_i$ alors
  $\Interp t_\ell(\vec x) = x_i$, donc $a\in x_i$ et
  $\Real{x_i}_\rho\subset\Real a_\rho$. Comme $u_i\in\Real{x_i}_\rho$ on a
  $u_i\in\Real a_\rho$. Mais $u_i=\Subst t{\vec u/\vec z}$ puisque $t=z_i$.
  
  Si $t=\App uv$ alors $\Interp t_\ell(\vec x) =\Fun_n\Interp u_\ell(\vec
  x,\Interp v_\ell(\vec x))$, et $a\in\Interp t_\ell(\vec x)$ entraîne qu'il
  existe un $x_0\subsetFin\Interp v_\ell(\vec x)$ tel que $(x_0,a)\in\Interp
  u_\ell(\vec x)$. Par hypothèse de récurrence on a donc $\Subst u{\vec u/\vec
    z}\in\Real{(x_0,a)}_\rho=\Real{x_0}_\rho\fleche\Real a_\rho$. Mais, comme
  $x_0\subset \Interp v_\ell(\vec x)$, par récurrence sur $v$ on a $\Subst
  v{\vec u/\vec z}\in\Real{x_0}_\rho=\bigcap_{b\in x_0}\Real b_\rho$. Par
  définition de $\fleche$ on a donc que $\App{\Subst u{\vec u/\vec z}}{\Subst
    v{\vec u/\vec z}}=\Subst t{\vec u/\vec z}\in\Real a_\rho$.

  Si $t=\Abs zv$ alors $\Interp t_\ell(\vec x)=\Trace_n\Interp v_{\ell.z}(\vec
  x)$ et $a\in\Interp t_\ell(\vec x)$ entraîne que $a$ est de la forme
  $(x_0,b)$ où $b\in\Interp v_{\ell.z}(\vec x, x_0)$. Par hypothèse de
  récurrence, pour tout $u\in\Real{x_0}_\rho$ on a $\Subst v{\vec u/\vec
  z,u/z}\in\Real b_\rho$~; mais par saturation de $\Real b_\rho$ ceci entraîne
  que $\App{\Abs z{\Subst v{\vec u/\vec z}}}u\in\Real b_\rho$ pour tout
  $u\in\Real{x_0}_\rho$. Donc $\Abs z{\Subst v{\vec u/\vec
  z}}=\Subst t{\vec u/\vec z}\in\Real{x_0}_\rho\fleche \Real b_\rho=\Real
  a_\rho$.
\end{proof}

\begin{coro}
  Soient $x_1$, \dots, $x_n$ dans $\E(\A)$. Si $\Interp t_\ell(\vec x)$ est non
  vide alors la réduction de tête de $t$ termine.
\end{coro}
\begin{proof}
  Comme $\N_0$ contient toutes les variables et est contenu dans tous les
  $\Real{x_i}_\rho$, on a $z_i\in\Real {x_i}_\rho$ pour $i=1,\dots,n$, donc par
  le lemme d'appartenance $\Subst t{\vec z/\vec z}=t\in\Real a_\rho$. Mais
  $\Real a_\rho\subset\N$, donc par définition de $\N$ la réduction de tête de
  $t$ termine.
\end{proof}

On termine la preuve du théorème~\ref{th:norm-tete} en montrant le lemme
suivant~:
\begin{lemme}
  Si $t$ est beta-équivalent à une forme nomale de tête $t_0$ alors pour toute
  liste $\ell=(z_1,\dots,z_n)$ contenant les variables libres de $t$ et de
  $t_0$, il existe $x_1$, \dots, $x_n$ dans $\E(\A)$ tels que $\Interp
  t_\ell(\vec x)$ est non vide.
\end{lemme}
Le théorème se déduit alors du corollaire au lemme d'appartenance.

\begin{proof}
  En vertu du théorème de correction du modèle de Engeler, l'interprétation de
  $t$ est égale à celle de la forme normale de tête $t_0$. Donc il suffit de
  montrer le lemme dans le cas où $t$ est en forme normale de tête.

  Soit $a\in\D(\A)$. On définit $a^m$ par récurrence sur $m$~: $a^0=a$ et
  $a^{m+1}=(\emptyset, a^m)$. Autrement dit, en utilisant l'analogie avec les
  types~:
  \begin{displaymath}
    a^m=\underbrace{\emptyset\fleche\dots\fleche\emptyset}_{m\ \times}\fleche a
  \end{displaymath}

  Si $t$ est en forme normale de tête alors on a soit $t=\App{z_i}u_1\dots
  u_m$, soit $t=\Abs zu$ où $u$ est en forme normale de tête. Dans le premier
  cas, par définition de l'interprétation on a~:
  \begin{displaymath}
    \Interp t_\ell(\vec x)=\{a,\,\exists y_1\subsetFin\Interp{u_1}(\vec x),
    \dots, \exists y_m\subsetFin\Interp{u_m}(\vec x),\,
    (y_m,\dots,(y_1,a)\dots)\in x_i\}
  \end{displaymath}
  Si on choisit $x_i$ tel que $a^m\in x_i$, comme $y_j=\emptyset \subsetFin
  \Interp{u_j}(\vec x)$ pour tout $\vec x$ et tout $j$ on a $a\in\Interp
  t_\ell(\vec x)$ et donc $\Interp t_\ell(\vec x)$ est non vide.
  
  Si maintenant $t=\Abs zu$ alors 
  \begin{displaymath}
    \Interp t_\ell(\vec x)=\{(x_0,a) \in\PowerFin{\D(\A)}\times\D(\A),\,
    a\in\Interp u_{\ell.z}(\vec x, x_0)\}
  \end{displaymath}
  Par récurrence sur $u$ il existe $\vec x$ et $x_0$ tel que $\Interp
  u_{\ell.z}(\vec x,x_0)$ est non vide d'où l'on déduit immédiatement que
  $\Interp t_\ell(\vec x)$ est non vide.  
\end{proof}

\bibliographystyle{plain}
\bibliography{biblio}
\end{document}

% The initial user name and password are 'admin' and 'lxYvi8sr'.

