Dlaczego nie można zadeklarować zasady indukcji cyfr Kościoła

Wyobraźmy sobie, że zdefiniowaliśmy liczby naturalne w rachunku różniczkowym lambda w zależności od typu jako liczby kościelne. Można je zdefiniować w następujący sposób:

SimpleNat = (R : Set) → R → (R → R) → R

zero : SimpleNat
zero = λ R z _ → z

suc : SimpleNat → SimpleNat
suc sn = λ R z s → s (sn R z s)

SimpleNatRec : (R : Set) → R → (R → R) → SimpleNat → R
SimpleNatRec R z s sn = sn R z s

Wydaje się jednak, że nie możemy zdefiniować cyfr kościelnych za pomocą następującego rodzaju zasady indukcji:

NatInd : (C : Nat -> Set) -> (C zero) -> ((n : Nat) -> C n -> C (suc n)) -> (n : Nat) -> (C n)

Dlaczego tak jest Jak mogę to udowodnić? Wydaje się, że problem polega na zdefiniowaniu typu Nat, który staje się rekurencyjny. Czy można zmienić rachunek lambda, aby to umożliwić?

type-theory lambda-calculus dependent-type

— Konstantin Solomatov
źródło

Pytanie, które zadajesz, jest interesujące i znane. Używasz tak zwanego impredykatywnego kodowania liczb naturalnych. Pozwól, że wyjaśnię trochę tła.

Biorąc pod uwagę konstruktor typu , możemy być zainteresowani „minimalnym” typem spełniającym . Pod względem teorii kategorii jest funktorem, a jest początkową algebrą Na przykład, jeśli to odpowiada liczbom naturalnym. Jeśli $T : \mathsf{Type} \to \mathsf{Type}$ $A$ $A \cong T(A)$ $T$ $A$ $T$ $T(X) = 1 + X$ $A$ a następnie jest rodzajem skończonych drzew binarnych. $T(X) = 1 + X \times X$ $A$

Pomysł z długą historią jest to, że początkowy -algebra jest typu (Używasz notacji Agda dla produktów zależnych, ale używam bardziej tradycyjnej notacji matematycznej.) Dlaczego tak powinno być? Cóż, zasadniczo koduje zasadę rekurencji dla początkowej algebry: biorąc pod uwagę dowolną algebrę o morfizmie struktury $T$

ZA : = \prod_{X : T. y p mi} (T. (X) \to X) \to X .

$A \mathrel{{:}{=}} \prod_{X : \mathsf{Type}} (T(X) \to X) \to X.$

A

$A$

T

$T$

T

$T$

Y

$Y$

, otrzymujemy homomorfizm algebry

przez

f : T (Y) \to Y

$f : T(Y) \to Y$

ϕ : A \to Y

$\phi : A \to Y$

Widzimy więc, że

jestz pewnościąsłabopoczątkowe. Aby było to początkowe, musielibyśmy wiedzieć, że

jest również wyjątkowy. Nie jest to prawdą bez dalszych założeń, ale szczegóły są techniczne i nieprzyjemne i wymagają przeczytania jakiegoś materiału tła. Na przykład, jeśli potrafimy wykazać zadowalającetwierdzenie parametryczne, wówczas wygrywamy, ale są też inne metody (takie jak masowanie definicji

i zakładanie

maksiomu i ekstensywności funkcji).

ϕ (za) = za Y fa .

$\phi(a) = a \, Y \, f.$

A

$A$

ϕ

$\phi$

A

$A$

K

$K$

$T(X) = 1 + X$

N. za t = \prod_{X : T. y p mi} ((1 + X) \to X) \to X = \prod_{X : T. y p mi} (X \times (X \to X)) \to X = \prod_{X : T. y p mi} X \to (X \to X) \to X .

$\mathsf{Nat} = \prod_{X : \mathsf{Type}} ((1 + X) \to X) \to X = \prod_{X : \mathsf{Type}} (X \times (X \to X)) \to X = \prod_{X : \mathsf{Type}} X \to (X \to X) \to X.$

Techniczna odpowiedź na twoje pytanie brzmi: istnieją modele teorii typów, w których typ SimpleNatzawiera egzotyczne elementy, które nie odpowiadają cyfrom, a ponadto elementy te łamią zasadę indukcji. Typ SimpleNatw tych modelach jest zbyt duży i jest tylko słabą algebrą początkową.

— Andrej Bauer
źródło

Zgadzam się, że odpowiedź jest świetna, ale kilka odniesień może się tu przydać: praca Geuversa na temat niemożności uzyskania indukcji oraz praca Neela K i Dereka Dreyera na temat uzyskania (pewnej) indukcji z parametryczności . Nie znam jednak artykułu, który w pełni bada związek.

— cody

Nie jestem zbyt silny na referencje w tej dziedzinie, dzięki @cody!

— Andrej Bauer