Tipe-W vs tipe Induktif

Teori tipe Martin-Löf menggunakan tipe-W untuk mendefinisikan struktur induktif seperti bilangan bulat, daftar, dll. Namun, kalkulus konstruksi induktif tidak menggunakannya dengan cara yang sama, tipe induktif tampaknya lebih mirip skema aksioma.

Apakah kedua pendekatan ini setara (tampaknya)? Adakah alasan filosofis mengapa yang satu lebih baik daripada yang lain (bagi saya, tipe-W terasa lebih intuitif, karena hanya pohon struktur khusus)? Yang lebih mudah dari sudut pandang implementasi (tipe induktif tampaknya lebih baik bagi saya, karena untuk tipe-W menjadi berguna, kita memerlukan setidaknya tipe dan produk yang terbatas untuk tersedia dalam inti sistem)

(Saya berasumsi bahwa dengan 'skema aksioma', Anda memikirkan pekerjaan Gimenez )

Secara ekstensi, skema aksioma tipe-G dan aksioma Gimenez setara.

Namun, dalam pengaturan yang intens, Anda tidak akan terlalu jauh dengan tipe-W: mereka terlalu ekstensional (dengan definisi pengkodean) yang cocok untuk pemrograman. Ini telah dibahas oleh beberapa penulis, terutama:

• Conor McBride: http://mazzo.li/epilogue/index.html%3Fp=324.html
• Peter Dybjer, "Mewakili set yang didefinisikan secara induktif oleh wellorderings dalam teori tipe Martin-Löf"
• Guogen & Luo, "Tipe data induktif: jenis pemesanan yang baik ditinjau kembali"