Logique combinatoire - Définition

La logique combinatoire et la correspondance de Curry-Howard

On constate que le modus ponens

ressemble à la règle de conservation des types quand on applique un combinateur de type α → β à un combinateur de type α. Examinons aussi les deux premiers axiomes de la présentation à la Hilbert de la logique propositionnelle à savoir:

P → Q → P

(P → Q → R) → (P → Q) → P → R.

Rappelons qu'ils permettent de formaliser le calcul propositionnel intuitionniste. On remarque que le premier axiome est identique au type de K et que le deuxième axiome est identique au type de S si l'on remplace la proposition P par α, la proposition Q par β et la proposition R par γ. Cette correspondance entre proposition et type et entre combinateur et démonstration s'appelle la correspondance de Curry-Howard. Elle met en parallèle le système de déduction à la Hilbert pour la logique propositionnelle intuitionniste et la logique combinatoire qui ont été, notons-le, découverts indépendamment.