Langages de programmation pour un calcul efficace

Il est impossible d'écrire un langage de programmation qui autorise toutes les machines qui s'arrêtent sur toutes les entrées et aucune autre. Cependant, il semble facile de définir un tel langage de programmation pour n'importe quelle classe de complexité standard. En particulier, nous pouvons définir un langage dans lequel nous pouvons exprimer tous les calculs efficaces et seulement les calculs efficaces.

Par exemple, pour quelque chose comme : prenez votre langage de programmation préféré, et après avoir écrit votre programme (correspondant à Turing Machine M ' ), ajoutez trois valeurs à l'en-tête: un entier c , et un entier k , et une sortie par défaut d . Lorsque le programme est compilé, sortir une machine de Turing M qui, étant donné l'entrée x de taille n, exécute M ' sur x pour c n k étapes. Si M ′ ne s'arrête pas avant le c n $P$$M'$$c$$k$$d$$M$$x$$n$$M'$$x$$c n^k$$M'$$c n^k$les étapes sont en hausse, sortir la sortie par défaut . Sauf erreur, ces langages de programmation nous permettront d'exprimer tous les calculs en P et rien de plus. Cependant, ce langage proposé est intrinsèquement non intéressant.$d$$P$

Ma question: existe-t-il des langages de programmation qui capturent des sous-ensembles de fonctions calculables (telles que toutes les fonctions efficacement calculables) de manière non triviale? S'il n'y en a pas, y a-t-il une raison à cela?

Un langage essayant d'exprimer uniquement des calculs de temps polynomiaux est le calcul lambda doux . Son système de types est enraciné dans une logique linéaire. Une thèse récente porte sur les calculs de temps polynomiaux et fournit un bon résumé des développements récents basés sur cette approche. Martin Hofmann travaille sur le sujet depuis un certain temps. Une ancienne liste de documents pertinents peut être trouvée ici ; Beaucoup de ses papiers continuent dans cette direction.

D'autres travaux adoptent l'approche consistant à vérifier que le programme utilise une certaine quantité de ressources, en utilisant des types dépendants ou un langage d'assemblage typé .

Pourtant, d'autres approches sont basées sur des calculs formels limités en ressources , tels que des variantes du calcul ambiant.

Ces approches ont la propriété que des programmes bien typés satisfont certaines limites de ressources prédéfinies. La ressource liée peut être du temps ou de l'espace, et peut généralement dépendre de la taille des entrées.

Les premiers travaux dans ce domaine portent sur des calculs fortement normalisants, ce qui signifie que tous les programmes bien typés s'arrêtent. Le système F , alias le calcul lambda polymorphe, se normalise fortement. Il n'a pas d'opérateur de point fixe, mais est néanmoins assez expressif, bien que je ne pense pas que l'on sache à quelle classe de complexité il correspond. Par définition, tout calcul fortement normalisant exprime une classe de calculs de terminaison.

Le langage de programmation Charity est un langage fonctionnel assez expressif qui s'arrête sur toutes les entrées. Je ne sais pas quelle classe de complexité il peut exprimer, mais la fonction Ackermann peut être écrite dans Charity.

Jetez un œil à l'article de Guillaume Bonfante qui a proposé deux caractérisations pour Logspace et le temps polynomial à l'aide de langages de programmation.

Guillaume Bonfante, Quelques langages de programmation pour Logspace et Ptime, AMAST 2006, LNCS 4019, pp. 66-80, 2006

Je voudrais également mentionner la théorie de la complexité implicite en tant qu'approche, car je l'ai vue apparaître dans plusieurs questions quelque peu liées. Pour citer cette réponse de Neel Krishnaswami :

La technique de base consiste à relier les classes de complexité aux sous-systèmes de logique linéaire (les soi-disant "logiques linéaires légères"), avec l'idée que l'élimination des coupures pour le système logique devrait être complète pour la classe de complexité donnée (comme LOGSPACE, PTIME, etc.). Ensuite, via Curry-Howard, vous obtenez un langage de programmation dans lequel précisément les programmes de la classe donnée sont exprimables.

Je suis surpris que personne n'ait mentionné la récursion primitive. En se limitant aux boucles bornées (c'est-à-dire que le nombre d'itérations pour chaque boucle doit être calculé avant le début de la boucle) le programme résultant est récursif primitif, et donc total. Douglas Hofstadter a proposé un langage de programmation, BLOOP, qui permettait toutes et seulement les fonctions récursives primitives.

Voir aussi Pola un langage pour la programmation PTIME et les travaux de Japaridze sur l'arithmétique PTIME, par exemple http://arxiv.org/abs/0902.2969