Jak powinienem myśleć o siatkach próbnych?

W swojej odpowiedzi na to pytanie , Stephane Gimenez wskazał mi algorytm normalizacji wielomian czasu do dowodów w logice liniowej. Dowód w artykule Girarda wykorzystuje siatki próbne, które są aspektem logiki liniowej, o której tak naprawdę niewiele wiem.

Teraz próbowałem już czytać artykuły na temat siatek próbnych (takie jak notatki Pierre-Louis Curien na ich temat), ale tak naprawdę ich nie rozumiałem. Moje pytanie brzmi: jak mam o nich myśleć? Przez „jak o nich myśleć” mam na myśli zarówno nieformalną intuicję stojącą za nimi (np. Jak zachowują się obliczeniowo lub w jaki sposób są powiązane z sekwencjami), a także jakie twierdzenia na ich temat powinienem sam udowodnić, aby naprawdę je zdobyć.

Odpowiadając na to pytanie, możesz założyć (1), że znam dobrze teorię dowodu logiki liniowej (w tym rzeczy takie jak przebieg dowodu eliminacji cięć, a także w formie zogniskowanej), (2) ich kategoryczną semantykę pod względem przestrzeni koherencji lub poprzez splot w ciągu dnia i (3) bardzo podstawowe podstawy konstrukcji GoI.

Siatki próbne są interesujące zasadniczo z trzech powodów:

1) TOŻSAMOŚĆ DOWODÓW. Stanowią odpowiedź na problem „kiedy dwa dowody są takie same”? W rachunku różniczkowym możesz mieć wiele różnych dowodów tej samej twierdzenia, które różnią się tylko tym, że rachunek różny wymusza porządek wśród reguł dedukcyjnych, nawet jeśli nie jest to konieczne. Oczywiście można dodać relację równoważności do kolejnych dowodów rachunku różniczkowego, ale potem trzeba wykazać, że eliminacja cięć zachowuje się poprawnie w klasach równoważności, a także konieczne jest przejście do przepisywania modulo, które jest o wiele bardziej techniczne niż zwykłe przepisywanie. Sieci sprawdzające rozwiązują problem radzenia sobie z klasami równoważności, zapewniając składnię, w której każda klasa równoważności jest zwinięta na jednym obiekcie. Ta sytuacja jest i tak nieco idealistyczna, ponieważ z wielu powodów sieci dowodowe są często rozszerzane o pewną formę równoważności.

2) BRAK KOMUTATYWNYCH KROKÓW ELIMINACJI. Eliminacja cięć w siatkach próbnych przybiera zupełnie inny smak niż w sekwencyjnych rachunkach, ponieważ znikają etapy przemiennej eliminacji cięć. Powodem jest to, że w sieciach dowodowych reguły odliczeń są powiązane jedynie ich relacją przyczynową. Przypadki przemienne generowane są przez fakt, że jedną regułę można ukryć za pomocą innej przyczynowo niezwiązanej reguły. Nie może się to zdarzyć w sieciach dowodowych, w których reguły przyczynowo niepowiązane są daleko od siebie. Ponieważ większość przypadków eliminacji cięć ma charakter przemienny, uzyskuje się uderzające uproszczenie eliminacji cięć. Jest to szczególnie przydatne do badania rachunku lambda z wyraźnymi podstawieniami (ponieważ wykładnicze = wyraźne podstawienia). Ponownie sytuacja ta jest idealizowana, ponieważ niektóre prezentacje sieci próbnych wymagają kroków przemiennych. Jednak,

3) KRYTERIA POPRAWNOŚCI. Siatki próbne można zdefiniować przez tłumaczenie kolejnych dowodów rachunku różniczkowego, ale zwykle system siatek dowodowych nie jest jako taki akceptowany, chyba że jest wyposażony w kryterium poprawności, tj. Zbiór zasad teoretyczno-graficznych charakteryzujących zbiór wykresów uzyskany przez przetłumaczenie kolejny rachunek różniczkowy. Powodem wymagania kryterium poprawności jest to, że wolny język graficzny generowany przez zestaw konstruktorów sieci proof (zwanych linkami) zawiera „zbyt wiele grafów”, w tym sensie, że niektóre wykresy nie odpowiadają żadnym dowodom. Znaczenie podejścia opartego na kryteriach poprawności jest zwykle całkowicie niezrozumiane. Jest to ważne, ponieważ daje nieindukcyjne definicje tego, co jest dowodem, zapewniając szokująco odmienne spojrzenie na charakter dedukcji. Fakt, że charakterystyka jest nieindukcyjna, jest zwykle krytykowany, podczas gdy jest dokładnie tym, co interesujące. Oczywiście nie jest łatwo poddać się formalizacji, ale znowu taka jest jego siła: siatki dowodowe zapewniają wgląd, który nie jest dostępny w zwykłej indukcyjnej perspektywie na dowodach i warunkach. Fundamentalnym twierdzeniem dla siatek dowodowych jest twierdzenie sekwencjonowania, które mówi, że każdy wykres spełniający kryterium poprawności może być indukcyjnie rozłożony jako sekwencyjny dowód różniczkowy (przełożenie z powrotem na prawidłowy wykres).

Pozwolę sobie stwierdzić, że nie jest precyzyjne stwierdzenie, że siatki dowodowe to klasyczna i liniowa wersja naturalnej dedukcji. Chodzi o to, że rozwiązują (lub próbują rozwiązać) problem tożsamości dowodów i że naturalna dedukcja z powodzeniem rozwiązuje ten sam problem przy minimalnej intuicyjnej logice. Ale siatki dowodowe można wykonać również w przypadku systemów intuicyjnych i systemów nieliniowych. W rzeczywistości działają lepiej dla systemów intuicyjnych niż dla systemów klasycznych.

$-A$$A$$-A$$A$

Girard zauważył, że naturalne odliczenie jest właśnie w ten sposób asymetryczne. Dlatego pasuje do intuicyjnej logiki. Siatki dowodowe reprezentują próbę Girarda wynalezienia symetrycznej formy naturalnej dedukcji.

$\land\to$

$\Gamma \vdash A$$\vdash \Gamma^\perp, A$

Coś, co przeoczyłem w mojej oryginalnej odpowiedzi: siatki próbne są sposobem pisania dowodów, a wiemy, że dowody są programami. Siatki próbne są więc także sposobem pisania programów.

Tradycyjna notacja funkcjonalna do pisania programów jest asymetryczna, podobnie jak naturalna dedukcja. Sieci dowodowe wskazują więc na sposób pisania programów w symetrycznej formie. W ten sposób na obraz wkraczają rachunki procesowe.

Innym sposobem przedstawienia symetrii jest programowanie logiczne, które zbadałem w dwóch artykułach: Podstawy programowe dla programów logiki kierunkowej i aspekty programowania logicznego wyższego rzędu

Skupiam się na tym, jak siatki próbne są powiązane z rachunkiem sekwencyjnym, pozostawiając bardziej dynamiczne rzeczy.

Siatki próbne abstrakcyjne sekwencyjne dowody różniczkowe: siatka próbna reprezentuje zestaw następnych prób różniczkowych. Sieci dowodowe zapominają o nieistotnych różnicach między kolejnymi dowodami rachunku różniczkowego (np. Która formuła jest rozkładana poniżej której). Ważnym twierdzeniem jest tutaj „sekwencjonowanie”, które przekształca siatkę próbną w sekwencyjny dowód różniczkowy.

Odnosi się to głównie do części „pytania, jak zachowują się obliczeniowo”. Jednym ze sposobów dobrego zrozumienia sieci dowodowych z perspektywy obliczeniowej jest przyjrzenie się nieco bardziej konkretnym interpretacjom (np. Algebraicznym procesom).

Możesz być zainteresowany:

• Artykuł Abramsky'ego (sekcja CLL na temat wyrażeń dowodowych): Interpretacje obliczeniowe logiki liniowej . W tym dokumencie przedstawiono także wyniki, które są zbliżone do wyników dla siatek próbnych, więc może pomóc w drugim aspekcie pytania.

• Artykuł Hondy i Laurenta, w którym pokazano, w jaki sposób określony rodzaj siatek próbnych, zwanych spolaryzowanymi siatkami próbnymi, odpowiada procesom rachunku pi, i który jest wspomniany powyżej przez Martina Bergera: dokładna zgodność między pisanym rachunkiem pi i spolaryzowanym dowodem- sieci

• (tutaj bezwstydnie reklamuję własną pracę) Projekt: Proof Nets in Process Algebraic Form

Istnieje również kilka prac związanych z siatkami dowodowymi i rachunkiem lambda, które również dają istotne intuicje. Na przykład następujące: Delia Kesner i Stéphane Lengrand:

• Operatory zasobów dla rachunku λ

Być może zainteresuje Cię ten rodzaj pracy (bardzo zorientowanej na aspekty teoretyczne), która polega na Proof Structures, aby szczegółowo udowodnić właściwość Silnej Normalizacji LL, autorstwa Michele Pagani i Lorenza Tortora de Falco.

• Silna właściwość normalizacyjna dla logiki liniowej drugiego rzędu (ten artykuł zawiera ładną mapę ważnych twierdzeń).

Ogólnie, jakie twierdzenia należy zbadać? Cóż, raczej nie jestem autorytetem, ale możesz chcieć przyjrzeć się „Sekwencjonowaniu” (odnoszącemu się do siatek dowodowych i sekwencyjnych dowodów; patrz oryginalny dokument TCS na LL) i silnym dowodzie normalizacji (raczej zaangażowanym, jak oczekiwano, ale wielu ważnych Twierdzenia PN są z tym związane [lub służą do jego udowodnienia]).

Jeśli jesteś zaznajomiony z ustawianiem ostrości, być może zainteresuje Cię ten artykuł Andreoli:

• Skupienie i siatki próbne w logice liniowej i nieprzemiennej

Mam nadzieję że to pomoże. Ponownie odniesienia te są naprawdę niewyczerpujące.

najlepiej, Dimitris

Ostatnio przeprowadzono interesującą pracę nad ściślejszym powiązaniem siatki próbnej z kalkulatorem skupionym, wykorzystując warianty „wieloogniskowe”, w których można mieć kilka lewych otworów jednocześnie, i badając dowody „maksymalnie skoncentrowane”. Jeśli wybierzesz rachunek różniczkowy, maksymalnie skoncentrowane dowody mogą odpowiadać siatkom dowodowym MLL lub, w klasycznej logice , dowodom ekspansji ( Izomorfizm między dowodami ekspansji i wieloogniskowymi dowodami sekwencyjnymi, Kaustuv Chaudhuri, Stefan Hetzl i Dale Miller, 2013)

Możesz sprawdzić mój artykuł „ Przegląd sieci próbnych i matryc dla logiki podstrukturalnej ”.

Abstrakcyjny:

Ten artykuł jest przeglądem dwóch rodzajów „skompresowanych” schematów próbnych, \ emph {metoda matrycy} i \ emph {siatki próbne}, stosowanych w różnych logikach, począwszy od hierarchii podstrukturalnej, aż po klasyczne niesocjacyjny system Lambka. Zapewniono nowe podejście do siatek próbnych dla tych ostatnich. Opisy siatek próbnych i macierzy podane są w jednolitej notacji opartej na sekwencjach, dzięki czemu właściwości schematów dla różnych układów logicznych można łatwo porównać.