Curry-Howard i programy z niekonstruktywnych dowodów

29

To jest kolejne pytanie do

Jaka jest różnica między dowodami a programami (lub między propozycjami i typami)?

Jaki program odpowiadałby niekonstruktywnemu (klasycznemu) dowodowi formy ? (Załóżmy, że jest interesującą zależnością rozstrzygalną, np. ta TM nie zatrzymuje się w krokach ).k T.(mi,k)¬k T.(mi,k)T.mik

(ps: Zadaję to pytanie częściowo dlatego, że jestem zainteresowany dowiedzieć się więcej o tym, co Neel rozumie przez „ tłumaczenie Godela-Gentzena jest przemianą kontynuującą” w jego komentarzu ).

Kaveh
źródło
2
Częściowa odpowiedź na stronie 2 niniejszych notatek z wykładu . To trochę tajemnicze; Spróbuję wykopać coś bardziej kompletnego.
Dave Clarke
Napisanie mojej odpowiedzi zajmuje mi trochę więcej czasu niż planowałem, ponieważ popełniłem błąd, decydując się na udowodnienie rzeczy, które znałem, a nie tylko ich twierdzenie. :)
Neel Krishnaswami
1
Najnowszy JSL miał ten artykuł . Istotą jest to, że zawartość obliczeniowa klasycznych dowodów może silnie zależeć od tego, jak zdecydujesz się je wyodrębnić. Jeszcze go nie strawiłem, ale pomyślałem, że go tam wyrzucę.
Mark Reitblatt
Ale określiłeś, że T jest relatywną relacją, więc wynika z tego, że istnieją konstruktywne dowody twojej propozycji. Logika klasyczna jest podzbiorem logiki intuicyjnej, a Ty określiłeś, że T należy do tego podzbioru, nazywając go rozstrzygalnym.
strzyżyk romano
strzyżyku, tak też myślałem na początku! Ale twierdzenie P w przykładzie P \ / ~ P w pytaniu, jeśli faktycznie jest kwantyfikowane dla całego k, a ta kwantyfikacja T niekoniecznie jest rozstrzygalna.
jbapple,

Odpowiedzi:

25

To interesujące pytanie. Oczywiście nie można oczekiwać, aby mieć program, który decyduje za każdym czy k T ( e , k ) posiada lub nie, jak będzie to decydować o powstrzymanie problem. Jak już wspomniano, istnieje kilka sposobów interpretacji dowodów obliczeniowych: rozszerzenia Curry-Howarda, wykonalność, dialektyka i tak dalej. Ale wszystkie interpretowałyby obliczeniowo twierdzenie, o którym wspomniałeś mniej więcej w następujący sposób.mikT.(mi,k)

Dla uproszczenia rozważ równoważne klasyczne twierdzenie

(1) jajot(¬T.(mi,jot)¬T.(mi,ja))

Jest to (konstruktywnie) równoważne do wspomnianego, ponieważ biorąc pod uwagę , możemy zdecydować, czy k T ( e , k ) utrzymuje się, czy nie, po prostu sprawdzając wartość ¬ T ( e , i ) . Jeśli ¬ T ( e , i ) utrzymuje, to i ¬ T ( e , i ), a zatem ¬ i T ( e , i ) . Jeśli z drugiej stronyjakT.(mi,k)¬T.(mi,ja)¬T.(mi,ja)ja¬T.(mi,ja)¬jaT.(mi,ja) nie obejmuje wtedy (1) mamyj ( ¬ T ( e , j ) ), co oznaczaj T ( e , j ) .¬T.(mi,ja)jot(¬T.(mi,jot))jotT.(mi,jot)

Teraz znowu nie możemy obliczyć w (1) dla każdego podanego e, ponieważ ponownie rozwiązalibyśmy problem zatrzymania. Wszystkie powyższe interpretacje zrobiłyby, patrząc na równoważne twierdzeniejami

(2) faja(¬T.(mi,fa(ja))¬T.(mi,ja))

Funkcja nazywa się funkcją Herbranda. Próbuje obliczyć kontrprzykład j dla każdego potencjalnego świadka i . Oczywiste jest, że (1) i (2) są równoważne. Od lewej do prawej jest to konstruktywne, wystarczy wziąć i = i w (2), gdzie i jest założonym świadkiem (1). Od prawej do lewej trzeba klasycznie rozumować. Załóżmy, że (1) nie było prawdą. Następnie,fajotjaja=jaja

(3) jajot¬(¬T.(mi,jot)¬T.(mi,ja))

Niech będzie funkcją świadczącą o tym, tjfa

(4) i¬(¬T(e,f(i))¬T(e,i))

Teraz weźmy w (2) i mamy ( ¬ T ( e , f ( i ) ) ¬ T ( e , i ) ) , dla niektórych i . Ale przyjmując i = i w (4) otrzymujemy negację tego, sprzeczność. Stąd (2) implikuje (1).f=f(¬T(e,f(i))¬T(e,i))ii=i

Mamy więc, że (1) i (2) są klasycznie równoważne. Ale interesujące jest to, że (2) ma teraz bardzo prostego konstruktywnego świadka. Po prostu weź jeśli T ( e , f ( 0 ) ) się nie utrzymuje, ponieważ wtedy wniosek (2) jest prawdziwy; albo weźmy i = 0, jeśli T ( e , f ( 0 ) ) utrzymuje się, ponieważ wtedy ¬ T ( e , f ( 0 )i=f(0)T(e,f(0))ja=0T.(mi,fa(0)) nie obowiązuje, a przesłanka (2) jest fałszywa, co czyni ją ponownie prawdą.¬T.(mi,fa(0))

Stąd sposobem na obliczeniową interpretację klasycznego twierdzenia, takiego jak (1), jest przyjrzenie się (klasycznie) równoważnemu sformułowaniu, które można konstruktywnie udowodnić, w naszym przypadku (2).

Różne wspomniane powyżej interpretacje różnią się jedynie sposobem wyskakiwania funkcji . W przypadku wykonalności i interpretacji dialektycznej jest to wyraźnie podane przez interpretację, w połączeniu z pewną formą tłumaczenia negatywnego (jak Goedel-Gentzen). W przypadku rozszerzeń Curry-Howard z operatorami call-cc i kontynuującymi funkcja f wynika z faktu, że program może „wiedzieć”, w jaki sposób zostanie użyta określona wartość (w naszym przypadku i ), więc f jest kontynuacją programu wokół punktu, gdzie I jest obliczany.fafajafaja

Inną ważną kwestią jest to, że chcesz, aby przejście z (1) do (2) było „modułowe”, tj. Jeśli (1) zostanie użyte do udowodnienia (1 '), to jego interpretacja (2) powinna być użyta w podobny sposób aby udowodnić interpretację (1 '), powiedz (2'). Robią to wszystkie wspomniane powyżej interpretacje, w tym negatywne tłumaczenie Goedel-Gentzen.

Paulo
źródło
8
Witamy! Wspaniale jest zobaczyć tutaj eksperta teoretycznego.
Neel Krishnaswami,
1
Dzięki Paulo, twoja odpowiedź wyjaśniła część obrazu w powiązanym problemie, nad którym pracuję.
Kaveh
17

Dość dobrze wiadomo, że arytmetyka klasyczna i intuicyjna są równorzędne.

Jednym ze sposobów wykazania tego jest „negatywne osadzenie” logiki klasycznej w logice intuicyjnej. Załóżmy więc, że są formułami klasycznej arytmetyki pierwszego rzędu. Teraz możemy zdefiniować formułę intuicyjnej logiki w następujący sposób:ϕ

G()=¬¬G(ϕψ)=¬¬(G(ϕ)G(ψ))G()=¬G(¬ϕ)=¬G(ϕ)G(ϕψ)=¬(¬G(ϕ)¬G(ψ))G(x.ϕ)=x.¬¬G(ϕ)G(x.ϕ)=¬x.¬(G(ϕ))G(P)=¬¬P

Zauważ, że jest w zasadzie homomorfizmem, który utkwił w dodatkowych nie-nieobecnych wszędzie, z wyjątkiem tego, że w rozbieżnościach i egzystencjalnościach używa dualności de Morgana, aby przekształcić je w koniunkcje i uniwersalia. (Jestem pewien, że nie jest to dokładne tłumaczenie Godela-Gentzena, ponieważ przygotowałem go do tej odpowiedzi - w zasadzie wszystko, co napiszesz za pomocą podwójnej negacji + dualności de Morgana, zadziała. Ta różnorodność okazuje się być ważna dla interpretacyjne obliczenia klasycznej logiki; patrz poniżej.)G(ϕ)

Po pierwsze: oczywiste jest, że to tłumaczenie zachowuje klasyczną prawdę, więc jest prawdziwe, jeśli i tylko jeśli ϕ jest, klasycznie rzecz biorąc.G(ϕ)ϕ

Po drugie: jest to mniej oczywiste, ale nadal tak jest, w przypadku formuł w fragment, sprawdzalność w intuicyjnej i klasycznej logice pokrywają się. Aby to udowodnić, należy najpierw spojrzeć na formuły zaczerpnięte z tej gramatyki:,,,¬

A,B::=x.A(x)|AB|AB|¬A|¬¬P

A następnie możemy udowodnić jako lemat (przez indukcję na ), że G ( A )A można uzyskać intuicyjnie. Możemy więc teraz wykazać równoważność formuł ujemnych, wykonując indukcję nad strukturą dowodu (np. Rachunek sekwencyjny) i wykorzystać poprzedni lemat do symulacji prawa wykluczonego środka.G(A)A

Więc jak powinieneś o tym myśleć intuicyjnie?

  • Po pierwsze, pogląd teoretyczny. Jeśli spojrzysz na reguły rachunku sekwencyjnego, zobaczysz, że jedyne miejsce, w którym klasyczna i intuicyjna logika poważnie się różni, to reguły rozróżnienia i egzystencji. Wykorzystujemy ten fakt, aby pokazać, że dowody w jednej logice tych formuł można przełożyć na dowody w drugim. To pokazuje, jak myśleć o logice konstruktywnej jako rozszerzeniu logiki klasycznej o dwa nowe łączniki i . To, co nazywamy „klasycznym istnieniem” i „klasycznym rozłączeniem”, to tylko skróty obejmujące , koniunkcję i negację, więc aby mówić o faktycznym istnieniu, musieliśmy wprowadzić nowe łączniki.

  • Po drugie, jest widok topologiczny. Teraz modelem klasycznej logiki (jako rodziny zestawów) jest algebra boolowska (tj. Rodzina podzbiorów zamkniętych w dowolnych związkach, przecięciach i uzupełnieniach). Okazuje się, że model logiki intuicyjnej jest przestrzenią topologiczną , a zdania interpretowane są jako zbiory otwarte. Ich interpretacja negacji jest wnętrzem dopełniacza, a następnie łatwo jest wykazać, że , co oznacza, że ​​podwójna negacja wysyła nas do najmniejszego klopenu pokrywającego każde otwarcie --- a klopeny tworzą Algebra boolowska.¬¬¬P=¬P

Teraz dzięki Curry-Howard wiemy, jak interpretować dowody w intuicyjnej logice jako programy funkcjonalne. Tak więc, jedna możliwa odpowiedź (ale nie jedyna) na pytanie „jaka jest konstruktywna treść klasycznego dowodu?” jest następujący:

Zawartość obliczeniowa klasycznego dowodu jest dowolną zawartością obliczeniową tłumaczenia jego dowodu (zgodnie z tłumaczeniem negatywnym).

Spójrzmy więc na tłumaczenie . Oznacza to, że konstruktywna treść wykluczonego środka jest tym samym, co stwierdzenie, że ¬ P i ¬ ¬ P nie mają - tzn. Brak sprzeczności. W tym sensie w prawie wykluczonego środka nie ma tak naprawdę dużo treści obliczeniowych.G(A¬A)=¬(¬G(A)¬¬G(A))¬P¬¬P

Aby zobaczyć, co to konkretnie, pamiętaj, że konstruktywnie, negacja jest zdefiniowana jako . Więc ta formuła jest ( ( G ( A ))¬A==A . Poniższy bit kodu Ocaml zilustruje:((G(A))((G(A))))

type bot = Void of bot
type 'a not = 'a -> bot

let excluded_middle : ('a not * 'a not not) not = fun (u, k) -> k u 

To znaczy, jeśli dostaniesz nie-A i nie-nie-A, możesz po prostu przekazać pierwszą negację drugiemu, aby uzyskać pożądaną sprzeczność.

Czym są kontynuacje transformacji w stylu przejścia?

  • ττ
  • 3+5C[3+5]3+5
  • τταα
  • miτ(τα)αmi
  • Ale musimy to zrobić dziedzicznie, aby każdy subtermin programu jasno określał jego kontynuację.

Teraz,

  • ϕ¬¬ϕ
  • Jednakże, chociaż nasze tłumaczenie wykorzystuje negację, tak naprawdę nigdy nie eliminuje fałszywej propozycji - więc tłumaczenie działa parametrycznie w tej propozycji.
  • α
  • ϕ(ϕα)α
  • To jest transformacja CPS.

Widziałem transformację „a” CPS, ponieważ, jak wspomniałem wcześniej, istnieje wiele negatywnych tłumaczeń, które pozwalają udowodnić to twierdzenie, a każde z nich odpowiada innej transformacji CPS. Pod względem operacyjnym każda transformacja odpowiada innej kolejności oceny . Nie ma więc wyjątkowej interpretacyjnej interpretacji klasycznej logiki, ponieważ masz do wyboru, a wybory różnicowe mają bardzo różne cechy operacyjne.

Neel Krishnaswami
źródło
3
To świetna odpowiedź. Przypomniało mi to artykuł Wadlera „Call-by-value jest dwojakie od call-by-name”: homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html , który zawiera bardzo niezapomnianą anegdotę w sekcji 4, aby wyjaśnić związek między callCC a wykluczonym środkiem.
sclv,
8

Są całe konferencje na temat niekonstruktywnych dowodów jako programów i nie jestem ekspertem w tej dziedzinie. Powyżej Neel Krishnaswami nawiązał do dłuższej odpowiedzi, którą przygotowuje, która, sądząc po jego pracy tutaj, będzie doskonała. To tylko smak odpowiedzi.

P,P¬P

Set Implicit Arguments.

Axiom callcc : forall (A B : Set), ((A -> B) -> A) -> A.

Lemma lem : forall (A B:Set), sum A (A -> B).
Proof.
  intros.
  eapply callcc.
  intros H.
  right.
  intros.
  apply H.
  left.
  assumption.
Defined.

Recursive Extraction lem.

podaje kod O'Caml:

type ('a, 'b) sum =
  | Inl of 'a
  | Inr of 'b

(** val callcc : (('a1 -> 'a2) -> 'a1) -> 'a1 **)

let callcc =
  failwith "AXIOM TO BE REALIZED"

(** val lem : ('a1, 'a1 -> no) sum **)

let lem =
    callcc (fun h -> Inr (fun h0 -> h (Inl h0)))

Najczystsze wprowadzenie do tego, jakie widziałem, znajduje się w „Teście pojęcia kontroli formułami jako typy” Tima Griffina .

jbapple
źródło
3
Powinieneś spróbować wypakować do Schematu i powiedzieć, że procedura wyodrębnienia powinna wypakować callccdo Schematu callcc. Wtedy możesz faktycznie wypróbować różne rzeczy.
Andrej Bauer,