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

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?

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 ) → $Y$$\forall a \ldotp (a \to a) \to 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!$a$$a$$a$

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.