Logique combinatoire
Un article de Wikipédia, l'encyclopédie libre.
Vous avez de 
Cet article s'occupe de logique combinatoire, au sens qu'a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu avec ce que l'on appelle logique combinatoire en électronique.
La logique combinatoire est une notation introduite par Moses Schönfinkel et Haskell Curry pour supprimer le besoin de variables en mathématiques. Plus récemment elle a été utilisé 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.
[modifier] Ensembles de combinateurs
L'exemple le plus simple est le combinateur I (identité) défini par
- (I x) = x
pour tout terme 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
pour tous termes x et y. Ou en suivant la même convention de notation que dans le lambda-calcul :
- (K x y) = x
Le troisième combinateur S est une version généralisée de l'application :
- (S x y z) = (x z (y z))
S applique x à y après les avoir appliqués à 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
pour tout terme x.
[modifier] Bibliographie
- Jean-Pierre Ginisti, La logique combinatoire, Paris, PUF (coll. « Que sais-je? » n°3205), 1997, 127 p.
