Kalkulus Lambda adalah sistem formal dalam logika matematika untuk mengekspresikan perhitungan berbasis abstraksi dan menerapkan fungsi menggunakan pengikatan dan substitusi variabel. Ini adalah model universal yang dapat diterapkan pada desain mesin Turing apa pun. Kalkulus lambda pertama kali diperkenalkan oleh Church, seorang ahli matematika terkenal, pada tahun 1930-an.
Sistem terdiri dari membangun anggota lambda dan melakukan operasi pengurangan pada mereka.
Penjelasan dan Aplikasi
Huruf Yunani lambda (λ) digunakan dalam ekspresi lambda dan istilah lambda untuk menunjukkan pengikatan variabel dalam suatu fungsi.
Kalkulus Lambda dapat tidak diketik atau diketik. Pada varian pertama, fungsi hanya dapat digunakan jika mampu menerima data jenis ini. Kalkuli lambda yang diketik lebih lemah, dapat mengekspresikan nilai yang lebih kecil. Tapi, di sisi lain, mereka memungkinkan Anda untuk membuktikan lebih banyak hal.
Salah satu alasan ada begitu banyak jenis yang berbeda adalah keinginan para ilmuwan untuk berbuat lebih banyak tanpa melepaskan kesempatan untuk membuktikan teorema kalkulus lambda yang kuat.
Sistem ini memiliki aplikasi di berbagai bidang matematika, filsafat, linguistik, dan ilmu komputer. Pertama-tama, kalkulus lambda adalah kalkulus yang telah memainkan peran penting dalam perkembangan teori bahasa pemrograman. Ini adalah gaya kreasi fungsional yang diterapkan sistem. Mereka juga merupakan topik hangat penelitian dalam teori kategori ini.
Untuk boneka
Kalkulus lambda diperkenalkan oleh ahli matematika Gereja Alonzo pada tahun 1930-an sebagai bagian dari penelitiannya tentang dasar-dasar sains. Sistem asli terbukti tidak konsisten secara logika pada tahun 1935 ketika Stephen Kleen dan J. B. Rosser mengembangkan paradoks Kleene-Rosser.
Kemudian, pada tahun 1936, Church memilih dan menerbitkan hanya bagian yang relevan dengan perhitungan, yang sekarang disebut kalkulus lambda yang tidak diketik. Pada tahun 1940 ia juga memperkenalkan teori yang lebih lemah tetapi konsisten secara logis yang dikenal sebagai sistem tipe prima. Dalam karyanya, ia menjelaskan seluruh teori secara sederhana, sehingga dapat dikatakan bahwa Gereja menerbitkan kalkulus lambda untuk boneka.
Sampai tahun 1960-an, ketika hubungannya dengan bahasa pemrograman menjadi jelas, hanyalah formalisme. Berkat aplikasi Richard Montagu dan ahli bahasa lainnya dalam semantik bahasa alami, kalkulus telah mendapat tempat baik dalam linguistik dan ilmu komputer.
Asal usul simbol
Lambda tidak berarti kata atau akronim, itu berasal dari referensi dalam Matematika Utama Russell diikuti oleh dua perubahan tipografi. Contoh notasi: untuk fungsi f dengan f (y)=2y + 1 adalah 2ŷ + 1. Dan di sini kita menggunakan tanda sisipan (“topi”) di atas y untuk memberi label pada variabel input.
Gereja pada awalnya bermaksud menggunakan simbol yang serupa, tetapi pembuat huruf tidak dapat menempatkan simbol "topi" di atas huruf. Jadi, mereka malah mencetaknya sebagai "/\y.2y+1". Pada episode penyuntingan berikutnya, juru ketik mengganti "/ \" dengan karakter yang mirip secara visual.
Pengantar kalkulus lambda
Sistem terdiri dari bahasa istilah, yang dipilih oleh sintaks formal tertentu, dan seperangkat aturan transformasi yang memungkinkan mereka untuk dimanipulasi. Poin terakhir dapat dianggap sebagai teori persamaan atau sebagai definisi operasional.
Semua fungsi dalam kalkulus lambda bersifat anonim, artinya tidak memiliki nama. Mereka hanya mengambil satu variabel input, dan currying digunakan untuk mengimplementasikan plot dengan banyak variabel.
istilah Lambda
Sintaks kalkulus mendefinisikan beberapa ekspresi sebagai valid dan yang lainnya tidak valid. Sama seperti string karakter yang berbeda adalah program C yang valid dan ada juga yang tidak. Ekspresi sebenarnya dari kalkulus lambda disebut "istilah lambda".
Tiga aturan berikut memberikan definisi induktif yang dapatberlaku untuk konstruksi semua konsep yang valid secara sintaksis:
Variabel x itu sendiri adalah istilah lambda yang valid:
- jika T adalah LT dan x tidak konstan, maka (lambda xt) disebut abstraksi.
- jika T dan s adalah konsep, maka (TS) disebut aplikasi.
Tidak ada lagi istilah lambda. Dengan demikian, suatu konsep valid jika dan hanya jika dapat diperoleh dengan penerapan berulang dari ketiga aturan ini. Namun, beberapa tanda kurung dapat dihilangkan sesuai dengan kriteria lain.
Definisi
Ekspresi Lambda terdiri dari:
- variabel v 1, v 2, …, v n, …
- simbol abstraksi 'λ' dan titik '.'
- tanda kurung ().
Set dapat didefinisikan secara induktif:
- Jika x adalah variabel, maka x;
- x tidak konstan dan M, maka (λx. M) Λ;
- M, N, lalu (MN).
Penunjukan
Untuk menjaga notasi ekspresi lambda tetap rapi, konvensi berikut biasanya digunakan:
- Kurung luar dihilangkan: MN bukan (MN).
- Aplikasi diasumsikan tetap asosiatif: seseorang dapat menulis MNP alih-alih ((MN) P).
- Badan abstraksi memanjang lebih jauh ke kanan: x. MN berarti x. (MN), bukan (λx. M) N.
- Urutan abstraksi dikurangi: x.λy.λz. N dapat menjadi xyz. N.
Variabel bebas dan terikat
Operator menghubungkan non-konstantanya di mana pun ia berada di badan abstraksi. Variabel yang termasuk dalam ruang lingkup disebut terikat. Dalam ekspresi x. M, bagian x sering disebut sebagai pengikat. Seolah mengisyaratkan bahwa variabel menjadi grup dengan penambahan X x ke M. Semua variabel tidak stabil lainnya disebut bebas.
Misalnya, dalam ekspresi y. x x y, y - terikat tidak permanen, dan x - bebas. Dan perlu juga dicatat bahwa variabel dikelompokkan berdasarkan abstraksi "terdekat". Dalam contoh berikut, solusi kalkulus lambda diwakili oleh kemunculan tunggal x, yang terkait dengan suku kedua:
λ x. y (λ x. z x)
Himpunan variabel bebas M dinotasikan sebagai FV (M) dan didefinisikan oleh rekursi pada struktur suku sebagai berikut:
- FV (x)={x}, di mana x adalah variabel.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) FV (N).
Sebuah rumus yang tidak mengandung variabel bebas disebut tertutup. Ekspresi lambda tertutup juga dikenal sebagai kombinator dan setara dengan istilah dalam logika kombinatorial.
Singkatan
Arti ekspresi lambda ditentukan oleh bagaimana mereka dapat dipersingkat.
Ada tiga jenis pemotongan:
- α-transform: mengubah variabel terikat (alfa).
- β-reduction: menerapkan fungsi ke argumennya (beta).
- η-transform: mencakup pengertian ekstensionalitas.
Ini jugakita berbicara tentang kesetaraan yang dihasilkan: dua ekspresi adalah -ekuivalen jika mereka dapat -ditransformasikan menjadi komponen yang sama, dan / -ekivalen didefinisikan dengan cara yang sama.
Istilah redex, kependekan dari reducible turnover, mengacu pada subtopik yang dapat dikurangi dengan salah satu aturan. Kalkulus lambda untuk boneka, contoh:
(λ x. M) N adalah redeks beta dalam ekspresi untuk menggantikan N dengan x dalam M. Komponen yang direduksi redeks disebut pereduksi. Reduksi (λ x. M) N adalah M [x:=N].
Jika x tidak bebas dalam M, x. M x juga em-REDEX dengan regulator M.
α-transformasi
Alpha rename memungkinkan Anda mengubah nama variabel terikat. Misalnya, x. x dapat memberikan y. y. Suku-suku yang hanya berbeda dalam transformasi alfa dikatakan ekuivalen. Seringkali, saat menggunakan kalkulus lambda, -ekuivalen dianggap timbal balik.
Aturan yang tepat untuk konversi alfa tidak sepenuhnya sepele. Pertama, dengan abstraksi ini, hanya variabel-variabel yang terkait dengan sistem yang sama yang diganti namanya. Misalnya, transformasi alfa x.λ x. x dapat menyebabkan y.λ x. x, tetapi ini mungkin tidak mengarah ke y.λx.y Yang terakhir memiliki arti yang berbeda dari aslinya. Ini analog dengan konsep pemrograman bayangan variabel.
Kedua, transformasi alfa tidak mungkin dilakukan jika akan mengakibatkan ditangkapnya abstraksi lain yang tidak permanen. Misalnya, jika Anda mengganti x dengan y dalam x.λ y. x, maka Anda bisa mendapatkany.λy. u, yang tidak sama sama sekali.
Dalam bahasa pemrograman dengan cakupan statis, konversi alfa dapat digunakan untuk menyederhanakan resolusi nama. Pada saat yang sama, berhati-hatilah agar konsep variabel tidak menutupi penunjukan di area yang berisi.
Dalam notasi indeks De Bruyne, dua suku ekuivalen alfa mana pun secara sintaksis identik.
Penggantian
Perubahan yang ditulis oleh E [V:=R] adalah proses mensubstitusi semua kemunculan bebas dari variabel V dalam ekspresi E dengan pergantian R. Substitusi dalam bentuk didefinisikan oleh lambda rekursi kalkulus pada struktur konsep sebagai berikut (catatan: x dan y - variabel saja, dan M dan N - ekspresi apa pun).
x [x:=N] N
y [x:=N] y jika x y
(M 1 M 2) [x:=N] (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] x. M
(λ y. M) [x:=N] y y. (M [x:=N]) jika x y, asalkan y FV (N).
Untuk substitusi ke dalam abstraksi lambda, terkadang diperlukan -transform sebuah ekspresi. Misalnya, tidak benar bahwa (λ x. Y) [y:=x] menghasilkan (λ x. X) karena x yang disubstitusi seharusnya bebas, tetapi akhirnya terikat. Penggantian yang benar dalam kasus ini adalah (λ z. X) sampai dengan -ekuivalensi. Perhatikan bahwa substitusi didefinisikan secara unik hingga lambda.
β-pengurangan
Pengurangan beta mencerminkan gagasan penerapan suatu fungsi. Beta-reduktif didefinisikan dalam istilahsubstitusi: ((X V. E) E ') adalah E [V:=E'].
Misalnya, dengan asumsi beberapa pengkodean 2, 7, ×, ada -reduksi berikut: ((λ n. N × 2) 7) → 7 × 2.
Reduksi beta dapat dilihat sama dengan konsep reduksibilitas lokal di bawah deduksi alami melalui isomorfisme Curry-Howard.
η-transform
Konversi ini mengungkapkan gagasan ekstensionalitas, yang dalam konteks ini adalah bahwa dua fungsi adalah sama ketika memberikan hasil yang sama untuk semua argumen. Konversi ini menukar antara x. (F x) dan f setiap kali x tampaknya tidak bebas di f.
Tindakan ini dapat dianggap sama dengan konsep kelengkapan lokal dalam deduksi alami melalui isomorfisme Curry-Howard.
Bentuk dan perpaduan normal
Untuk kalkulus lambda yang tidak bertipe, aturan reduksi umumnya bukan normalisasi kuat atau lemah.
Namun demikian, dapat ditunjukkan bahwa reduksi bergabung ketika dijalankan sebelum transformasi (yaitu, dua bentuk normal dapat dianggap sama jika transformasi dari satu ke bentuk lainnya dimungkinkan).
Oleh karena itu, baik suku-suku normalisasi kuat maupun suku-suku penyesuaian lemah memiliki bentuk normal tunggal. Untuk istilah pertama, setiap strategi pengurangan dijamin menghasilkan konfigurasi yang khas. Sedangkan untuk kondisi normalisasi lemah, beberapa strategi reduksi mungkin tidak menemukannya.
Metode pemrograman tambahan
Ada banyak idiom pembuatan untuk kalkulus lambda. Banyak dari mereka awalnya dikembangkan dalam konteks menggunakan sistem sebagai dasar semantik bahasa pemrograman, secara efektif menerapkannya sebagai konstruksi tingkat rendah. Karena beberapa gaya menyertakan kalkulus lambda (atau sesuatu yang sangat mirip) sebagai cuplikan, teknik ini juga digunakan dalam pembuatan praktis, tetapi kemudian dapat dianggap tidak jelas atau asing.
Konstanta bernama
Dalam kalkulus lambda, pustaka berbentuk kumpulan fungsi yang telah ditentukan sebelumnya, di mana suku-sukunya hanyalah konstanta konkret. Kalkulus murni tidak memiliki konsep kekekalan bernama karena semua istilah lambda atom adalah variabel. Tetapi mereka juga dapat ditiru dengan mengambil yang bisa berubah sebagai nama konstanta, menggunakan abstraksi lambda untuk mengikat volatil itu di dalam tubuh, dan menerapkan abstraksi itu ke definisi yang dimaksud. Jadi jika Anda menggunakan f untuk mewakili M di N, Anda bisa mengatakan
(λ f. N) M.
Pengarang sering memperkenalkan konsep sintaksis seperti let untuk memungkinkan sesuatu ditulis dengan cara yang lebih intuitif.
f=M ke N
Dengan merangkai definisi seperti itu, seseorang dapat menulis "program" kalkulus lambda sebagai nol atau lebih definisi fungsi diikuti oleh satu anggota lambda, menggunakan definisi yang membentuk sebagian besar program.
Keterbatasan penting dari let ini adalah bahwa nama f tidak didefinisikan dalam M,karena M berada di luar lingkup pengikatan abstraksi lambda f. Ini berarti bahwa atribut fungsi rekursif tidak dapat digunakan sebagai M dengan let. Sintaks letrec yang lebih maju, yang memungkinkan Anda untuk menulis definisi fungsi rekursif dalam gaya ini, sebagai gantinya menggunakan kombinator titik tetap.
Analog tercetak
Tipe ini adalah formalisme yang diketik yang menggunakan simbol untuk mewakili abstraksi fungsi anonim. Dalam konteks ini, tipe biasanya objek yang bersifat sintaksis yang ditetapkan ke istilah lambda. Sifat yang tepat tergantung pada kalkulus yang bersangkutan. Dari sudut pandang tertentu, LI yang diketik dapat dianggap sebagai penyempurnaan dari LI yang tidak diketik. Tetapi di sisi lain, mereka juga dapat dianggap sebagai teori yang lebih mendasar, dan kalkulus lambda yang tidak diketik adalah kasus khusus dengan hanya satu jenis.
Typed LI adalah dasar dari bahasa pemrograman dan tulang punggung bahasa fungsional seperti ML dan Haskell. Dan, secara lebih tidak langsung, gaya penciptaan yang imperatif. Kalkuli lambda yang diketik memainkan peran penting dalam pengembangan sistem tipe untuk bahasa pemrograman. Di sini, tipabilitas biasanya menangkap properti program yang diinginkan, misalnya, tidak akan menyebabkan pelanggaran akses memori.
Balku lambda yang diketik terkait erat dengan logika matematika dan teori pembuktian melalui isomorfisme Curry–Howard, dan dapat dianggap sebagai bahasa internal kelas kategori, misalnya, yangsederhananya adalah gaya penutupan Cartesian.
