Langages de programmation avec fonctions canoniques

29

Existe-t-il des langages de programmation (fonctionnels?) Où toutes les fonctions ont une forme canonique? C'est-à-dire que deux fonctions qui renvoient les mêmes valeurs pour tout l'ensemble d'entrée sont représentées de la même manière, par exemple si f (x) a renvoyé x + 1, et g (x) a renvoyé x + 2, alors f (f (x )) et g (x) généreraient des exécutables indiscernables lors de la compilation du programme.

Peut-être plus important encore, où / comment pourrais-je trouver plus d'informations sur la représentation canonique des programmes (la recherche sur "programmes de représentation canonique" a été moins que fructueuse)? Cela semble être une question naturelle à poser, et je crains de ne pas savoir le terme approprié pour ce que je recherche. Je suis curieux de savoir s'il est possible qu'un tel langage soit Turing complet, et sinon, à quel point un langage de programmation peut être expressif, tout en conservant une telle propriété.

Mon expérience est plutôt limitée, donc je préférerais des sources avec moins de prérequis, mais les références à des sources plus avancées peuvent aussi être cool, car de cette façon, je saurai vers quoi je veux travailler.

math4tots
la source

Réponses:

38

La mesure dans laquelle cela est possible est en fait une question ouverte majeure dans la théorie du calcul lambda. Voici un bref résumé de ce qui est connu:

  • Le calcul lambda simplement tapé avec l'unité, les produits et l'espace de fonction a une simple propriété de formes canoniques. Deux termes sont égaux si et seulement s'ils ont la même forme bêta-normale et éta-longue. Le calcul de ces formes normales est également assez simple.

  • L'ajout de types de somme complique grandement les choses. Le problème d'égalité est encore décidable (le mot-clé à rechercher est "égalité de coproduit"), mais les algorithmes connus fonctionnent pour des raisons extrêmement délicates et à ma connaissance il n'y a pas de théorème de forme normale totalement satisfaisant. Voici les quatre approches que je connais:

  • L'ajout de types illimités, tels que les nombres naturels, rend le problème indécidable. Fondamentalement, vous pouvez maintenant encoder le dixième problème de Hilbert.

  • L'ajout de récursivité rend le problème indécidable, car avoir des formes normales rend l'égalité décidable, et cela vous permettrait de résoudre le problème d'arrêt.

Neel Krishnaswami
la source
Cet article étend l'équivalence avec les coproduits à l'équivalence avec les sommes mais il n'y a pas de syntaxe de forme canonique "unique", vous choisissez une "fonction de saturation" qui est assez intelligente pour détecter quand les deux termes que vous comparez ont des sous-termes qui s'avèrent faux. Il est plus similaire à Ahmed-Licata-Harper en ce qu'ils utilisent tous deux la mise au point.
Max Nouveau
Avec seulement l'unité, les produits et les fonctions, la cardinalité de tout ce que vous pouvez éventuellement écrire est 1, tandis que si vous ajoutez des sommes, vous obtenez soudainement de nombreuses cardinalités différentes (et vous pouvez faire un "calcul utile"). Ces faits sont-ils liés?
glaebhoerl
1
bλX:b.λy:b.XλX:b.λy:b.y