Memecahkan persamaan fungsional untuk fungsi yang tidak diketahui dalam kalkulus lambda

Apakah ada teknik untuk menyelesaikan persamaan fungsional untuk fungsi yang tidak diketahui dalam kalkulus lambda?

Misalkan saya memiliki fungsi identitas yang didefinisikan secara ekstensi sebagai:

$I x = x$

(yaitu, dengan menuliskan persamaan untuk perilaku yang diharapkan dari fungsi itu) dan sekarang saya ingin menyelesaikannya untuk dengan melakukan beberapa transformasi aljabar untuk mendapatkan rumus intens untuk fungsi tersebut:$I$

$I = \lambda x.x$

yang memberitahu bagaimana tepatnya fungsi melakukan apa yang diharapkan (yaitu, bagaimana mengimplementasikannya dalam kalkulus lambda).

Tentu saja fungsi identitas digunakan hanya sebagai contoh. Saya tertarik pada metode yang lebih umum untuk menyelesaikan persamaan tersebut. Secara khusus, saya ingin menemukan fungsi yang memenuhi persyaratan berikut:$B$

$B\;f\;(\lambda x.M) = (\lambda x.f M)$

yaitu, "menyuntikkan" fungsi yang diberikan ke dalam fungsi lambda yang diberikan ( λ x . M ) sebelum "tubuh" M (yang merupakan ekspresi lambda sewenang-wenang), mungkin dengan mengambilnya terpisah dan membangun yang baru, sehingga menjadi parameter fungsi f diterapkan.$f$$(\lambda x.M)$$M$$f$

Ini adalah masalah yang diketahui, dikenal sebagai Unifikasi Pesanan Tinggi .

Sayangnya, masalah ini secara umum tidak dapat ditentukan. Ada fragmen decidable, yang dikenal sebagai Fragmen Pola Miller. Ini digunakan secara luas dalam, antara lain, pemeriksaan ketik program dependen dengan metavariables atau pencocokan pola. Fragmen ini adalah tempat variabel unifikasi diterapkan hanya untuk variabel program terikat yang berbeda.

Makalah ini memberikan tutorial yang bagus tentang cara kerja unifikasi tingkat tinggi, dan berjalan melalui (relatif) implementasi sederhana itu.

Sayangnya, sepertinya fungsi Anda tidak termasuk dalam fragmen pola ini. Yang mengatakan, apa yang saya cari terlihat sangat mirip dengan komposisi fungsi. Apakah fungsi berikut memuaskan properti Anda?

$B = \lambda f\ g\ x\ \ldotp f\ (g\ x)$

Kita punya:

• $B\ f\ (\lambda x . M)$
• dengan α- equivalence$= B\ f\ (\lambda y . [y/x]M)$$\alpha$
• $= \lambda x . f\ ((\lambda y. [y/x]M) x)$
• $= \lambda x . f\ ([x/y][y/x]M)$
• $= \lambda x . f\ M$

Saya pikir saya punya jawaban parsial, mengenai persamaan dengan fungsi identitas:

$I x = x$

Kami ingin menyelesaikannya dengan mencari formula untuk , yang akan berbentuk ( λ hal . M ) dengan beberapa ekspresi M yang belum diketahui sebagai tubuhnya. Mari gantikan dengan saya dalam persamaan asli:$I$$(\lambda p.M)$$M$$I$

$(\lambda p.M)\; x = x$

lalu terapkan fungsi ke di sebelah kiri:$x$

$M[p/x] = x$

$M$$p$$x$

$I = (\lambda x.x)$

yang tentu saja merupakan jawaban yang tepat :)

$\omega$

$\omega\;\omega = \omega\;\omega$

$\omega$$(\lambda x.M)$$M$

$(\lambda x.M)\;\omega = \omega\;\omega$

$M$

$M [x/\omega] = \omega\;\omega$

$x$$M$$\omega$$\omega\;\omega$$M$$x\;x$

$\omega = (\lambda x.x\;x)$

yang memang demikian :)

Tapi saya punya perasaan, bahwa itu bisa menjadi sangat mudah hanya karena sisi kanan sudah dalam bentuk yang kita cari.