Rachunek Lambda dla funkcji odwracalnych (obliczalnych r-Turinga)


19

Interesuje mnie koncepcja „kompletności r-Turinga”, zdefiniowana przez Axelsena i Glück (2011) . System jest gotowy do r-Turinga, jeśli może obliczyć ten sam zestaw funkcji, co odwracalna maszyna Turinga, bez generowania żadnych „śmieciowych” danych. Jest to to samo, co możliwość obliczenia każdej funkcji, która jest (a) obliczalna i (b) iniekcyjna.

Chciałbym obliczeniowo zbadać przestrzeń obliczalnych funkcji iniekcyjnych. W tym celu szukam „najbardziej minimalnego” odwracalnego języka programowania --- czegoś, co może odgrywać równoważną rolę dla obliczalności r-Turinga, którą rachunek lambda odgrywa dla obliczalności Turinga.

Wiem, że istnieje wiele języków odwracalnych, które ludzie opracowali i udowodnili, że są kompletne. Są one jednak opracowywane z myślą o praktycznych zastosowaniach, dlatego ich autorzy koncentrują się na nadaniu im wyrazistych cech, a nie na minimalizacji.

Czy ktoś wie, czy tak minimalny odwracalny język został opisany, czy też prowadzone są badania w tym kierunku? Jestem dość nowy w literaturze na ten temat, więc łatwo mogłem to przegapić. Alternatywnie, czy ktoś ma wgląd w to, jak można stworzyć taki język?

Poniżej znajduje się podsumowanie tego, czego szukam. Nie wiem, czy można go stworzyć, modyfikując sam rachunek lambda, czy też należałoby użyć zupełnie innego rodzaju języka.

  • Pełny język r-Turinga - oblicza wszystkie obliczalne funkcje odwracalne i może tylko obliczać funkcje odwracalne
  • Składnia i semantyka są jak najmniejsze. (Np. Rachunek Lambda ma tylko definicje funkcji i aplikacje, i nic więcej.) Nie jest konieczne, aby składnia lub semantyka była powiązana z tymi z rachunku lambda, chociaż mogą być.
  • Program = dane. Oznacza to, że programy działają na wyrażeniach, a nie na jakichkolwiek innych danych. Gwarantuje to, że dane wyjściowe programu można zawsze interpretować jako program. To prawdopodobnie oznacza, że ​​musi to być funkcjonalny, a nie imperatywny styl języka.
  • Istnieje jakiś systematyczny sposób przekonwertowania programu na jego odwrotność, który nie wymaga znacznie więcej obliczeń niż ten, który jest wykonywany w obliczeniach odwrotnych. (Nie wszystkie języki odwracalne mają tę właściwość, ale niektóre mają.)

Powinienem podkreślić, że podejście Axelsen i Glück do obliczeń odwracalnych różni się od dobrze znanego podejścia ze względu na Bennetta, w którym program (na ogół nieodwracalny) jest odwracalny poprzez zwrócenie pewnych informacji o historii obliczeń wraz z danymi wyjściowymi. Kompletność r-Turinga polega na możliwości obliczenia funkcji iniekcyjnych bez żadnych dodatkowych danych wyjściowych. Istnieje kilka rzeczy zwanych odmianami „odwracalnego rachunku lambda”, które są odwracalne w sensie Benneta - nie tego szukam.


r-Turing complete wydaje się być względnie nową definicją i warto byłoby zobaczyć dowód, że nie jest to to samo, co Turing complete i interpretacje / analizy innych autorów niż ci, którzy wprowadzili tę koncepcję (i linki nieopłacane, jeśli możliwe)
dniu

Odpowiedzi:


4

Nie znam się zbyt dobrze na tym obszarze, ale istnieje pewna niedawna praca ze strony społeczności języków programowania, która może cię zainteresować, oparta na idei ograniczania się do języka typu izomorfizmów. W szczególności możesz rzucić okiem

  • Typy ułamkowe : Roshan P. James, Zachary Sparks, Jacques Carette i Amr Sabry

a także różne powiązane publikacje, które można znaleźć na stronie internetowej Amr Sabry .

Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.