Mengapa penting untuk fungsi anonim dalam kalkulus lambda?

Saya menonton ceramah oleh Jim Weirich, berjudul ' Adventures in Functional Programming '. Dalam kuliah ini, ia memperkenalkan konsep kombinator-Y, yang pada dasarnya menemukan titik tetap untuk fungsi-fungsi tingkat tinggi.

Salah satu motivasi, seperti yang ia sebutkan, adalah untuk dapat mengekspresikan fungsi rekursif dengan menggunakan kalkulus lambda sehingga teori oleh Gereja (apa pun yang dapat dihitung secara efektif dapat dihitung dengan menggunakan kalkulus lambda) tetap ada.

Masalahnya adalah bahwa suatu fungsi tidak dapat memanggil dirinya sendiri begitu saja, karena lambda kalkulus tidak mengizinkan fungsi bernama, yaitu,

tidak tahan dengan nama ' ', itu harus didefinisikan secara anonim:$n$

Mengapa penting bagi lambda calculus untuk memiliki fungsi yang tidak disebutkan namanya? Prinsip apa yang dilanggar jika ada fungsi yang dinamai? Atau apakah saya hanya salah paham tentang video jim?

Teorema utama mengenai masalah ini adalah karena ahli matematika Inggris dari akhir abad ke-16, yang disebut William Shakespeare . Makalahnya yang paling terkenal tentang masalah ini berjudul " Romeo dan Juliet " diterbitkan pada tahun 1597, meskipun pekerjaan penelitian dilakukan beberapa tahun sebelumnya, menginspirasi tetapi pendahulu seperti Arthur Brooke dan William Painter.

Hasil utamanya, dinyatakan dalam Babak II. Adegan II , adalah teorema yang terkenal :

Apa namanya? apa yang kita sebut mawar
Dengan nama lain akan berbau manis;

Teorema ini dapat secara intuitif dipahami sebagai "nama tidak berkontribusi pada makna".

Bagian terbesar dari makalah ini dikhususkan untuk contoh yang melengkapi teorema dan menunjukkan bahwa, meskipun nama tidak memberikan makna, mereka adalah sumber masalah yang tak ada habisnya.

Seperti yang ditunjukkan oleh Shakespeare, nama dapat diubah tanpa mengubah makna, operasi yang kemudian disebut -conversion oleh Gereja Alonzo dan para pengikutnya. Akibatnya, tidak selalu mudah untuk menentukan apa yang dilambangkan dengan nama. Ini menimbulkan berbagai masalah seperti mengembangkan konsep lingkungan di mana asosiasi makna-nama ditentukan, dan aturan untuk mengetahui apa lingkungan saat ini ketika Anda mencoba menentukan makna yang terkait dengan nama. Ini membingungkan para ilmuwan komputer untuk sementara waktu, sehingga menimbulkan kesulitan teknis seperti masalah Funarg yang terkenal$\alpha$. Lingkungan tetap menjadi masalah dalam beberapa bahasa pemrograman populer, tetapi secara fisik umumnya dianggap tidak aman untuk lebih spesifik, hampir sama mematikannya dengan contoh yang dikerjakan oleh Shakespeare dalam makalahnya.

Masalah ini juga dekat dengan masalah yang diangkat dalam teori bahasa formal , ketika huruf dan sistem formal harus didefinisikan hingga isomorfisma , sehingga menggarisbawahi bahwa simbol - simbol huruf adalah entitas abstrak , independen dari bagaimana mereka "terwujud" sebagai elemen dari beberapa set.

Hasil utama oleh Shakespeare ini menunjukkan juga bahwa sains kemudian menyimpang dari sihir dan agama, di mana makhluk atau makna mungkin memiliki nama sejati .

Kesimpulan dari semua ini adalah bahwa untuk pekerjaan teoretis, seringkali lebih mudah untuk tidak dibebani dengan nama, meskipun mungkin terasa lebih sederhana untuk pekerjaan praktis dan kehidupan sehari-hari. Tetapi ingatlah bahwa tidak semua orang memanggil Ibu adalah ibumu.

Catatan :
Masalah ini baru-baru ini ditangani oleh ahli logika Amerika abad ke-20 Gertrude Stein . Namun, rekan-rekan matematikawannya masih merenungkan implikasi teknis yang tepat dari teorema utamanya :

Mawar adalah mawar adalah mawar adalah mawar.

diterbitkan pada tahun 1913 dalam komunikasi singkat berjudul "Sacred Emily".

$\lambda$$\lambda$$\pi$$\nu x.P$$\pi$

$\lambda$$\lambda$$\lambda$

$\mathsf{let} f = M \mathsf{in} N$$(\lambda f.N)M$$\lambda$

Saya percaya idenya adalah bahwa nama tidak perlu. Apa pun yang tampaknya memerlukan nama dapat ditulis sebagai fungsi anonim.

Anda dapat memikirkan kalkulus lambda seperti bahasa rakitan. Seseorang dalam ceramah tentang majelis mungkin mengatakan "Tidak ada pohon warisan berorientasi objek dalam bahasa majelis." Anda mungkin berpikir cara cerdas untuk menerapkan pohon warisan, tapi bukan itu intinya. Intinya adalah bahwa pohon warisan tidak diperlukan pada tingkat paling dasar tentang bagaimana komputer fisik diprogram.

Dalam kalkulus lambda intinya adalah bahwa nama tidak diperlukan untuk menggambarkan suatu algoritma pada tingkat paling dasar.

Saya menikmati 3 jawaban di sini sejauh ini - terutama analisis Shakespearen @ babou - tetapi mereka tidak menjelaskan apa yang saya pikir adalah inti dari pertanyaan.

λ-calculus mengikat nama ke fungsi setiap kali Anda menerapkan fungsi ke fungsi. Masalahnya bukan kurangnya nama.

"Masalahnya adalah bahwa suatu fungsi tidak dapat memanggil dirinya sendiri hanya" dengan merujuk pada namanya.

(Dalam Lisp murni, nama -> fungsi mengikat tidak dalam ruang lingkup di dalam tubuh fungsi. Untuk fungsi memanggil dirinya dengan namanya, fungsi harus merujuk ke lingkungan yang merujuk ke fungsi. Lisp murni tidak memiliki struktur data siklik. Tidak murni Lisp melakukannya dengan memutasikan lingkungan yang merujuk fungsi.)

Seperti yang ditunjukkan oleh @MartinBerger, alasan historis bahwa λ-calculus tidak membiarkan fungsi memanggil dirinya dengan nama adalah upaya untuk mengesampingkan paradoks Curry ketika mencoba menggunakan λ-calculus sebagai dasar matematika, termasuk logika deduktif. Ini tidak berhasil karena teknik seperti kombinator Y memungkinkan rekursi bahkan tanpa referensi sendiri.

Dari Wikipedia:

Jika kita dapat mendefinisikan fungsi r = (λ.x x x ⇒ y)maka r r = (r r ⇒ y).

Jika r rbenar maka yitu benar. Jika r rsalah maka r r ⇒ yitu benar, yang merupakan kontradiksi. Begitu yjuga benar dan seperti yhalnya pernyataan apa pun, pernyataan apa pun dapat dibuktikan benar.

r radalah perhitungan yang tidak berakhir. Dianggap sebagai logika r radalah ekspresi untuk nilai yang tidak ada.