La logique combinatoire est une notation introduite par Moses Schönfinkel et Haskell Curry pour supprimer le besoin de variables en mathématiques et pour minimiser le nombre d'opérateurs nécessaires pour définir le calul des prédicats à la suite de Henry M. Sheffer. Plus récemment elle a été utilisée en informatique comme modèle théorique de calcul et comme base pour la conception de langages de programmation fonctionnels.
Elle est basée sur les combinateurs, qui sont des fonctions d'ordre supérieur qui utilisent uniquement l'application de fonctions et éventuellement d'autres combinateurs pour définir un résultat à partir de leurs arguments. Elle a des liens très forts avec le lambda calcul avec la logique intuitionniste grâce à la correspondance de Curry-Howard.
Ensembles de combinateurs
L'exemple le plus simple est le combinateur I (identité) défini par
- (I x) = x
Un autre combinateur simple est K, qui fabrique des fonctions constantes : (K x) est la fonction qui, pour tout paramètre, retourne x, autrement dit
- ((K x) y) = x
- (K x y) = x
- (S x y z) = (x z (y z))
Remarquez qu'une fois qu'on a S et K, I devient inutile puisqu'il peut être reconstruit :
- ((S K K) x)
- = (S K K x)
- = (K x (K x))
- = x
Bibliographie
- Haskell Curry et Robert Feys, Combinatory Logic I. North Holland 1958. La plupart du contenu de cet ouvrage fut rendu obsolète par l'ouvrage de 1972 et les suivants.
- H. Curry, J. R. Hindley etJ. P. Seldin, Combinatory Logic II. North-Holland, 1972. Une rétrospective complète de la logique combinatoire, incluant une approche chronologique.
- Jean-Pierre Ginisti, La logique combinatoire, Paris, PUF (coll. « Que sais-je? » n°3205), 1997, 127 p.
- M. Shönfinkel, In: J. van Heijenoort, Editor, From Frege to Gödel, Harvard University Press, Cambridge, MA (1967), pp. 355–366 1924.
- J.-L. Krivine, Lambda-calcul, types et modèles, Masson, 1990, chap. Logique combinatoire, traduction anglaise accessible sur le site de l'auteur [1]
.
