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

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

\begin{document}

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

\date{\emph{7 décembre  2000}}

\maketitle 


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

\section*{Exercice 1}

Soit les deux termes $\I\equiv \lambda x . x$ et l'entier
de Church $\Un$ correspondant à 1.

\begin{enumerate}

\item Rappelez la forme de \Un.
\item Montrez que $I\conv{\beta\eta} \Un$
  
\item Considérons la conversion $\conv{\I\Un}$ obtenue en ajoutant à la
    $\beta$-conversion $\conv{\beta}$ l'égalité $\I \conv{\I\Un} \Un$.
    Donnez les règles d'inférence qui la définissent.
\item Montrez que $\conv{\I\Un} = \conv{\beta\eta}$.

\end{enumerate}

\section*{Exercice 2}

On écrit $M\jnt N$ si il existe $L$ tel que $L\rarabeta M$ et
$L\rarabeta N$.

\begin{enumerate}
\item Montrez que $(\lambda x . a x) b \jnt (\lambda y . y b) a$.
\item Montrez que $(\lambda x . x c) c \jnt (\lambda x . x x) c$.
\end{enumerate}

\section*{Exercice 3}

Donnez l'arbre de preuve en déduction naturelle de $p \vee (q \vee r)
\Rightarrow (p \vee q) \vee r$.

\end{document}
