\documentclass{article}

\usepackage[latin1]{inputenc}
\usepackage{amsmath,amssymb}


\title{TD de Sémantique -- 2}
\date{27 septembre 2002}
\author{}


\newcommand{\LL}{\mathcal{L}}
\newcommand{\DD}{\mathcal{D}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\rar}{\rightarrow}
\newcommand{\subst}[1]{\ensuremath{\langle#1\rangle}}
\newcommand{\fv}[1]{\textsf{fv}(#1)}
\newcommand{\lift}{\Uparrow}
\newcommand{\shift}{\uparrow}
\newcommand{\oo}{\circ}

\begin{document}

\maketitle

\noindent\textbf{Exercice 1}\\
\begin{enumerate}
\item Soit $(E,\rar)$ un système de réécriture abstrait. Donner trois
  formulations de Church Rosser. Montrer que
  la propriété diamant implique Church Rosser. Montrer que la
  confluence locale et la normalisation forte impliquent Church Rosser
  (lemme de Newman). Définir la forme normale. Donner un exemple de
  système localement confluent non confluent.
\item On suppose que $\rar$ est acyclique et à branchement fini;
  montrer que $e\in E$ termine ssi il n'a qu'un nombre fini de réduits
  (lemme de K{\oe}nig).
\item On rappelle le lemme de projection pour $\lambda \upsilon$: si
  $M\rar_{\lambda\upsilon} N$ 
  alors $\upsilon(M)\rar_{\beta}^{*} \upsilon(N)$. Montrer comment ce
  lemme implique la confluence de $\lambda\upsilon$
\end{enumerate}

\vspace{1cm}

\noindent\textbf{Exercice 2}\\
On se place dans le système $\lambda\upsilon$:
$$
\begin{array}{rcll}
(\lambda M)N & \rar & M[N/] & (B) \\
(M\,N)[s] & \rar & (M[s]\,N[s]) & (App) \\
(\lambda M)[s] & \rar & (\lambda M[s]) & (Lambda) \\
0[M/] & \rar & M & (FVar) \\
n+1[M/] & \rar & n & (RVar) \\
0[\lift s] & \rar & 0 & (FVarLift) \\
n+1[\lift s] & \rar & n[s][\shift] & (RVarLift) \\
n[\shift] & \rar & n+1 & (VarShift)
\end{array}
$$
\begin{enumerate}
\item Donner l'encodage de $I$ et $\Omega$, vérifier que
  $\Omega\rar^{*}\Omega$.
\item Etablir le lemme de projection
\end{enumerate}

\vspace{1cm}

\newpage

\noindent\textbf{Exercice 3}\\
\begin{enumerate}
\item Donner le type Caml des $\lambda$-termes du système $\lambda\upsilon$.
\item On se propose de représenter en Caml les formules de la logique
  du premier
ordre dans un type de la forme (``syntaxe abstraite d'ordre supérieur'')
\begin{verbatim}
type formula = Forall of var->formula | ...
\end{verbatim}
\begin{enumerate}
\item Achever de définir le type \verb|formula| (on prendre par
  exemple un seul symbole de prédicat unaire). Définir la fonction \\
\verb|test (var->bool)->formula->bool| telle que \verb|test p| donne
la \\
sémantique des formules dans l'interprétation \verb|p| du prédicat.
Définir les fonctions
  de conversion \verb|hoas_to_db| et \verb|db_to_hoas|. Réfléchir à
  des conditions de ``bonne conformation''.
\item Définir de même le type \verb|lambda| des lambda termes de
  manière a rendre la substitution fonctionnelle. Montrer qu'un
  tel type et des opérations Caml ``élémentaires'' permettent de construire
  une fonction divergente.
\end{enumerate}
\end{enumerate}

\vspace{1cm}

\noindent{\textbf{Exercice 4}}\\
On se propose d'enrichir le système $\lambda\upsilon$ pour prendre en
compte la composition. On considère ainsi la syntaxe
$$
\begin{array}{ccll}
M,N & ::= & \lambda M ~|~ M\,N ~|~ M[s] & (termes) \\
s,t & ::= & M/~|~s\oo t ~|~ \lift s ~|~ \shift &
(substitutions) \\
\end{array}
$$
et le système $\lambda\upsilon$ enrichi de la règle 
$$
M[s][t]~~\rar~~M[s\oo t] \qquad (Clos)
$$
\begin{enumerate}
\item Montrer que la résolution des paires critiques introduit les
  règles suivantes:
$$
\begin{array}{rcll}
(s\oo t)\oo u & \rar & s\oo (t\oo u) & (AssEnv) \\
M/\oo s & \rar & (\lift s)\oo M[s]/  & (MapSl) \\
0[M/] & \rar & M & (FVar) \\
0[(\lift s)\oo t] & \rar & 0[t] & (FVarLift2) \\
\shift\oo(\lift s) &\rar &s\oo \shift & (ShiftLift1) \\
\shift \oo ((\lift s)\oo t) & \rar &s \oo (\shift \oo t)  & (ShiftLift2) \\
(\lift s)\oo (\lift t) & \rar & \lift (s\oo t) & (Lift1) \\
(\lift s) \oo ((\lift t)\oo u) & \rar & (\lift (s\oo t))\oo u & (Lift2) \\
\end{array}
$$
\item On s'intéresse à la PSN de ce système:
\begin{enumerate}
\item Soient $M_0,N_0$ deux termes et $M_{n+1}=N_n$,
  $N_{n+1}=M_n[\shift\oo N_n]$. Montrer que $\shift\oo(M_n/(\shift\oo
  N_n/))~~\rar^{*}~~\shift\oo(M_{n+1}/\oo(\shift\oo N_{n+1}/))$.
\item En déduire que le terme $\lambda x((\lambda yz.x)\, x\,x)$ admet
  une réduction infinie.
\end{enumerate}
\end{enumerate}
\end{document}



