Kerangka kerja logis vs teori tipe

Ringkasan. Kerangka kerja logis adalah bahasa meta untuk formalisasi sistem deduktif, di mana deduksi menjadi objek sintaksis.

Tentu saja apa yang dianggap sebagai bahasa meta cukup kabur, dan akan sangat membantu untuk memahami perkembangan historis kerangka kerja logis. Kerangka logis pertama adalah Automath de Bruijn (1), yang didasarkan pada -calculus. Banyak gagasan dari keluarga bahasa Automath telah menemukan jalan mereka ke kerangka logis modern. Karya Martin-Löf tentang teori tipe-konstruktif, juga didasarkan pada -calculi, juga berpengaruh. $\lambda$ $\lambda$

$\lambda$ $A \rightarrow B$ $\Pi x^A. B$ $A \rightarrow B$ $\Pi x^A. B$

\frac{Γ ⊢ M : A \to B Γ ⊢ N : A}{Γ ⊢ M N : B} \frac{Γ ⊢ M : Π x^{A} . B Γ ⊢ N : A}{Γ ⊢ M N : B {N / x}}

$\newcommand{\TYPES}[3]{#1 \vdash #2 : #3} \newcommand{\SUBST}[2]{\{#1/#2\}} \frac{ \TYPES{\Gamma}{\color{red}{M}}{A \rightarrow B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{\color{red}{MN}}{B} } \qquad \frac{ \TYPES{\Gamma}{{\color{red}M}}{\Pi x^A. B} \qquad \TYPES{\Gamma}{\color{red}{N}}{A} }{ \TYPES{\Gamma}{{\color{red}{MN}}}{B\SUBST{{\color{red}N}}{x}} }$

Di sebelah kiri kita memiliki aturan untuk -calculus yang diketik sederhana , di sebelah kanan aturan yang menggeneralisasi kiri dengan tipe dependensi. Kita melihat bahwa suatu nilai 'mengalir' ke dalam tipe pada kesimpulan di sebelah kanan. $\lambda$

Saya pikir asisten bukti interaktif Isabelle menggunakan logika urutan kedua intuitionistic berdasarkan -calculus, tanpa angka atau tipe data rekursif sebagai kerangka kerja logis. Berbagai lainnya telah diusulkan. $\lambda$

Salah satu keuntungan menggunakan -calculi sebagai kerangka kerja logis adalah bahwa konstruksi yang mengikat seperti universal quantifiers dapat diimplementasikan menggunakan kerangka -binder. Perhatikan bahwa sebagian besar kerangka kerja logis lemah secara eksplisit: kerangka kerja mendukung penalaran tingkat objek, tetapi tidak cukup untuk melakukan banyak penalaran meta-teoretis di luar fakta bahwa pernyataan tingkat objek tertentu adalah teorema. Bahkan logika-logam biasanya sangat lemah sehingga membuktikan teorema deduksi untuk logika objek gaya Hilbert adalah mustahil. Tentu saja tidak ada yang mencegah Anda menggunakan teori tipe yang lebih kuat sebagai kerangka kerja logis. $\lambda$ $\lambda$

Untuk alasan praktis dan historis ini, sebagian besar kerangka kerja logis yang digunakan saat ini diketikkan -calculi, yaitu teori-jenis. Lihat (3, 4) untuk diskusi lebih mendalam tentang kerangka kerja logis. $\lambda$

N. de Bruijn: Bahasa Matematika OTOMATIS, Penggunaannya, dan Beberapa Perluasannya.
RF Harper, F. Honsell, G. Plotkin: Kerangka untuk Mendefinisikan Logika .
F. Pfenning: Kerangka kerja logis.
F. Pfenning: Kerangka kerja logis - Pengantar Singkat .

Martin Berger
sumber

Apakah Anda tahu tentang buku pengantar tentang asisten bukti (kerangka logis) yang cocok untuk seseorang yang sudah tahu dasar-dasar kalkulus lambda yang diketik sederhana dan logika urutan pertama?

Trismegistos

@ Trismegistos aku takut tidak. Saya sarankan untuk belajar asisten tertentu. Agda adalah yang termudah untuk masuk karena pada dasarnya Haskell, tetapi dengan tipe dependen. Dalam pengalaman saya, kerangka kerja logis tidak sepenting dimensi asisten pembuktian lainnya. Misalnya Isabelle adalah prover generik yang dapat Anda instantiate dengan logika yang berbeda, jadi sangat memaparkan kerangka logis. Tetapi Isabelle / HOL adalah satu-satunya lembaga yang digunakan dalam praktek. Ini karena semua taktik pembuktian, semua dukungan yang tepat telah ditulis untuk logika objek HOL. Dan kegunaan pepatah tergantung pada mereka.

Martin Berger

Kerangka kerja logis vs teori tipe

Jawaban: