Mengapa tidak mungkin untuk menyatakan prinsip induksi untuk angka Gereja

17

Bayangkan, kita mendefinisikan bilangan alami dalam kalkulus lambda yang diketik secara dependen sebagai angka Gereja. Mereka mungkin didefinisikan dengan cara berikut:

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

Namun, tampaknya kita tidak dapat mendefinisikan angka Gereja dengan jenis prinsip Induksi berikut:

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

Kenapa gitu? Bagaimana saya bisa membuktikan ini? Tampaknya masalahnya adalah dengan menentukan tipe untuk Nat yang menjadi rekursif. Apakah mungkin untuk mengubah lambda calculus untuk mengizinkan ini?

Konstantin Solomatov
sumber

Jawaban:

20

Pertanyaan yang Anda ajukan menarik dan diketahui. Anda menggunakan penyandian impredikatif dari bilangan asli. Biarkan saya jelaskan sedikit latar belakangnya.

T:TypeTypeAAT(A)TATT(X)=1+XAT(X)=1+X×XA

T

A:=X:Type(T(X)X)X.
ATTYf:T(Y)Yϕ:AY
ϕ(a)=aYf.
AϕAK

T(X)=1+X

NSebuaht=X:Tyhale((1+X)X)X=X:Tyhale(X×(XX))X=X:TyhaleX(XX)X.

Jawaban teknis untuk pertanyaan Anda adalah ini: ada model teori tipe di mana tipe SimpleNatmengandung elemen eksotis yang tidak sesuai dengan angka, dan terlebih lagi, elemen ini melanggar prinsip induksi. Jenis SimpleNatdalam model ini terlalu besar dan hanya aljabar awal yang lemah .

Andrej Bauer
sumber
8
Saya setuju bahwa jawabannya bagus, tetapi beberapa referensi mungkin berguna di sini: makalah Geuvers tentang non-derivasi induksi dan makalah Neel K dan Derek Dreyer tentang mendapatkan (beberapa) induksi dari parametrik . Saya tidak menyadari makalah yang sepenuhnya mengeksplorasi hubungan itu.
cody
Saya tidak terlalu kuat pada referensi di area ini, terima kasih @cody!
Andrej Bauer