Curry-Howard i programy z niekonstruktywnych dowodów

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 ). $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$ $T$ $e$ $k$

(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 ).

lo.logic pl.programming-languages proof-theory

— Kaveh
źródło

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

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:

To interesujące pytanie. Oczywiście nie można oczekiwać, aby mieć program, który decyduje za każdym czy 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. $e$ $\forall k T(e, k)$

Dla uproszczenia rozważ równoważne klasyczne twierdzenie

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

Jest to (konstruktywnie) równoważne do wspomnianego, ponieważ biorąc pod uwagę , możemy zdecydować, czy utrzymuje się, czy nie, po prostu sprawdzając wartość . Jeśli utrzymuje, to a zatem . Jeśli z drugiej strony $i$ $\forall k T(e, k)$ $\neg T(e, i)$ $\neg T(e, i)$ $\exists i \neg T(e, i)$ $\neg \forall i T(e, i)$ nie obejmuje wtedy (1) mamy co oznacza . $\neg T(e, i)$ $\forall j (\neg T(e, j) \to \bot)$ $\forall j T(e, j)$

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

(2) $\forall f \exists i' (\neg T(e, f(i')) \to \neg T(e, i'))$

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

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$

Niech będzie funkcją świadczącą o tym, tj $f'$

(4) $\forall i \neg (\neg T(e, f'(i)) \to \neg T(e, i))$

Teraz weźmy w (2) i mamy , dla niektórych . Ale przyjmując w (4) otrzymujemy negację tego, sprzeczność. Stąd (2) implikuje (1). $f = f'$ $(\neg T(e, f'(i')) \to \neg T(e, i'))$ $i'$ $i = 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 się nie utrzymuje, ponieważ wtedy wniosek (2) jest prawdziwy; albo weźmy jeśli utrzymuje się, ponieważ wtedy $i' = f(0)$ $T(e, f(0))$ $i' = 0$ $T(e, f(0))$ nie obowiązuje, a przesłanka (2) jest fałszywa, co czyni ją ponownie prawdą. $\neg T(e, f(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 wynika z faktu, że program może „wiedzieć”, w jaki sposób zostanie użyta określona wartość (w naszym przypadku ), więc jest kontynuacją programu wokół punktu, gdzie jest obliczany. $f$ $f$ $i$ $f$ $i$

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

Witamy! Wspaniale jest zobaczyć tutaj eksperta teoretycznego.

— Neel Krishnaswami,

Dzięki Paulo, twoja odpowiedź wyjaśniła część obrazu w powiązanym problemie, nad którym pracuję.

— Kaveh

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: $\phi$

\begin{array}{lcl} G (⊤) & = & \neg \neg ⊤ \\ G (ϕ \land ψ) & = & \neg \neg (G (ϕ) \land G (ψ)) \\ G (⊥) & = & \neg ⊤ \\ G (\neg ϕ) & = & \neg G (ϕ) \\ G (ϕ \lor ψ) & = & \neg (\neg G (ϕ) \land \neg G (ψ)) \\ G (\forall x . ϕ) & = & \forall x . \neg \neg G (ϕ) \\ G (\exists x . ϕ) & = & \neg \forall x . \neg (G (ϕ)) \\ G (P) & = & \neg \neg P \end{array}

$\begin{array}{lcl} G(\top) & = & \lnot\lnot\top \\ G(\phi \land \psi) & = & \lnot\lnot(G(\phi) \land G(\psi)) \\ G(\bot) & = & \lnot\top \\ G(\lnot\phi) & = & \lnot G(\phi) \\ G(\phi \vee \psi) & = & \lnot(\lnot G(\phi) \land \lnot G(\psi)) \\ G(\forall x.\;\phi) & = & \forall x.\; \lnot\lnot G(\phi) \\ G(\exists x.\;\phi) & = & \lnot \forall x.\; \lnot(G(\phi)) \\ G(P) & = & \lnot\lnot P \\ \end{array}$

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(\phi)$

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(\phi)$ $\phi$

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: $\forall, \implies, \land, \lnot$

\begin{array}{lcl} A, B & ::= & \forall x . A (x) | A ⟹ B | A \land B | \neg A | \neg \neg P \end{array}

$\newcommand{\bnfalt}{\;\;|\;\;} \begin{array}{lcl} A,B & ::= & \forall x.\;A(x) \bnfalt A \implies B \bnfalt A \land B \bnfalt \lnot A \bnfalt \lnot\lnot P \end{array}$

A następnie możemy udowodnić jako lemat (przez indukcję na ), że $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) \implies 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. $\exists$ $\vee$ $\forall$
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. $\lnot\lnot\lnot P = \lnot 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 i mają - tzn. Brak sprzeczności. W tym sensie w prawie wykluczonego środka nie ma tak naprawdę dużo treści obliczeniowych. $G(A \vee \lnot A) = \lnot(\lnot G(A) \land \lnot\lnot G(A))$ $\lnot P$ $\lnot\lnot P$

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

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?

$\tau$ $\tau$
$3+5$ $C[3+5]$ $3 + 5$
$\tau$ $\tau \to \alpha$ $\alpha$
$e$ $\tau$ $(\tau \to \alpha) \to \alpha$ $e$
Ale musimy to zrobić dziedzicznie, aby każdy subtermin programu jasno określał jego kontynuację.

Teraz,

$\phi$ $\lnot\lnot\phi$
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.
$\bot$ $\alpha$
$\phi$ $(\phi \to \alpha) \to \alpha$
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

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,

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.

$\forall P, P \lor \lnot 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

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,