Saya mulai membaca semakin banyak makalah penelitian bahasa. Saya merasa sangat menarik dan cara yang baik untuk mempelajari lebih lanjut tentang pemrograman secara umum. Namun, biasanya ada bagian di mana saya selalu berjuang dengan (ambil misalnya bagian ketiga dari ini ) karena saya tidak memiliki latar belakang teoritis dalam ilmu komputer: Ketik Aturan.
Apakah ada buku bagus atau sumber daya daring yang tersedia untuk memulai di area ini? Wikipedia sangat kabur dan tidak terlalu membantu pemula.
Jawaban:
Di sebagian besar sistem tipe, aturan tipe bekerja bersama untuk menentukan penilaian formulir:
Ini menyatakan bahwa dalam konteks ekspresi e memiliki tipe τ . Γ adalah pemetaan variabel bebas e ke tipenya.Γ e τ
Γ e
Suatu sistem tipe akan terdiri dari serangkaian aksioma dan aturan (sistem formal aturan inferensi , seperti yang ditunjukkan oleh Raphael).
Aksioma adalah bentuk
Ini menyatakan bahwa keputusan berlaku (selalu).Γ ⊢ e : τ
Contohnya adalah
yang menyatakan bahwa dengan asumsi bahwa tipe variabel adalah τ , maka ekspresi x memiliki tipe τ .x τ x τ
Aturan inferensi mengambil fakta yang telah ditentukan dan membangun fakta yang lebih besar darinya. Misalnya aturan inferensi
mengatakan bahwa jika saya memiliki turunan dari fakta dan derivasi dari fakta Γ ⊢ e 2 : τ , maka saya dapat memperoleh derivasi dari fakta Γ ⊢ e 1 e 2 : τ ′ . Dalam hal ini, ini adalah aturan untuk aplikasi fungsi mengetik.Γ ⊢ e1: τ→τ′ Γ ⊢ e2:τ Γ ⊢ e1 e2: τ′
Ada dua cara membaca aturan ini:
Beberapa aturan inferensi juga memanipulasi dengan menambahkan bahan baru ke dalamnya (lihat-bawah ke atas). Berikut adalah aturan untuk λ -straksi:Γ λ
Aturan inferensi diterapkan secara induktif berdasarkan sintaks ekspresi yang dianggap membentuk pohon derivasi. Di daun pohon (di atas) akan ada aksioma, dan cabang akan dibentuk dengan menerapkan aturan inferensi. Di bagian paling bawah pohon adalah ekspresi yang Anda tertarik mengetik.
Misalnya, derivasi dari pengetikan ekspresi adalahλ f. λ x . f x
Dua buku yang sangat bagus untuk belajar tentang sistem tipe adalah:
Kedua buku ini sangat komprehensif, namun mulai perlahan, membangun fondasi yang kuat.
sumber
Ada tutorial online interaktif lucu tentang kalkulus sekuens, yang dapat membantu membangun beberapa intuisi dan merasakan bagaimana inferensi bekerja: Tutorial Interaktif Kalkulus Sequent
sumber
Di halaman Wikipedia itu direkomendasikan " Ketik Sistem, Luca Cardelli, Survei Komputasi ACM ", yang merupakan survei 2 halaman yang dapat membantu Anda memahami cara membaca aturan. Bagaimanapun, cara membaca aturan dijelaskan dengan sempurna di halaman Wikipedia (atau bahkan lebih baik dalam survei 2 halaman). Namun untuk memahami semuanya, Anda perlu memahami apa itu sistem pengetikan (disusun oleh beberapa aturan), di mana artikel Wikipedia " Type system " adalah awal yang baik (dan Anda memiliki beberapa buku di bagian " Referensi " itu. halaman jika Anda ingin melangkah lebih jauh).
sumber