%% Time-stamp: <modifié par Pierre Lescanne le 27 Nov 2002 à 16h35>
%% /MIM-1/REECRITURE/TERMINAISON/terminaison.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\slidesmag{5}

\usepackage{amsfonts,amsmath,amsthm}
\usepackage{fancybox}
%\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips


\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\color{red}{\textit{Logique cominatoire}}}

\author{}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\definecolor{mauve}{rgb}{1,0,1}
\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\renewcommand{\emph}[1]{\rouge{#1}}

%--- symboles ---
\renewcommand{\phi}{\varphi}
\newcommand{\Emb}{\bl{\ensuremath{\cal EMB}}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\shat}{\ensuremath{\hat{\sigma}}}
\newcommand{\pref}{\mathop{\textbf{\textsl{prefix}}}}
\newcommand{\IN}{\ensuremath{\mathcal{IN}}}
\newcommand{\gtmult}{\ensuremath{>_{mult}}}
\newcommand{\dminus}{\mbox{\ensuremath{\stackrel{\raisebox{+.01ex}{.}}{-}}}}
%\newcommand{\Nat}{\textsf{I}\hspace{-.7pt}\textsf{N}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Natstar}{\Nat_\star}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\newcommand{\M}{{\cal M}}
\newcommand{\Ra}{\ensuremath{\mathop{\Rightarrow}}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\set}[2]{\{#1~|~#2\}}
\newcommand{\da}{\downarrow}
\newcommand{\jgbl}{\mathop{\da}}
\newcommand{\lpo}{<_{lpo}}
\newcommand{\lepo}{\le_{lpo}}
\newcommand{\SCL}{\bl{\textsf{S}}}
\newcommand{\ICL}{\bl{\textsf{I}}}
\newcommand{\KCL}{\bl{\textsf{K}}}
\newcommand{\interpl}[1]{\llbracket#1\rrbracket_{`l}}
\newcommand{\interpCL}[1]{\llbracket#1\rrbracket_{CL}}


%\newcommand{\inferTwoLabel}[4]{\bl{
% {#1} \quad 
% \begin{array}{c}
%   #2 \hspace{2em} #3\\
%   \hline \noalign{\vskip 1pt}#4
%  \end{array}}}

%\newcommand{\leafLabel}[2]{\bl{
% {#1} \quad
%  \begin{array}{c}
%  #2
%  \end{array} }}

%\newcommand{\inferLabel}[3]{
%    \rouge{#1} \quad 
%    \bl{\begin{array}{c}
%      #2\\
%      \hline \noalign{\vskip 1pt}#3
%    \end{array}
%  }}
\newenvironment{bdp}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}
    
\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

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

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

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

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix{\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix{\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix{\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{+} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raE}{\rasub{E}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\Rar}{\subar{R}}
\newcommand{\rastarR}{\rasupsub{*}{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}
\newcommand{\remb}{\rasub{\Emb}}
\newcommand{\plgt}{\rasupsub{+}{\Emb}}
\newcommand{\plonge}{\xymatrix{\ar@{<-}[r]_{\Emb}^{*} &}}

%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{mauve}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

%\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
%  \begin{center}                % mais ca peut t'interesser
%    \large\bf
%    \color{cyan}{\shadowbox{#1}}%
%  \end{center}
%  \markright{#1}
%  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{green}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}
%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 
\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%%------------------------------------------------------
%\begin{slide}
%  \begin{center}
%    {\large \bf \color{green}{\textit{Indécidabilité de la terminaison}}}
%\end{center}
%\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique combinatoire}
Il s'agit d'une structure algébrique avec trois opérateurs.
\begin{itemize}
\item \VERT{Un opérateur binaire} l'\emph{application},
\item \VERT{Deux constantes} \bleu{\textsf{S}} et \bleu{\textsf{K}}.
\end{itemize}

\begin{eqnarraybleu}
  M, N &::=& \SCL ~|~ \KCL  ~|~ x ~|~ M~N
\end{eqnarraybleu}

Forment les \emph{CL-termes.}

Si \bleu{M} et \bleu{P} sont deux CL-termes on
note l'application de \bleu{M} à  \bleu{P} tout simplement par la 
concaténation soit \bleu{M\;P}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique combinatoire}
On définit deux règles de réduction 
\bl{
  \begin{eqnarray*}
    \SCL x y z &\rasub{CL} & xz (yz)\\
    \KCL x y  &\rasub{CL} & x
  \end{eqnarray*}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La logique combinatoire}
On définit deux règles de réduction 
  \begin{eqnarraybleu}
    \SCL x y z &\rasub{CL} & xz (yz)\\
    \KCL x y  &\rasub{CL} & x
  \end{eqnarraybleu}
\begin{scriptsize}
    \xymatrix @C 1 pt @R 5pt{
      &&& \ar@{-}[ld]\ar@{-}[rd]\\
      && \ar@{-}[ld]\ar@{-}[rd] && x &&&&&&&\ar@{-}[rrd]\ar@{-}[lld]\\
      &\ar@{-}[ld]\ar@{-}[rd] && y && \ar[rr] %
      &&&&\ar@{-}[ld]\ar@{-}[rd]&&&&\ar@{-}[ld]\ar@{-}[rd] \\
      \SCL && z &&&&&& x && z && y && z} %
\qquad \quad
    \xymatrix @C 1 pt @R 5pt{
      &&\ar@{-}[ld]\ar@{-}[rd]\\
      &\ar@{-}[ld]\ar@{-}[rd] && y&& \ar[rr] &&& x\\
      \KCL && x}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques termes}
\begin{eqnarraybleu}
  \SCL \KCL \KCL x & \rasub{CL} & \KCL x (\KCL  x)\\
  & \rasub{CL} & x
\end{eqnarraybleu}
On appelle très naturellement ce terme \bleu{\ICL} et on retient la règle 
\begin{eqnarraybleu}
  \ICL x &\rarasub{CL} & x
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques termes}
On remarque que 
\begin{eqnarraybleu}
  \SCL \ICL \ICL x &\rasub{CL} & \ICL x (\ICL x) \\
  &\rasub{CL} & x~ x
\end{eqnarraybleu}
donc 
\begin{eqnarraybleu}
  \SCL \ICL \ICL (\SCL \ICL \ICL)  &\rarasub{CL} &   \SCL \ICL \ICL (\SCL \ICL \ICL)    
\end{eqnarraybleu}

\bleu{\SCL \ICL \ICL} correspond à \bleu{`w} et \bleu{\SCL \ICL
  \ICL(\SCL \ICL \ICL)} correspond à \bleu{`W}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques termes}
\begin{eqnarraybleu}
  \SCL (\KCL \SCL) \KCL~ x y z &\rasub{CL} & \KCL \SCL x (\KCL x) y z \\
  &\rasub{CL} & \SCL (\KCL x) y z\\
  &\rasub{CL} & \KCL x z (y z)\\
  &\rasub{CL} & x (y z).
\end{eqnarraybleu}
Donc \bleu{ \SCL (\KCL \SCL) \KCL} équivaut à \bleu{B `= `l x y z . x (y z)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Questions}
Quel combinateur satisfait \bleu{\textsf{F} x y \rasub{CL} y}~?

Que vaut 
\begin{displaymathbleu}
  \SCL (\textsf{B} \textsf{B} \SCL) (\KCL \KCL) ?
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Types}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Typage}
On a tout d'abord:
\begin{eqnarraybleu}
  &"|-"& \SCL :  (`a "->" `b  "->" `g) "->" (`a "->" `b)"->" `a "->" `g\\
  &  "|-" & \KCL :   `a "->" `b  "->" `a.
\end{eqnarraybleu}
Associé à la règle 
\begin{displaymathbleu}
  \prooftree
  "|-" \emph{M:} `s "->"  `t \qquad "|-" \emph{N:} `s %
  \justifies "|-" \emph{M N:} `t
  \using \VERT{(App)}
  \endprooftree
\end{displaymathbleu}
on voit qu'on a une correspondance de Curry-Howard entre la logique
combinatoire et la logique propositionnelle intuitionniste à la Hilbert.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Typage}
On a de plus 
\begin{eqnarraybleu}
  &  "|-" & \ICL  :  `a "->" `a \\
  &  "|-" & \textsf{B}  :   (`a "->" `b)  "->"  (`g "->" `a)  "->" `g "->" `b,\\
   x : `a "->" `b  "->" `g &  "|-" & \SCL ~x  :  (`a "->" `b)"->" `a "->" `g
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Correspondance avec le lambda-calcul}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Des CL-termes vers les $`l$-termes }%
On peut donner une interprétation \bleu{\interpl{\_}} des CL-termes
vers les lambda-termes.
\begin{eqnarraybleu}
  \interpl{\KCL} & = & `l x y . x\\
  \interpl{\SCL} & = & `l x y z. x~z~(y~z)\\
  \interpl{M_1~M_2} & = &\interpl{M_1}~\interpl{M_2}\\
  \interpl{x} & = & x
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Des CL-termes vers les $`l$-termes }%
Cette interprétation préserve les types.

Autrement dit si \bleu{M} est le terme de preuve de \bleu{`s} dans la
logique propositionnelle intuitionniste à la Hilbert, %
\ali alors \bleu{\interpl{M}} est terme de preuve de \bleu{`s} dans la
déduction naturelle pour la logique propositionnelle intuitionniste. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Abstractions dans les CL-termes}%
On définit une opération d'abstraction \bleu{[x]. M} sur les CL-termes
de la façon suivante

Si \bleu{x\notin FV(M)} alors 
\begin{eqnarraybleu}
  [x]. M & =&  \KCL M
\end{eqnarraybleu}
sinon
\begin{eqnarraybleu}
  [x] . (M_1 ~ M_2) & = & \SCL ~([x] . M_1) ~ ([x] . M_2)\\ %
  {[x]} . x & = & \ICL
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Abstractions dans les CL-termes}%
Par exemple,
\begin{eqnarraybleu}
  [x] . \KCL &=& \KCL~\KCL \\[2pt]  
  [x] . \SCL~ x  & = & \SCL~ ([x] . \SCL)~([x] . x) \\
  & = & \SCL~ (\KCL~\SCL)~ \textsf{I}
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Abstractions dans les CL-termes}%
\begin{eqnarraybleu}
  [x] . [y] . \KCL~x~y &=& [x] . \SCL ~ ([y]. (\KCL~x))~ ([y]. y) \\
  &=& [x] . \SCL ~ (\KCL~(\KCL~x))~ \ICL \\
  &=& \SCL ~ ([x] . \SCL)~([x] . (\KCL~(\KCL~x))~ \ICL) \\
  &=& \SCL ~ (\KCL~\SCL)~(\SCL ~ ([x] . (\KCL~(\KCL~x))) ~ ([x] . \ICL)\\
  &=& \SCL ~ (\KCL~\SCL)~(\SCL ~ (\SCL ([x] . \KCL)~([x]
  . (\KCL~x))~(\KCL~\ICL)\\
  &=& \SCL ~ (\KCL~\SCL)~(\SCL ~ (\SCL (\KCL~
  \KCL)~(\SCL~(\KCL~\KCL)~\ICL))~(\KCL~\ICL)
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Typage des abstractions}%
\parbox{18cm}{\fbox{Si \bleu{x: `s, `G "|-" M : `t} alors \bleu{`G
      "|-" [x]. M : `s "->" `t}.}} 

Par induction sur la structure de \bleu{M}.

\begin{itemize}
\item si  \bleu{x\notin FV(M)} alors \bleu{`G "|-" \KCL  M : `s "->"
      `t} pour n'importe quel \bleu{`s}.
  \item si \bleu{x\in FV(M)} et \bleu{M `= M_1~M_2} alors par
    induction \bleu{x: `s, `G "|-" M_1 : `r "->" `t} et \bleu{x: `s,
      `G "|-" M_1 : `r} et \bleu{`G "|-" [x]. M_1 : `s "->" `r "->"
      `t} et \bleu{`G "|-" [x]. M_2 : `s "->" `r}.  On prend
    \bleu{\SCL : (`s "->" `r "->" `t) "->" (`s "->" `r) "->" `s "->"
      `t}.  Par conséquent \bleu{`G "|-" \SCL~ [x]. M_1~ [x]. M_2 : `s "->"
      `t}.  C. Q. F. D. 
  \item si \bleu{x\in FV(M)} et \bleu{M `= x} alors \bleu{`G "|-"
      \ICL:`s "->" `s}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Réduction}%
\parbox{12cm}{\fbox{\bleu{([x] . M)~N \rasub{CL} M[x:=N]}}}

\emph{Démonstration:} Par induction sur la définition de \bleu{[x] .
  M}.
\begin{itemize}
\item si  \bleu{x\notin FV(M)} alors 
  \begin{eqnarraybleu}
    ([x] . M)~N &`=& \KCL~M~N \\
    &=& M = M[x:=N].
  \end{eqnarraybleu}
\item si \bleu{x\in FV(M)} et \bleu{M `= x} alors \bleu{[x] . M `= I}
  et \bleu{([x] . M)~N = N = x [x:=N]}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Réduction}%
\parbox{12cm}{\fbox{\bleu{([x] . M)~N \rasub{CL} M[x:=N]}}}
\begin{itemize}
  \item si \bleu{x\in FV(M)} et \bleu{M `= M_1~M_2} alors par
    induction 
    \begin{eqnarraybleu}
      ([x]. M_1~M_2)~N &=& \SCL~([x]. M_1)~([x]. M_2)~N \\
      & \rasub{CL} &(([x]. M_1)~N)~(([x]. M_2)~N) \\
      &=& M_1[x:=N]~ M_2[x:=N] \\
      &=&  (M_1~ M_2)[x:=N].
\end{eqnarraybleu}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Des $`l$-termes vers les CL-termes}%
On peut donner une interprétation \bleu{\interpCL{\_}} des lambda-termes
vers les CL-termes.
\begin{eqnarraybleu}
  \interpCL{`l x . M} & = & [x] .  \interpCL{M} \\
  \interpCL{M_1~M_2} & = &\interpCL{M_1}~\interpCL{M_2}\\
  \interpCL{x} & = & x
\end{eqnarraybleu}
\vfill
On a \bleu{M \rabeta N} implique \bleu{\interpCL{M} \rasub{CL} \interpCL{N}}.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Des $`l$-termes vers les CL-termes}%
Cette interprétation préserve les types.

Autrement dit si \bleu{M} est le terme de preuve de \bleu{`s} dans la
déduction naturelle de la 
logique propositionnelle intuitionniste %
\ali alors \bleu{\interpl{M}} est terme de preuve de \bleu{`s} dans la
logique propositionnelle intuitionniste à la Hilbert.  %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Des $`l$-termes vers les CL-termes}%
La taille de \bleu{\interpCL{M}} est en \bleu{O(3^n)} où
\bleu{n} est la taille de \bleu{M}.

Clairement, \bleu{\interpCL{\interpl{M}}} n'est pas en général égal à \bleu{M}.
\vfill 
\end{slide}
\end{document}
