Théorie de réalisabilité: différence de puissance entre le calcul lambda et les machines de Turing

J'ai trois sous-questions liées, qui sont soulignées par des points dans la liste ci-dessous (non, elles ne pourraient pas être divisées, si vous vous le demandez). Andrej Bauer a écrit ici que certaines fonctions sont réalisables avec une machine de Turing, mais pas avec le lambda-calcul. Une étape clé de son raisonnement est la suivante:

Cependant, si nous utilisons le calcul lambda, alors [le programme] c est supposé calculer un nombre représentant une machine de Turing à partir d'un terme lambda représentant une fonction f. Cela ne peut pas être fait (je peux expliquer pourquoi, si vous le posez séparément).

• Je voudrais voir une explication / une preuve informelle.

Je ne vois pas comment appliquer le théorème de Rice ici; cela s'appliquerait au problème "est-ce que cette machine de turing T et ce lambda terme équivalent L?", car appliquer ce prédicat à des termes équivalents donne le même résultat. Cependant, la fonction requise peut calculer des MT différentes, mais équivalentes, pour des termes lambda différents, mais équivalents.

• De plus, si le problème concerne l'introspection d'un terme lambda, je pense que le codage de Gödel d'un terme lambda serait également acceptable, n'est-ce pas?

D'une part, étant donné que son exemple implique de calculer, dans le calcul lambda, le nombre d'étapes nécessaires à une machine de Turing pour effectuer une tâche donnée, je ne suis pas très surpris.

• Mais comme ici le lambda-calcul ne peut pas résoudre un problème lié à la machine de Turing, je me demande si on peut définir un problème similaire pour le lambda-calcul et le prouver insoluble pour les machines de Turing, ou s'il existe une différence de puissance en faveur de Turing Machines (ce qui me surprendrait).

John Longley a publié un article très détaillé dans une enquête sur les problèmes en jeu, "Notions de calculabilité à un type plus élevé" .

L'idée de base est que la thèse de Church-Turing ne concerne que les fonctions de - et le calcul ne se résume pas à cela! En particulier, lorsque nous écrivons des programmes, nous utilisons des fonctions de type plus élevé (telles que ).$\mathbb{N} \to \mathbb{N}$$(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$

Afin de définir complètement un modèle de calcul de type supérieur, nous devons spécifier la convention d'appel des fonctions, afin de permettre à une fonction d'appeler une autre fonction qu'elle reçoit en tant qu'argument. Dans le lambda calcul, la convention d'appel standard est que nous représentons les fonctions par des termes lambda, et la seule chose que vous pouvez faire avec un lambda dans le lambda calcul est de l'appliquer. Dans les codages typiques avec les machines Turing, nous passons des fonctions sous forme d'arguments en corrigeant un codage Godel particulier, puis des chaînes représentant l'index de la machine que vous souhaitez transmettre en tant qu'argument.

La différence de codage signifie que vous pouvez analyser la syntaxe de l'argument avec un codage de type TM et vous ne pouvez pas utiliser une représentation standard du lambda-calcul. Donc, si vous recevez un terme lambda pour une fonction de type , vous ne pouvez tester son comportement qu'en lui transmettant des particuliers - vous ne pouvez pas analyser la structure du terme en aucune façon. Ce n'est tout simplement pas assez d'informations pour comprendre le code du terme lambda.$\mathbb{N} \to \mathbb{N}$$n$

Une chose à noter est qu'avec les types plus élevés, si une langue est moins expressive à un ordre, elle est plus expressive à un ordre, car les fonctions sont contravariantes. De même, il existe des fonctions que vous pouvez écrire dans LC et que vous ne pouvez pas utiliser avec un codage de type TM (car elles reposent sur le fait que vous pouvez transmettre des arguments fonctionnels et savoir que le récepteur ne peut pas regarder à l'intérieur de la fonction que vous lui avez attribuée). .

EDIT: Voici un exemple de fonction définissable dans PCF, mais pas dans les encodages TM + Goedel. Je vais déclarer la isAlwaysTruefonction

 isAlwaysTrue : ((unit → bool) → bool) → bool

qui doit renvoyer true si son argument ignore son argument et renvoie toujours true, doit renvoyer false si son argument renvoie false sur une entrée et passe dans une boucle si son argument passe dans une boucle sur une entrée. Nous pouvons définir cette fonction assez facilement, comme suit:

isAlwaysTrue p = p (λ(). true) ∧ p (λ(). false) ∧ p (λ(). ⊥)

où ⊥est le calcul en boucle et ∧est l'opérateur and sur les booléens. Cela fonctionne parce qu'il n'y a que trois habitants unit → booldans PCF et nous pouvons donc les énumérer de manière exhaustive. Toutefois, dans un modèle de style TM + Goedel-encoding, vous ppouvez tester le temps nécessaire à son argument pour renvoyer une réponse et renvoyer différentes réponses en fonction de cela. Ainsi, la mise en œuvre de isAlwaysTrueTM avec les applications ne répondrait pas aux spécifications.

Qu'est-ce que Neel a dit, et aussi ce qui suit.

Je voudrais souligner ( encore , encore et encore ) que la représentation des intrants et des extrants est importante. Si nous sommes autorisés à changer de représentation, nous pouvons réaliser à peu près n'importe quoi (par exemple, rendre toute fonction donnée calculable). Ainsi, passer d'une représentation des fonctions par -terms à une représentation par des nombres de Gödel n'est pas acceptable si notre modèle de calcul est -calculus (car alors l'opération de currying devient non calculable par -calculus).$\mathbb{N} \to \mathbb{N}$$\lambda$$\lambda$$\lambda$

Une déclaration qui est réalisable dans le modèle -term mais pas dans le modèle de Turing n'est pas "toutes les fonctions ont un code de Gödel", ce qui est un peu ridicule. Je vais essayer d’en trouver un meilleur et d’éditer cette réponse.$\lambda$$\mathbb{N} \to \mathbb{N}$

Edit on 2013-10-07: Voici ce que je voulais dire par "currying devient impossible à calculer". Supposons que nous utilisions le -calculus non typé comme modèle de calcul, mais que nous décidions ensuite de représenter mappages avec les codes de Gödel (des machines de Turing, codés sous forme de chiffres de l'Église). Cela semble inoffensif, non? Après tout, nous pensons que le mantra "Les machines de Turing et les calculus sont équivalents".$\lambda$$\mathbb{N} \to \mathbb{N}$$\lambda$

Eh bien, pour que cette nouvelle représentation soit réellement une représentation valide de , nous devons également réaliser une application et un currying (parce que "représenter des fonctions" signifie la même chose que "représenter un objet exponentiel "). Plus précisément, nous avons besoin d'un -term tel que, chaque fois que le chiffre d'église représente alors est représenté par . (J'écris ici pour le chiffre de l'église représentant le nombre .) Such an$\mathbb{N} \to \mathbb{N}$$\lambda$$\mathtt{app}$$\overline{n}$$f : \mathbb{N} \to \mathbb{N}$$f(k)$$\mathtt{app} \; \overline{n} \; \overline{k}$$\overline{n}$$n$$\mathtt{app}$est facilement disponible parce qu’il s’agit d’un interprète pour les machines de Turing, implémenté dans le -calculus.$\lambda$

Mais qu'en est-il currying? Pour cela, nous avons besoin de ce qui suit. Supposons que est un ensemble représenté. Quelle que soit la carte calculée par un -term , nous devons montrer que la transposition est également calculé par certains -term . Mais considérons l'exemple où est l'ensemble ofmaps représenté par -terms, et est l'application. Alors serait une carte qui sert d’identité sur$X$$f : X \times \mathbb{N} \to \mathbb{N}$$\lambda$$t$$\tilde{f} : X \to (\mathbb{N} \to \mathbb{N})$$\lambda$$s$$X$$\mathbb{N} \to \mathbb{N}$$\lambda$$f$$\tilde{f}$$\mathbb{N} \to \mathbb{N}$, mais son réalisateur est un terme qui convertit termes représentant les mappes en codes de Gödel correspondants. Un tel terme n'existe pas (par exemple parce qu'il serait discontinu dans un modèle sémantique topologique).$\lambda$$\lambda$$\mathbb{N} \to \mathbb{N}$$\lambda$

Vous pouvez essayer de objecter que je n'aurais pas dû utiliser l'ensemble représenté spécifique de maps représenté par -terms, car nous avons "accepté" que ceux-ci soient représentés par des codes de Gödel . Mais vous auriez tort. Tout d'abord, j'aurais pu utiliser un différent avec une preuve plus complexe qui vous échapperait tout en obtenant le même résultat. Deuxièmement, est là dans la catégorie et la définition de exponentielle exige que le travail de curry concerne tous les objets. Vous devez respecter la catégorie. Vous ne pouvez pas simplement le boucher au hasard et en retirer des objets (vous pouvez le faire, mais vous êtes alors un boucher).$X$$\mathbb{N} \to \mathbb{N}$$\lambda$$X$$X$