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

%% Time-stamp: <modifié par Pierre Lescanne le 31 Oct 2001 à 09h47>

\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}

%% 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{\color{red}{\textit{Introduction au lambda-calcul}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\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}

%------------------------------------------------------
\begin{slide}
  \maketitle \addtocounter{slide}{-1} \slidepagestyle{empty}


\vfill 

\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}?
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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
  (Barendregt, Berry, Boehm, de Bruijn, Girard, Hindley, Klop,
  Krivine, Levy, Plotkin, Scott, mais aussi Curien, Statmann etc.)
\end{description}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}, \hfill\rouge{abstraction}
\item \bleu{(M N)} si \bleu{M\in\Lambda} et
  \bleu{N\in\Lambda}.\hfill\rouge{application}
\end{enumerate}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Qu'y a-t-il derrière la syntaxe?}

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

\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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é ${\tiny \Lambda}$\texttt{x}, puis $\lambda$\texttt{x}.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples de termes}
\bleu{I \equiv \lambda x. x} 

\bleu{K \equiv \lambda x y. x}

\bleu{S \equiv \lambda x y z. x z (y z)}

\bleu{B\equiv \lambda x y z. x (y z)}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemples de termes}
\bleu{I \equiv \lambda x. x} \hfill \rouge{\bleu{I} est la fonction identité}

\bleu{K \equiv \lambda x y. x} \hfill \rouge{\bleu{K c} est la
  fonction constante \bleu{c}}

\bleu{S \equiv \lambda x y z. x z (y z)} \hfill \rouge{\bleu{S a b c}
  distribue \bleu{c}}

\bleu{B\equiv \lambda x y z. x (y z)} \hfill \rouge{\bleu{B} permute
  l'effet des parenthèses}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{Variables et substitutions}}}
 \end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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*}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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*}

\vspace*{12pt}
  \subheading{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*}
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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*}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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*}
  
\subheading{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*}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}.
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}.
\vspace*{20pt}
\subheading{\Huge ATTENTION !}
Une variable peut être \rouge{à la fois libre et liée} dans un terme.

Par exemple :  \bleu{x (\lambda x. x)}.
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Convention}
  \begin{enumerate}
  \item Au lieu de \bleu{\lambda x_1(...(\lambda x_n. M)...)}\\
\hspace*{30pt}  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)} \\
\hspace*{30pt}  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}
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le produit cartésien et la curryfication} 
%============== La curryfication ===============

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

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).
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}.

\vspace*{20pt}

Quand on écrit \bleu{M[x:=P]} on ne remplace pas simplement les
occurrences de \bleu{x} dans \bleu{M} par \bleu{P}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Substitution} 

Ainsi
\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.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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\not\in FV(M)} ou \bleu{y\not\in FV(P)}
  \item \bleu{(\lambda y . M)[x:=P] = \lambda \VERT{z} .  (M[y:=\VERT{z}][x:=P])} \\ 
    \hspace*{20pt} si \bleu{x\in FV(M)} et \bleu{y\in FV(P)} \\ 
    \hspace*{20pt} et \VERT{$z$} est une \rouge{nouvelle} variable
  \item \bleu{(M_1 M_2)[x:=P] = M_1[x:=P] M_2[x:=P]}
  \end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}{8cm}
  Il n'existe aucun sous-terme dans lequel une variable apparaît à la
  fois libre et liée.
\end{minipage}
\end{Large}
}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'$\alpha$-conversion} 
\[\bl{\lambda x . N \eqa \lambda y . (N [x:=y])}\hspace{20pt}{y\not\in 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}\]
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'$\alpha$-conversion} 
L'$\alpha$-conversion ne change pas la «signification» des termes.
\vfill
\heading{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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Substitution et convention de Barendregt} 
Avec la convention de Barendregt, la définition des substitutions devient 
beaucoup plus simple.
\vspace{20pt}
\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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{red}{\textit{La $\beta$-réduction et les autres 
          réductions}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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]}\]
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{R-réduction} 
\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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice} 
Réduire
\vspace*{20pt}
\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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{D'autres exemples de réductions} 
\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*}}

\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*}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{D'autres exemples de réductions} 
\rouge{La réduction par $\beta$ et $\eta$}

\begin{center}
  \bleu{\rasub{\beta\eta} = \rabeta \cup \rasub{\eta}}.
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}
\end{slide}
%------------------------------------------------------
\begin{slide}
\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}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Proposition} \fbox{\VERT{Congruence de \bleu{\rarabeta}}}

Cas \begin{scriptsize}
$\infer{M\rarabeta N}{\lambda x. M\rarabeta\lambda x.N}$
\end{scriptsize}

On doit montrer que 
\begin{itemize}
\item sous l'\rouge{hypothèse} \bleu{M\rarabeta N} 
\item on a la
  \rouge{conclusion} \bleu{\lambda x. M\rarabeta\lambda x.N}.
\end{itemize}
La démonstration est \rouge{par induction} sur la taille de l'arbre de
preuve de \bleu{M\rarabeta N} (qui utilise les règles de la définition
de \bleu{\rarabeta} et celle de \bleu{\rabeta}).


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Proposition} \fbox{\VERT{Congruence de \bleu{\rarabeta}}}

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}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}. 
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Fermeture transitive, réflexive et symétrique} 
\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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'égalité extensionnelle} 

\bleu{\conv{\beta}} décrit l'égalité \VERT{intentionnelle}.

Autrement dit, si \bleu{M\conv{\beta}N} si \bleu{M} et \bleu{N} ont le
même «comportement».

Deux termes sont \rouge{ extensionnellement équivalents} s'ils prennent
les mêmes «valeurs» quand on les appliquent au même terme.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'égalité extensionnelle} 

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

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'égalité extensionnelle} 

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

\vfill 
\end{slide}
%%------------------------------------------------------
\begin{slide}
\rouge{Proposition} \fbox{\bleu{\conv{\textsf{ext}} = \conv{\beta\eta}}.}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Proposition} \fbox{\bleu{\conv{\textsf{ext}} = \conv{\beta\eta}}.}

\vspace*{10pt}

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

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{Proposition} \fbox{\bleu{\conv{\textsf{ext}} = \conv{\beta\eta}}.}

\vspace*{10pt}

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

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Contexte}
  \rouge{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 x. D[~]} alors \bleu{C[A]= \lambda x. D[A]},
\item  si \bleu{C[~]= M D[~]} alors \bleu{C[A]= M D[A]},
\item etc.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Stabilité par contexte} 
\rouge{Proposition}
\bleu{\raR}, \bleu{\raraR} et \bleu{\conv{R}} sont stables par
contexte.

\bleu{\raraR} et \bleu{\conv{R}} sont compatibles.
\end{slide}
%------------------------------------------------------
\begin{slide}
 \fbox{\bleu{\raR} est stable par contexte.}

\rouge{Démonstration :}  \bleu{M\raR N} alors  \bleu{C[M]\raR C[N]} 

\begin{footnotesize}
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}
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Stabilité par substitution} 
\rouge{Proposition}
\fbox{\bleu{M\raraR N} implique \bleu{A[x:=M]\raraR A[x:=N]}.}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Stabilité par substitution} 
\rouge{Proposition}
\fbox{\bleu{M\raraR N} implique \bleu{A[x:=M]\raraR A[x:=N]}.}
\rouge{Démonstration :} 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:=N]}.
\item \rougeMa{A\equiv y}, alors  \bleu{A[x:=M] \equiv y \raraR y \equiv
    A[x:= N]} par réflexivité.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Stabilité par substitution (suite)} 
\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:=M]} 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}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Stabilité par substitution (suite)} 
\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}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice} 

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

\bleu{M\raR N} implique \bleu{A[x:=M]\raR A[x:=N]}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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))}

\bleu{\mathsf{W}_F \equiv (\lambda x. F (x x))}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice} 
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}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice} 

\begin{enumerate}
\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}
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Redex et formes normales} 
  \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-irreductible et si \bleu{M\conv{R}N}.
  \end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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_{ext}}, mais il faut le prouver. 

La forme normale si elle existe est la valeur intentionnelle.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{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}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Entiers de Church} 
  \begin{itemize}
  \item 
    \bleu{(\lambda f x. f(f x))\equiv \textbf{2}} correpond au nombre
    entier \VERT{deux}.
    
  \item 
    \bleu{(\lambda f x .x) \equiv T} 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}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice}  
\begin{enumerate}
\item 
Montrez que
\begin{center}
  \bleu{\textbf{1}\rasub{\eta} I \equiv \lambda x .x }.
\end{center}


\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}}~?
\item Écrivez l'opération ``successeur''.
\end{enumerate}
\end{slide}
%------------------------------------------------------
\end{document}

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