Kalkulus Lambda untuk fungsi yang dapat dibalik (r-Turing computable)

19

Saya tertarik pada konsep "r-Turing kelengkapan", seperti yang didefinisikan oleh Axelsen dan Glück (2011) . Suatu sistem r-Turing lengkap jika dapat menghitung serangkaian fungsi yang sama dengan mesin Turing yang dapat dibalik, tanpa menghasilkan data "sampah". Ini sama dengan kemampuan untuk menghitung setiap fungsi yang keduanya (a) dapat dihitung, dan (b) injeksi.

Saya ingin mengeksplorasi secara komputasional ruang fungsi injeksi yang dapat dihitung. Untuk melakukan ini saya sedang mencari bahasa pemrograman reversibel "paling minimal" --- sesuatu yang dapat memainkan peran setara untuk r-Turing komputabilitas yang dimainkan oleh kalkulus lambda untuk komputabilitas Turing.

Saya tahu bahwa ada banyak bahasa yang dapat dibalik yang telah dikembangkan dan terbukti lengkap oleh r-Turing. Namun, ini sedang dikembangkan dengan aplikasi praktis dalam pikiran, dan penulis mereka berkonsentrasi pada memberi mereka fitur ekspresif daripada membuatnya minimal.

Adakah yang tahu apakah bahasa seminimal mungkin seperti itu telah dideskripsikan, atau apakah ada penelitian ke arah itu? Saya cukup baru dalam literatur tentang topik ini, jadi saya bisa dengan mudah melewatkannya. Atau, apakah ada yang punya wawasan tentang bagaimana bahasa seperti itu dapat dibuat?

Di bawah ini adalah ringkasan dari apa yang saya cari. Saya tidak tahu apakah itu dapat dibuat dengan memodifikasi kalkulus lambda itu sendiri, atau apakah jenis bahasa yang benar-benar berbeda harus digunakan.

  • r-Turing bahasa lengkap - menghitung semua fungsi yang dapat dibalik yang dapat dihitung, dan hanya dapat menghitung fungsi yang dapat dibalik
  • Sintaks dan semantik seminimal mungkin. (Misalnya, kalkulus Lambda hanya memiliki definisi fungsi dan aplikasi, dan tidak ada yang lain.) Sintaks atau semantik tidak perlu terkait dengan kalkulus lambda, meskipun mungkin saja demikian.
  • Program = data. Yaitu, program beroperasi pada ekspresi daripada jenis data lainnya. Ini menjamin bahwa keluaran suatu program selalu dapat diartikan sebagai suatu program. Ini mungkin menyiratkan bahwa itu harus menjadi gaya bahasa fungsional dan bukan imperatif.
  • Ada beberapa cara sistematis untuk mengubah program menjadi kebalikannya, yang tidak melibatkan perhitungan yang jauh lebih banyak daripada yang terlibat dalam benar-benar melakukan perhitungan terbalik. (Tidak semua bahasa yang dapat dibalik memiliki properti ini, tetapi beberapa bahasa memiliki properti ini.)

Saya harus menekankan bahwa pendekatan Axelsen dan Glück terhadap komputasi reversibel sangat berbeda dari pendekatan terkenal karena Bennett, di mana program (secara umum tidak dapat dibalik) dibuat tidak dapat dibalik dengan mengembalikan beberapa informasi tentang sejarah perhitungan bersama dengan output. r-Turing kelengkapan adalah tentang kemampuan untuk menghitung fungsi injeksi tanpa output tambahan. Ada beberapa hal yang disebut variasi "kalkulus lambda reversibel" yang dapat dibalik dalam pengertian Bennet - itu bukan yang saya cari.

Nathaniel
sumber
r-Turing lengkap tampaknya seperti definisi yang relatif baru dan akan sangat membantu untuk melihat bukti bahwa itu tidak sama dengan Turing lengkap & interpretasi / analisis oleh penulis lain daripada mereka yang memperkenalkan konsep (& tautan non bayar per tayang jika mungkin)
vzn

Jawaban:

4

Saya tidak terlalu akrab dengan daerah tersebut, tetapi ada beberapa karya terbaru dari komunitas bahasa pemrograman yang mungkin menarik bagi Anda, berdasarkan gagasan untuk membatasi ke bahasa isomorfisma jenis. Khususnya, Anda bisa melihatnya

  • Jenis Pecahan oleh Roshan P. James, Zachary Sparks, Jacques Carette, dan Amr Sabry

serta berbagai publikasi terkait yang dapat Anda temukan di situs web Amr Sabry .

Noam Zeilberger
sumber