Mengetik dalam kalkulus kertas konstruksi?

10

Dalam karya klasik kalkulus konstruksi ada aturan yang menyatakan

masukkan deskripsi gambar di sini (halaman 7 dari pdf, halaman 101 dari dokumen asli)

Aturan ini berarti bahwa konteks apa pun dapat direduksi menjadi anggota konteks itu. Sepertinya ini seharusnya tidak benar, karena akan memerlukan

1 ≅ Nat
3 ≅ Nat
1 ≅ 3

jika Nat adalah sebuah konteks.

Saya pikir interpretasi terbaik adalah bahwa delta yang lebih rendah dimaksudkan untuk menjadi M. Terutama mengingat aturan yang diberikan pada halaman berikutnya.

Jadi apakah ini hanya kesalahan ketik, atau aturan logis yang tidak saya mengerti?

lo.logic calculus-of-constructions sequent-calculus pengguna833970
sumber

Jawaban:

11

Γ⊢M:ΔΓ⊢M≅M

Γ⊢N≅M

Agak kontra-intuitif, membuktikan bahwa sistem dengan konversi mengetik sama dengan yang tanpa jenis sangat sulit, dan diselesaikan pada 2010 oleh Siles dan Herbelin .

cody
sumber
"Perawatan modern" di sini berarti "perawatan komputer yang sebagian besar tertarik pada perhitungan".
Andrej Bauer
Cukup adil. Saya hampir mengemukakan teori tipe "Swedia" vs "Prancis", tetapi saya tidak yakin perbedaan itu benar-benar ada.
cody
Tidak ada perbedaan seperti itu, sebagaimana disaksikan oleh fakta bahwa Thierry Coquand tinggal di Swedia. Mereka semua komputasi.
Andrej Bauer
@cody: Saya pikir hampir semua modern, perawatan komputer-kecakapan menggunakan penilaian yang diketik, karena ini adalah cara yang paling nyaman untuk mendapatkan eta untuk pi / sigma. (Tentu saja Coq dan Agda mendukung hal itu.)
Neel Krishnaswami
@NeelKrishnaswami Konversi diketik diperlukan untuk eta masuk akal dalam kebanyakan situasi, tapi saya mendapat kesan bahwa itu bisa membuat meta-teori jauh lebih rumit. Mungkin saya sepenuhnya salah dan itu sebenarnya membuat semuanya sederhana. Ada juga pertanyaan untuk mengoptimalkan pemeriksaan konversi untuk melakukan pekerjaan paling sedikit, termasuk kewajiban pemeriksaan jenis tambahan. Tentunya ini akan menjadi pertanyaan lanjutan yang bagus.
cody