Properti Church-Rosser untuk kalkulus lambda yang diketik secara dependen?

Sudah diketahui secara umum bahwa properti Church-Rosser berlaku untuk reduksi dalam kalkulus lambda yang diketik sederhana. Ini menyiratkan bahwa kalkulus konsisten, dalam arti bahwa tidak semua persamaan yang melibatkan -terms dapat diturunkan: misalnya, K I , karena mereka tidak memiliki bentuk normal yang sama.$\beta \eta$$\lambda$$\neq$

Diketahui juga bahwa seseorang dapat memperluas hasil ke pasangan yang sesuai dengan jenis produk.

Tapi saya ingin tahu apakah seseorang dapat memperluas hasil untuk kalkulus lambda yang diketik secara dependen (mungkin) dengan tipe polimorfik, misalnya Kalkulus Konstruksi?

Referensi apa pun juga akan sangat bagus!

Terima kasih

Mungkin bermanfaat untuk dengan cepat memberikan contoh-counter untuk CR dalam kalkulus yang diketik dengan dan :$\beta$$\eta$

$$t=\lambda x:A.(\lambda y:B.\ y)\ x$$

Dan kami memiliki dan t → n λ y : B .

$$t\rightarrow_\beta \lambda x: A.x$$ $$t\rightarrow_\eta \lambda y:B.y$$

Langsung bahwa jika , maka dua istilah yang dihasilkan, pada kenyataannya, setara , tetapi tidak ada alasan untuk ini menjadi kasus, pada istilah yang tidak diketik .$A\equiv B$$\alpha$

Pada istilah yang diketik , cukup jelas bahwa harus sama dengan untuk istilah yang dihasilkan diketik dengan baik. Kesulitan besar yang terjadi adalah ini:B $A$$B$$t$

Untuk sistem yang diketik secara dependen, pertemuan perlu dibuktikan sebelum pengawetan tipe!

Ini karena Anda memerlukan properti -injectivity untuk membuktikan inversi, yang diperlukan untuk membuktikan pelestarian / pengurangan subjek.$\Pi$

$$\Pi x:A.B=_{\beta\eta}\Pi x:A'.B'\ \Leftrightarrow\ A=_{\beta\eta}A'\wedge B=_{\beta\eta} B'$$

Jadi Anda bahkan tidak dapat membuktikan bahwa -pengurangan mempertahankan tipe tanpa pertemuan, tetapi pertemuan bahkan tidak berpegang pada istilah yang tidak diketik / diketik dengan buruk!$\beta\eta$

Keluar dari lingkaran setan ini memerlukan beberapa trik teknis, yang sulit untuk diringkas di sini, tetapi bisa dibilang yang paling sederhana untuk dipahami adalah dengan hanya berhenti tertarik pada -pengurangan, tetapi sebaliknya berkonsentrasi pada -perbaikan :$\eta$$\eta$$t\rightarrow_{\eta*}\lambda x:A.t\ x$

Tentu saja, Anda perlu membatasi aturan ini hanya untuk ketentuan non- dan non-diterapkan bahkan berharap untuk mendapatkan pemutusan hubungan kerja, tetapi dengan pembatasan ini tampaknya perilaku pengurangan jauh lebih baik berperilaku, dan meta-teori berhasil tanpa terlalu banyak masalah. Referensi yang bagus tampaknya adalah Neil Ghani, Eta-Ekspansi dalam Teori Ketergantungan Type .$\lambda$

Sebuah pendekatan yang berbeda, dan baru-baru ini cukup populer, dijelaskan oleh Abel, Untyped Algorithmic Equality for Martin-Löf's Framework Kerangka Kerja dengan Surjective Pairs .

Cukup banyak yang tahu tentang ini. Konsep Pure Type Systems (PTS) berguna untuk menunjukkan Church-Rosser (CR) untuk kelas besar dari mengetik -calculi. Parafrase (1):$\lambda$

• PTS dengan pengurangan β hanya memenuhi CR pada istilah yang diketik. Ini mengikuti langsung dari CR pada 'pseudoterms', bersama dengan pengurangan subjek.

• Untuk PTS dengan reduksi βη, CR pada himpunan pseudotermata salah. Lihat (2).

• Di PTS dengan reduksi βη CR berlaku untuk istilah yang diketik dengan baik dari tipe tetap . Lihat (1).

PTS adalah formalisme yang sangat umum dan mencakup Sistem F, Fω, LF serta kalkulus konstruksi. Dua yang terakhir diketik secara dependen. Keduanya (1, 2) adalah makalah yang cukup lama, dan saya membayangkan bahwa lebih banyak yang diketahui pada tahun 2015.

---

^{1. H. Geuvers, properti Church-Rosser untuk pengurangan βη dalam mengetik -calculi$\lambda$ .}

^{2. RP Nederpelt, Normalisasi yang kuat pada kalkulus lambda yang diketik dengan tipe terstruktur lambda .}