\documentclass{article}

\usepackage{francais,t1enc}
\usepackage[all]{xy}
\usepackage{latexsym}

\renewcommand{\S}{\textbf{S}}
\newcommand{\N}{\texttt{\small |}\!\textsf{N}}
\newcommand{\vDash}{\mathop{|\!\!\!=}}
\newcommand{\Y}{\mathbf{Y}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\I}{\mathbf{I}}

\input{/home/plescann/ARTICLES/macros_lambda.tex}

\begin{document}
\title{Magist�re d'Informatique et Mod�lisation}
\author{\textsf{Exercices de $\lambda$-calcul}}

\date{Novembre -- d�cembre 2001}

\maketitle 


\section*{Exercice~1}
Un terme $M\in\Lambda$ tel que pour tout $F\in\Lambda$, on ait $M\,F =_\beta
F(M\,F)$ est appel� un \emph{combinateur de point fixe}.
\begin{enumerate}
\item Soit $A \equiv \lambda x y \cdot y (x x y)$ et $\Theta \equiv A A$.  Soit
  $F$ un terme quelconque.  Montrez que $\Theta F \rarabeta F(\Theta F)$.
  
\item Soit $\Y \equiv \lambda f \cdot (\lambda x \cdot f(x x))
  (\lambda x \cdot f(x x))$ et $G \equiv \lambda y f \cdot f(y f)$.
  R�duisez $\Y G$ trois fois. D�duisez-en une d�rivation qui lie $\Y
  G$ et $\Theta$.
  
\item �tant donn�s deux termes $M$ et $N$ et $x$ une variable, montrez
  que $x M \rarabeta N$ implique qu'il existe $N'$ tel que $N =_\beta x N'$.

\item Montrez que si $M$ est un combinateur de point fixe et $x$ une
  variable quelconque, alors il existe $P$ tel que $M x \rarabeta x P$.


\item Montrez que si $M$ est un combinateur de point fixe, il existe
  $Q$ tel que $M \rarabeta \lambda y \cdot Q$.

\item Montrez que  si $M$ est un combinateur de point fixe,  $\lambda
  x \cdot M x \rarabeta \lambda y \cdot Q$.

\item Conclure que  si $M$ est un combinateur de point fixe,  $\lambda
  x \cdot M x =_\beta M$.

\item Montrez que les trois propositions suivantes sont �quivalentes~:
  \begin{itemize}
  \item[(i)] $M$ est un combinateur de point fixe,
  \item[(ii)] $M =_\beta G M$.
  \item[(iii)] $M$ est un point fixe de $G$.
  \end{itemize}
  
\item Construisez une suite infinie $(\Y^i)_{i\in \Nat}$ de
  combinateurs points fixes.  \emph{(Cette question peut-�tre r�solue
    en admettant la pr�c�dente)}.

  
\item Que dire des termes $\Y^0$, $\Y^1$ et $\Y^2$ et de leurs formes
  normales~?

\end{enumerate}

\newpage
\section*{Exercice~2}
Une th�orie est incoh�rente (ou inconsistante), si pour $A$ et tout
$B$, $A=B$.  On rappelle que $\S = \lambda x y z . x z (yz)$, $\K =
\lambda xy. x$ et $\I= \lambda x. x$.  On veut montrer que, si on
ajoute au $\lambda$-calcul, l'identit� $\S = \K$, il devient
incoh�rent.
\begin{enumerate}
\item De  $\S ABC = \K ABC$, d�duisez une identit� de la forme $MN = M$.
\item En rempla�ant $A$ par $\I$ et $C$ par $\I$ dans l'identit�
  pr�c�dente, d�duisez $B\I = \I$.
\item En choisissant $B$ de fa�on appropri�e dans $B\I = \I$, montrez
  que, pour tout~$P$, on a $P=\I$.
\item Quelle est l'identit� directement d�duite de $\S = \K$ qui
  r�duit � $P=\I$ ?
\end{enumerate}


\end{document}
% LocalWords:  combinateurs
