Toute langue qui n'est pas complète de Turing ne peut pas écrire elle-même un interprète. Je n'ai aucune idée de l'endroit où je l'ai lu, mais je l'ai vu utilisé à plusieurs reprises. Il semble que cela donne lieu à une sorte de langage complet «ultime» non Turing; celui (s) qui ne peutêtre interprété par une machine de Turing. Ces langages ne seraient pas nécessairement capables de calculer toutes les fonctions totales des naturels aux naturels, ni nécessairement isomorphes (c'est-à-dire que les langages ultimes A et B existent de telle sorte qu'il existe une fonction F que A peut calculer mais B ne peut pas). Agda peut interpréter le système T de Godel et Agda est total, de sorte qu'un langage aussi ultime devrait être strictement plus puissant que le système T de Godel semble-t-il. Il me semble qu'un tel langage serait au moins aussi puissant que agda (même si je n'ai aucune preuve, juste un pressentiment).
Des recherches ont-elles été faites dans ce sens? Quels résultats sont connus (à savoir est-ce qu'un tel langage "ultime" est connu)?
Bonus: je crains qu'il existe un cas pathologique qui ne peut pas calculer des fonctions que le système T de Godel pourrait encore ne peut être interprété que par une machine de Turing car il permet de calculer des fonctions vraiment étranges. Est-ce le cas ou pouvons-nous savoir qu'un tel langage serait capable de calculer tout ce que le système T de Godel pourrait calculer?
Réponses:
C'est une question mal formulée, alors essayons d'abord de la comprendre. Je vais le faire dans le style de la théorie de la calculabilité. Ainsi j'utiliserai des nombres au lieu de chaînes: un morceau de code source est un nombre, plutôt qu'une chaîne de symboles. Cela n'a pas vraiment d'importance, vous pouvez remplacer par tout au long ci-dessous.s t r i n gN string
Soit une fonction d'appariement .⟨m,n⟩
Disons qu'un langage de programmation est donné par les données suivantes:L=(P,ev)
Le fait que soit décidable signifie qu'il existe une carte calculable totale v a l i d : N → { 0 , 1 } telle que v a l i d ( n ) = 1P valid:N→{0,1} . De manière informelle, nous disons qu'il est possible de dire si une chaîne donnée est un morceau de code valide. La fonction e v est essentiellement un interprète pour notre langage: e v ( m , n ) exécute le code m sur l'entrée n - le résultat peut être indéfini.valid(n)=1⟺n∈P ev ev(m,n) m n
Nous pouvons maintenant introduire une terminologie:
D'autres définitions de " interprète L 2 " sont possibles, mais je ne vais pas entrer dans le détail maintenant.L1 L2
On dit que et L 2 sont équivalents s’ils s’interprètent.L1 L2
Il y a le langage "le plus puissant" des machines de Turing (que vous appelez "une machine de Turing") dans lequel n ∈ N est un codage d'une machine de Turing et φ ( n , m ) est la fonction calculable partielle qui "exécute l'encodage de la machine de Turing par n sur l'entrée m ". Ce langage peut intercepter tous les autres langages, évidemment car nous avions besoin que e v soit calculable.T=(N,φ) n∈N φ(n,m) n m ev
Notre définition des langages de programmation est très détendue. Pour que les éléments suivants passent, exigons trois autres conditions:
Un résultat classique est le suivant:
Théorème: si une langue peut s'interpréter elle-même, elle n'est pas totale.
Preuve. Supposons que est le programme universel pour un langauge totale L mis en œuvre en L , à savoir, pour tout m ∈ P et n ∈ N , eu L L m ∈ P n ∈ N
Comme successeur, diagonale et e v ( u , - ) sont implémentées dans L , il en est de même de leur composition k ↦
Observez que nous pourrions remplacer la carte successeur par toute autre carte sans point fixe.
Voici un petit théorème qui, je pense, effacera un malentendu.
Théorème: Chaque langue totale peut être interprétée par une autre langue totale.
Preuve. Soit une langue totale. On obtient un total L ' qui interprète L en accolant à L son évaluateur e v . Plus précisément, soit P ' = { ⟨ 0 , n ⟩ | ) = { e v ( n , m ) si b = 0 , e v ( m 0 , m 1 ) si b = 1L L′ L L e v et définir e v ' comme
e v ' ( ⟨ b , n ⟩ , mP′= { ⟨ 0 , n ⟩ | n ∈ P} ∪ { ⟨ 1 , 0 ⟩ } e v′ De
toute évidence,L'est totale carLest totale. Pour voir queL'peut simulerLil suffitprendreu=⟨1,0
Exercice: [ajouté le 2014-06-27] Le langage construit ci-dessus n'est pas fermé sous composition. Fixer la preuve du théorème pour que L ′ satisfasse aux exigences supplémentaires si L le fait.L′ L′ L
En d'autres termes, vous n'avez jamais besoin de la pleine puissance des machines de Turing pour interpréter un langage total - un langage total légèrement plus puissant L ' suffit. Le langage L ' est strictement plus puissant que L car il interprète L , mais L ne s'interprète pas lui-même.L L′ L′ L L L
la source
is_total
, qui n'est pas non plus cmputable, mais ne pourrions pas implémenter l'évaluation (car il faudrait également calculer le bit de la fonction résultante). En général, je dirais que ce n'est pas un langage de programmation si vous ne pouvez même pas implémenter un analyseur.Cette déclaration est incorrecte. Considérez le langage de programmation dans lequel la sémantique de chaque chaîne est "Ignorez votre entrée et arrêtez immédiatement". Ce langage de programmation n'est pas Turing complet mais chaque programme est un interprète du langage.
la source