Comment rendre la Lambda Calculus forte normalisante sans système de type?

Je peux penser à quelques réponses possibles provenant de la logique linéaire.

Le plus simple est le lambda-calcul affiné: considérons uniquement les termes lambda dans lesquels chaque variable apparaît au plus une fois. Cette condition est préservée par réduction et il est immédiat de voir que la taille des termes affines diminue strictement à chaque étape de réduction. Par conséquent, le lambda-calcul affiné non typé se normalise fortement.

Des exemples plus intéressants (en termes d'expressivité) sont donnés par les lambda-calculs dits «légers», issus des sous-systèmes de logique linéaire introduits par Girard dans «Light Linear Logic» (Information et calcul 143, 1998), ainsi comme "Soft Linear Logic" de Lafont (Théorie Informatique 318, 2004). Il existe plusieurs de ces calculs dans la littérature, peut-être une bonne référence est le "calcul lambda léger affine et normalisation forte du temps polynomial" de Terui (Archive for Mathematical Logic 46, 2007). Dans cet article, Terui définit un lambda-calcul dérivé de la logique affine légère et prouve un fort résultat de normalisation pour cela. Même si les types sont mentionnés dans l'article, ils ne sont pas utilisés dans la preuve de normalisation. Ils sont utiles pour une formulation soignée de la propriété principale du lambda-calcul léger affine, à savoir que les termes d'un certain type représentent exactement les fonctions Polytime. Des résultats similaires sont connus pour le calcul élémentaire, en utilisant d'autres lambda-calculs "légers" (l'article de Terui contient d'autres références).

En remarque, il est intéressant de noter que, en termes de théorie de la preuve, le lambda-calcul affiné correspond à une logique intuitionniste sans la règle de contraction. Grishin a observé (avant l'introduction de la logique linéaire) qu'en l'absence de contraction, la théorie naïve des ensembles (c'est-à-dire avec une compréhension sans restriction) est cohérente (c'est-à-dire que le paradoxe de Russel ne donne pas de contradiction). La raison en est que l'élimination des coupures pour la théorie naïve des ensembles sans contraction peut être prouvée par un argument simple de diminution de taille (comme celui que j'ai donné ci-dessus) qui ne repose pas sur la complexité des formules. Via la correspondance Curry-Howard, c'est exactement la normalisation du lambda-calcul affine non typé. C'est en traduisant le paradoxe de Russel en logique linéaire et en "peaufinant" les modalités exponentielles afin qu'aucune contradiction ne puisse être dérivée que Girard a proposé une logique linéaire légère. Comme je l'ai mentionné ci-dessus, en termes de calcul, la logique linéaire légère donne une caractérisation des fonctions calculables en temps polynomial. En termes de théorie de la preuve, une théorie cohérente des ensembles naïfs peut être définie dans une logique linéaire légère telle que les fonctions prouvées totales sont exactement les fonctions calculables en temps polynomial (il y a un autre article de Terui à ce sujet, "Light affine set theory: A naive théorie des ensembles du temps polynomial ", Studia Logica 77, 2004).

Damiano Mazza
la source

Je dirais que Light Affine Lambda Calculus de Terui est typé, étant donné les restrictions sur l'utilisation des variables affines, les opérateurs de lettrage étant stratifiés et la monoïdité de l'opérateur!. C'est juste que ces restrictions sont introduites de manière informelle. Le LLL de Girard est également tapé.

Martin Berger

@Martin: Je ne suis pas d'accord. Les contraintes structurelles imposées aux termes affines légers sont de nature différente de celles d'un système de typage. La plus grande différence est que le typage est nécessairement inductif alors que la formation de puits (c'est-à-dire la stratification, l'utilisation affine, etc.) peut être définie comme une propriété combinatoire d'un terme. Ainsi, par exemple, lorsque vous tapez un terme, vous devez généralement taper ses sous-termes, tandis qu'un sous-terme d'un terme stratifié n'a pas besoin d'être stratifié.

Damiano Mazza

Désolé, une dernière chose à propos de LLL de Girard: le système est évidemment typé car il implique des formules. Cependant, comme je l'ai mentionné dans ma réponse, les formules ne jouent aucun rôle dans l'élimination des coupures LLL. En fait, des points fixes de formules arbitraires peuvent être ajoutés (y compris la formule paradoxale de Russel, qui équivaut à sa propre négation!) Sans que LLL devienne incohérent. En effet, l'élimination de coupure est valable pour des raisons "purement structurelles", indépendamment du fait que vous pouvez attacher des types à vos preuves (techniquement, le théorème d'élimination de coupure pour LLL peut être prouvé dans des réseaux de preuve non typés).

Damiano Mazza

OK, si vous faites de l'inductance une condition pour que quelque chose soit un système de frappe. C'est un point de vue intéressant que je n'avais jamais rencontré auparavant.

Martin Berger

... et c'est un point de vue que je dirais erroné. Par exemple, dans les systèmes impliquant le sous-typage (plus généralement, lorsque l'on considère une interprétation extrinsèque des types au sens de Reynolds), il est très naturel d'avoir une vision coinductive du typage. Il existe de nombreux exemples dans la littérature (même si je pense que cela est sous-estimé).

Noam Zeilberger

L'article original de Church et Rosser, «Certaines propriétés de conversion», décrit quelque chose qui peut être un exemple de ce que vous recherchez.

$\lambda x.M$ $x$ $M$

$B$ $A$ $m$ $A$ $B$ $m$

Ainsi, même si vous pouvez écrire des termes sans terminaison dans le calcul lambda strict (non typé), chaque terme de forme normale se normalise fortement; c'est-à-dire que chaque séquence de réductions atteindra cette forme normale unique.

Rob Simmons
la source

m

$m$

Fini l'énoncé du théorème cette fois-ci, merci. La partie que j'ai écrite comme [équivalence modulo alpha] était à l'origine "(dans les applications de la règle I)", ce qui signifie la même chose à moins que je ne me souvienne pas correctement de la règle I.

Rob Simmons

Comment rendre la Lambda Calculus forte normalisante sans système de type?

Réponses: