Logique combinatoire

Si M est un combinateur typé, alors toute chaine de réduction qui commence en M est finie. On appelle cette propriété la forte normalisation.

La formule

B : (α → β) → (γ → α) → γ → β

signifie (dans le langage de Coq, par exemple) que B est une preuve de la formule propositionnelle (α → β) → (γ → α) → γ → β.

B ≡ S (K S) K

fournit alors une preuve effective de la formule dans la théorie de Hilbert qui n'emploie que le modus ponens et les axiomes K et S.

Cela demande un petit travail de réécriture: Tout d'abord, on rétablit les parenthèses

B ≡ (S (K S)) K

ensuite, on introduit l'opérateur ⇒

B ≡ (S ⇒ (K ⇒ S)) ⇒ K

enfin, on emploie la notation postfixée :

B ≡ K S K ⇒ S ⇒ ⇒

Alors cette formule donne les étapes de la démonstration dans le sens de la déduction[10]. ⇒ dénote le recours au modus ponens ; K et S, l'utilisation des axiomes K et S. Plus, précisément Q ≡ I P ⇒ signifie que si I est la démonstration de P → Q, et P la démonstration de P, alors I P ⇒ est bien celle de Q. Malheureusement cette formule ne fournit pas les opérations de substitutions qui doivent être utilisées dans l'introduction des axiomes.

La notation préfixée,

B ≡ ⇒ ⇒ S ⇒ K S K

représente le sens de la démonstration dans le langage de Coq[11]. Ici, les informations manquantes sont les formules des P employés dans les modus ponens.

(*
demonstration à l'aide de Coq du syllogisme Barbara
par la logique propositionnelle a la Hilbert
*)
Section Logique_propositionnelle_a_la_Hilbert.
Variable P Q R : Prop.
(* le modus ponens *)
Ltac MP := fun P => match goal with
                      |- ?G => assert(TMP: P->G); [  | apply TMP;clear TMP]
                      end.
Ltac K := match goal with
           | |- (?P -> ?Q -> ?P) => tauto
           | |- _ => fail
          end.
Ltac S := match goal with
           | |- (?P -> ?Q -> ?R)->(?P->?Q)->?P->?R => tauto
           | |- _ => fail
          end.
(* syllogisme Barbara. *)
Theorem B : (P->Q)->(R->P)->(R->Q).
MP((P->Q)->(R->P->Q)).
MP((P->Q)->(R->P->Q)->((R->P)->(R->Q))).
S.
MP((R->P->Q)->((R->P)->(R->Q))).
K.
S.
K.
Qed.
End Logique_propositionnelle_a_la_Hilbert.

Notons ${\displaystyle [\![-]\!]_{\lambda }}$ la traduction des combinateurs vers le λ-calcul, elle est définie par :

• si ${\displaystyle x}$ désigne une variable, ${\displaystyle [\![x]\!]_{\lambda }=x}$ ;
• ${\displaystyle [\![{\mathsf {K}}]\!]_{\lambda }=\lambda x.\lambda y.x}$ ;
• ${\displaystyle [\![{\mathsf {S}}]\!]_{\lambda }=\lambda x.\lambda y.\lambda z.xz(yz)}$ ;
• ${\displaystyle [\![M\,N]\!]_{\lambda }=[\![M]\!]_{\lambda }\,[\![N]\!]_{\lambda }}$, pour tous combinateurs ${\displaystyle M}$ et ${\displaystyle N}$.

Avant de définir la représentation du λ-calcul en logique combinatoire nous avons besoin de définir une abstraction dans la logique combinatoire [12]. Si ${\displaystyle M}$ est un terme, on définit ${\displaystyle [x].M}$ qui va jouer le rôle de ${\displaystyle \lambda x.M}$.

${\displaystyle {\begin{array}{llcl}(a)&{[}x].M&=&{\mathsf {K}}M\qquad {\textrm {si}}~x\notin FV(M)\\(b)&{[}x].x&=&{\mathsf {I}}\\(c)&{[}x].Ux&=&U\qquad {\textrm {si}}~x\notin FV(U)\\(d)&{[}x].UV&=&{\mathsf {S}}([x].U)([x].V)\qquad {\textrm {si}}~{\textrm {ni}}~(a)~{\textrm {ni}}~(c)~{\textrm {ne}}~{\textrm {s'appliquent}}.\end{array}}}$

On définit l'interprétation des termes ${\displaystyle M}$ du λ-calcul en termes ${\displaystyle [\![M]\!]_{CL}}$ de la logique combinatoire:

${\displaystyle {\begin{array}{rcl}{[}\![x]\!]_{CL}&=&x\\{[}\![MN]\!]_{CL}&=&[\![M]\!]_{CL}[\![N]\!]_{CL}\\{[}\![\lambda x.M]\!]_{CL}&=&[x].[\![M]\!]_{CL}\end{array}}}$

Le combinateur de point fixe de Turing, noté ${\displaystyle \Theta }$ a pour expression en λ-calcul ${\displaystyle (\lambda x.\lambda y.y\,(x\,x\,y))\,(\lambda x.\lambda y.y\,(x\,x\,y))}$. On peut alors calculer :

${\displaystyle {\begin{array}{rcl}[\![\lambda y.y\,(x\,x\,y))]\!]_{CL}&=&[y].[\![y\,(x\,x\,y))]\!]_{CL}\\&=&S([y].[\![y]\!]_{CL})([y].[\![xxy]\!]_{CL})\\&=&SI([\![xx]\!]_{CL})\\&=&SI(xx)\end{array}}}$

puis

${\displaystyle {\begin{array}{rcl}[\![\lambda x.\lambda y.y\,(x\,x\,y))]\!]_{CL}&=&[x].[\![\lambda y.y\,(x\,x\,y))]\!]_{CL}\\&=&[x].SI(xx)\\&=&S([x].SI)([x].xx)\\&=&S(S([x].S)([x].I))(S([x].x)([x].x)\\&=&S(S(KS)(KI))(SII)\end{array}}}$

On définit alors deux combinateurs A et Θ

A:=S (S (K S) (K I)) (S I I)

Θ: =A A

Θ est un combinateur de point fixe.

On observe que, qu'il s'agisse du λ-terme ou de sa traduction en tant que combinateur, on a ${\displaystyle \Theta x~{\stackrel {*}{\longrightarrow }}~x(\Theta x)}$