Algorytm określania równości funkcji na prostym typie rachunku lambda?

Wiemy, że równość beta po prostu wpisanych terminów lambda jest rozstrzygalna. Biorąc pod uwagę M, N: σ → τ, jest rozstrzygalne, czy dla wszystkich X: σ, MX $≃_β$ NX?

— MaiaVictor
źródło

Wikipedia po prostu Lambda Calculus / STLC . skoro nie jest ukończony przez Turinga, czy istnieje jakiś inny podstawowy model obliczeń, który jest równoważny? przydatne może być również zbadanie algorytmu wykrywania zatrzymania, który według wikipedii ma decydujące znaczenie dla STLC ...

— dniu

@Marzio: Właściwie myślę, że problemem jest sposób sformułowania pytania, co jest dość nieprecyzyjne. Po prawidłowym sformułowaniu jest to pytanie na poziomie badawczym. Lepszym sformułowaniem byłoby: wiemy, że równość beta prostych pojęć lambda jest rozstrzygalna. Biorąc pod uwagę

M, N : σ \to τ

$M,N:\sigma\rightarrow\tau$ , czy jest rozstrzygalne, czy dla wszystkich

X : σ

$X:\sigma$ ,

M X ≃_{β} N X

$MX\simeq_\beta NX$ ? Odpowiedź jest generalnie przecząca (więc nie istnieje algorytm taki jak ten poszukiwany przez Vicliba). Choć może się tego spodziewano, nie jest to z góry oczywiste i jest konsekwencją kilku artykułów z lat 90.

— Damiano Mazza

@DamianoMazza: ok, rzeczywiście nie głosowałem za jego zamknięciem ... Skasuję mój komentarz, zostawię twój i poczekam na komentarz / edycję OP.

— Marzio De Biasi,

@DamianoMazza i Marzio, nie wiem wystarczająco dużo, aby postawić tak formalne pytanie. Chciałbym to zrobić, ale nie uczę się tego w mojej szkole. W rzeczywistości nawet wyszukiwanie go w „równości beta”, którego tak naprawdę próbowałem przed zadaniem pytania, daje mi tak mało wyników, że prawie tak, jakby ten termin nawet nie istniał. Więc nawet nie mam pojęcia, gdzie się tego uczysz i czytasz. Czy uprzejmie wskazalibyście mi właściwe miejsce do rozpoczęcia samodzielnego studiowania tematu? Pytanie zaktualizowane.

— MaiaVictor

@Viclib: równoważność beta jest pojęciem technicznym, unikałem wspominania o tym w mojej odpowiedzi. Z grubsza, dwa terminy są równoważne beta, gdy dają ten sam wynik. Zatem powiedzenie dla wszystkich oznacza, że i obliczają tę samą funkcję. Jeśli chodzi o wskazówki do poznania rachunku lambda (na maszynie lub bez typu), uważam, że notatki Petera Selingera oraz notatki z wykładów Sørensena i Urzyczyna na temat Curry-Howarda są doskonałymi miejscami początkowymi.

M X ≃_{β} N X

$MX\simeq_\beta NX$

X

$X$

M

$M$

N

$N$

— Damiano Mazza

Jak powiedziałem w moim komentarzu, odpowiedź brzmi „nie”.

Ważną kwestią do zrozumienia (mówię to dla Vicliba, który zdaje się uczyć o tych rzeczach) jest to, że posiadanie języka programowania / zestawu maszyn, w których wszystkie programy / obliczenia kończą się w żaden sposób, nie implikuje równości funkcji (tj. Czy dwa programy / maszyny obliczają tę samą funkcję) jest rozstrzygalne. Prosty przykład: weźmy zestaw maszyn Turinga o wielomiarowym zegarze. Z definicji wszystkie takie maszyny kończą się na wszystkich wejściach. Teraz, biorąc pod uwagę dowolną maszynę Turinga , istnieje maszyna Turinga która podana w danych wejściowych ciąg symulujekroki obliczania na stałym wejściu (powiedzmy, pusty ciąg) i akceptuje, jeśli kończy się co najwyżej $M$ $M_0$ $x$ $|x|$ $M$ $M$ $|x|$ kroki lub odrzuca inaczej. Jeśli jest maszyną Turinga, która zawsze natychmiast odrzuca, zarówno , i są (oczywiście) taktowane wielomianowo, a jednak jeśli moglibyśmy zdecydować, czy i obliczają tę samą funkcję (lub, w tym przypadku, decydują o tym samym języku), moglibyśmy zdecydować, czy (która, pamiętajmy, jest dowolną maszyną Turinga) kończy się na pustym łańcuchu. $N$ $M_0$ $N$ $M_0$ $N$ $M$

W przypadku po prostu wpisanego -calculus (STLC) działa podobny argument, z tym wyjątkiem, że ocena mocy ekspresyjnej STLC nie jest tak banalna jak w powyższym przypadku. Kiedy pisałem swój komentarz, miałem na myśli kilka artykułów Hillebranda, Kanellakisa i Mairsona z początku lat 90., które pokazują, że stosując bardziej złożone typy niż zwykłe typy liczb całkowitych Kościoła, można zakodować w STLC wystarczająco skomplikowane obliczenia powyższego argumentu do działania. Właściwie widzę teraz, że potrzebny materiał jest już w uproszczonym dowodzie Mairsona na twierdzenie Statmana: $\lambda$

Harry G. Mairson, Prosty dowód twierdzenia Statmana. Theoretical Computer Science, 103 (2): 387-394, 1992. (Dostępne tutaj online ).

W tym dokumencie, przedstawia Mairson że podawane dowolną maszynę Turinga , jest uproszczona i term zawierające funkcje przejściowego . (Nie jest to a priori oczywiste, jeśli wziąć pod uwagę wyjątkowo słabą moc ekspresyjną STLC na liczbach całkowitych Kościoła. Rzeczywiście, kodowanie Mairsona nie jest natychmiastowe). Z tego nie jest trudno zbudować termin $M$ $\sigma$ $\lambda$ $\delta_M:\sigma\rightarrow\sigma$ $M$

$t_M:\mathtt{nat}[\sigma]\rightarrow\mathtt{bool}$

(gdzie jest instancją na typu liczb całkowitych Kościoła) tak, że zmniejsza się do jeśli kończy co najwyżej kroków, gdy podał pusty ciąg znaków lub w przeciwnym razie redukuje do . Jak wyżej, gdybyśmy mogli zdecydować, że funkcja reprezentowana przez jest stałą , zdecydowalibyśmy się o zakończeniu na pustym łańcuchu. $\mathtt{nat}[\sigma]$ $\sigma$ $t_M\,\underline{n}$ $\underline{1}$ $M$ $n$ $\underline{0}$ $t_M$ $\underline{0}$ $M$

— Damiano Mazza
źródło

Prawdopodobnie możliwe jest również zastosowanie kodowania wielowymiarowych funkcji wielomianowych w STLC, a następnie odwołanie się do twierdzenia Matiyasevicha .

— cody

Więc STLC nie jest ukończony, ale jest wystarczająco silny, aby zakodować funkcję przejścia maszyny Turinga !? Więc maszynę Turinga można zdefiniować jako taśmę plus działający na niej program STLC?

— MaiaVictor,

@Viclib: Pomyśl o tym: symulowanie jednego kroku dowolnej maszyny Turinga nie wymaga dużej mocy obliczeniowej. Zasadniczo potrzebujesz tylko skończonych typów danych (z if-then-else), list (z podstawowymi operacjami: przeciw, ogon itp.) I uporządkowanych par. (W rzeczywistości, rozszerzona teza Kościoła-Turinga twierdzi, że tak niska złożoność jest wspólna dla każdego rozsądnego modelu maszyny). Tym, czego brakuje STLC, jest zdolność do uruchamiania przejść TM „ad libitum”, niezależnie od danych wejściowych: może iterować je tylko kilka razy równą wieży wykładniczej wielkości wejściowej (patrz artykuł Mairsona).

— Damiano Mazza

@cody: Dzięki, nie znałem tego papieru. Chyba masz racje.

— Damiano Mazza