Testowanie, czy arbitralny dowód jest okrągły?

13

Myślałem o dowodach i natknąłem się na ciekawą obserwację. Tak więc dowody są równoważne programom za pomocą izomorfizmu Curry'ego-Howarda, a dowody kołowe odpowiadają nieskończonej rekurencji. Wiemy jednak z problemu zatrzymania, że ​​ogólne testowanie, czy dowolny program powróci na zawsze, jest nierozstrzygalne. Czy Curry-Howard oznacza, że ​​nie ma „kontrolera dowodu”, który mógłby ustalić, czy dowód używa rozumowania kołowego?

Zawsze uważałem, że dowody powinny składać się z łatwych do sprawdzenia kroków (które odpowiadają zastosowaniu reguł wnioskowania), a sprawdzenie wszystkich kroków daje pewność, że wniosek jest następujący. Ale teraz zastanawiam się: może tak naprawdę niemożliwe jest napisanie takiego sprawdzania dowodów, ponieważ nie ma sposobu, aby obejść problem zatrzymania i wykryć okrągłe rozumowanie?

logic curry-howard hewasonlyacat
źródło

Odpowiedzi:

15

Ogromna większość systemów dowodowych nie pozwala na nieskończone, okrągłe dowody, ale robią to przez to, że ich języki nie są Turinga kompletne.

W normalnym języku funkcjonalnym jedynym sposobem na uruchomienie programu na zawsze jest rekurencja, a pod względem teorii zwykle patrzymy na rekurencję jako na kombinator , program typu : oznacza to, że bierze funkcję wywołującą inny argument „ja” i zamienia ją w pojedynczą funkcję rekurencyjną.∀ a . ( a → a ) → aY∀a.(a→a)→a

Teraz stosuje izomorfizm Curry-Howard, aby w ten sposób: mamy dowód, że dla każdej propozycja jeśli zakłada się, to możemy okazać . W ten sposób możemy udowodnić wszystko!aaa

Kluczem tutaj jest to, że kombinator Y jest wbudowany w język, jest traktowany jako aksjomat. Jeśli więc nie chcesz, aby powodowało to problemy, po prostu pozbądź się tego jako aksjomat!

Z tego powodu większość formalnych systemów dowodowych wymaga uzasadnienia Twojej rekursji. Akceptują tylko funkcje, które mogą udowodnić, że się zatrzymają. W rezultacie odrzucają niektóre programy, które się zatrzymują, ale których nie mogą tego udowodnić.

Coq robi to w dość ograniczony sposób: wymaga tylko, aby wszelkie funkcje rekurencyjne miały argument, w którym jakiekolwiek wywołania rekurencyjne używają tylko ściśle mniejszych wersji tego argumentu. Agda robi coś podobnego, ale z nieco bardziej fantazyjnym sprawdzaniem, aby zaakceptować kilka innych programów.

jmite
źródło
1
Czy Coq wyklucza pewne uzasadnione twierdzenia, które w innym przypadku można by udowodnić? Czy też zawsze istnieją obejścia, gdy moduł sprawdzania całości jest zbyt konserwatywny? (Zakładam, że odpowiedź jest taka sama dla innych asystentów dowodowych opartych na teorii typu zależnego?)
Stovetop
1
@boyers FWIW, w Coq można użyć Functionlub Program Fixpointkonstrukcji, aby udowodnić, że jakaś funkcja jest całkowita, jeśli sprawdzanie totalności zawiedzie. Prostym przykładem jest funkcja merge-sort na listach. Należy ręcznie udowodnić, że dzielimy listy (o długości> 1) na ściśle mniejsze listy podrzędne.
Anton Trunov
@boyers Tak, muszą być rzeczy, których nie można udowodnić w Coq, według pierwszego twierdzenia Gödela. W praktyce rzadko się je spotyka, ale zawsze pojawia się przekątny argument: Coq nie może udowodnić samego Coq, może jedynie udowodnić podzbiór (bardzo duży podzbiór, umysł, w tym wszystkie funkcje, ale z dolnym limitem, ile rekurencji poradzi sobie). Pamiętam, że czytałem, że teoria Coqa jest równoważna z aksjomatami Peano plus istnienie pewnej dużej porządkowej (a więc dowodów, które zakładają, że jeszcze większa porządkowa nie pasuje), ale nie mogę teraz znaleźć odniesienia.
Gilles „SO- przestań być zły”
@AntonTrunov W tym kontekście Programi tym podobne są czerwone śledzie. Nie zmieniają teorii. To, co robią, to cukier składniowy, aby użyć miary jako dowodu: zamiast rozumować, że obiekt, którym jesteś zainteresowany, staje się mniejszy, dodajesz poziom pośredni: oblicz inny obiekt staje się mniejszy (np. Pewien rozmiar) i udowodnij, że jest zmniejsza się Zobacz Wfbibliotekę.
Gilles „SO- przestań być zły”
@Gilles Zakładam, że kontekst dotyczył praktycznej (konkretnej) strony, na przykład gdy zawodzi heurystyka Coqa ... Czy możesz spróbować znaleźć wspomniany artykuł? Link byłby bardzo mile widziany.
Anton Trunov