Z grubsza mówiąc, z głębokim osadzeniem logiki (1) definiujesz typ danych reprezentujący składnię twojej logiki, i (2) podajesz model składni oraz (3) udowadniasz, że aksjomaty dotyczące twojej składni są solidne z szacunkiem do modelu. W przypadku płytkiego osadzania pomijasz kroki (1) i (2), po prostu zaczynasz od modelu i udowadniasz powiązania między formułami. Oznacza to, że płytkie osadzanie zwykle wymaga mniej pracy, aby zejść z ziemi, ponieważ reprezentują pracę, którą zwykle wykonujesz z głębokim osadzeniem.
Jeśli jednak masz głębokie osadzenie, zwykle łatwiej jest pisać refleksyjne procedury decyzyjne, ponieważ pracujesz z formułami, które faktycznie mają składnię, nad którą możesz się powtarzać. Ponadto, jeśli Twój model jest dziwny lub skomplikowany, zwykle nie chcesz bezpośrednio pracować z semantyką. (Na przykład, jeśli użyjesz biortogonalności, aby wymusić dopuszczalne zamknięcie, lub użyjesz modeli w stylu Kripke, aby wymusić właściwości ramki w logice separacji lub podobnych grach). Jednak głębokie osadzenie prawie na pewno zmusi cię do myślenia o zmiennym wiązaniu i podstawieniach , który napełni twoje serce gniewem, ponieważ jest to (a) banalne i (b) niekończące się źródło irytacji.
Prawidłowa sekwencja, którą powinieneś podjąć to: (1) spróbuj poradzić sobie z płytkim osadzeniem. (2) Kiedy zabraknie pary, spróbuj użyć taktyki i oferty, aby uruchomić procedury decyzyjne, które chcesz uruchomić. (3) Jeśli to również zabraknie pary, zrezygnuj i zastosuj składnię zależną od typu do głębokiego osadzania.
- Zaplanuj kilka miesięcy na (3), jeśli jest to twój pierwszy raz. Ty będziesz musiał zapoznać się z zaawansowane funkcje swojego asystenta dowód na pobyt SANE. (Ale jest to inwestycja, która się opłaci.)
- Jeśli asystent dowodu nie ma zależnych typów, pozostań na poziomie 2.
- Jeśli Twój język obiektowy jest wpisany w sposób zależny, pozostań na poziomie 2.
Nie próbuj też wchodzić stopniowo po drabinie. Kiedy zdecydujesz się wejść po drabinie złożoności, zrób cały krok naraz. Jeśli robisz rzeczy krok po kroku, otrzymasz wiele twierdzeń, które są dziwne i bezużyteczne (np. Otrzymasz wiele półsymetrycznych składni i twierdzeń, które mieszają składnię i semantykę w dziwny sposób), które będziesz ostatecznie muszę wyrzucić.
EDYCJA: Oto komentarz wyjaśniający, dlaczego stopniowe wchodzenie po drabinie jest tak kuszące i dlaczego (ogólnie) prowadzi do cierpienia.
A ⋆ BjaA ⋆ B⟺B ⋆ A( A ⋆ B ) ⋆ C.⟺A ⋆ ( B ⋆ C)( Ja⋆ A ) ⋆ ( B ⋆ C)A ⋆ ( B ⋆ ( C⋆ Ja) )
⋆
To prawda i działa! Należy jednak pamiętać, że koniunkcja jest również ACUI, podobnie jak dysjunkcja. Więc przejdziesz ten sam proces w innych dowodach, z różnymi typami danych listy, a następnie będziesz miał trzy składnie dla różnych fragmentów logiki separacji, i będziesz miał metatheorems dla każdego z nich, które nieuchronnie będą różne, a zobaczysz, że szukasz metateheoremu, który udowodniłeś dla rozdzielania koniunkcji dla rozłączenia, a potem będziesz chciał mieszać składnie, a potem oszalejesz.
Lepiej jest wycelować w największy fragment, z którym możesz sobie poradzić przy rozsądnym wysiłku, i po prostu zrób to.
Ważne jest, aby zrozumieć, że istnieje spektrum od głębokiego do płytkiego. Głęboko modelujesz części swojego języka, które powinny w jakiś sposób uczestniczyć w indukcyjnym sporze o jego konstrukcję, resztę lepiej pozostawić w płytkiej perspektywie bezpośredniej semantyki podłoża logiki.
Na przykład, jeśli chcesz się zastanowić nad Hoare Logic, możesz modelować język wyrażeń w płytki sposób, ale zarys języka przypisywania jeśli-podczas powinien być konkretnym typem danych. Nie musisz wprowadzać struktury x + y lub a <b, ale musisz pracować z
while
itp.W innych odpowiedziach pojawiły się aluzje do typów zależnych. Przypomina to pradawny problem reprezentowania języków za pomocą segregatorów w rozsądny sposób, tak aby były one tak płytkie, jak to możliwe, ale nadal dopuszczają pewne argumenty indukcyjne. Mam wrażenie, że jury wciąż nie ocenia wszystkich różnych podejść i artykułów, które pojawiły się w ciągu ostatnich 10-20 lat na ten temat. „Wyzwanie POPLmark” dla różnych społeczności asystentów ds. Dowodu również w pewnym stopniu dotyczyło tego.
Co dziwne, w klasycznym HOL bez typów zależnych podejście HOL-Nominal autorstwa C. Urbana działało całkiem dobrze na płytkie wiązanie, chociaż nie nadążało za zmianami kulturowymi w tych społecznościach formalizacji języka programowania.
źródło