Makalah ini menunjukkan bahwa ada kombinator (mewakili perhitungan simbolik) yang tidak dapat diwakili oleh kalkulus Lambda (jika saya memahami hal-hal dengan benar):
Ada beberapa hal yang mungkin ingin dilakukan seseorang dalam praktik dan yang tidak dapat diungkapkan secara langsung dalam kalkulus lambda.
Kalkulus SF adalah contohnya. Kekuatan ekspresifnya bukanlah berita; bagian yang menarik dari makalah (tidak ditampilkan dalam slide) adalah teori kategori di baliknya. Kalkulus SF analog dengan implementasi lisp di mana Anda mengizinkan fungsi untuk memeriksa representasi argumen mereka - sehingga Anda dapat menulis hal-hal seperti (print (lambda (x) (+ x 2)))⟹ "(lambda (x) (+ x 2))".
Contoh penting lainnya adalah paralel atau Plotkin . Secara intuitif, ada hasil umum yang menyatakan bahwa lambda calculus berurutan: fungsi yang mengambil dua argumen harus memilih satu untuk dievaluasi terlebih dahulu. Tidak mungkin menulis istilah lambda orsedemikian rupa sehingga ( or⊤ ⊥) ⟹ ⊤, ( or⊥ ⊤) ⟹ ⊤ dan or⊥ ⊥ ⟹ ⊥ (di mana term adalah istilah yang tidak berakhir dan ⊤ adalah istilah yang mengakhiri). Ini dikenal sebagai "paralel atau" karena implementasi paralel dapat membuat satu langkah dari setiap pengurangan dan berhenti setiap kali salah satu argumen berakhir.
Namun hal lain yang tidak dapat Anda lakukan dalam kalkulus lambda adalah input / output. Anda harus menambahkan primitif ekstra untuk itu.
Tentu saja, semua contoh ini dapat direpresentasikan dalam kalkulus lambda dengan menambahkan satu tingkat tipuan, yang pada dasarnya mewakili istilah lambda sebagai data. Tapi kemudian model menjadi kurang menarik - Anda kehilangan hubungan antara fungsi-fungsi dalam bahasa model dan abstraksi lambda.
Jawaban untuk pertanyaan Anda tergantung pada bagaimana Anda mendefinisikan "perhitungan" dan "terwakili". The thread di LTU yang sclv disebutkan , di sisi lain, sebagian besar terdiri dari orang-orang berbicara melewati satu sama karena lain untuk definisi sejajar dari berbagai istilah.
Perbedaannya tentu bukan kekuatan komputasi - setiap sistem yang dipertimbangkan setara dengan Turing. Yang menjadi masalah adalah bahwa kesetaraan Turing belaka tidak benar-benar mengatakan apa-apa tentang struktur atau semantik ekspresi. Untuk itu, dalam model yang sangat minimalis perhitungan yang membutuhkan pengkodean yang kompleks atau non-sepele negara awal, mungkin bahkan tidak jelas apakah sistem ini mampu perhitungan universal, atau apakah ilusi universalitas sedang dibuat oleh interpretasi seseorang dari sistem . Misalnya, lihat diskusi milis ini mengenai mesin Turing 2-negara, 3-simbol, khususnya masalah yang diangkat oleh Vaughan Pratt.
Bagaimanapun, perbedaan yang ditarik adalah antara sesuatu seperti:
Turing-equivalence hanya menyiratkan bahwa suatu sistem memenuhi kriteria ketiga untuk setiap fungsi yang dapat dihitung, sedangkan yang paling sering adalah kriteria pertama yang kita pedulikan, baik dalam sistem logika formal atau bahasa pemrograman (sejauh apa pun itu sebenarnya berbeda).
Itu deskripsi yang sangat informal, tetapi ide yang penting dapat dipastikan lebih tepat. Dalam utas LtU tersebut di atas dapat ditemukan beberapa referensi untuk pekerjaan yang ada di sepanjang garis yang sama.
Logika kombinatori Schönfinkel dan λ-kalkulus Gereja awalnya dirancang sebagai abstraksi suling dari penalaran logis, dan dengan demikian, struktur peta mereka sangat rapi ke penalaran logis dan sebaliknya. Mereka juga membawa asumsi ekstensionalitas , seperti yang dijelaskan oleh aturan pengurangan-eta:, di λx. f xmana xtidak terjadi f, sama dengan hanya fsendirian.
Dalam praktiknya, gagasan ekstensionalitas yang sangat ketat bisa terlalu membatasi, sementara intensionalitas yang tidak terkendali membuat penalaran lokal tentang sub-ekspresi menjadi sulit atau tidak mungkin.
SF-calculus adalah kalkulus combinator yang dimodifikasi yang memberikan, sebagai operasi primitif, bentuk terbatas dari analisis intensif: Kemampuan untuk mendekonstruksi ekspresi yang diterapkan sebagian, tetapi bukan nilai-nilai primitif atau ekspresi non-normal. Ini terjadi untuk memetakan dengan baik ke ide-ide seperti pencocokan pola seperti yang ditemukan dalam bahasa pemrograman atau gaya makro seperti yang ditemukan di Lisps, tetapi tidak dapat dijelaskan dalam SK- atau λ-kalkulus tanpa, secara efektif, menerapkan juru bahasa untuk mengevaluasi istilah "intensional".
Jadi, dalam ringkasan: SF-kalkulus tidak dapat diwakili secara langsung dalam λ-kalkulus dalam arti bahwa representasi terbaik yang paling mungkin melibatkan penerapan penerjemah kalkulus SF, dan alasan untuk ini adalah perbedaan semantik mendasar: Apakah ekspresi memiliki internal struktur, atau mereka didefinisikan murni oleh perilaku eksternal mereka?
Kalkulus SF Barry Jay dapat melihat struktur istilah yang diterapkannya, yang non-fungsional. Kalkulus Lambda dan logika kombinasi tradisional berfungsi murni, jadi tidak bisa melakukan ini.
Ada banyak ekstensi dari lambda-calculus yang melakukan hal-hal yang melanggar kemurnian, yang sebagian besar memerlukan perbaikan strategi penulisan ulang sampai tingkat tertentu, seperti menambahkan status, kontrol (misalnya, melalui kelanjutan), atau variabel logika.
sumber