\documentclass{article}

\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{latexsym}

\newcommand{\vDash}{\mathop{|\!\!\!=}}
\renewcommand{\phi}{\varphi}

\renewcommand{\S}{\textbf{S}}
\newcommand{\Un}{\textsf{\textbf{1}}}
\newcommand{\N}{\texttt{\small |}\!\textsf{N}}
\newcommand{\Y}{\mathbf{Y}}
\newcommand{\K}{\mathbf{K}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\T}{\mathbf{T}}
\newcommand{\F}{\mathbf{F}}
\newcommand{\jnt}{\uparrow}
\newcommand{\ou}{\ensuremath{\mathbf{ou}\ }}
\newcommand{\non}{\ensuremath{\mathbf{non}}}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\raraR}{\rarasub{R}}


\begin{document}

\title{Magistère d'Informatique et Modélisation}
\author{Partiel de Logique}

\date{\emph{14 novembre  2001}}

\maketitle 


\centerline{\textit{Documents autorisés.  Rédigez chaque partie sur
    une copie séparée}}

\section*{Exercice 1}

Donnez l'arbre de preuve en déduction naturelle de \[\vdash (\phi \vee
(\phi \Ra \bot)) \Rightarrow (((\phi \Ra
\psi)\Ra \phi) \Ra \phi).\]



\section*{Exercice 2}

Le $R$-graphe d'un terme $M$, noté $G_R(M)$, a pour support $\{N
\in\lambda ~|~ M\rara N\}$.  Il y a un arc entre $P$ et $Q$ dans
$G_R(M)$ si et seulement si $P \raR Q$.  S'il y a plusieurs redex dans
$P$ qui conduisent à un $R$-réduction menant à $Q$, alors il y a
plusieurs flèches dans $G_R(M)$ (en toute rigueur $G_R(M)$ est un
multigraphe).

\begin{enumerate}
\item Tracez  $G_\beta(W W W)$ quand $W \equiv \lambda x y \cdot x y y$.
  
\item $M$ est \emph{fortement $\beta$-normalisable} si toute
  $\beta$-réduction qui démarre en $M$ s'arrête.  Montrez que si $M$
  est fortement $\beta$-normalisable, alors $G_\beta(M)$ a un support
  fini et $M$ a une forme $\beta$-normale.  Que pensez-vous de la
  réciproque à savoir que ``si $M$ est $\beta$ fortement normalisable,
  alors $G_\beta(M)$ a un support fini et $M$ a une forme
  $\beta$-normale alors $M$ est fortement $\beta$-normalisable''?

\item Montrez qu'il n'y a pas de terme $M$ dont le graphe $G_\beta(M)$
  est :

  \begin{center}
    \begin{math}
      \xymatrix{
        & . \ar[ld]\ar[dr]\ar[d]&\\
        .\ar[dr] & . \ar[d]& .\ar[ld]\\
        & . & }
  \end{math}
\end{center}

%   C'est a dire.
%                .
%               /|\
%              / | \
%              . .  .
%              \ | /
%               \|/
%                .


\end{enumerate}



\end{document}
