Dlaczego Coq ma Prop?

Coq ma typ Prop dowodu nieistotne propozycje, które są odrzucane podczas ekstrakcji. Jaki jest tego powód, jeśli używamy Coq tylko do dowodów. Rekwizyt jest impredykatywny, więc Prop: Prop, Coq automatycznie wyszukuje indeksy wszechświata i zamiast tego możemy używać Type (i) wszędzie. Wygląda na to, że Prop bardzo wszystko komplikuje.

Czytałem, że istnieją filozoficzne powody oddzielenia Seta i Propa w książce Luo, jednak nie znalazłem ich w książce. Czym oni są?

$\mathtt{Prop}$ jest bardzo przydatny do ekstrakcji programu, ponieważ pozwala nam usuwać części kodu, które są bezużyteczne. Na przykład, aby wyodrębnić algorytm sortowania, udowodnilibyśmy zdanie „dla każdej listy istnieje lista taka, że jest uporządkowane, a jest permutatiom z ”. Jeśli zapiszemy to w Coq i wyodrębnimy bez użycia , otrzymamy:k k k ℓ P r o $\ell$$k$$k$$k$$\ell$$\mathtt{Prop}$

1. „dla wszystkich jest ” da nam mapę, która przenosi listy do list,$\ell$$k$sort
2. „takie, że jest uporządkowane” da funciton, który biegnie przez i sprawdza, czy jest posortowany, i$k$verify$k$
3. „ jest permutacją ” daje permutację, która prowadzi do . Zauważ, że to nie tylko mapowanie, ale także mapowanie odwrotne wraz z programami weryfikującymi, czy te dwie mapy są rzeczywiście odwrotne.ℓ ℓ $k$$\ell$pi$\ell$$k$pi

Podczas gdy dodatkowe rzeczy nie są całkowicie bezużyteczne, w wielu aplikacjach chcemy się ich pozbyć i zachować sprawiedliwość sort. Można to osiągnąć, jeśli użyjemy aby stwierdzić, że „ jest uporządkowane”, a „ jest permutacją ”, ale nie „dla wszystkich istnieje ”. k k ℓ ℓ $\mathtt{Prop}$$k$$k$$\ell$$\ell$$k$

Ogólnie powszechnym sposobem na wyodrębnienie kodu jest rozważenie wyrażenia w postaci gdzie jest wprowadzane, jest wyjściem, a wyjaśnia, co to znaczy, że jest poprawnym wyjściem. (W powyższym przykładzie i to typy list, a to „ jest uporządkowane, a jest permutacją .”) Jeśli znajduje się w to wyodrębnij daje mapę taką, że dla wszystkichx y ϕ ( x , y ) y A B ϕ ( ℓ , k ) k k ℓ ϕ P r o p f : A → B ϕ ( x , f ( x ) ) x ∈ A ϕ S e t g g ( x ) ϕ ( x $\forall x : A \,.\, \exists y : B \,.\, \phi(x, y)$$x$$y$$\phi(x,y)$$y$$A$$B$$\phi(\ell, k)$$k$$k$$\ell$$\phi$$\mathtt{Prop}$$f : A \to B$$\phi(x, f(x))$$x \in A$ . Jeśli znajduje się w wtedy również uzyskać funkcję takie, że jest dowodem na to, że posiada, dla każdego . Często dowód jest bezużyteczny obliczeniowo i wolimy się go pozbyć, zwłaszcza gdy jest głęboko zagnieżdżony w innym wyrażeniu. daje nam taką możliwość.$\phi$$\mathtt{Set}$$g$$g(x)$x ∈ A P r o $\phi(x, f(x))$$x \in A$$\mathtt{Prop}$

Dodano 2015-07-29: Istnieje pytanie, czy moglibyśmy całkowicie uniknąć , automatycznie optymalizując „bezużyteczny wyodrębniony kod”. Do pewnego stopnia możemy to zrobić, na przykład cały kod wyodrębniony z negatywnego fragmentu logiki (rzeczy zbudowane z pustego typu, typu jednostki, produktów) jest bezużyteczny, ponieważ tylko tasuje wokół jednostki. Ale przy użyciu należy podjąć autentyczne decyzje projektowe . Oto prosty przykład, w którym oznacza, że ​​jesteśmy w a oznacza, że ​​jesteśmy w . Jeśli wyciągniemy z P r o p Σ T y p e ∃ P r o p Π n : N Σ b : { 0 , 1 } Σ k : $\mathsf{Prop}$$\mathsf{Prop}$$\Sigma$$\mathsf{Type}$$\exists$$\mathsf{Prop}$n b k Π n : N Σ b : { 0 , 1 } ∃ k :

$$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \Sigma_{k : \mathbb{N}} \; n = 2 \cdot k + b$$ otrzymamy program, który rozkłada na najniższy bit a pozostałe bity , tzn. oblicza wszystko. Jeśli wyciągniemy z wówczas program obliczy tylko najniższy bit . Maszyna nie może powiedzieć, który jest prawidłowy, użytkownik musi powiedzieć mu, czego chce.$n$$b$$k$ $$\Pi_{n : \mathbb{N}} \Sigma_{b : \{0,1\}} \exists_{k : \mathbb{N}} \; n = 2 \cdot k + b$$ $b$

$\mathrm{Prop}$ jest impredykacyjny , co tworzy bardzo ekspresyjny system dowodowy. Jest jednak „zbyt” ekspresyjny w następującym znaczeniu:

$$\mathrm{impredicative\ Prop} + \mathrm{large\ elimination} + \mathrm{excluded\ middle}$$

jest niespójny. Zwykle chcesz zachować możliwość dodania wykluczonego środka, więc jednym z rozwiązań jest utrzymanie dużej eliminacji i uczynienie Prop predykatywnym. Drugim jest powstrzymanie dużej eliminacji.

Coq zrobił oba! Zmienili nazwę predykatywnej Prop na Set i wyłączili dużą eliminację w Prop.

Ekspresyjność uzyskana przez impredykatywność jest „uspokajająca” w tym sensie, że 99% „rozsądnej” matematyki można z nią sformalizować i wiadomo, że jest spójna w stosunku do teorii mnogości. To sprawia, że ​​prawdopodobnie nie osłabią go do czegoś takiego jak Agda, która ma tylko predykatywne wszechświaty.

Nawet jeśli nie jesteś zainteresowany wydobywaniem programów, fakt, że Propjest impredykatywny, pozwala ci budować modele, których nie możesz zbudować za pomocą predykcyjnej wieży wszechświatów. IIRC Thorsten Altenkirch ma model Systemu F wykorzystujący impredykatywność Coqa.