Apa itu induksi-induksi?

Apa itu induksi-induksi ?

Sumber daya yang saya temukan adalah:

• buku HoTT , di akhir bab 5.7.
• Artikel nLab
• sebuah makalah yang disebut definisi induktif-induktif
• posting blog ini juga menyebutkan tipe induktif-induktif

Dua referensi pertama terlalu singkat untuk saya, dan dua yang terakhir terlalu teknis. Adakah yang bisa menjelaskannya dalam istilah awam? Akan lebih baik jika ada kode Agda.

Tambahan 2016-10-03: Saya mencampur induksi-induksi dan rekursi-induksi (bukan pertama kali saya melakukan itu!). Saya minta maaf atas kekacauan ini. Saya memperbarui jawaban untuk mencakup keduanya.

Saya menemukan penjelasan dalam makalah Forsberg & Setzer A axiomatisation terbatas definisi induktif-induktif menerangi.

Induksi-rekursi

Definisi induktif-rekursif adalah definisi di mana kami mendefinisikan tipe dan tipe keluarga secara bersamaan dengan cara khusus:$A$$B : A \to \mathsf{Type}$

1. $A$ didefinisikan sebagai tipe induktif.
2. $B$ didefinisikan oleh rekursi pada .$A$
3. Krusial, definisi dapat menggunakan .$A$$B$

Tanpa persyaratan ketiga, pertama kita bisa mendefinisikan dan kemudian secara terpisah .$A$$B$

Ini contoh bayi. Tentukan induktif untuk memiliki konstruktor berikut:$A$

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

Tipe keluarga didefinisikan oleh$B$

• $B(a) = \mathtt{bool}$
• $B(\ell(x, f)) = \mathtt{nat}$ .

Jadi, apa yang ada di ? Pertama-tama kita memiliki elemen Karena itu, ada tipe yang didefinisikan sebagai . Oleh karena itu, kita dapat membentuk dua elemen baru dan di . Sekarang kita memiliki , jadi kita juga dapat membentuk untuk setiap elemen dan Kita bisa terus seperti ini . Tahap selanjutnya adalah sejak itu $A$

$$a : A.$$ $B(a)$$\mathtt{bool}$ $$\ell(a, \mathtt{false})$$ $$\ell(a, \mathtt{true})$$ $A$$B(\ell(a, \mathtt{false})) = B(\ell(a, \mathtt{true})) = \mathtt{nat}$$n : \mathtt{nat}$ $$\ell(\ell(a, \mathtt{false}), n) : A$$ $$\ell(\ell(a, \mathtt{true}), n) : A$$ $$B(\ell(\ell(a, \mathtt{true}), n)) = \mathtt{nat}$$ ada untuk setiap elemen dan elemen Kita dapat terus berjalan. Sedikit pemikiran mengungkapkan bahwa kurang lebih adalah dua salinan daftar bilangan asli, berbagi daftar kosong yang sama. Saya akan meninggalkannya sebagai latihan untuk mencari tahu mengapa.$m : \mathtt{nat}$ $$\ell(\ell(\ell(a, \mathtt{true}), n), m) : A$$ $$\ell(\ell(\ell(a, \mathtt{false}), n), m) : A$$ $A$

Induksi-induksi

Definisi induktif-induktif juga mendefinisikan tipe dan secara bersamaan tipe keluarga :$A$$B : A \to \mathsf{Type}$

1. $A$ didefinisikan secara induktif
2. $B$ didefinisikan secara induktif, dan itu bisa merujuk ke$A$
3. Krusial, bisa merujuk ke .$A$$B$

Penting untuk memahami perbedaan antara induksi-rekursi dan induksi-induksi. Dalam induksi-rekursi kita mendefinisikan dengan menyediakan persamaan dari bentuk mana adalah konstruktor untuk . Dalam definisi induktif-induktif kita mendefinisikan dengan menyediakan konstruktor untuk membentuk unsur-unsur .$B$

$$B(\mathsf{c}(\ldots)) = \cdots$$ $\mathsf{c}(\ldots)$$A$$B$$B$

Mari kita merumuskan kembali contoh kita sebelumnya sebagai induksi-induksi. Pertama-tama kita mendapatkan tpye diberikan secara induktif :$A$

• $a : A$
• $\ell : \big(\sum_{x : A} B(x)\big) \to A$

Tipe keluarga didefinisikan oleh konstruktor berikut:$B$

• $\mathsf{Tru} : B(a)$
• $\mathsf{Fal} : B(a)$
• jika dan maka$x : A$$y : B(x)$$\mathsf{Zer} : B(\ell(x,y))$
• jika dan dan maka .$x : A$$y : B(x)$$z : B(\ell(x,y))$$\mathsf{Suc}(z) : B(\ell(x,y))$

Seperti yang Anda lihat, kami memberikan aturan untuk menghasilkan elemen yang sama dengan mengatakan bahwa adalah (isomoprhic) boolean, dan adalah (isomorfik ke) bilangan alami .$B$$B(a)$$B(\ell(x,y))$