Le calcul lambda et la logique combinatoire sont-ils les mêmes?

26

Je lis actuellement " Lambda-Calculus and Combinators " par Hindley et Seldin. Je ne suis pas un expert, mais je me suis toujours intéressé au calcul lambda en raison de son implication dans la programmation fonctionnelle (à commencer par Lisp et SICP, et maintenant avec R et Haskell).

Dans " Calcul binaire lambda et logique combinatoire" , John Tromp déclare:

La CL peut être considérée comme un sous-ensemble du calcul lambda ... les théories sont largement les mêmes, devenant équivalentes en présence de la règle de l'extensionnalité.

Dans quelles conditions utiliserait-on une logique combinatoire au lieu du lambda calcul ?

Toutes les références seraient appréciées.

combinatory-logic functional-programming lambda-calculus Shane
la source
Jetez un oeil à "Lambda calcul: sa syntaxe et sémantique" par HP Barendregt.
Kaveh

Réponses:

15

Ce qui distingue la logique combinatoire, c'est qu'elle est libre de variables. Ceci est parfois utile en métamathématique et en logique philosophique, où le statut des variables est délicat.

Il peut également être utile dans les implémentations, car la gestion des variables peut être un casse-tête. Cf., par exemple, Hughes, 1982, Super-combinators: A new implementation method for applicative languages

Charles Stewart
la source
3
La logique combinatoire n'est plus considérée comme utile dans les implémentations, et elle n'a jamais été utilisée car «la gestion des variables peut être un casse-tête». Des combinateurs et des variantes ont été utilisés pour implémenter la réduction des graphes pour les langages paresseux, mais de nos jours Haskell (le langage paresseux le plus important) utilise des techniques beaucoup plus raisonnables pour implémenter la réduction des graphes.
Blaisorblade
Voir par exemple S. Peyton Jones, 1992, "Implémentation de langages fonctionnels paresseux sur le matériel d'origine: la Spineless Tagless G-machine" - research.microsoft.com/copyright/accept.asp?path=/users/simonpj/…
Blaisorblade
2
@Blaisorblade: des combinateurs et des variantes ont été utilisés pour implémenter la réduction des graphes pour les langages paresseux - Attention: Haskell et ghc ne sont pas les mêmes, et la littérature contient plusieurs Haskells basés sur des supercombinateurs. Mais c'est vrai, l'état de l'art de la programmation fonctionnelle a trouvé les avantages d'efficacité de la gestion des environnements qui l'emportent sur sa complexité. Vous voyez toujours des supercombinateurs utilisés, par exemple, dans la programmation logique d'ordre supérieur, où ce n'est pas vrai. Les supercombinateurs font toujours partie de l'inventaire des techniques utilisées dans la mise en œuvre de la programmation d'ordre supérieur.
Charles Stewart
Les supercombinateurs évitent uniquement les variables libres, pas celles liées, donc à mon humble avis, elles ne peuvent pas être considérées comme des utilisations de la logique combinatoire en soi. Ce sont surtout des termes lambda spéciaux. Il y a des différences beaucoup plus petites entre les supercombinateurs, les programmes lambda-levés (s'il y en a, pas sûr) et la mise en œuvre de GHC (où les pointeurs d'une fermeture vers ses variables libres peuvent être copiés à partir de la fonction hôte, grâce à la pureté). Cela dit, je pensais également au récent Utrecht Haskell Compiler, qui est très similaire au GHC, mais l'IIRC utilise le lambda-lifting; ce n'est pas encore CL.
Blaisorblade
Je ne connaissais pas la programmation logique d'ordre supérieur - j'ai trouvé cet article dessus: springerlink.com/content/t68777w270713p5n . Malheureusement, il est peu probable que j'aurai le temps de le lire.
Blaisorblade
4

En me référant au commentaire de John Tromp, je veux remarquer que la logique combinatoire est très différente du calcul lambda. Puisque votre intérêt découle de la programmation fonctionnelle, vous ne voulez vraiment pas en savoir beaucoup sur la logique combinatoire.

Mon tutoriel préféré sur la logique combinatoire se trouve dans ces notes de cours de l'Université de Cambridge.

Cependant, ils sont introduits pour expliquer la mise en œuvre de langages dits paresseux (ou applicatifs); comme mentionné dans mon commentaire précédent, ces techniques sont désormais obsolètes.

Blaisorblade
la source
Étant donné que les langages combinatoires ne sont plus utilisés pour implémenter des langages paresseux / applicatifs, quelles sont les techniques de pointe actuellement? Et existe-t-il un nom / une catégorie pour classer ces techniques?
CMCDragonkai
@CMCDragonkai Voir les commentaires sur cstheory.stackexchange.com/a/306/989 pour discussion. La réponse pratique courte est "voir les articles sur ce que fait GHC": il existe une variété de techniques différentes (y compris la machine STG et des optimisations telles que l'analyse de rigueur) qui sont combinées pour rendre les programmes paresseux rapides.
Blaisorblade