Klasifikasi Kalkulator Lambda Diketik / Tidak Diketik

Adakah yang bisa menjelaskan secara singkat (jika mungkin!) Atau merujuk saya ke referensi, meringkas perbedaan antara kalkulus lambda yang tidak diketik dan kalkulus lambda yang diketik lebih umum?

Saya terutama mencari pernyataan dari kekuatan ekspresif mereka, ekivalen dengan sistem logika / aritmatika atau metode perhitungan, dan analogi dengan bahasa pemrograman jika berlaku.

Walaupun saya tentu ingin membaca, sesuatu seperti tabel referensi yang menguraikan kalkulus dan persamaan / perbedaan / tempat dalam hierarki akan menjadi referensi BESAR untuk membantu saya memilahnya.

Tidak mengatakan di bawah ini benar, hanya mencoba membuat sketsa bersama beberapa tayangan yang saya harus melihat apakah mereka setidaknya berfungsi sebagai titik awal (atau sesuatu untuk diperbaiki!)

Kalkulus lambda yang tidak diketik - mis. untuk logika urutan pertama - tidak dapat melakukan X

Cukup ketik lambda calculus - eq to ... logic, terkait dengan Lisp?

Lambda 'Polimorfik' - dll.

Kalkulus Konstruksi - logika intusionis?

Combinatory Logic - sebanding dengan ??? mengetik kalkulus lambda, terkait dengan jenis bahasa APL / J

Jika ini mengikat ke kubus lambda dan tiga kapaknya semua lebih baik.

Sementara saya akrab dengan dasar-dasar kalkulus lambda dan pemrograman dengan bahasa fungsional, saya belum pernah membungkukkan kepala, atau membuat koneksi signifikan ke, sistem jenis yang terlibat dan rasa yang berbeda dari kalkulus lambda (dan mungkin pi?).

Ketika saya mencoba untuk meneliti ini saya tidak bisa membantu tetapi menemukan diri saya teralihkan, membuka banyak tab browser dan bercabang ke banyak arah saya tidak pernah masuk ke salah satu dari mereka dengan kedalaman!

Saya tidak yakin apakah yang saya minta itu masuk akal, tapi mudah-mudahan setidaknya saya sudah cukup melukis gambar untuk menyarankan beberapa bacaan yang dapat menjelaskan apa yang saya cari?

Meja Anda agak bingung; ini yang lebih baik.

• Kalkulus lambda yang tidak diketik - tidak ada interpretasi logis, seperti yang dicatat Andrej
• Cukup ketik lambda calculus - logika proposisional intuitionistic
• Kalkulus lambda polimorfik - logika orde dua murni (yaitu, tanpa penjumlah urutan pertama)
• Jenis dependen - generalisasi logika tingkat pertama
• Kalkulus konstruksi - generalisasi logika tingkat tinggi

Ketergantungan tipe lebih umum daripada kuantifikasi tingkat pertama, karena mengubah bukti menjadi objek yang dapat Anda kuantifikasi. Kalkulator Lambda yang sesuai dengan FOL intuitionistic biasa ada, tetapi tidak cukup banyak digunakan untuk memiliki nama khusus - orang cenderung langsung ke tipe dependen.

Anda juga dapat menghubungkan bentuk sintaksis kalkulus dengan sistem logis.

• Kalkulus Combinator (mis., Combinator SKI) - Sistem gaya Hilbert
• Bentuk A-normal - kalkulus berurutan
• Kalkulus lambda yang diketik biasa - deduksi alami

$\lambda$$\lambda$$\lambda$nat$\lambda$$0$$T$

$\lambda$$\lambda$

$\lambda$$\lambda$

$\lambda$$\lambda$$\lambda$Ulambda : U -> (U -> U)gamma : (U -> U) -> U$\lambda$$\mathbb{U}$$\lambda$$\mathcal{C}$$\mathbb{U}$$\mathbb{U}$$[\mathcal{C}^{\mathrm{op}}, \mathsf{Set}]$$\mathbb{U} \cong \mathbb{U}^{\mathbb{U}}$

Referensi:

• Dana S. Scott: " Lambda Calculus: Some Models, Some Philosophy ", Studi Logika dan Fondasi Matematika, Volume 101, 1980, Halaman 223-265, Simposium Kleene

• Hendrik Pieter Barendregt: " Kalkulus lambda: sintaks dan semantiknya ", Elsevier, 1984.

Diskusi yang cukup komprehensif tentang hal ini dapat ditemukan dalam buku ini: Lectures on the Curry-Howard Isomorphism . Ini didasarkan pada versi lama yang tersedia secara bebas: Ceramah tentang Curry-Howard Isomorphism .