Kalkulus Lambda ialah sistem formal dalam logik matematik untuk menyatakan pengiraan berasaskan abstraksi dan menggunakan fungsi menggunakan penggantian mengikat dan berubah. Ini adalah model universal yang boleh digunakan pada reka bentuk mana-mana mesin Turing. Kalkulus lambda mula diperkenalkan oleh Church, seorang ahli matematik terkenal, pada tahun 1930-an.
Sistem ini terdiri daripada membina ahli lambda dan menjalankan operasi pengurangan ke atasnya.
Penjelasan dan Aplikasi
Huruf Yunani lambda (λ) digunakan dalam ungkapan lambda dan istilah lambda untuk menandakan pengikatan pembolehubah dalam fungsi.
Kalkulus Lambda boleh dinyahtaip atau ditaip. Dalam varian pertama, fungsi hanya boleh digunakan jika ia mampu menerima data jenis ini. Lambda calculi yang ditaip adalah lebih lemah, boleh menyatakan nilai yang lebih kecil. Tetapi, sebaliknya, ia membenarkan anda membuktikan lebih banyak perkara.
Salah satu sebab terdapat begitu banyak jenis yang berbeza ialah keinginan saintis untuk melakukan lebih banyak perkara tanpa melepaskan peluang untuk membuktikan teorem kalkulus lambda yang kukuh.
Sistem ini mempunyai aplikasi dalam pelbagai bidang matematik, falsafah, linguistik dan sains komputer. Pertama sekali, kalkulus lambda ialah kalkulus yang telah memainkan peranan penting dalam pembangunan teori bahasa pengaturcaraan. Ia adalah gaya penciptaan berfungsi yang dilaksanakan oleh sistem. Mereka juga menjadi topik penyelidikan hangat dalam teori kategori ini.
Untuk boneka
Kalkulus lambda telah diperkenalkan oleh ahli matematik Gereja Alonzo pada tahun 1930-an sebagai sebahagian daripada penyelidikannya ke dalam asas sains. Sistem asal terbukti secara logiknya tidak konsisten pada tahun 1935 apabila Stephen Kleen dan J. B. Rosser mengembangkan paradoks Kleene-Rosser.
Kemudian, pada tahun 1936, Gereja memilih dan menerbitkan hanya bahagian yang berkaitan dengan pengiraan, yang kini dipanggil kalkulus lambda yang tidak ditaip. Pada tahun 1940 beliau juga memperkenalkan teori yang lebih lemah tetapi konsisten secara logik yang dikenali sebagai sistem jenis perdana. Dalam karyanya, dia menerangkan keseluruhan teori dalam istilah mudah, jadi boleh dikatakan bahawa Gereja menerbitkan kalkulus lambda untuk boneka.
Sehingga tahun 1960-an, apabila hubungannya dengan bahasa pengaturcaraan menjadi jelas, λ hanyalah formalisme. Terima kasih kepada aplikasi Richard Montagu dan ahli bahasa lain dalam semantik bahasa semula jadi, kalkulus telah mendapat tempat dalam kedua-dua linguistik dan sains komputer.
Asal usul simbol
Lambda bukan bermaksud perkataan atau akronim, ia berasal daripada rujukan dalam Matematik Utama Russell diikuti dengan dua perubahan tipografi. Contoh tatatanda: untuk fungsi f dengan f (y)=2y + 1 ialah 2ŷ + 1. Dan di sini kita menggunakan karet (“topi”) di atas y untuk melabelkan pembolehubah input.
Gereja pada asalnya bertujuan untuk menggunakan simbol yang serupa, tetapi penyusun taip tidak dapat meletakkan simbol "topi" di atas huruf. Jadi sebaliknya mereka mencetaknya pada asalnya sebagai "/\y.2y+1". Dalam episod pengeditan seterusnya, jurutaip menggantikan "/ \" dengan watak yang serupa secara visual.
Pengenalan kepada kalkulus lambda
Sistem ini terdiri daripada bahasa istilah, yang dipilih oleh sintaks formal tertentu, dan satu set peraturan transformasi yang membolehkannya dimanipulasi. Titik terakhir boleh dianggap sebagai teori persamaan atau sebagai definisi operasi.
Semua fungsi dalam kalkulus lambda adalah awanama, bermakna ia tidak mempunyai nama. Mereka hanya mengambil satu pembolehubah input dan kari digunakan untuk melaksanakan plot dengan berbilang pembolehubah.
Syarat Lambda
Sintaks kalkulus mentakrifkan beberapa ungkapan sebagai sah dan yang lain sebagai tidak sah. Sama seperti rentetan aksara yang berbeza adalah program C yang sah dan ada yang tidak. Ungkapan sebenar kalkulus lambda dipanggil "istilah lambda".
Tiga peraturan berikut memberikan definisi induktif yang bolehdigunakan pada pembinaan semua konsep yang sah secara sintaksis:
Pembolehubah x itu sendiri ialah istilah lambda yang sah:
- jika T ialah LT dan x bukan pemalar, maka (lambda xt) dipanggil abstraksi.
- jika T dan s adalah konsep, maka (TS) dipanggil aplikasi.
Tiada yang lain ialah istilah lambda. Oleh itu, sesuatu konsep adalah sah jika dan hanya jika ia boleh diperolehi dengan penggunaan berulang ketiga-tiga peraturan ini. Walau bagaimanapun, beberapa kurungan mungkin ditinggalkan mengikut kriteria lain.
Definisi
Ungkapan Lambda terdiri daripada:
- pembolehubah v 1, v 2, …, v n, …
- simbol abstraksi 'λ' dan titik '.'
- kurung ().
Set Λ boleh ditakrifkan secara induktif:
- Jika x ialah pembolehubah, maka x ∈ Λ;
- x tidak tetap dan M ∈ Λ, kemudian (λx. M) ∈ Λ;
- M, N ∈ Λ, kemudian (MN) ∈ Λ.
Penetapan
Untuk memastikan notasi ungkapan lambda tidak berselerak, konvensyen berikut biasanya digunakan:
- Kurungan luar ditiadakan: MN bukannya (MN).
- Aplikasi diandaikan kekal bersekutu: seseorang boleh menulis MNP dan bukannya ((MN) P).
- Isi abstraksi memanjang lebih jauh ke kanan: λx. MN bermaksud λx. (MN), bukan (λx. M) N.
- Jujukan pengabstrakan dikurangkan: λx.λy.λz. N boleh menjadi λxyz. N.
Pembolehubah bebas dan terikat
Pengendali λ menyambung bukan pemalarnya di mana sahaja ia berada dalam badan pengabstrakan. Pembolehubah yang termasuk dalam skop dipanggil terikat. Dalam ungkapan λ x. M, bahagian λ x sering dirujuk sebagai pengikat. Seolah-olah membayangkan pembolehubah menjadi satu kumpulan dengan penambahan X x kepada M. Semua pembolehubah lain yang tidak stabil dipanggil percuma.
Sebagai contoh, dalam ungkapan λ y. x x y, y - terikat tidak kekal dan x - bebas. Dan ia juga perlu diperhatikan bahawa pembolehubah dikelompokkan mengikut abstraksi "terdekat". Dalam contoh berikut, penyelesaian kalkulus lambda diwakili oleh kejadian tunggal x, yang berkaitan dengan sebutan kedua:
λ x. y (λ x. z x)
Set pembolehubah bebas M dilambangkan sebagai FV (M) dan ditakrifkan melalui pengulangan ke atas struktur sebutan seperti berikut:
- FV (x)={x}, dengan x ialah pembolehubah.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Formula yang tidak mengandungi pembolehubah bebas dipanggil tertutup. Ungkapan lambda tertutup juga dikenali sebagai penggabung dan bersamaan dengan istilah dalam logik gabungan.
Singkatan
Maksud ungkapan lambda ditentukan oleh cara ia boleh dipendekkan.
Terdapat tiga jenis potongan:
- α-transform: menukar pembolehubah terikat (alfa).
- β-reduction: menggunakan fungsi pada hujahnya (beta).
- η-transform: merangkumi tanggapan lanjutan.
Ini jugakita bercakap tentang kesetaraan yang terhasil: dua ungkapan adalah setara β jika ia boleh diubah menjadi β kepada komponen yang sama, dan kesetaraan α / η ditakrifkan secara serupa.
Istilah redex, singkatan kepada perolehan boleh dikurangkan, merujuk kepada subtopik yang boleh dikurangkan dengan salah satu peraturan. Kalkulus Lambda untuk boneka, contoh:
(λ x. M) N ialah redex beta dalam ungkapan untuk menggantikan N dengan x dalam M. Komponen yang dikurangkan redex dipanggil pengurangannya. Pengurangan (λ x. M) N ialah M [x:=N].
Jika x tidak percuma dalam M, λ x. M x juga em-REDEX dengan pengawal selia M.
α-transformasi
Nama semula Alpha membolehkan anda menukar nama pembolehubah terikat. Contohnya, x. x boleh memberi λ y. y. Istilah yang berbeza hanya dalam penjelmaan alfa dikatakan setara α. Selalunya, apabila menggunakan kalkulus lambda, α-setara dianggap timbal balik.
Peraturan yang tepat untuk penukaran alfa bukanlah perkara remeh sepenuhnya. Pertama, dengan abstraksi ini, hanya pembolehubah yang dikaitkan dengan sistem yang sama dinamakan semula. Contohnya, penjelmaan alfa λ x.λ x. x boleh membawa kepada λ y.λ x. x, tetapi ini mungkin tidak membawa kepada λy.λx.y Yang terakhir mempunyai makna yang berbeza daripada yang asal. Ini adalah analog dengan konsep pengaturcaraan bayang-bayang berubah-ubah.
Kedua, transformasi alfa tidak boleh dilakukan jika ia akan mengakibatkan ditangkap oleh abstraksi lain yang tidak kekal. Contohnya, jika anda menggantikan x dengan y dalam λ x.λ y. x, maka anda boleh mendapatkanλy.λy. u, yang tidak sama sama sekali.
Dalam bahasa pengaturcaraan dengan skop statik, penukaran alfa boleh digunakan untuk memudahkan peleraian nama. Pada masa yang sama, menjaga agar konsep pembolehubah tidak menutup penetapan dalam kawasan yang mengandungi.
Dalam notasi indeks De Bruyne, mana-mana dua istilah setara alfa adalah sama secara sintaksis.
Penggantian
Perubahan yang ditulis oleh E [V:=R] ialah proses menggantikan semua kejadian bebas pembolehubah V dalam ungkapan E dengan perolehan R. Penggantian dari segi λ ditakrifkan oleh lambda rekursi kalkulus pada struktur konsep seperti berikut (nota: x dan y - pembolehubah sahaja, dan M dan N - sebarang ungkapan λ).
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, dengan syarat y ∉ FV (N).
Untuk penggantian kepada abstraksi lambda, kadangkala perlu α-transform ekspresi. Sebagai contoh, adalah tidak benar bahawa (λ x. Y) [y:=x] menghasilkan (λ x. X) kerana x yang digantikan sepatutnya bebas, tetapi akhirnya terikat. Penggantian yang betul dalam kes ini ialah (λ z. X) sehingga kesetaraan α. Ambil perhatian bahawa penggantian ditakrifkan secara unik sehingga lambda.
β-reduction
Pengurangan beta mencerminkan idea menggunakan fungsi. Beta-reduktif ditakrifkan dalam istilahpenggantian: ((X V. E) E ') ialah E [V:=E'].
Sebagai contoh, andaikan beberapa pengekodan 2, 7, ×, terdapat pengurangan β berikut: ((λ n. N × 2) 7) → 7 × 2.
Pengurangan beta boleh dilihat sama seperti konsep pengurangan tempatan di bawah potongan semula jadi melalui isomorfisme Curry-Howard.
η-transform
Penukaran ini menyatakan idea pelanjutan, yang dalam konteks ini ialah dua fungsi adalah sama apabila ia memberikan hasil yang sama untuk semua hujah. Penukaran ini bertukar antara λ x. (F x) dan f apabila x nampaknya tidak percuma dalam f.
Tindakan ini boleh dianggap sama seperti konsep kesempurnaan tempatan dalam potongan semula jadi melalui isomorfisme Curry-Howard.
Bentuk dan gabungan biasa
Untuk kalkulus lambda yang tidak ditaip, peraturan pengurangan β secara amnya bukan normalisasi kuat atau lemah.
Walau bagaimanapun, dapat ditunjukkan bahawa pengurangan β bergabung apabila dijalankan sebelum transformasi α (iaitu, dua bentuk normal boleh dianggap sama jika perubahan α dari satu ke satu lagi mungkin).
Oleh itu, kedua-dua istilah penormalan kuat dan istilah pelarasan lemah mempunyai satu bentuk biasa. Untuk istilah pertama, sebarang strategi pengurangan dijamin menghasilkan konfigurasi biasa. Manakala untuk keadaan normalisasi yang lemah, beberapa strategi pengurangan mungkin tidak menemuinya.
Kaedah pengaturcaraan tambahan
Terdapat banyak simpulan bahasa ciptaan untuk kalkulus lambda. Kebanyakannya pada asalnya dibangunkan dalam konteks menggunakan sistem sebagai asas untuk semantik bahasa pengaturcaraan, dengan berkesan menerapkannya sebagai binaan peringkat rendah. Memandangkan sesetengah gaya menyertakan kalkulus lambda (atau sesuatu yang hampir serupa) sebagai coretan, teknik ini juga boleh digunakan dalam penciptaan praktikal, tetapi kemudiannya boleh dianggap sebagai kabur atau asing.
Pemalar bernama
Dalam kalkulus lambda, pustaka berbentuk set fungsi yang ditakrifkan sebelum ini, di mana istilahnya hanyalah pemalar konkrit. Kalkulus tulen tidak mempunyai konsep yang dinamakan tidak boleh ubah kerana semua sebutan lambda atom adalah pembolehubah. Tetapi mereka juga boleh ditiru dengan mengambil yang boleh ubah sebagai nama pemalar, menggunakan abstraksi lambda untuk mengikat yang tidak menentu dalam badan, dan menggunakan abstraksi itu pada definisi yang dimaksudkan. Jadi jika anda menggunakan f untuk mewakili M dalam N, anda boleh sebut
(λ f. N) M.
Pengarang sering memperkenalkan konsep sintaksis seperti biarkan untuk membolehkan sesuatu ditulis dengan cara yang lebih intuitif.
f=M hingga N
Dengan merangkaikan takrifan sedemikian, seseorang boleh menulis "program" kalkulus lambda sebagai sifar atau lebih definisi fungsi diikuti oleh ahli lambda tunggal, menggunakan takrifan tersebut yang membentuk sebahagian besar atur cara.
Satu had ketara bagi let ini ialah nama f tidak ditakrifkan dalam M,memandangkan M berada di luar skop mengikat abstraksi lambda f. Ini bermakna atribut fungsi rekursif tidak boleh digunakan sebagai M dengan let. Sintaks letrec yang lebih maju, yang membolehkan anda menulis definisi fungsi rekursif dalam gaya ini, juga menggunakan penggabung titik tetap.
Analog bercetak
Jenis ini ialah formalisme bertaip yang menggunakan simbol untuk mewakili abstraksi fungsi tanpa nama. Dalam konteks ini, jenis biasanya objek bersifat sintaksis yang ditetapkan kepada istilah lambda. Sifat yang tepat bergantung pada kalkulus yang dipersoalkan. Dari sudut pandangan tertentu, LI yang ditaip boleh dianggap sebagai penambahbaikan LI yang tidak ditaip. Tetapi sebaliknya, ia juga boleh dianggap sebagai teori yang lebih asas, dan kalkulus lambda yang tidak ditaip ialah kes khas dengan hanya satu jenis.
Taip LI ialah asas bahasa pengaturcaraan dan tulang belakang bahasa berfungsi seperti ML dan Haskell. Dan, secara tidak langsung, gaya penciptaan yang penting. Lambda calculi yang ditaip memainkan peranan penting dalam pembangunan sistem jenis untuk bahasa pengaturcaraan. Di sini, kebolehtaipan biasanya menangkap sifat program yang diingini, contohnya, ia tidak akan menyebabkan pelanggaran akses memori.
Batul lambda yang ditaip berkait rapat dengan logik matematik dan teori bukti melalui isomorfisme Curry–Howard, dan boleh dianggap sebagai bahasa dalaman bagi kelas kategori, contohnya, yanghanyalah gaya penutupan Cartesian.
