%% Time-stamp: <modified on  7 Dec 2004 at 16:24 by Pierre Lescanne>
%% denotationnelle.tex
%\documentclass[handout,dvips]{beamer} 
\documentclass{beamer} 

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{color}
\usepackage{epsfig}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}
\usepackage{pslatex}

\title{Sémantique dénotationnelle du lambda-calcul}

\author{}

\date{}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                couleurs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{mes_couleurs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                symboles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{"->"}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\x}{\ensuremath{\textbf{x}}}
\newcommand{\y}{\ensuremath{\textbf{y}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\T}{\ensuremath{{\cal T}}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.50em}\lambda}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\interp}[3]{\llbracket#1\rrbracket^{#2}_{#3}}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        les symboles pour les substitutions explicites
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\newcommand{\Lift}{\Uparrow\!\!}
\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}

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

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

%%%%%%%%%%%%%%%%%%% -- B --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\raB}{\rasub{B}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                environnements
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\concept}[1]{\brunir{#1}}

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\begin{document}
%------------------------------------------------------
\frame{\titlepage}
%------------------------------------------------------
\section{Introduction}
\frame{\frametitle{Plan}\tableofcontents[current]}
%------------------------------------------------------
\frame{
\frametitle{Références}

Ce cours s'appuie sur la section 3.2 \\
du chapitre \textit{\bl{Functional Programming and Lambda Calculus}}
\\de Henk Barendregt \\dans le \verdir{\textit{Handbook of Theoretical
    Computer Science}}.

}
%------------------------------------------------------
\frame{
\frametitle{Le problème}
Donner un modèle au lambda-calcul c'est donner un objet mathématique \bleu{D}
\ali où l'espace des fonctions de \bleu{D} vers \bleu{D} \ali coïncide avec
\bleu{D} lui-même.

\bigskip

Autrement dit, il faut construire un objet tel que \bleu{D
  \mathop{{\stackrel{?}{=}}} D^D}. 

\bigskip

Pour des raisons de cardinalité, c'est impossible si l'on prend de
pures fonctions.

 
}
%------------------------------------------------------
\frame{
\frametitle{Le problème}
Mais doit-on décrire de pures fonctions?

\pause \bigskip 
\rouge{Non.}

\medskip 
On se restreint à des fonctions \concept{continues}
\ali pour une topologie fondée sur l'\concept{approximation}.

\bigskip

Quand une fonction s'évalue, elle approxime son résultat
\pause \ali éventuellement indéfiniment!
}
%------------------------------------------------------
\section{Bornes supérieures}
\frame{\frametitle{Plan}\tableofcontents[current]}
%------------------------------------------------------
\frame{
  \frametitle{Minimum et borne supérieure} %
  Soit  \bleu{(E, ``[= )} un ensemble  ordonné. 

  \bigskip

  S'il existe, le \emph{minimum} d'un sous-ensemble \bleu{A} de
  \bleu{E} est \ali l'élément noté \bleu{\min A} de \bleu{E} tel que
  \begin{displaymathbleu}
    \min A\in A\quad\wedge\quad (\forall a\in A)~ \min A``[=a.
  \end{displaymathbleu} % 
  
  Si elle existe, la \emph{borne supérieure} d'un ensemble \bleu{A} est
  \begin{displaymathbleu}
    \sup A = \min  \{x\in E ~|~ (\forall a\in A) ~a``[= x\}.
  \end{displaymathbleu}
  

}
%------------------------------------------------------
\frame{
  \frametitle{Maximum et borne inférieure} %
 
  S'il existe, le \emph{maximum} d'un sous-ensemble \bleu{A} de
  \bleu{E} est \ali l'élément noté \bleu{\max A} de \bleu{E} tel que
  \begin{displaymathbleu}
    \max A\in A\quad\wedge\quad (\forall a\in A)~ a ``[= \max A.
  \end{displaymathbleu} % 
  
  Si elle existe, la \emph{borne inférieure} d'un ensemble \bleu{A} est
  \begin{displaymathbleu}
    \inf  A = \max  \{x\in E ~|~ (\forall a\in A) ~x``[= a\}.
  \end{displaymathbleu}
  

}
%------------------------------------------------------
\frame{
  \frametitle{Produit cartésien d'ensembles ordonnés} %
Si \bleu{(A_1, ``[=_1)} et \bleu{(A_2, ``[=_2)} sont deux ensembles
ordonnés. 

Leur produit cartésien \bleu{A_1 `* A_2} est ordonné en \bleu{(A_1 `*
  A_2, ``[=_1 `* ``[=_2 )} par
\begin{displaymathbleu}
  (a_1, a_2) ``[=_1 `* ``[=_2 (b_1, b_2) \quad "<=>" \quad a_1
  ``[=_1 b_1 \wedge a_2 ``[=_2 b_2.
\end{displaymathbleu}


}
%------------------------------------------------------
\frame{
  \frametitle{Borne supérieure d'un produit cartésien} %
On remarque que %`* signifie \times
\begin{eqnarraybleu}
\sup (A_1 `* A_2) & = & \sup \{(a_1, \sup A_2) ~|~ a_1\in A_1\}\\
& = & \sup~ \{(\sup A_1, a_2) ~|~ a_2\in A_2\}
\end{eqnarraybleu}
\pause Pour calculer la borne supérieure d'un produit cartésien on peut
procéder composante par composante.\\
\begin{small}
  Avec d'autres notations: \begin{eqnarraybleu}
\sup_{(a_1,a_2)\in A_1 `* A_2}~(a_1, a_2) & = & %
\sup_{a_1\in A_1}~ \{(a_1, \sup_{a_2 \in A_2}~ a_2)\}\\
& = & \sup_{a_2\in A_2} \{(\sup_{a_1\in A_1} a_1, a_2)\}
\end{eqnarraybleu}
\end{small}

}
%------------------------------------------------------
\section{Treillis complet}
\frame{\frametitle{Plan}\tableofcontents[current]}
%------------------------------------------------------
\frame{
  \frametitle{Treillis complet} %``[= remplace \sqsubseteq
  Un ensemble ordonné \bleu{(D, ``[= )} est un \emph{treillis complet}
  si pour tout sous-ensemble \bleu{X ``(= D} la borne supérieure
existe. % ``(= remplace \subseteq

\medskip

Par abus de notation on écrira parfois \bleu{D} au lieu de \bleu{(D,
  ``[= )}.  

\medskip

Quand on écrira \bleu{D, D', ...} le lecteur devra comprendre sans
plus de précision qu'il s'agit d'un treillis complet ordonné par
\bleu{``[=, ``[=', ...}.


}
%------------------------------------------------------
\frame{
  \frametitle{Treillis complet} %
Dans un triellis complet,  chaque treillis a %
\begin{itemize}
\item  un maximum \concept{top} \bleu{\top = \sup D} %

\item et un minimum \concept{bottom} \bleu{\bot = \sup`{}}.
\end{itemize}
\pause \bigskip

% `{} est \emptyset
\bleu{\bot} \emph{est l'élément minimum de}   \bleu{D}.
\medskip
En effet, \bleu{D} est l'ensemble des majorants de \bleu{`{}}.

Donc le minimum de \bleu{D}, qui est \bleu{\bot}, \ali est aussi le minimum des
majorants de~\bleu{`{}}.

\bleu{\bot} est donc bien la borne supérieure de \bleu{`{}}.

}
%------------------------------------------------------
\frame{
  \frametitle{Treillis complet} %
\newcommand{\Xbar}{\overline{X}}

Dans un triellis complet \bleu{D},  chaque sous-ensemble \bleu{X} de \bleu{D} %
\ali a une \concept{borne inférieure}.
\begin{displaymathbleu}
\inf X = \sup  \{y ~|~ (\forall x\in X)~ y``[= x\}.
\end{displaymathbleu}
\pause
Notons tout d'abord que si \bleu{(`A a`:A)~a``[= x} alors \bleu{\sup A
  ``[= x}. 
\only<3>{\ali
\begin{footnotesize}
  C'est la définition de la borne supérieure qui le donne.
\end{footnotesize}}

\only<4>{\bigskip

Posons \bleu{\Xbar \triangleq \{y ~|~ (\forall x\in X)~ y``[= x\}}.


  Donc, \bleu{(`A x'`:X)~\sup \Xbar ``[= x'} donc
  \bleu{\sup \Xbar`:\Xbar}.  

Donc \bleu{\sup \Xbar = \max \Xbar}. }
}
%------------------------------------------------------
\frame{
  \frametitle{Dirigé} %
Un sous-ensemble \bleu{X ``(= D} est un \concept{dirigé} %
\begin{itemize}
\item si \bleu{X "/=" `{}} % `"/=" signifie \neq
\item et \bleu{(\forall x, y \in X)\quad (\exists z \in X) \quad [x
  ``[= z \wedge y ``[= z].}
\end{itemize}

}

%------------------------------------------------------
\frame{
  \frametitle{Fonctions continues} %
Une application \bleu{f: D "->" D'} est \concept{continue} si pour tout
dirigé \bleu{X ``(= D} on a
\bl{\(f(\sup  X) = \sup  f(X) = \sup  \{f(x) ~|~ x \in X\}.\)}
\medskip Cette notion de continuité coïncide avec une topologie.

\vspace*{12pt}

\verdir{Exercice}: Tout fonction \concept{continue} est \concept{croissante}.

}
%------------------------------------------------------
\frame{
  \frametitle{Exponentiation de treillis} %

L'\concept{espaces de fonctions}\bleu{[D "->" D']}  est donné par
\begin{displaymathbleu}
  [D "->" D'] = \{f: D "->" D' ~|~ f \textrm{~continue}\}
\end{displaymathbleu}

Cet ensemble est muni d'un ordre dérivé de l'ordre sur \bleu{D'}:

\begin{displaymathbleu}
f ``[= g \quad "<=>" \quad  (\forall d\in D) \quad f(d) ``[=' g(d)
\end{displaymathbleu}



}
%------------------------------------------------------
\frame{
  \frametitle{Produit de treillis} %
\verdir{Proposition}: \bleu{D `* D'} est un treillis complet où pour
\bleu{X ``(= D `* D'}.
\begin{displaymathbleu}
\sup  X = (\sup  (X)_0, \sup  (X)_1)
\end{displaymathbleu}
avec %
\begin{displaymathbleu}
(X)_0 = \{d\in D ~|~ (\exists d'\in D') \quad (d,d')\in X\}
\end{displaymathbleu}
\begin{displaymathbleu}
(X)_1 = \{d'\in D' ~|~ (\exists d\in D) \quad (d,d')\in X\}
\end{displaymathbleu}



}
%------------------------------------------------------
\frame{
  \frametitle{Exponentiation de treillis} %
\verdir{Proposition}: Soit \bleu{F ``(= [D "->" D']} un ensemble
de fonction continue.  

On définit \bleu{f(x) = \sup \{g(x) ~|~ g\in F\}}. 

Alors \bleu{f} est continue et dans \bleu{[D "->" D']} on a \bleu{f =
\sup  F}. 

Donc \bleu{[D "->" D']} est un treillis complet.

\vspace*{5pt}


}
%------------------------------------------------------
\frame{
\emph{Preuve :} Clairement \bleu{f} est le plus petit des majorants de \bleu{F}.
\begin{eqnarraybleu}
    f~(\\sup X) & = & \sup_{g\in F} g(\sup X)\\
  & = & \sup_{g\in F} \sup_{x\in X} g(x)\\
  & = & \sup_{x\in X} \sup_{g\in F} g(x)\\
  & = & \sup_{x\in X} f(x)
  \end{eqnarraybleu}
Donc \bleu{f} est continue.

}
%------------------------------------------------------
\frame{
  \frametitle{Commutation de $\sup$ et $\llbda$} %

Soit \bleu{\llbda x} la $`l$-abstraction dans la théorie des
ensembles. %

Autrement dit, si \bleu{\{(x, f(x)) ~|~ x\in A\}} est le graphe d'une
fonction,%
\ali \bleu{\llbda x . f(x)} est la fonction au sens ensembliste qui
lui est \ali associée.

\begin{displaymathbleu}
\sup \{\llbda x . f(x) ~|~ f\in F\} = \llbda x. \sup  \{f(x) ~|~ f\in F\}
\end{displaymathbleu}

}
%------------------------------------------------------
\frame{
\frametitle{Bottom}
On voit que 
\begin{eqnarraybleu}
  \bot_{D`*D'} &=& (\bot_D , \bot_{D'})\\
  \bot_{[D "->" D']} &=& \llbda d . \bot_{D'}
\end{eqnarraybleu}
Pour \bleu{\bot_{D`*D'}} cela vient du fait que \bleu{`{} = `{} `* `{}}.

D'autre part, \bleu{\llbda d . \bot_{D'}} est une fonction continue et
elle minore toutes les autres fonctions.
 
}
%------------------------------------------------------
\frame{
  \frametitle{Points fixes} %
\verdir{Proposition}: Si \bleu{f \in [D "->" D]} alors \bleu{f} a une
point fixe défini par
\begin{displaymathbleu}
Fix(f) = \sup_{n\in\Nat} f^n(\bot)
\end{displaymathbleu}

\pause\bigskip

On prouve par récurrence que \bleu{\{f^n(\bot) ~|~ n\in \Nat\}} est
dirigé.   Donc
\begin{displaymathbleu}
f(Fix(f)) = f(\sup_{n\in\Nat} f^n(\bot)) = \sup_{n\in\Nat}  f(f^n(\bot))) = Fix(f). 
\end{displaymathbleu}

\bigskip

Si \bleu{x} est un autre point fixe de \bleu{f} alors \bleu{f(x) = x}
et \bleu{\bot ``[= x}, %
\ali donc par croissance
de \bleu{f}, on a  \bleu{f^n(\bot) ``[= f^n(x) =x}. \ali Donc  \bleu{Fix(f)
  ``[= x}
 
}
%------------------------------------------------------
\frame{
  \frametitle{Continuité sur un produit} %
\verdir{Proposition}: Soit \bleu{f: D `* D' "->" D''}. \bleu{f} est continue si \bleu{f} est
continue en chacune de ses composantes, autrement dit, si 
\begin{itemize}
\item pour tout \bleu{x_0'}, \bleu{\llbda x . f(x,x_0')} est continue,
\item pour tout \bleu{x_0}, \bleu{\llbda x . f(x_0,x)} est continue.
\end{itemize}
 
 }
%------------------------------------------------------
\frame{
  \frametitle{Continuité de \bleu{Ap}} %
\verdir{Proposition}: La fonction  \bleu{Ap: [D "->" D'] `* D \quad "->" D'}
\ali définie par  \bleu{Ap(f,x) = f(x)} est continue.
 
 }
%------------------------------------------------------
\frame{
  \frametitle{Continuité de \bleu{\llbda}} %
\verdir{Proposition}: Soit \bleu{f: [D `* D' "->" D'']}. 

Pour tout \bleu{x\in D}, on a
\begin{itemize}
\item \bleu{\llbda y. f(x,y)\in [D' "->" D'']}.


\item 
  \bleu{\llbda x . \llbda y . f(x,y)\in [D "->" [D' "->" D'']]},\\
  autrement dit la fonction \bleu{x "|->" \llbda y . f(x,y)} \\ est une
  fonction continue.
\end{itemize}

}
%------------------------------------------------------
\section{Rétractions}
\frame{\frametitle{Plan}\tableofcontents[current]}
%------------------------------------------------------
\frame{
  \frametitle{Rétraction et réflexivité} %
  
  \bleu{D} est une \concept{rétraction} de \bleu{D'} (noté \bleu{D ``<
    D')} \ali s'il
  existe des fonctions continues 
  \begin{itemize}
  \item \bleu{F \in [D' "->" D]},
  \item \bleu{G \in [D "->" D']},
  \item \bleu{F `o G = id_D},
  \end{itemize}


\bigskip\bigskip

\bleu{D} est \concept{réflexif} si \bleu{[D "->" D] ``< D}
}
%------------------------------------------------------
\frame{
  \frametitle{Rétraction} %
Si \bleu{D ``< D'} par \bleu{F} et \bleu{G} alors \bleu{F} est
surjective et \bleu{G} est injective.  

On peut donc identifier \bleu{D} avec son image par \bleu{G},
c'est-à-dire \bleu{G(D) ``(= D'}.

Alors  \bleu{F} \concept{rétrécit} (fait se rétracter) l'espace le plus grand  \bleu{D'}
\ali vers le plus petit  \bleu{D}.


\bigskip

Nous allons voir maintenant comment un treillis réflexif peut-être
utilisé pour \concept{modéliser} le $`l$-calcul.


}
%------------------------------------------------------
\frame{
  \frametitle{Quelques notations} %
Soit \bleu{D} réflexif via \bleu{F} et \bleu{G}.\\%
\bleu{F} est une rétraction de \bleu{D} vers  \bleu{[D "->" D]}. \\%
Donc pour  \bleu{x\in D} on a \bleu{F(x) \in [D "->" D]}.\\%
De cette façon les éléments de \bleu{D} deviennent des fonctions sur
\bleu{D}
% `(!) un gros point c-à-d un \bullet
\begin{displaymathbleu}
x `(!)_F y = F(x)(y) \qquad \in D
\end{displaymathbleu}
Inversement \bleu{G} fait d'une fonction continue sur \bleu{D}
un élément de \bleu{D}.\\%
On peut écrire pour chaque  \bleu{f} continue.
\begin{displaymathbleu}
`l^G x `. f(x) = G(f)  \qquad \in D
\end{displaymathbleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Interprétation des $`l$-termes} %
Une \concept{valuation} dans \bleu{D} est une application \bleu{`r : Var
  "->" D}.

On peut modifier une valuation en un point:
\begin{displaymathbleu}
  \modval{`r}{x}{d} =\left\{
    \begin{array}[c]{l@{\quad}l}
      `r(y) & \textrm{if~} y \not`= x \\d & \textrm{if~} y `= x
    \end{array}
  \right.
\end{displaymathbleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Interprétation des $`l$-termes} %
On note \bleu{\interp{M}{D}{`r}} l'\concept{interprétation dans \bleu{D}
  sous la valuation \bleu{`r}} 

\bl{\begin{center}
  \begin{math}
    \begin{array}[c]{l@{\qquad}l}
\hline
M  &  \interp{M}{D}{`r}\\
\hline
x  &  `r(x)\\
P\ Q  &  \interp{P}{D}{`r} `(!)_F \interp{Q}{D}{`r} \\
`l x . P  &  `l^G d `. \interp{P}{D}{\modval{`r}{x}{d}}
    \end{array}
  \end{math}
\end{center}
}

}
%------------------------------------------------------
\frame{
  \frametitle{Des exemples 1/2} %
  \begin{eqnarraybleu}
    \interp{`l x . x}{D}{`r} & = & `l^G d `.d\\[3pt]
    \interp{`l x . `l y . x}{D}{`r} & = & `l^G d `.\interp{`l y .
      x}{D}{\modval{`r}{x}{d}} \\
    & = & `l^G d `.`l^G d' `.
    \interp{x}{D}{\modval{\modval{`r}{x}{d}}{y}{d'}} \\%
    & = & `l^G d `.`l^G d' `. d\\
    & = & G(\llbda d . G(\llbda d' . d))
  \end{eqnarraybleu}
  
}
%------------------------------------------------------
\frame{
  \frametitle{Des exemples 2/2} %
  \begin{eqnarraybleu}
    \interp{`l x . x y}{D}{`r} & = & `l^G d `.(d `(!)_F `r(y))\\
    & = & G(\llbda d . F(d)(`r(y))) \\[3pt]
    \interp{`l x . x x}{D}{`r} & = & `l^G d `.(d `(!)_F d) \\
    & = &G(\llbda d . F(d)(d))
\end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Exercice} %
\verdir{Exercice}: Calculer \bleu{\interp{(`l x . x y)(`l z . z)}{D}{`r}}.
\pause
\begin{eqnarraybleu}
  \interp{(`l x . x y)(`l z . z)}{D}{`r} &=& \interp{(`l x . x
    y)}{D}{`r}`(!)_F \interp{(`l z . z)}{D}{`r}\\
  &=& F(G(\llbda d . F(d)(`r(y))))(G(\llbda d' .d'))\\
  &=& (\llbda d . F(d)(`r(y)))\;(G(\llbda d' .d'))\\
  &=& F(G(\llbda d' .d'))(`r(y))\\
  &=& (\llbda d' .d')(`r(y))\\
  &=& `r(y)\\
  &=&  \interp{y}{D}{`r} 
\end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Notations} %
Clairement \bleu{\interp{M}{D}{`r}} ne dépend que des valeurs de
\bleu{`r} sur \bleu{FV(M)}. 

\newqsymbol{`ù}{\upharpoonright}
Soit \bleu{`ù} la restriction d'une fonction à un domaine.

On a 
\begin{displaymathbleu}
`r`ùFV(M) = `r'`ùFV(M) \quad "=>" \quad \interp{M}{D}{`r}=  \interp{M}{D}{`r'}
\end{displaymathbleu}
En particulier pour les termes sans variables libres (aussi appelés
termes clos ou combinateurs),
\begin{itemize}
\item \bleu{\interp{M}{D}{`r}} ne dépend pas de \bleu{`r}
\item et on peut écrire \bleu{\interp{M}{D}{}}.
\end{itemize}

De plus, si \bleu{D} est clair par le contexte, on écrira
\bleu{\interp{M}{}{}}. 


}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de correction} %
\verdir{Théorème}: Si \bleu{D} est réflexif, \ali alors \bleu{D} est un
modèle du lambda calcul.
\begin{displaymathbleu}
 M \conv{`b} N \quad "=>" \quad D \vDash M = N
\end{displaymathbleu}
où \bleu{D \vDash M = N} signifie que pour toute valuation \bleu{`r},
\bleu{\interp{M}{}{`r} = \interp{N}{}{`r}} 
}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de correction, démonstration 1/3} %
On démontre tout d'abord 
\begin{eqnarraybleu}
  \interp{M[x:=N]}{}{`r} &=& \interp{M}{}{\modval{`r}{x}{\interp{N}{}{`r}}}
\end{eqnarraybleu}
Posons \bleu{P^* `= P[x:=N]} et \bleu{`r^* `=
  \modval{`r}{x}{\interp{N}{}{`r}}}.

\begin{footnotesize}
  \begin{displaymathbleu}
    \begin{array}{llll}
      \hline% --------------------------------------
      M & \interp{M^*}{}{`r} & \interp{M}{}{`r^*} \\
      \hline% --------------------------------------
      x & \interp{N}{}{`r} & \interp{N}{}{`r} \\
      y & `r(y) & `r(y) \\
      P Q & \interp{P^*}{}{`r} `(!)_F \interp{Q^*}{}{`r} & %
          \interp{P}{}{`r^*} `(!)_F \interp{Q}{}{`r^*} & \textrm{par
            induction}\\
      `l y . P & `l^G d . \interp{P^*}{}{\modval{`r}{y}{d}} & %
      `l^G d . \interp{P}{}{\modval{`r^*}{y}{d}} & (\modval{`r}{y}{d})^* =
          \modval{`r^*}{y}{d}
    \end{array}
  \end{displaymathbleu}
\end{footnotesize}

}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de correction, démonstration 2/3} %
Pour la preuve de la règle \bleu{(`b)}:
\begin{eqnarraybleu}
  \interp{(`l x . M) N}{}{`r} & = & %
      (`l^G d . \interp{M}{}{\modval{`r}{x}{d}}) `(!)_F \interp{N}{}{`r}\\
      & = & F(G(\llbda d . \interp{M}{}{\modval{`r}{x}{d}}))(\interp{N}{}{`r})\\
      & = &(\llbda d . \interp{M}{}{\modval{`r}{x}{d}})(\interp{N}{}{`r})\\
      & = &\interp{M}{}{\modval{`r}{x}{\interp{N}{}{`r}}}\\
      & = & \interp{M[x:=N]}{}{`r}
\end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de correction, démonstration 3/3} %
  Pour la règle \bleu{(`x)} on a à montrer que \bleu{M \conv{`b} N
    \quad "=>" `l x. M \conv{`b} `l x . N} se traduit en la même règle
  au niveau de \bleu{D}, c'est-à-dire %
  \ali \bleu{D \vDash M = N \quad "=>"
    \quad D \vDash `l x. M = `l x. N}.

\begin{small}
\begin{eqnarraybleu}
  && (`A `r`:Var"->"D)\quad \interp{M}{}{`r} = \interp{N}{}{`r} \\
  & "=>" & (`A `r`:Var"->"D)\quad \interp{M}{}{\modval{`r}{x}{d}} = \interp{N}{}{\modval{`r}{x}{d}} \\
  & "=>" & (`A `r`:Var"->"D)\quad \llbda d . \interp{M}{}{\modval{`r}{x}{d}} = \llbda d . \interp{N}{}{\modval{`r}{x}{d}} \\
  & "=>" & (`A `r`:Var"->"D)\quad `l^G d . \interp{M}{}{\modval{`r}{x}{d}} = `l^G d . \interp{N}{}{\modval{`r}{x}{d}} \\
  & "=>" & (`A `r`:Var"->"D)\quad \interp{`l x. M}{}{`r} = \interp{`l x . N}{}{`r}
\end{eqnarraybleu}
\end{small}

}
%------------------------------------------------------
\section{Construction de réflexifs}
%------------------------------------------------------
\subsection{1ère  construction: le modèle
  d'Engeler}
\frame{\frametitle{Plan}\tableofcontents[currentsubsection]}
%------------------------------------------------------
\frame{
  \frametitle{Le support} %
\bleu{A} est un ensemble.
\begin{eqnarraybleu}
    B_0  & = &  A \\
    B_{n+1}  & = &  B_n \cup \{(`b,b) ~|~ b\in B_n \wedge `b ``(= B_n \wedge
    `b \verdir{\textrm{~est fini}}\},\\
    B  & = &  \bigcup_{n\in \Nat} B_n.
  \end{eqnarraybleu}

\bleu{D_A = {\cal P}(B) = \{x ~|~ x ``(= B\}} est un treillis complet  pour l'inclusion~\bleu{\subseteq}.

}
%------------------------------------------------------
\frame{
  \frametitle{Le support} %

\bleu{B} est obtenu en itérant la formation des paires \bleu{(`b, b)} à
partir de \bleu{(`{}, a)} pour \bleu{a\in A}. 

\bigskip

On suppose que \bleu{A} ne contient que des éléments «primitifs»,
  c-à-d pas d'éléments  \bleu{(`b, b)\in B}.

}
%------------------------------------------------------
\frame{
  \frametitle{Un exemple}
Soit \bleu{B_0 =\{0, 1\}}.
\medskip
Alors
\begin{eqnarraybleu}
  B_1 &=& \{(\emptyset, 0), (\{0\}, 0), (\{1\}, 0), (\{0, 1\}, 0), \\
  && \phantom{\{}(\emptyset, 1), (\{0\}, 1), (\{1\}, 1), (\{0, 1\}, 1)\}\\
  B_2 &=& \{(\emptyset, (\emptyset, 0)), ..., (\{(\{1\}, 0), (\{0,
  1\}, 1)\},~(\{0\}, 0)), ...\}
\end{eqnarraybleu}
}
%------------------------------------------------------
\frame{
  \frametitle{La rétraction et l'antirétraction de $D_A$} %
On définit \bleu{F: D_A "->" [D_A "->" D_A]} et %
\bleu{G: [D_A "->" D_A] "->" D_A}

\begin{eqnarraybleu}
    F(x)(y) & = & \{b ~|~  (\exists `b ``(= y) \quad (`b, b) \in x\}\\
    G(f) & = & \{(`b, b) ~|~ b \in f(`b)\}.
  \end{eqnarraybleu}


}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de réflexivité de $D_A$} %
\verdir{Théorème}: \bleu{D_A} est réflexif via \bleu{F} et \bleu{G}.

\pause \bigskip 

\emph{Démonstration :} 
\begin{eqnarraybleu}
  (F `o G)(f) (c) & = & F (\{(`d, d) ~|~ d \in f(`d)\})(c)\\
  & = & \{b ~|~  (\exists `b ``(= c) \quad (`b, b) \in \{(`d, d) ~|~ d\in f(`d)\}\}\\
  & = & \{b ~|~  (\exists `b ``(= c) \quad b\in f(`b)\}\\
  & = & \bigcup_{`b ``(= c} f(`b) \qquad \concept{\textrm{par continuité
      de~}} f\\
  & = & f(\bigcup_{`b ``(= c} `b) \\
  &=& f(c)
  \end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Images de \bleu{\I} et de \bleu{\K}} %
\begin{eqnarraybleu}
  \interp{\I}{D_A}{} & = & G(\llbda x . x) = \{(`b, b) ~|~ b`:`b\}\\\\
  \pause
  G(\llbda d' . d) & = & \{(`b,b)~|~ b\in d\}\\[4pt]
  \interp{\K}{D_A}{} & = & G(\llbda d .G(\llbda d' . d)) \\
  & = & \{(`g,c) ~|~ c\in \{G(\llbda d' . d) ~|~ d\in `g\}\\
  & = & \{(`g,c) ~|~ c\in \{(`b,b) ~|~ (`E d)~b \in d \wedge d \in
  `g\}\}\\
  & = & \{(`g, (`b, b)) ~|~ (`E d)~b \in d \wedge d \in `g\}
  \end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
  \frametitle{Image de \bleu{\S}} %
  \verdir{Exercice}: Donnez dans \bleu{D_A} l'image de \bleu{\S} par
  \bleu{\interp{`.}{D_A}{}}.  
  \vfill
}
%------------------------------------------------------
\frame{
  \frametitle{Théorème de cohérence du lambda calcul} %
\verdir{Théorème}: Le lambda-calcul est cohérent.


\pause \bigskip 

\emph{Démonstration :} On a vu que \bleu{\interp{\K}{D_A}{}} et
\bleu{\interp{\S}{D_A}{}} sont différents.

}
%------------------------------------------------------
\subsection{2ème construction: le modèle de Scott}
\frame{\frametitle{Plan}\tableofcontents[current,currentsubsection]}
%------------------------------------------------------
\frame{
  \frametitle{Un exemple de construction par limite} %
 %
Soit \bleu{p} un nombre premier.

 Les \concept{entiers $p$-adiques} (\textit{Jean-Pierre Serre} \textup{Cours
    d'arithmétique} (1970)), sont construits ainsi.


\pause \bigskip 

Posons \bleu{A_n= \mathbb{Z} / p^n\mathbb{Z}}.  

C'est l'anneau des classes d'entiers (mod $p^n$). 

Un élément de  \bleu{A_n} définit un élément de \bleu{A_{n-1 }}.

On obtient un homomorphisme surjectif
\begin{displaymathbleu}
  `v_n : A_n "->" A_{n-1}
\end{displaymathbleu}
de noyau \bleu{p^{n-1} A_n}.


}
%------------------------------------------------------
\frame{
  \frametitle{Un exemple de construction par limite} %
La suite 
\bleu{
  ... "->" A_n "->" A_{n-1} "->" ... A_2 "->" A_1
}
forme un «cône». 
\bigskip

\bleu{\mathbb{Z}_p} est la limite du cône \bleu{(A_n, `v_n)}.

\bleu{\mathbb{Z}_p} est l'\concept{anneau des entiers $p$-adiques}.

Un élément \bleu{a} de \bleu{\mathbb{Z}_p} est une suite
\bleu{(a_n)_{n`:\Nat}} avec
\begin{itemize}
\item \bleu{a_n`:A_n},
\item \bleu{`v_n(a_n) = a_{n-1}} si \bleu{n\ge2}.
\end{itemize}

L'addition et la multiplication de \bleu{\mathbb{Z}_p} sont définies
«coordonnées par coordonnées». 


}
%------------------------------------------------------
\frame{
  \frametitle{Un exemple de construction par limite} %
%
\bleu{\mathbb{Z}_p} est un sous-anneau du produit
\bleu{`P_{n\ge1}A_n}.

Pour qu'un élément de \bleu{\mathbb{Z}_p} ne soit pas inversible, il
suffit qu'il ne soit pas divisible par \bleu{p}.

Etc. 

}
%------------------------------------------------------
\frame{
  \frametitle{Cône et limite d'un cône}
Un cône est une suite 
\bleu{
  ... "->" A_n "->" A_{n-1} "->" ... A_2 "->" A_1
}
où chaque \bleu{"->"} est une surjection.
\bigskip

La limite d'un cône est une objet \bleu{A} tel que le diagramme
ci-dessus commute pour tous \bleu{n`:\Nat}

\centerline{\xymatrix{
A_n & \ar[l]\ar[d]A\\
& A_{n+1}\ar[ul]
}}

}
%------------------------------------------------------
\frame{
  \frametitle{Cône et limite d'un cône}
Si $B$ est une autre solution 
\centerline{\xymatrix{
&& B\ar[dll]\ar[ddl]\\
A_n & \\
& A_{n+1}\ar[ul]
}}
alors il existe un morphisme (une application)
$B "->" A$ tel que 
\centerline{\xymatrix{
    && B\ar[dll]\ar[ddl]\ar[dl]\\
    A_n & \ar[l]\ar[d]A\\\
    & A_{n+1}\ar[ul] }} 
}
%------------------------------------------------------
\frame{
  \frametitle{Un passage à la limite} %
On souhaite passer à la limite non plus des ensembles d'entiers \ali mais des
espaces de fonctions.

\vspace*{8pt}
\begin{center}
  \begin{Large}
    Plus précisément
  \end{Large}
\end{center}

}
%------------------------------------------------------
\frame{
  \frametitle{Un passage à la limite} %
\begin{tiny}
\xymatrix @R 4pt  @C 12pt{
&&& &&& &&& && D_\infty \ar[dddddddddd]^{ = D_{\infty}}\\
&&&&&&& D_n \ar[dddddddd]^{ = D_{n+1}}\\
&&&&& \ar@{.>}[dddddd]\\
&&& D_1 \ar[dddd]^{ = D_2}\\
& D_0 \ar[dd]^{ = D_1}\\
D_0 \ar@<1ex>[r]^{i_0} &\ar@<1ex>[l]^{j_0}& \ar@<1ex>[r]^{i_1} &\ar@<1ex>[l]^{j_1}&
\ar@{.>}@<1ex>[r]^{i_.} &\ar@{.>}@<1ex>[l]^{j_.}& \ar@<1ex>[r]^{i_n} &
\ar@<1ex>[l]^{j_n}%
           &\ar@{.>}@<1ex>[rrr]^{i_\infty} &&&\ar@{.>}@<1ex>[lll]^{j_\infty}\\
& D_0 \\
&&& D_1 \\
&&&&&\\
&&&&&&& D_n \\
&&& &&& &&& && D_\infty 
}
\end{tiny}

}
%------------------------------------------------------
\frame{
\frametitle{$D_n$}
On prend pour \bleu{D_0} un treillis complet, par exemple \bleu{\{\bot,\top\}}.

On pose 
\begin{itemize}
\item \bleu{D_1 = [D_0 "->" D_0]}, 
\item \bleu{D_2 = [D_1 "->" D_1]}, 
\item \qquad $\vdots$
\item \bleu{D_{n+1} = [D_n "->" D_n]},
\item \qquad $\vdots$
\end{itemize}


}
%------------------------------------------------------
\frame{
\frametitle{$i_0$ et $j_0$}
Soit l'injection \concept{\fbox{\bleu{i_0 : D_0 "->" D_{1} \quad i_0(d) = \llbda d' . d}}}
\medskip
et la surjection \concept{\fbox{\bleu{j_0 : D_{1} "->" D_{0} \quad j_0(f) = f(\bot)}}}.

\begin{itemize}
\item \bleu{i_0} et  \bleu{j_0} sont continues
\item  \bleu{i_0(\bot_{D_0}) = \bot_{[D_0 "->" D_0]} = \bot_{D_{1}}},
\item \bleu{j_0(\bot_{D_{1}}) = j_0(\llbda d' .  \bot_{D_0}) =
    (\llbda d' .  \bot_{D_0}) (\bot_{D_0}) = \bot_{D_{0}} }
\item \bleu{j_0 `o i_0 = id_0}
\item \bleu{i_0 `o j_0 ``[= id_1}
\end{itemize}


}
%------------------------------------------------------
\frame{
\frametitle{$j_0 `o i_0$}
On a \bleu{j_0 `o i_0 = id_{D_0}}, en effet,
\begin{eqnarraybleu}
  j_0 `o i_0 (d) & = & j_0(\llbda d' . d)\\
  & = & (\llbda d' . d) (\bot_{D_0}) \\
  & = & d
\end{eqnarraybleu}


}
%------------------------------------------------------
\frame{
\frametitle{$i_0 `o j_0$}
Inversement \bleu{i_0 `o j_0 ``[= id_{D_{1}}}, en effet
\begin{eqnarraybleu}
  i_{0} `o j_0(d)& = & i_0(d(\bot_{D_0}))\\
  & = & \llbda d' . d(\bot_{D_0})\\
  & ``[= & d
\end{eqnarraybleu}
La fonction constamment égale à la valeur de \bleu{d} sur
\bleu{\bot_{D_0}} est plus petite que \bleu{d}, car \bleu{d} est
croissante.  

}
%------------------------------------------------------
\frame{
\frametitle{$i_{n+1}$ et $j_{n+1}$}
On définit

   \concept{\fbox{\bleu{i_{n+1} (g) = i_n `o g `o j_n}}}
   \qquad 
   \concept{\fbox{\bleu{j_{n+1}(g) = j_n `o g `o i_n}}}
\medskip
On voit que
\begin{eqnarraybleu}
  i_{n+1} : [[D_n "->" D_n] "->" [D_{n+1} "->" D_{n+1}]] &`=& [D_{n+1} "->" D_{n+2}]\\
  j_{n+1} : [[D_{n+1} "->" D_{n+1}] "->" [D_n "->" D_n]] &`=& [D_{n+2} "->" D_{n+1}]\\
  j_{n+1} `o i_{n+1} &=& id_{D_{n+1}}\\
  i_{n+1} `o j_{n+1} &``[=& id_{D_{n+2}}
\end{eqnarraybleu}


}
%------------------------------------------------------
\frame{
\frametitle{$j_{n+1} `o i_{n+1}$}
On a \bleu{j_{n+1} `o i_{n+1} = id_{D_{n+1}}}, en effet,
\begin{eqnarraybleu}
  j_{n+1} `o i_{n+1} (g) & = & j_{n+1}(i_n `o g `o j_n) \\
  & = & j_n `o i_n `o g `o j_n `o i_n \\
  & = & g
\end{eqnarraybleu}


}
%------------------------------------------------------
\frame{
\frametitle{$i_{n+1} `o j_{n+1}$}
Inversement \bleu{i_{n+1} `o j_{n+1} ``[= id_{D_{n+2}}}, en effet
\begin{eqnarraybleu}
  i_{n+1} `o j_{n+1}(g) & = & i_{n+1}(j_n `o g `o i_n) \\
  & = & i_n `o j_n `o g `o i_n `o j_n \\
  & ``[= & g
\end{eqnarraybleu}

}
%------------------------------------------------------
\frame{
\frametitle{$D_\infty$}
Le support de \bleu{D_\infty} et \bleu{\{(x_n)_{n\in\Nat} ~|~ x_n\in
  D_n \wedge x_n = j_n(x_{n+1})\}}.


\bigskip 


Son ordre est
\bleu{\x ``[=_\infty \y \qquad "<=>" \qquad (\forall n\in \Nat)\quad
  x_n ``[= y_n}.


}
%------------------------------------------------------
\frame{
\frametitle{De $D_\infty "->" D_\infty$ vers $D_\infty$}
Soit \bleu{f: [D_\infty "->" D_\infty]}.  Posons \bleu{\y =
  f(\x)}.

Cela définit une suite de fonctions \bleu{f_n: [D_n "->" D_n]}.

On voit que 
\begin{eqnarraybleu}
  f_n(j_n(x_{n+1})) & = & f_n(x_n)\\
  & = & y_n \\
  & = &  j_n(y_{n+1}) \\
  & = & j_n(f_{n+1}(x_{n+1}))
\end{eqnarraybleu}
Donc \bleu{f_n `o j_n = j_n `o f_{n+1}},.

}
%------------------------------------------------------
\frame{
Soit encore 
\begin{eqnarraybleu}
  f_n & = & f_n `o j_n `o i_n \\
  & = & j_n `o f_{n+1} `o i_n \\
  & = & j_n(f_{n+1}).
\end{eqnarraybleu}
Posons \bleu{d_0 = j_0(f_0)} et \bleu{d_{n+1} = f_n}. 

La suite \bleu{(d_n)_{n\in\Nat}} appartient à~\bleu{D_\infty}.

Posons donc \bleu{j_\infty : [[D_\infty "->" D_\infty] "->"D_\infty]:
  (f_n)_{n\in\Nat} "|->" (d_n)_{n\in\Nat}}.

\bleu{j_\infty} est surjective.


}
%------------------------------------------------------
\frame{
\frametitle{De $D_\infty$ vers $[D_\infty "->" D_\infty]$}
Réciproquement, on définit l'injection \bleu{i_\infty:(x_n)_{n\in\Nat}
  "|->" (x_{n+1})_{n\in\Nat}} qui associe à une suite \bleu{\x} de
\bleu{D_\infty} une fonction de \bleu{[D_\infty "->" D_\infty]}.
\medskip
La fonction \bleu{f(\y) = i_\infty(\x)(\y)} est définie par 
\begin{displaymathbleu}
  f_n(y_n) = x_{n+1}(y_n)
\end{displaymathbleu}

On voit que \bleu{j_\infty `o i_\infty = id_{D_\infty}} et donc que
\bleu{j_\infty} est une \verdir{rétraction} de~\bleu{D_\infty}.

\begin{center}
  \concept{Donc \bleu{D_\infty} est un modèle du lambda-calcul.}
\end{center}

}
\end{document}

% LocalWords:  cardinalité approxime sup bottom Fix Ap réflexif Retracts FV Var
% LocalWords:  retract valuation réflexivité s'évalue pt d'Engeler Scott
