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,