Języki programowania z funkcjami kanonicznymi

29

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

math4tots
źródło

Odpowiedzi:

38

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:

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

Neel Krishnaswami
źródło
Ten artykuł rozszerza równoważność z koproduktami na równoważność z sumami, ale nie ma „pojedynczej” kanonicznej składni formy, wybierasz „funkcję nasycenia”, która jest wystarczająco inteligentna, aby wykryć, kiedy dwa porównywane terminy mają podteksty, które okażą się fałszywe. Jest najbardziej podobny do Ahmeda-Licaty-Harpera, ponieważ oba używają skupienia.
Max New
Przy samej jednostce, produktach i funkcjach liczność wszystkiego, co można zapisać, wynosi 1, natomiast jeśli dodasz sumy, nagle otrzymasz wiele różnych liczności (i możesz wykonać „przydatne obliczenia”). Czy te fakty są powiązane?
glaebhoerl
1
bλx:b.λy:b.xλx:b.λy:b.y