Pracuję nad dowodem twierdzenia wyższego rzędu, którego ujednolicenie wydaje się najtrudniejszym podproblemem.Ujednolicenie wyższego rzędu
Jeśli algorytm Hueta jest nadal uważany za najnowocześniejszy, czy ktoś ma jakiekolwiek linki do jego wyjaśnień, które są napisane tak, aby były zrozumiałe dla programisty, a nie dla matematyka?
A może nawet przykłady użycia tego miejsca i zwykły algorytm pierwszego rzędu?
Najnowocześniejsze — tak, o ile wiem, wszystkie algorytmy bardziej lub mniej wziąć taki sam kształt jak Huet'S (śledzę teorii programowania logicznego, choć moja wiedza jest styczna) warunkiem trzeba pełny wyższego rzędu dopasowywanie: podtrobania, takie jak dopasowanie wyższego rzędu (unifikacja, w której jeden termin jest zamknięty) i rachunek wzoru Dale'a Millera, są rozstrzygalne.
Należy zauważyć, że algorytm Hueta jest najlepszy w następującym znaczeniu: — to jest jak algorytm półdecydowania, ponieważ znajdzie unifikatory, jeśli istnieją, ale nie ma gwarancji, że wygasną, jeśli tego nie zrobią. Ponieważ wiemy, że unifikacja wyższego rzędu (w rzeczy samej, unifikacja drugiego rzędu) jest nierozstrzygalna, nie można zrobić nic lepszego.
Wyjaśnienie: Pierwsze cztery rozdziały pracy doktorskiej Conala Elliotta, Extensions and Applications of Higher-Order Unification, powinny pasować do rachunku. Ta część waży prawie 80 stron, z gęstą teorią typu, ale dobrze umotywowaną i jest najbardziej czytelnym kontem, jakie widziałem.
Przykłady: Algorytm Hueta wymyśli towary dla tego przykładu: [X (o), Y (succ (0))]; które z konieczności zakwestionuje algorytm unifikacji pierwszego rzędu.
Przykład unifikacji wyższego rzędu (naprawdę dopasowanie drugiego rzędu) to: f 3 == 3 + 3, gdzie == to modulo alfa, beta i konwersja eta (ale nie przypisuje żadnego znaczenia "+"). Istnieją cztery rozwiązania:
\ x -> x + x
\ x -> x + 3
\ x -> 3 + x
\ x -> 3 + 3
W przeciwieństwie do pierwszego ujednolicenia/dopasowania nie dałoby rozwiązania.
HOU jest bardzo przydatne w przypadku korzystania z HoA (wyższego rzędu Abstract Syntax), do kodowania języków z zmiennej wiążące unikając złożoność zmiennej chwytania itp
Mój pierwszy kontakt z tematem był papier „Udowodnienie i stosowanie transformacji programu wyrażonych za pomocą wzorów drugiego rzędu "Gerarda Hueta i Bernarda Langa. Jak pamiętam, artykuł ten "został napisany, aby mógł go zrozumieć programista". A gdy zrozumiesz dopasowywanie drugiego rzędu, HOU nie ma wiele do zrobienia. Kluczowym rezultatem Huet's jest to, że elastyczny/elastyczny przypadek (zmienne jako nagłówek terminu i jedyny przypadek nie pojawiający się w dopasowaniu) jest zawsze możliwy do rozwiązania.
Mam pewność, czy te algorytmy działają na "otwory". Załóżmy, że mam T == \ f \ x. (fx) = x + x. Następnie (T _), tj. Oryginalny T z "dziurą" dla f ma postać \ x. (_ x) = x + x. Ale ze względu na reguły przechwytywania istnieje również ograniczenie boczne teraz, gdy x nie powinno występować w _, więc jedynym rozwiązaniem jest _ = \ y.y + y, ale nie \ y.y + x, \ y.x + y, \ y.x + x. Nie znalazłem papieru, ale pokazałem w ten sposób "dziury". –
Dodałbym do lektury rozdział w tomie 2 z Handbook of Automated Reasoning. Ten rozdział jest prawdopodobnie bardziej dostępny dla początkującego i kończy się z rachunkiem λΠ, w którym zaczyna się papier Conal Elliott .
Preprint znajduje się tutaj:
wyższego rzędu Ujednolicenie i dopasowanie
Gilles Dowek, 2001
http://www.lsv.fr/~dowek/Publi/unification.ps
Conal Elliott papier jest bardziej formalny i concerntrated na jednym z wariantów, a także wprowadza na końcu rachunek λΠΣ, który ma również typy sumowe oprócz typów produktów.
Bye
Istnieje również 1993 papier Functional Unification of Higher-Order Patterns (tylko 11 stron, z czego 4 są bibliografia i kod dodatek) Tobias Nipkow użytkownika. Abstrakcyjny:
Kompletne opracowanie algorytmu zjednoczeniowego na tzw wzorców wyższego rzędu, podklasą $ \ lambda $ -terms, są prezentowane. Punktem wyjścia jest sformułowanie ujednolicenia przez transformację, wynik bezpośrednio wykonywanego programu funkcjonalnego. W końcowym kroku rozwoju wynik jest dostosowywany do $ \ lambda $ -terms w notacji de Bruijna. Algorytmy działają dla terminów po prostu wpisanych i bez typu.
Jeden z nielicznych przypadków, w których zadawano naprawdę dobre (nie można google lub trudne do znalezienia google) pytanie, a otrzymywano trudną do zdobycia, wysoką jakość odpowiedzi. –
+1 do was obojga - lol, to pewnie dlatego wasze statystyki wynoszą 300-600 zamiast 31,2K lub coś w tym stylu. Prawdopodobnie odpowiadasz tylko na pytania, na które niewielu innych może odpowiedzieć. –
Dokładny cytowany Conal Elliott podał inną odpowiedź :-D. – Blaisorblade