Cet article suggère qu'il existe des combinateurs (représentant des calculs symboliques) qui ne peuvent pas être représentés par le calcul Lambda (si je comprends bien les choses):
Il y a plusieurs choses que l'on peut vouloir faire dans la pratique et qui ne peuvent pas être exprimées directement dans le calcul lambda.
Le calcul SF est un exemple. Son pouvoir expressif n'est pas une nouveauté; la partie intéressante de l'article (non montrée dans les diapositives) est la théorie des catégories derrière elle. Le calcul SF est analogue à une implémentation lisp où vous autorisez les fonctions à inspecter la représentation de leur argument - vous pouvez donc écrire des choses comme (print (lambda (x) (+ x 2)))⟹ "(lambda (x) (+ x 2))".
Un autre exemple important est le parallèle de Plotkin ou . Intuitivement, il y a un résultat général qui déclare que le calcul lambda est séquentiel: une fonction qui prend deux arguments doit en choisir un pour évaluer d'abord. Il est impossible d'écrire un terme lambda ortel que ( or⊤ ⊥) ⟹ ⊤, ( or⊥ ⊤) ⟹ ⊤ et or⊥ ⊥ ⟹ ⊥ (où ⊥ est un terme sans terminaison et ⊤ est un terme en terminaison). Ceci est connu comme «parallèle ou» car une implémentation parallèle pourrait faire une étape de chaque réduction et s'arrêter chaque fois qu'un des arguments se termine.
Une autre chose que vous ne pouvez pas faire dans le calcul lambda est l'entrée / sortie. Vous devez lui ajouter des primitives supplémentaires.
Bien sûr, tous ces exemples peuvent être représentés dans le calcul lambda en ajoutant un niveau d'indirection, représentant essentiellement les termes lambda sous forme de données. Mais alors le modèle devient moins intéressant - vous perdez la relation entre les fonctions dans le langage modélisé et les abstractions lambda.
La réponse à votre question dépend de la façon dont vous définissez les «calculs» et «représentés». Le thread sur LtU mentionné par sclv , d'autre part, se compose principalement de personnes qui se parlent en raison de définitions mal alignées de divers termes.
La distinction n'est certainement pas celle de la puissance de calcul - chaque système considéré est équivalent à Turing. Le problème est que la simple équivalence de Turing ne dit rien sur la structure ou la sémantique d'une expression. D'ailleurs, dans les modèles de calcul extrêmement minimalistes qui nécessitent des encodages complexes ou des états initiaux non triviaux, il peut même ne pas être clair si un système est capable de calcul universel, ou si une illusion d'universalité est créée par l'interprétation du système par quelqu'un. . Par exemple, consultez cette discussion sur la liste de diffusion concernant une machine de Turing à 2 états et 3 symboles, en particulier les préoccupations soulevées par Vaughan Pratt.
En tout cas, la distinction établie est entre quelque chose comme:
L'équivalence de Turing implique seulement qu'un système remplit le troisième critère pour toute fonction calculable, alors que c'est le plus souvent le premier critère qui nous intéresse, dans un système formel de logique ou un langage de programmation (dans quelle mesure ceux-ci diffèrent réellement).
C'est une description très informelle, mais l'idée essentielle peut être définie plus précisément. Dans le thread LtU susmentionné, vous trouverez quelques références à des travaux existants dans le même sens.
La logique combinatoire de Schönfinkel et le λ-calcul de Church ont été initialement conçus comme des abstractions distillées du raisonnement logique, et en tant que tels, leur structure correspond très bien au raisonnement logique et vice versa. Ils portent également une hypothèse d' extensionnalité , telle que décrite par la règle de réduction éta:, λx. f xoù xne se produit pas dans f, équivaut à juste fseul.
Dans la pratique, une notion très stricte d'extensionnalité peut être trop limitative, tandis que l'intensionnalité non restreinte rend le raisonnement local sur les sous-expressions difficile ou impossible.
Le SF-calcul est un calcul combinateur modifié qui fournit, en tant qu'opération primitive, une forme limitée d'analyse intensionnelle: la capacité de déconstruire des expressions partiellement appliquées, mais pas des valeurs primitives ou des expressions non normalisées. Cela arrive à bien correspondre à des idées comme la correspondance de motifs que l'on trouve dans les langages de programmation de style ML ou les macros comme dans Lisps, mais ne peut pas être décrite dans le calcul SK ou λ sans, en fait, implémenter un interpréteur pour évaluer les termes "intensionnels".
Donc, en résumé: le SF-calcul ne peut pas être représenté directement dans le λ-calcul dans le sens où la meilleure représentation possible implique très probablement la mise en œuvre d'un interprète SF-calcul, et la raison en est une différence sémantique fondamentale: les expressions ont-elles des internes ou sont-ils définis uniquement par leur comportement extérieur?
Le calcul SF de Barry Jay est capable d'examiner la structure des termes auxquels il est appliqué, qui n'est pas fonctionnelle. Le calcul lambda et la logique combinatoire traditionnelle sont purement fonctionnels et ne peuvent donc pas le faire.
Il existe de nombreuses extensions du lambda-calcul qui font des choses qui violent la pureté, dont la plupart nécessitent de corriger la stratégie de réécriture dans une certaine mesure, comme l'ajout d'état, de contrôles (par exemple via des continuations) ou de variables logiques.
la source