%% /home/plescann/MIM-1/LOGIQUE/LAMBDA/transp.tex

%% Time-stamp: <version du Sat  4 Nov 2000 à 10h44 par Pierre Lescanne>

% \documentclass[%
%   slidesonly,%  Pour sortir les transparents seuls
%   semrot,%      Permettre des rotations eventuelles
%   semhelv,%    Helvetica
%   a4%           A4 paper
%   ]{seminar}
\documentclass{article}
\usepackage{fullpage}
\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}
\usepackage{amssymb, amsmath, amsfonts}

%% Time-stamping  
%% compute the time in hours and minutes; 
%  \newcount\timehh\newcount\timemm \timehh=\time 
%  \divide\timehh by 60 \timemm=\time
%  \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
%  \newcommand{\timestamp}
%  { {\protect\small\sl\today\ -- 
%  \ifnum\timehh<10 0\fi\number\timehh\,h\,
%    \ifnum\timemm<10 0\fi\number\timemm}}
%                                           % avec dvips

% \def\printlandscape{\special{landscape}}    % pour sortir en landscape
%                                             % avec dvips

% \slidesmag{5}
% \articlemag{1}

% \rotateheaderstrue       % si tu combines slide et slide*


\title{{\textit{Introduction au lambda-calcul}}}

\author{}

\date{}

 

\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\rougeMa}[1]{\textcolor{red}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\eqa}{\mathop{\equiv_\alpha}}
\newcommand{\Y}{\mathsf{Y}}


\newcommand{\inferTwoLabel}[4]{
{#1} \quad 
 \bl{\begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{
 {#1} \quad
  \bl{\begin{array}{c}
  #2
  \end{array}}}

\newcommand{\inferLabel}[3]{
    {#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}

 \newcommand{\inferTwo}[3]{\bl{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}}

 \newcommand{\infer}[2]{\bl{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<<->>}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\raraR}{\rarasub{R}}

%%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
  \begin{center}                % mais ca peut t'interesser
    \large\bf
    \color{cyan}{\shadowbox{#1}}%
  \end{center}
  \markright{#1}
  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}


\maketitle

  \section{Les fonctions comme citoyens de première classe}
  \vspace*{20pt}
  
  On peut faire que les \rouge{preuves} soient \VERT{citoyens de
    première classe}, mais pourquoi pas les \rouge{fonctions}?

\section{Quelques dates}
\begin{description}
\item[autour de 1870] un Italien\footnote{dont j'ai oublié le nom.}
  s'oppose à Cantor sur le point de savoir quel est le concept de base
  des mathématiques prétendant que ça devrait être les fonctions.
\item[1920] \emph{Schönfinkel} initie la logique combinatoire,
\item[1925] \emph{Haskell Curry }crée la logique combinatoire,
\item[1936] \emph{Alonso Church} crée le $\lambda$-calcul,
\item[1970-...] Explosion du $\lambda$-calcul dûe à l'informatique
  (de Bruijn, Barendregt, Berry, Boehm, Girard, Klop, Krivine, Levy, Plotkin,
  Scott, mais aussi Curien, Statmann etc.)
\end{description}


\section{Des notations différentes, un même concept}

\begin{center}
\begin{math}
\begin{array}{lc|c}
\VERT{\textrm{en maths}} & x \mapsto x & f \mapsto (x \mapsto f(f(x)))\\
\VERT{\textrm{en CAML}} & \texttt{fun x -> x} &  \texttt{fun f -> (fun x ->
  (f (f x)))} \\
\VERT{\textrm{en } \lambda\textrm{-calcul}} & \lambda x.x & \lambda
f.(\lambda x.(f (f x)))
\end{array}
\end{math}
\end{center}

\section{La syntaxe}

La classe \bleu{\Lambda} est la plus petite classe qui contient 
\begin{enumerate}
\item \bleu{x} si \bleu{x} est une variable,
\item \bleu{\lambda x .M} si \bleu{M\in\Lambda},
\item \bleu{(M N)} si \bleu{M\in\Lambda} et  \bleu{N\in\Lambda}.
\end{enumerate}

\section{Qu'y a-t-il derrière la syntaxe?}

\subsection{Signification des termes}
On peut voir les termes comme des abstractions des fonctions ou des
programmes fonctionnels.

Dans \bleu{\lambda x .M}, on dit que \bleu{M} est le \rouge{corps} de la
fonction ou du programme.

Dans \bleu{(M N)}, on peut voir \bleu{M} comme une fonction que l'on
\rouge{applique} au paramètre \bleu{N}.  La \rouge{valeur} va s'obtenir par
«réduction» (approche intentionnelle).

Le lambda-calcul décrit les fonctions par leur \rouge{comportement}.

\subsection{L'anecdote derrière la syntaxe}

Au début Church voulait écrire \texttt{\^x}. 

Mais au temps des machines à
écrire on ne savait écrire que \texttt{\^{}x}.

Ce qui a donné ${ \Lambda}$\texttt{x}, puis $\lambda$\texttt{x}.


\section{Variables et substitutions}

  \subsection{Les variables liées}
  \begin{eqnarray*}
 BV(\bl{x}) & = & \emptyset\\
BV(\bl{\lambda x .M}) & = & BV(\bl{M}) \cup \{\bl{x}\}\\
BV(\bl{M N})& = & BV(\bl{M}) \cup BV(\bl{N})
  \end{eqnarray*}

\subsection{Exemples}
  \begin{eqnarray*}
BV(\bl{\lambda x .x}) & = & \{\bl{x}\}\\
BV(\bl{\lambda f.(\lambda x.(f (f x)))})& = & \{\bl{f},\bl{x}\}\\
BV(\bl{\lambda f.(\lambda x.(f (f x y) y))})& = & \{\bl{f},\bl{x}\}
  \end{eqnarray*}


  \subsection{Les variables libres}
  \begin{eqnarray*}
 FV(\bl{x}) & = & \{\bl{x}\}\\
FV(\bl{\lambda x .M}) & = & FV(\bl{M}) - \{\bl{x}\}\\
FV(\bl{M N})& = & FV(\bl{M}) \cup FV(\bl{N})
  \end{eqnarray*}
  
\subsection{Exemples}
  \begin{eqnarray*}
FV(\bl{\lambda x .x}) & = & \emptyset\\
FV(\bl{\lambda f.(\lambda x.(f (f x)))})& = & \emptyset\\
FV(\bl{\lambda f.(\lambda x.(f (f x y) y))})& = & \{\bl{y}\}\\
FV(\bl{\lambda x.(f (f x))})& = & \{\bl{f}\}
  \end{eqnarray*}

  \subsection{Les variables libres (suite)} Un terme qui n'a pas de
  variable libre est dit \rouge{clos} ou \rouge{fermé} ou est appelé un
  \rouge{combinateur}.

  \subsection{Les variables libres (suite)} Un terme qui n'a pas de
  variable libre est dit \rouge{clos} ou \rouge{fermé} ou est appelé un
  \rouge{combinateur}.
\vskip 3 mm
{\large ATTENTION !}
Une variable peut être \rouge{à la fois libre et liée} dans un terme.

Par exemple :  \bleu{x (\lambda x. x)}.

\section{Convention}
  \begin{enumerate}
  \item Au lieu de \bleu{\lambda x_1(...(\lambda x_n. M)...)}, on écrit \bleu{\lambda x_1...x_n. M}.

Par exemple: \bleu{\lambda f x . f(f x)}.

\item Au lieu de \bleu{(...(M N_1)...N_p)}, on écrit \bleu{M
    N_1...N_p} ou \bleu{M\vec{N}}, si \bleu{\vec{N} = (N_1...N_p)}.

Par exemple: \bleu{\lambda x y g .  g x y}.
  \end{enumerate}
\bleu{((\lambda x . x) y) y)} donne \bleu{(\lambda x . x) y y}

\section{Le produit cartésien et la curryfication} 
%============== La curryfication ===============

\noindent Il n'y a pas de produit cartésien dans le $\lambda$-calcul simple.  

\noindent Si on veut écrire:
\bl{\[\lambda (x, y) . f(x, y)\]}
on le remplace par
\bl{\[\lambda x y . f x y\]}
C'est la \rouge{curryfication} (nommée après Haskell Curry).

\section{Substitution} 
  
\subsection{Substitution}
  Substituer une variable par un terme ne consiste pas simplement à
  remplacer toutes les occurrences de la variable par ce terme, à
  cause du \rouge{phénomène de capture}.

\vskip 2 mm

Quand on écrit \bleu{M[x:=P]} on ne remplace pas simplement les
occurrences de \bleu{x} dans \bleu{M} par \bleu{P}.

 

Ainsi on a :
\bl{ 
  \begin{eqnarray*}
x (\lambda x.x)[x:=y] &\not=& y(\lambda x.y)\\
(\lambda y . x)[x:=y] &\not=& \lambda x . x
\end{eqnarray*}}
donc il faut être prudent.

  \subsection{Substitution avec renommage} 
  \begin{enumerate}
  \item \bleu{x[x:=P] = P}
  \item \bleu{y[x:=P] = y}
  \item \bleu{(\lambda x . M)[x:=P] = \lambda x . M}
  \item \bleu{(\lambda y . M)[x:=P] = \lambda y . (M[x:=P])} \\ 
    \hspace*{20pt} si \bleu{x\notin FV(M)} ou \bleu{y\notin FV(P)}
  \item \bleu{(\lambda y . M)[x:=P] = \lambda {z} .  (M[y:={z}][x:=P])} \\ 
    \hspace*{20pt} si \bleu{x\in FV(M)} et \bleu{y\in FV(P)} \\ 
    \hspace*{20pt} et {$z$} est une \rouge{nouvelle} variable
  \item \bleu{(M_1 M_2)[x:=P] = M_1[x:=P] M_2[x:=P]}
  \end{enumerate}

\subsection{La convention de Barendregt} 
  
  C'est une \rouge{convention sur les variables libres} d'un terme
  \rouge{dans un énoncé mathématique}.
  
\vspace*{20pt}

  \fbox{

    \begin{large}
\begin{minipage}{15cm}
  Il n'existe aucun sous-terme dans lequel une variable apparaît à la
  fois libre et liée.
\end{minipage}
\end{large}
}

\section{L'$\alpha$-conversion} 
\subsection{Définition}
\[\bl{\lambda x . N \eqa \lambda y . (N [x:=y])}\hspace{20pt}{y\notin FV(N)}\]
\[\inferTwo{M_1\eqa N_1}{M_2\eqa N_2}{M_1 M_2 \eqa N_1 N_2}\]
\[\infer{M\eqa N}{\lambda z.M\eqa\lambda z.N}\]
\[\bl{x\eqa x}\]


L'$\alpha$-conversion ne change pas la «signification» des termes.


  \subsection{Substitution et convention de Barendregt} 
{\bf La convention de Barendregt}
\begin{itemize}
\item On suppose que dans tout théorème que l'on énonce, on suit la
  convention de Barendregt.
\item Si l'on a un terme qui ne satisfait pas la convention de
  Barendregt, on s'y ramène par $\alpha$-conversion
\end{itemize}
\vskip 2 mm

Avec la convention de Barendregt, la définition des substitutions devient 
beaucoup plus simple:
\begin{itemize}
\item \bleu{x[x:=P] = P}
\item \bleu{y[x:=P] = y}
\item \bleu{(\lambda y. M)[x:=P] = \lambda y.M[x:=P]}
\item \bleu{(M_1 M_2)[x:=P]= M_1[x:=P] M_2[x:=P]}
\end{itemize}


\section{La $\beta$-réduction et les autres 
          réductions}

\subsection{La règle $\beta$} 
Les fonctions sont faites pour calculer !

Les réductions d'un terme représentent son calcul.

La \rouge{$\beta$-réduction} est l'étape élémentaire.

\[\bl{(\lambda x . M) P \rabeta M[x:=P]}\]

\subsection{R-réduction} 
On se donne un ensemble \bleu{R} de règles, c-à-d de paires de termes, 
par exemple \bleu{\beta}.

\bleu{M\raR N} signifie que \bleu{M} se réduit à \bleu{N} par \bleu{R} 
en une étape.

\begin{scriptsize}
\[\inferLabel{\mbox{(règle)}}{(M,N)\in R}{M\raR N}
~~~~~ \inferLabel{(\xi)}{M\raR N}{\lambda x M \raR \lambda x N}\]
\[\inferLabel{\mbox{(congruence gauche)}}{M\raR N}{M P \raR N P}
~~~~~
\inferLabel{\mbox{(congruence droite)}}{M\raR N}{P M \raR P N}\]

\end{scriptsize}

  \subsection{Exercice} 
Réduire :
\begin{itemize}
\item \bleu{\lambda y. (\lambda x.x)z}
\item \bleu{(\lambda f x. f(f x))(\lambda x.x)}
\item \bleu{(\lambda f x. f(f x))(\lambda f x. f x)}
\end{itemize}

\subsection{D'autres exemples de reductions} 
\rouge{La réduction $\eta$}: Pour tout \bleu{M\in\Lambda} et \bleu{x\not\in
  FV(M)}, 
\bl{\begin{eqnarray*}
\lambda x.M x & \rasub{\eta} & M.
\end{eqnarray*}}
\vskip 3 mm
\rouge{L'expansion $\eta$} : Pour tout \bleu{M\in\Lambda} et \bleu{x\not\in
  FV(M)}, \bl{\begin{eqnarray*}
M & \rasub{\eta_{exp}}& \lambda x.M x.
\end{eqnarray*}}

\rouge{La réduction par $\beta$ et $\eta$}

\begin{center}
  \bleu{\rasub{\beta\eta} = \rabeta \cup \rasub{\eta}}.
\end{center}

\subsection{Fermeture transitive et réflexive} 
\begin{scriptsize}
\[\inferLabel{\mbox{(cas de base)}}{M\raR N}{M\raraR N}
~~~~~
\leafLabel{\mbox{(réflexivité)}}{M\raraR M}\]
\[\inferTwoLabel{\mbox{(transitivité)}}{M\raraR N}{N\raraR L}{M\raraR L}\]
\end{scriptsize}
\newline

\rouge{Proposition} \fbox{\VERT{Congruence de \bleu{\rarabeta}}}

\begin{scriptsize}
\[\infer{M\rarabeta N}{\lambda x. M\rarabeta\lambda x.N} \]
\[\inferTwo{M\rarabeta N}{P\rarabeta Q}{M P\rarabeta N Q}\]
\end{scriptsize}
\vskip 3 mm
{\bf Démonstration} 
On fait une récurrence sur la longueur de l'arbre de preuve et on
choisit de montrer la première inférence. Trois cas se présentent:
\begin{enumerate}
\item \bleu{M\rabeta N}, on a utilisé le «cas de base», alors par
  $(\xi)$, \bleu{\lambda x. M\rabeta\lambda x.N} et on conclut par le
  «cas de base». 
\item \bleu{M\equiv N}, alors \bleu{\lambda x. M\equiv\lambda x.N} et
  conclut par «réflexivité».
  
\item Il existe \bleu{P} tel que \bleu{M\rarabeta P} et
  \bleu{P\rarabeta N}.  Par induction, on tire,
  \begin{itemize}
  \item \bleu{\lambda x. M\rarabeta\lambda x.P} 
  \item et \bleu{\lambda x. P\rarabeta\lambda x.N},
  \end{itemize}
et par «transitivité» \bleu{\lambda x. M\rarabeta\lambda x.N}.
\end{enumerate}

\subsection{Fermeture transitive, réflexive et symétrique} 
Avec les règles
\begin{scriptsize}
\[\inferLabel{\mbox{(cas de base)}}{M\raR N}{M\conv{R} N}
~~~~~
\leafLabel{\mbox{(réflexivité)}}{M\conv{R} M}\]
\[\inferTwoLabel{\mbox{(transitivité)}}{M\conv{R} N}{N\conv{R}
  L}{M\conv{R} L}
~~~~~
\inferLabel{\mbox{(symétrie)}}{M\conv{R} N}{N\conv{R} M}\]
\end{scriptsize}
\noindent on obtient la fermeture transitive, réflexive et symétrique
de~\bleu{\raR}. 

\begin{itemize}
\item Elle s'écrit \bleu{=_R} ou \bleu{\conv{R}},
\item Elle se dit \rouge{\bleu{R}-égal} ou \rouge{\bleu{R}-convertible} ou
  \rouge{\bleu{R}-équivalent} .
\end{itemize}

  \section{L'égalité extensionnelle} 

\subsection{Définition}

\bleu{\conv{\beta}} décrit l'égalité \VERT{intentionnelle}, si
\bleu{M\conv{\beta}N} et si \bleu{M} et \bleu{N} ont le même
«comportement» (c'est à dire même comportement pour la $\beta$-réduction.

Deux termes sont \rouge{ extensionnellement équivalent} s'ils prennent
le mêmes «valeurs» quand on les appliquent au même terme.


\subsection{Règle}
On a aussi la règle
\[\inferLabel{\mbox{(ext)}}{M x = N x}{M = N} ~~~~~~~~~~~~ x\not\in FV(M N)\]

Par les règles \bl{\textsf{cas de base pour $\beta$}} +
\bl{\textsf{réflexivité}} + \bl{\textsf{transitivité}} +
\bl{\textsf{symétrie}} + \bl{\textsf{ext}} on définit une relation
\bleu{\conv{\textsf{ext}}}.

\vskip 3 mm
Et on récupère la proposition :
\rouge{Proposition} \fbox{\bleu{\conv{ext}} est équivalent 
    à \bleu{\conv{\beta\eta}}.}

\vskip 3 mm

{\bf Démonstration}\\

\begin{itemize}
\item
\rouge{Pour montrer que \bleu{\conv{\beta\eta} \subseteq
    \conv{\textsf{ext}}}} 
\VERT{il suffit de montrer que si
\bleu{P\rasub{\eta}Q} alors \bleu{P \conv{\textsf{ext}}Q}}\\
donc il suffit de montrer que pour \bleu{x\not\in FV(M)}
\bleu{(\lambda x.  M x) \conv{\textsf{ext}} M}

En fait, il suffit de montrer qu'on a \bleu{(\lambda x. M x) x
  \conv{\beta} M x}.

Par le \emph{cas de base} et la définition de \bleu{\rabeta}, cela
vient de \bleu{(\lambda x. M x) x
  \rabeta (M x)[x:=x]\equiv M x}.
\item
\rouge{Pour montrer que \bleu{\conv{\textsf{ext}} \subseteq
  \conv{\beta\eta}},}, \VERT{il suffit de montrer que
\bl{\textsf{ext}} est une règle dérivée dans \bleu{\conv{\beta\eta}}.}


Supposons \bleu{M x \conv{\beta\eta} N x} avec \bleu{x\not\in FV(M N)},
alors   \bleu{\lambda x. M x \conv{\beta\eta} \lambda x. N x} par $\xi$,
donc par $\eta$ appliquée deux fois, on a :\\


\bleu{M \xymatrix{&\ar@{>}[l]^{\eta}}\lambda x. M x \conv{\beta\eta}
  \lambda x. N x \rasub{\eta} N}, soit \bleu{M \conv{\beta\eta}N}.
\end{itemize}

\section{Contexte} 
Un contexte \bleu{C[\ ]} est défini ainsi
\begin{enumerate}
\item \bleu{[~]} est un contexte,
\item si \bleu{M\in \Lambda} et si \bleu{C[~]} est un contexte alors
  \bleu{M C[~]} et \bleu{C[~] M} sont des contextes,
\item si \bleu{C[~]} est un contexte alors \bleu{\lambda x.C[~]} est
  un contexte.
\end{enumerate}

  \subsection{Définition} {Si \bleu{C[~]} est un contexte et
    \bleu{A\in\Lambda} alors \bleu{C[A]} est défini par induction sur
    \bleu{C[~]}} :

\begin{itemize}
\item \bleu{[A] = A},
\item si \bleu{C[~]= \lambda D[~]} alors \bleu{C[A]= \lambda D[A]},
\item  si \bleu{C[~]= M D[~]} alors \bleu{C[A]= M D[A]},
\item etc.
\end{itemize}

\subsection{Stabilité par contexte} 
\rouge{Proposition}
\bleu{\raR}, \bleu{\raraR} et \bleu{\conv{R}} sont stables par
contexte ou compatibles.

\fbox{\bleu{\raR} est stable par contexte.}
\vskip 3 mm
{\bf Démonstration :}\\

On montre que si\bleu{M\raR N} alors  \bleu{C[M]\raR C[N]}, par
induction sur la structure de \bleu{C[~]}, sachant que \bleu{M\raR N}.

\begin{enumerate}
\item \bleu{C[~]=[~]} alors \bleu{C[M] = M} et \bleu{C[N] = N},
  évident.
\item \bleu{C[~]=A D[~]}, 
  \begin{itemize}
  \item par induction \bleu{D[M] \raR D[N]},
  \item d'autre part, \bleu{C[M]=A D[M]} et \bleu{C[N]=A D[N]},
  \item donc par congruence à droite  \bleu{C[M]\raR C[N]}.
\end{itemize}
\item \bleu{C[~]=D[~] A},  comme 2 en changeant «droite» en «gauche».
\item \bleu{C[~]=\lambda x. D[~] A}, par induction \bleu{D[M] \raR
    D[N]}, d'où la conclusion par ($\xi$).
\end{enumerate}

\subsection{Stabilité par substitution} 

\rouge{Proposition}
\fbox{\bleu{M\raraR N} implique \bleu{A[x:=M]\raraR A[x:=N]}.}
\vskip 5 mm
{\bf Démonstration :}
\vskip 1 mm
L'hypothèse est \bleu{M\raraR N}. La démonstration se fait par induction sur
\bleu{A}.
\begin{itemize}
\item \rougeMa{A\equiv x}, alors  \bleu{A[x:=M] \equiv M \raraR N \equiv A[x:=M]}.
\item \rougeMa{A\equiv y}, alors  \bleu{A[x:=M] \equiv y \raraR y \equiv
    A[x:=M]}, par réflexivité.
\end{itemize}

\begin{itemize}
\item \rougeMa{A\equiv \lambda y.B}, \\
par induction \bleu{B[x:=M] \raraR
    B[x:=N]}, \\
donc \bleu{A[x:=M] \equiv \lambda y.B[x:=N]} et
  \bleu{A[x:=N] \equiv \lambda y.B[x:=N]}, \\
par congruence de
  \bleu{\raraR}, on a \bleu{\lambda y.B[x:=M]\raraR  \lambda
    y.B[x:=N]}.
\end{itemize}

\begin{itemize}
\item \rougeMa{A\equiv B B'} \\
par induction \bleu{B[x:=M] \raraR B[x:=N]}
  et \bleu{B'[x:=M] \raraR B'[x:=N]}, \\
par définition de la
  substitution \bleu{A[x:=M] \equiv B[x:=M] B'[x:=M]}\\
 et \bleu{A[x:=N] \equiv B[x:=N] B'[x:=N]}, \\
par congruence de \bleu{\raraR} on a
  \bleu{A[x:=M]\raraR A[x:=N]}.
\end{itemize}
  \subsection{Exercice} 

Montrez que ça ne peut pas marcher pour \bleu{\raR},c'est à dire qu'on n'a
pas :

\bleu{M\raR N} implique \bleu{A[x:=M]\raR A[x:=N]}.

  \subsection{D'autres exemples de termes} 
\bleu{\omega \equiv \lambda x. x x}

\bleu{\Omega \equiv (\lambda x. x x) (\lambda x. x x)}

\bleu{\mathsf{Y} \equiv \lambda f.(\lambda x. f (x x))(\lambda x. f (x
  x))}
$\mathsf{Y}$ est appelé combinateur point fixe de Curry.

\bleu{\mathsf{W}_F \equiv (\lambda x. F (x x))}

\subsection{Exercices} 

\begin{enumerate}
\item Montrez que \bleu{\Omega} se réécrit vers un unique terme. Lequel?
Plus précisément, montrez qu'il existe un terme unique \bleu{M\in
  \Lambda} tel que \bleu{\Omega\rabeta M}.
\item Montrez que \bleu{\Y F \rarabeta F(\mathsf{W}_F \mathsf{W}_F)}.
\item Montrez que \bleu{F(\Y F) \rarabeta F(\mathsf{W}_F
    \mathsf{W}_F)}.
\item Conclure que  \bleu{\Y F \conv{\beta} F(\Y F)}.
\end{enumerate}

  \section{Redex et formes normales} 

\subsection{Définitions}
  \begin{itemize}
  \item Un R-redex est un terme \bleu{M} tel que \bleu{(M, N) \in R}.
  \item \bleu{N} et le R-contracté de \bleu{M}.
  \item Un terme  \bleu{M} est R-irreductible si \bleu{M} ne contient
    aucun  R-redex.
  \item Un terme  \bleu{N} est une forme normale de  \bleu{M}, si
    \bleu{N} est R-irréductible et si \bleu{M\conv{R}N}.
\end{itemize}


  \subsection{Formes normales} 

On n'affirme 
\begin{itemize}
\item ni l'existence (cf \bleu{\Omega}),
\item ni l'unicité, il y a unicité pour \bleu{\beta} et \bleu{\beta
    \cup \eta_{exp}}, mais il faut le prouver. 
\end{itemize}
La forme normale si elle existe est la valeur intentionnelle.

\subsection{Exercice} 

Lesquels de ces termes sont des formes normales ?

\bleu{(\lambda x .x)}

\bleu{((\lambda x y.x)v)w}

\bleu{((\lambda x y.x v))w}

\bleu{(\lambda x y.x)v w}

  \section{Entiers de Church} 
  \subsection{Définition}  
\begin{itemize}
  \item 
    \bleu{(\lambda f x. f(f x))\equiv \textbf{2}} correspond au nombre
    entier \VERT{deux}.
    
  \item 
    \bleu{(\lambda f x .x) \equiv K} correspond à \VERT{zéro}.

  \item     
    \bleu{(\lambda f x .f x)\equiv \textbf{1}} correspond à \VERT{un}.
  \item Plus généralement l'entier \VERT{\textbf{n}} est le
    terme  \bleu{(\lambda f x. (f^n x))}.
\end{itemize}

\subsection{Exercices} 
\begin{enumerate}
\item 
Montrez que  \bleu{\textbf{1}\rasub{\eta} I}.


\item Calculez 
  \begin{itemize}
  \item \bleu{\textbf{1}\textbf{2}}, 
  \item \bleu{\textbf{2}\textbf{1}}, 
  \item \bleu{\textbf{2}\textbf{2}}, 
\end{itemize}

\item A quoi correspond \bleu{\textbf{m}\textbf{n}}~?
\end{enumerate}

\end{document}

% LocalWords:  Cantor Haskell Alonso Church Barendregt Levy Klop Krivine Sch
% LocalWords:  Plotkin nfinkel Redex R-redex