Języki programowania z funkcjami kanonicznymi

Czy są jakieś (funkcjonalne?) Języki programowania, w których wszystkie funkcje mają formę kanoniczną? Oznacza to, że dowolne dwie funkcje, które zwracają te same wartości dla całego zestawu danych wejściowych, są reprezentowane w ten sam sposób, np. Jeśli f (x) zwrócił x + 1, a g (x) zwrócił x + 2, to f (f (x )) i g (x) generowałyby nierozróżnialne pliki wykonywalne podczas kompilacji programu.

Być może, co ważniejsze, gdzie / jak mogę znaleźć więcej informacji na temat kanonicznej reprezentacji programów (Googling „kanoniczne programy reprezentacji” okazały się mniej niż owocne)? Wydaje się, że to naturalne pytanie, i obawiam się, że po prostu nie znam właściwego terminu na to, czego szukam. Jestem ciekawy, czy taki język może być kompletny w Turingu, a jeśli nie, jak wyrazisty możesz mieć język programowania, zachowując taką właściwość.

Moje tło jest raczej ograniczone, więc wolałbym źródła o mniejszej liczbie wymagań wstępnych, ale odniesienia do bardziej zaawansowanych źródeł też mogą być fajne, ponieważ dzięki temu będę wiedział, nad czym chcę pracować.

Zakres, w jakim jest to możliwe, jest w rzeczywistości głównym otwartym pytaniem w teorii rachunku lambda. Oto krótkie podsumowanie tego, co wiadomo:

• Prosty typ rachunku lambda z jednostką, produktami i przestrzenią funkcji ma prostą właściwość form kanonicznych. Dwa warunki są równe wtedy i tylko wtedy, gdy mają taką samą beta-normalną, eta-długą formę. Obliczenie tych normalnych form jest również dość proste.

• Dodanie typów sum znacznie komplikuje sprawy. Problem równości jest wciąż rozstrzygalny (słowo kluczowe do wyszukania to „równość koproduktów”), ale znane algorytmy działają z bardzo trudnych powodów i według mojej wiedzy nie istnieje całkowicie zadowalające twierdzenie o normalnej formie. Oto cztery znane mi podejścia:

  • Neil Ghani, Beta-Eta Equality for Coproducts , TLCA 1995.
  • Vincent Balat, Roberto di Cosimo, Marcelo Fiore, Ekstensywna normalizacja i częściowa ocena ukierunkowana na typ dla rachunku lambda na maszynie z sumami , POPL 2004.
  • Sam Lindley, Exticient Recriting with Sums , TLCA 2007.
  • Arbob Ahmad, Daniel R. Licata i Robert Harper, Prooforetyczna procedura decyzyjna dla rachunku Fincul Lambda-Calculus . WMM 2007.

• Dodanie niepowiązanych typów, takich jak liczby naturalne, sprawia, że ​​problem jest nierozstrzygalny. Zasadniczo możesz teraz zakodować dziesiąty problem Hilberta.

• Dodanie rekurencji sprawia, że ​​problem jest nierozstrzygalny, ponieważ posiadanie normalnych form sprawia, że ​​równość jest rozstrzygalna, a to pozwala rozwiązać problem zatrzymania.