Langages de programmation avec fonctions canoniques

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.

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:

  • Neil Ghani, Beta-Eta Equality for Coproducts , TLCA 1995.
  • Vincent Balat, Roberto di Cosimo, Marcelo Fiore, Normalisation extensionnelle et évaluation partielle dirigée par type pour le calcul lambda typé avec sommes , POPL 2004.
  • Sam Lindley, Réécriture extensionnelle avec sommes , TLCA 2007.
  • Arbob Ahmad, Daniel R. Licata et Robert Harper, A Pro-Theoretic Decision Procedure for the Finitary Lambda-Calculus . WMM 2007.

• 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.