Explication simple de la raison pour laquelle certaines fonctions calculables ne peuvent pas être représentées par un terme tapé?

En lisant l'article An Introduction to the Lambda Calculus , je suis tombé sur un paragraphe que je ne comprenais pas vraiment, à la page 34 (en italique):

Dans chacun des deux paradigmes, il existe plusieurs versions de calcul lambda typé. Dans de nombreux systèmes importants, en particulier ceux de l'Église, il est vrai que les termes qui ont un type possèdent toujours une forme normale. Par l'insolvabilité du problème d'arrêt, cela implique que toutes les fonctions calculables ne peuvent pas être représentées par un terme typé, voir Barendregt (1990), Théorème 4.2.15. Ce n'est pas si mauvais que cela puisse paraître, car pour trouver de telles fonctions calculables qui ne peuvent pas être représentées, il faut se tenir debout. Par exemple, en 2, le calcul lambda typé du second ordre, seules les fonctions récursives partielles ne peuvent pas être représentées qui se trouvent être totales, mais ce n'est pas prouvable dans l'analyse mathématique (arithmétique du second ordre).

Je connais la plupart de ces concepts, mais pas le concept d'une fonction récursive partielle, ni le concept d'une fonction prouvée totale. Cependant, ce n'est pas ce que je souhaite apprendre.

Je cherche une explication simple pour expliquer pourquoi certaines fonctions calculables ne peuvent pas être représentées par un terme tapé, ainsi que pourquoi de telles fonctions ne peuvent être trouvées que "en se tenant debout sur la tête".

Étant donné que vous ne voulez pas apprendre de concepts précis, voici une explication intuitive. Dans la discussion ci-dessous, "fonction" se réfère toujours à une fonction mappant des nombres naturels à des nombres naturels (éventuellement indéfinis à certains arguments).

Tout langage de programmation qui a

1. syntaxe calculable et règles d'évaluation, et
2. implémente toutes les fonctions calculables totales

implémente nécessairement certaines fonctions partielles .

Pour voir cela, supposons que ce soit le cas que toutes les fonctions définissables dans ce langage soient totales. Parce que le langage a une syntaxe calculable, nous pouvons énumérer toutes les définitions de fonctions (simplement énumérer toutes les chaînes et filtrer celles qui provoquent des erreurs syntaxiques). Parce que les règles d'évaluation sont calculables, la deuxième hypothèse nous permet de conclure que dans notre langage, nous pouvons définir la fonction totale eval(n,m)qui évalue la n-ième fonction définissable m(il s'agit essentiellement d'un mini-interprète écrit dans la langue elle-même). Mais alors la fonction

λ k . (1 + eval(k,k))

est une fonction définissable totale qui est différente de toute fonction définissable totale, une contradiction.

Le -calculus simplement tapé remplit la première condition et ne définit que les fonctions totales. Il ne remplit donc pas la deuxième condition.$\lambda$

En ce qui concerne "se tenir debout", pour un -calculus fortement normalisant, il est assez facile de fournir une fonction totale qui n'est pas définissable dans le calcul, à savoir la procédure de normalisation elle-même. Peu importe la fantaisie de votre calcul fortement normalisant, il pourrait s'agir de la théorie polymorphe -calculus, ou de la théorie de type Martin-Lof, ou du calcul des constructions. (Exercice: si vous pouviez implémenter la procédure de normalisation, vous pourriez implémenter ci-dessus.)$\lambda$$\lambda$eval

Je trouve que la réponse de Merijn gère assez bien la première partie de votre question. Je vais essayer de répondre à la deuxième partie: pourquoi trouver des fonctions qui sont calculables mais non représentables dans le polymorphe -calculus nécessite "de se tenir debout".$\lambda$

Je crains que cela nécessite une explication des concepts qui ne vous intéressent pas. Une fonction récurrente partielle est un -term qui représente une fonction de à . Un -term appliqué au représentant d'un nombre naturel est envoyé à si et seulement si n'a pas une forme normale. Si aucun numéro n'est envoyé à$\lambda$$\mathbb{N}$$\mathbb{N}\cup\{\bot\}$$\lambda$$t$$n$$\bot$$t\ n$$\bot$on dit que la fonction est totale . Maintenant, l'idée est qu'aucune théorie logique$T$ peut prouver qu'un terme $t$ représente une fonction totale pour chaque fonction totale $t$, il y a toujours des "angles morts" où $t$ se termine sur toutes les entrées $n$, mais la déclaration

est indécidable dans $T$. Si la déclaration ci-dessus est prouvable dans$T$, nous disons que la fonction représentée par $t$est prouvée totale . Que toutes les fonctions totales ne sont pas$T$ est une conséquence de (une variante de) le théorème d'incomplétude de Godel pour $T$.

Maintenant, le fait est que la grande majorité des programmes que nous souhaitons concrètement écrire (tri de liste, parcours de graphe, systèmes d'exploitation) ne sont pas seulement des fonctions totales, mais sont prouvées totales dans des systèmes logiques raisonnables, comme Peano Arithmetic.

Maintenant pour le polymorphe $\lambda$-calcul. On peut montrer que les termes que l'on peut taper dans ce calcul sont exactement les termes qui représentent les fonctions prouvées totales en arithmétique peano du second ordre. Le second ordre Peano Arithmetic est beaucoup, beaucoup plus puissant que le Peano Arithmetic ordinaire.

Cela signifie par les explications ci-dessus qu'il existe des termes qui sont totaux mais pas prouvés totaux, mais de telles fonctions sont extrêmement rares, car elles sont déjà rares pour Peano Arithmetic (et tellement plus rares dans la théorie du second ordre). D'où la déclaration «debout sur la tête».

Je trouve qu'il est un peu difficile d'écrire de manière concise la preuve, mais j'espère que cette explication vous fournira suffisamment d'intuition pour voir pourquoi les termes typés simples ne peuvent pas représenter tous les termes non typés.

Le calcul lambda simplement tapé se normalise fortement. Chaque$\beta$la réduction nous rapprochera de la forme normale. Lorsque la fonction$f :: \alpha \rightarrow \beta \rightarrow \gamma$ est appliqué à une valeur de type $\alpha$ ce sera $\beta$ réduire à une fonction de type $\beta \rightarrow \gamma$. Étant donné un nombre fini d'arguments, il faut un nombre fini d'étapes de réduction pour atteindre$\beta$- forme normale, dans laquelle il n'y a plus de réductions possibles.

Pour comparer cela avec le calcul lambda non typé. L'un des combinateurs UTLC les plus célèbres est le$Y$-Combinateur:

$Y = λf.(λx.f\; (x\; x))\; (λx.f\;(x\;x))$

Lorsque nous essayons de réduire la $Y$-combinator ce qui se passe:

Peu importe les fonctions que nous transmettons, nous sommes coincés dans une séquence infinie de réductions! Si nous essayions d'épingler un type STLC sur l'UTLC$Y$-combinator, nous trouvons rapidement cela impossible, car l'application de fonction ne réduit pas le type comme requis dans le STLC. le$Y$-combinator est clairement calculable (il représente, en utilisant la récursivité, le concept d'une boucle infinie), mais il ne peut pas être représenté dans le STLC, car tous les termes STLC sont fortement normalisants.