Tout d'abord, je suppose que vous avez déjà entendu parler de la thèse de Church-Turing, qui stipule que tout ce que nous appelons le "calcul" est quelque chose qui peut être fait avec une machine de Turing (ou l'un des nombreux autres modèles équivalents). Ainsi, une Turing-complet de la langue est celui dans lequel tout calcul peut être exprimé. À l'inverse, une Turing-incomplète de la langue est un calcul qui ne peut pas être exprimé.
Ok, ce n'était pas très instructif. Permettez-moi de donner un exemple. Il y a une chose que vous ne pouvez pas faire quelque Turing-incomplète de la langue: vous ne pouvez pas écrire un simulateur de machine de Turing (sinon, vous pouvez encoder n'importe quel calcul sur la simulation de machine de Turing).
Ok, qui encore n'était pas très instructif. la vraie question est, est ce utile de programme ne peut pas être écrit dans un de Turing-incomplète de la langue? Eh bien, personne n'est venu avec une définition de "programme" qui comprend tous les programmes de quelqu'un, quelque part, a écrit à des fins utiles, et qui ne comprennent pas tous les machine de Turing calculs. De sorte que la conception d'une Turing-incomplète de la langue dans laquelle vous pouvez écrire tous les programmes utiles, est encore très long terme but de la recherche.
Maintenant il ya plusieurs différents types de Turing-incomplète langues, et ils diffèrent en ce qu'ils ne peuvent pas le faire. Cependant, il ya un thème commun. Si vous êtes à la conception d'une langue, il existe deux moyens principaux pour s'assurer que le langage Turing-complet:
Regardons quelques exemples de non-Turing langues que certaines personnes pourraient néanmoins appel langages de programmation.
-
Les premières versions de FORTRAN n'ont pas d'allocation dynamique de la mémoire. Vous avez eu à déterminer à l'avance la quantité de mémoire de votre calcul besoin et allouer que. En dépit de cela, le FORTRAN était une fois la plupart des langage de programmation largement utilisé.
L'évidente limitation pratique est que vous devez prévoir les besoins en mémoire de votre programme avant de l'exécuter. Cela peut être difficile, et peut-être impossible si la taille de l'entrée de données n'est pas limité à l'avance. À l'époque, la personne de l'alimentation de l'entrée de données est souvent la personne qui a écrit le programme, de sorte qu'il n'était pas une grosse affaire. Mais ce n'est pas vrai pour la plupart des programmes écrits aujourd'hui.
-
Coq est un langage conçu pour prouver des théorèmes. Maintenant prouver des théorèmes et des programmes en cours d'exécution sont très étroitement liés, de sorte que vous pouvez écrire des programmes en Coq comme vous démontrer un théorème. Intuitivement, une preuve du théorème "A implique B" est une fonction qui prend une preuve d'Un théorème comme argument et retourne une preuve du théorème B.
Étant donné que l'objectif du système est de prouver des théorèmes, vous ne pouvez pas laisser le programmeur d'écrire des fonctions arbitraires. Imaginez la langue vous a permis de vous écrire un idiot en fonction récursive, qui vient d'appeler lui-même (choisir la ligne qui utilise votre langue préférée):
theorem_B boom (theorem_A a) { return boom(a); }
let rec boom (a : theorem_A) : theorem_B = boom (a)
def boom(a): boom(a)
(define (boom a) (boom a))
Vous ne pouvez pas laisser l'existence d'une telle fonction vous convaincre que A implique B, ou autre chose qui vous serait en mesure de prouver quoi que ce soit et pas seulement vrai théorèmes! Afin de Coq (et des démonstrateurs) l'interdiction de l'arbitraire de la récursivité. Lorsque vous écrivez une fonction récursive, vous devez prouver qu'il se termine toujours, de sorte que chaque fois que vous l'exécutez sur présentation de la preuve du théorème de Un vous de savoir qu'il va construire une preuve de théorème B.
La pratique immédiate de la limitation de Coq, c'est que vous ne pouvez pas écrire arbitraire des fonctions récursives. Depuis que le système doit être en mesure de rejeter tous les non-terminaison des fonctions, l'indécidabilité du problème de l'arrêt (ou plus généralement de Riz le théorème de) assure qu'il y mettent fin à des fonctions qui sont rejetés en tant que bien. Un ajout pratique de la difficulté, c'est que vous devez aider le système à prouver que votre fonction ne se terminent.
Il y a beaucoup de recherches en cours sur la fabrication de systèmes d'épreuves plus de la programmation de langue-comme sans compromettre leur garantir que si vous avez une fonction de A vers B, il est aussi bon comme une preuve mathématique que A implique B. l'Extension du système à accepter plus de résiliation de fonctions est l'un des sujets de recherche. Une autre extension directions notamment faire face à un tel "monde réel" des préoccupations en entrée/sortie et de la concurrence. Un autre défi est de faire de ces systèmes accessibles au commun des mortels (ou peut-être convaincre le commun des mortels qu'ils sont en fait accessibles).
-
Programmation synchrone, les langues sont des langues conçu pour la programmation des systèmes temps-réel, c'est-à-dire où le programme doit répondre en moins de n cycles d'horloge. Ils sont principalement utilisés pour les systèmes essentiels tels que les contrôles de véhicules ou de signalisation. Ces langages offrent de solides garanties sur la durée d'un programme à exécuter et la quantité de mémoire qu'il peut allouer.
Bien sûr, la contrepartie de ces garanties solides, c'est que vous ne pouvez pas écrire des programmes dont la consommation de la mémoire et temps d'exécution que vous n'êtes pas en mesure de prévoir à l'avance. En particulier, vous ne pouvez pas écrire un programme dont la consommation de mémoire ou de temps d'exécution dépend de la saisie des données.
Il y a beaucoup de langues spécialisées qui ne sont même pas essayer d'être langages de programmation et peuvent donc rester confortablement loin de Turing à l'exhaustivité: les expressions régulières, les données de langues, la plupart des langages de balisage, ...
Par la voie, Douglas Hofstadter a écrit plusieurs très intéressants ouvrages de vulgarisation scientifique sur le calcul, en particulier Gödel, Escher, Bach: an Eternal Golden Braid. Je ne me souviens pas s'il traite explicitement des limites de Turing-l'inachèvement, mais la lecture de ses livres sera certainement vous aider à comprendre plus de matériel technique.
