Comment le combinateur Y illustre-t-il «l'incohérence du calcul Lambda»?

44

Sur la page Wikipedia pour les combinateurs à point fixe est écrit le texte plutôt mystérieux

Le combinateur Y est un exemple de ce qui rend le calcul Lambda incohérent. Donc, il devrait être considéré avec suspicion. Cependant, il est prudent de considérer le combinateur Y lorsqu'il est défini uniquement en logique mathématique.

Suis-je entré dans une sorte de roman d'espionnage? Qu'entend-on par déclarations dans le monde que -calculus est "incohérent" et qu'il devrait être "considéré avec suspicion" ?λ

Ben I.
la source
3
FWIW, ce paragraphe est dans l'article Wikipedia depuis janvier 2014, date à laquelle il a été introduit dans cette réécriture massive de la quasi-totalité de l'article .
Ilmari Karonen

Réponses:

51

Il est inspiré d’événements réels, mais sa formulation est à peine reconnaissable et «devrait être considéré avec méfiance» n’a aucun sens.

La cohérence a un sens précis en logique: une théorie cohérente en est une où toutes les déclarations ne peuvent être prouvées. Danslogique classique, cela équivaut à l'absence d'une contradiction,savoir une théorie ne correspond pas si et seulement s'il y a une déclarationtelle que la théorierévèlefoiset sa négation.AA¬A

Alors qu'est-ce que cela signifie en ce qui concerne le calcul lambda? Rien. Le lambda calcul est un système de réécriture, pas une théorie logique.

Il est possible de visualiser le calcul lambda en relation avec la logique. Considérer les variables comme représentant une hypothèse dans une preuve, les abstractions lambda comme preuves sous une certaine hypothèse (représentée par la variable), et l’application comme assemblant une preuve conditionnelle et une preuve de l’hypothèse. La règle bêta correspond alors à la simplification d’une preuve en appliquant le modus ponens , principe fondamental de la logique.

Ceci, cependant, ne fonctionne que si la preuve conditionnelle est combinée avec une preuve de la bonne hypothèse. Si vous avez une preuve conditionnelle supposant que et que vous avez également une preuve de , vous ne pouvez pas les combiner ensemble. Si vous voulez que cette interprétation du calcul lambda fonctionne, vous devez ajouter une contrainte selon laquelle seules les preuves de l'hypothèse appropriée sont appliquées aux preuves conditionnelles. Cela s'appelle un système de types et la contrainte est la règle de typage qui dit que lorsque vous passez un argument à une fonction, le type de l'argument doit correspondre au type de paramètre de la fonction.n=3n=2

La correspondance de Curry-Howard est un parallèle entre les calculs typés et les systèmes de preuve.

  • les types correspondent à des déclarations logiques;
  • les termes correspondent aux preuves;
  • les types habités (c'est-à-dire qu'il existe un terme de ce type) correspondent à des énoncés vrais (c'est-à-dire qu'il existe une preuve de cet énoncé);
  • L’évaluation du programme (c’est-à-dire des règles telles que la version bêta) correspond à des transformations d’épreuves (qui auraient mieux permis de transformer les épreuves correctes en épreuves correctes).

Un calcul typé qui a un combinateur à point fixe tel que permet de construire un terme de tout type (essayez d'évaluer ). Ainsi, si vous prenez l'interprétation logique dans la correspondance de Curry-Howard, vous obtiendrez une théorie incohérente. Voir Le combinateur Y contredit-il la correspondance de Curry-Howard? pour plus de détails.YY(λx.x)

Ce n'est pas significatif pour le calcul lambda pur, c'est-à-dire pour le calcul lambda sans types.

Dans de nombreux calculs typés, il est impossible de définir un combinateur à point fixe. Ces calculs typés sont utiles en ce qui concerne leur interprétation logique, mais pas comme base pour un langage de programmation complet de Turing. Dans certains calculs typés, il est possible de définir un combinateur à point fixe. Ces calculs typés sont utiles comme base pour un langage de programmation complet de Turing, mais pas en ce qui concerne leur interprétation logique.

En conclusion:

  • Le lambda calcul n'est pas «incohérent», ce concept ne s'applique pas.
  • Un typé lambda - calcul qui attribue un type à chaque terme lambda est incompatible. Certains calculs lambda typés sont comme ça, d'autres rendent certains termes impossibles à typer et cohérents.
  • Les calculs lambda typés ne sont pas la seule raison d'être du calcul lambda, et même les calculs lambda typés incohérents sont des outils très utiles - mais non pour prouver des choses.
Gilles, arrête de faire le mal
la source
2
Wow, il y a beaucoup de choses à me défaire ici. Merci pour l'explication détaillée. Il va me falloir du temps pour essayer de tout comprendre.
Ben I.
4
Techniquement, l' affichage typées comme un i typé, vous pouvez faire une correspondance CH entre le calcul typées lambda et une logique. C'est juste une logique très, très ennuyeuse (et certainement incohérente). Les assistants de preuve comme NuPRL brouillent un peu les choses. Le langage objet de NuPRL contient le calcul lambda non typé et vous pouvez facilement définir le combinateur Y. NuPRL divise les choses un peu différemment, de sorte qu'il a un système de raffinement de type plutôt qu'un système de type. L'exercice ne consiste pas à produire des termes bien typés, mais à produire les dérivations de typage.
Derek Elkins
Est-ce juste moi, ou est-ce bizarre d'imposer le paradigme "propositions en tant que types" à un lambda calcul non typé? J'ai toujours vu des gens parler de logique dans le calcul lambda non typé en introduisant des objets spécifiques sous forme de valeurs booléennes trueet false, ainsi, les propositions étaient des objets qui produisaient des valeurs booléennes. (et ont été pris en considération que les propositions sur le domaine des choses où il fait sortir une valeur booléenne).
Trivial (prouve chaque affirmation) et contient des contradictions sont deux propriétés différentes. Bien qu'ils soient équivalents dans la logique classique, un système peut être incohérent et non trivial pour les logiques paraconsistantes.
Taemyr
1
"Incohérent", pour une logique basée sur le λ-calcul, signifie "assigne chaque type à un terme" et non "assigne un type à chaque terme" (bien que le premier découle du dernier); il existe de nombreux langages basés sur le λ-calcul qui correspondent à des logiques incohérentes mais où tous les termes du λ-calcul ne sont pas typables.
Jonathan Cast
6

Je voudrais ajouter un à ce que @Giles a dit.

La correspondance de Curry-Howard établit un parallèle entre termes (plus précisément, les types de termes ) et les systèmes de preuve.λλ

Par exemple, a le type (où signifie "fonction de à "), ce qui correspond à la déclaration logique . La fonction a le type , correspondant à . Nous pouvons convertir n'importe quel type de lambda-calcul en une tautologie logique par, dans un sens, un "filtrage" sur des fonctions.λx.λy.xa(ba)ababa(ba)λx.λy.xy(ab)(ab)(ab)(ab)

Le problème se pose lorsque nous considérons le combinateur Y, défini comme . Le problème se pose parce que nous nous attendons à ce que le combinateur Y, en tant que combinateur à "point fixe", ait le type (car il prend une fonction d'un type à ce même type et trouve un point pour cette fonction, qui a ce type). En convertissant cela en une instruction logique, on obtient . C'est une contradiction:λf.(λx.f(xx))(λx.f(xx))(aa)a(aa)a

(aa)aaa(¬a¬a)(¬a)¬a¬a

Si vous acceptez dans un système de types, le système de types devient incohérent. Cela signifie que nous pouvons soit(aa)a

  • Interdit les types tels que dans un système de types (cela vous donne le type simplement calculus ), ou(aa)aλ
  • Vivez avec le système de types incohérent en tant que système de déduction logique.
Orthographe non contextuelle
la source
1
CH associe des types à des propositions, des programmes à des preuves et même des réductions à des transformations de preuves. Il ne s'agit pas que de types. Ensuite, seuls les types habités correspondent aux tautologies. est un type de calcul lambda (polymorphe) même si aucun terme ne l’habite. En supposant que vous entendiez des types tels que , puis accepter de tels types convient parfaitement, la question est de savoir si ce type a un habitant ou non. Inversement, nous pouvons ajouter des termes primitifs au STLC, ce qui rendra la logique correspondante incohérente sans étendre le système de types. a,b.aba.(aa)a
Derek Elkins
@DerekElkins, quel genre de termes primitifs? Aussi, si je comprends bien, c'est juste pour supposer (a -> a) -> a est toujours habité qui produisent l'incohérence? Donc, il n'y a plus d'incohérence avec un langage de programmation qui nécessite une preuve de résiliation? Ou existe-t-il une autre source d'incohérence dans le calcul lambda non typé ou typé Hindley-Milner?
Hibou57
1
@ Hibou57 Termes primitifs, ie constantes, comme fix. Vous pouvez simplement affirmer qu'il ya une constante pour chaque type . Cela vous donnera déjà un système incohérent en ce qui concerne CH, car cela impliquerait que chaque type soit habité par . Vous pouvez également ajouter -rules pour faire calculer, ce qui transformerait, par exemple, le STLC avec naturals en un système complet de Turing, mais vous n'avez pas à ajouter ces règles de calcul, et le système serait toujours incohérent. fixAAfix(λx.x)δfix
Derek Elkins