„Minimalna” intuicyjna teoria typów?

Dziwi mnie, że ludzie ciągle dodają nowe typy do teorii typów, ale wydaje się, że nikt nie wspomina o teorii minimalnej (lub nie mogę jej znaleźć). Myślałem, że matematyk uwielbia minimalne rzeczy, prawda?

Jeśli dobrze rozumiem, w teorii typów z impredykatywnym wystarczy Propλ-abstrakcja i Π-typy. Mówiąc wystarczająco, mam na myśli, że można go użyć jako intuicyjnej logiki. Inne typy można zdefiniować następująco:

$$\bot \stackrel{def}{=} \Pi \alpha: Prop. \alpha \\ \neg A \stackrel{def}{=} A \to \bot \\ A \land B \stackrel{def}{=} \Pi C: Prop. (A \to B \to C) \to C \\ A \lor B \stackrel{def}{=} \Pi C: Prop. (A \to C) \to (B \to C) \to C \\ \exists_{x: S}(P(x)) \stackrel{def}{=} \Pi \alpha: Prop. (\Pi x: S. P x \to \alpha) \to \alpha \\ $$

Moje pierwsze pytanie brzmi: czy one ( λ, Π) naprawdę wystarczają? Moje drugie pytanie brzmi: czego potrzebujemy minimalnie, jeśli nie mamy impredykatu Prop, takiego jak w MLTT? W MLTT kodowanie Church / Scott / cokolwiek nie działa.

Edycja: powiązane

Aby rozwinąć wyjaśnienia Gallais, teorię typów z impredykatywną Prop i typy zależne można postrzegać jako pewien podsystem rachunku konstrukcji, zazwyczaj zbliżony do teorii typów Kościoła . Związek między teorią typów Kościoła a CoC nie jest taki prosty, ale został zbadany, w szczególności w doskonałym artykule Geuversa .

Jednak dla większości celów systemy można uznać za równoważne. Rzeczywiście, możesz sobie z tym poradzić bardzo mało, zwłaszcza jeśli nie interesuje Cię klasyczna logika, wtedy jedyne, czego naprawdę potrzebujesz, to aksjomat nieskończoności : w CoC nie można udowodnić, że każdy typ ma więcej niż 1 element! Ale z aksjomatem wyrażającym, że jakiś typ jest nieskończony, powiedzmy, że typ liczb naturalnych z zasadą indukcji i aksjomatem , można dojść dość daleko: większość matematyki na poziomie licencjackim można sformalizować w tym systemie (w pewnym sensie jest to trudne zrobić pewne rzeczy bez wykluczonego środka).$0\neq 1$

Bez impredicative Prop potrzebujesz trochę więcej pracy. Jak zauważono w komentarzach, system rozciągającym (układ z funkcjonalną ekstensjonalności w stosunku równości) można dostać się tylko i Π -types, B O O l , puste i jednostki typu ⊥ i ⊤ i W typy. W ustawieniu intensywnym nie jest to możliwe: potrzebujesz o wiele więcej indukcyjnych. Należy pamiętać, że aby zbudować użytecznych W-typy, trzeba być w stanie zbudować rodzajów poprzez eliminację ponad B o, o, l tak:$\Sigma$$\Pi$$\mathrm{Bool}$$\bot$$\top$$\mathrm{Bool}$

$$\mathrm{if}\ b\ \mathrm{then}\ \top\ \mathrm{else}\ \bot$$

Do wykonywania meta-matematyki prawdopodobnie potrzebujesz co najmniej jednego wszechświata (powiedzmy, aby zbudować model arytmetyki Heytinga).

$\Pi\Sigma$

Przydatnym omówieniem jest artykuł Czy ZF to hack? Freek Wiedijk, który faktycznie porównuje liczby twarde we wszystkich tych systemach (liczba reguł i aksjomatów).

Problem z kodowaniem Kościoła polega na tym , że nie można uzyskać zasad indukcji dla swoich typów, co oznacza, że ​​są one prawie bezużyteczne, jeśli chodzi o udowodnienie oświadczeń na ich temat.

Jeśli chodzi o minimalność systemu, jedną ze ścieżek wspomnianych w komentarzach jest użycie kontenerów i typów (W / M), jednak są one raczej ekstensywne, więc nie jest to zbyt wygodne w pracy w systemach takich jak Coq lub Agda.

Bardziej praktycznym podejściem jest użycie wielomianowego funktora zdefiniowanego jako rozszerzenie opisu, a nie jako kontenera. Teorię gospodarza należy zamknąć tylko w stałych Π , Σ oraz μ i ν (i równości dla indeksowanych funktorów wielomianowych). Otrzymujesz taką samą moc ekspresji jak w przypadku typu (W / M) bez niedogodności: można faktycznie udowodnić zasadę indukcji bez potrzeby funkcjonalnej ekstensywności.$\Pi$$\Sigma$$\mu$$\nu$

$\mu$$\nu$