Bagaimana Anda menyandikan algoritma abstrak Lamping menggunakan kombinator interaksi?

Kombinator interaksi telah diusulkan sebagai target kompilasi untuk kalkulus λ sebelumnya. Makalah itu mengimplementasikan kalkulus λ penuh. Diketahui juga bahwa adalah mungkin untuk mengoptimalkan pengkodean interaksi-bersih dari kalkulus-λ untuk subset dari istilah-istilah yang memiliki tipe-EAL. Makalah itu mengimplementasikan subset kalkulus λ dengan menerjemahkan istilah λ tipe-EAL ke jaring interaksi yang bisa dibilang lebih kompleks daripada kombinator interaksi, karena mereka menggunakan alfabet label tak terbatas untuk duplikator grup.

Saya ingin tahu apakah mungkin untuk menggabungkan kedua proposal. Yaitu, apakah ada pengkodean untuk algoritma abstrak - yaitu, λ-istilah yang bertipe EAL - sebagai kombinator interaksi?

Saya tidak mengetahui adanya implementasi algoritma Lamping secara langsung di kombinator interaksi. Saya tahu bahwa keberadaan label integer adalah fitur yang diperlukan dari algoritma Lamping, bahkan untuk istilah yang dapat diketik-EAL, karena label mencerminkan bersarangnya kotak eksponensial dalam jaring bukti, dan algoritma Lamping pada dasarnya adalah pelaksanaan jaring bukti menggunakan geometri interaksi, seperti yang pertama kali diamati oleh Gonthier, Abadi dan Lévy . Jadi pertanyaan penerapan algoritma dalam kombinator interaksi bermuara untuk mewakili kotak eksponensial dalam jaring bukti menggunakan kombinator. Ini pada dasarnya adalah apa yang dilakukan Mackie dan Pinto di koran mereka.

Tentu saja, encoding Mackie dan Pinto mendukung semua -terms, yang menggunakan kotak logika linier penuh, sedangkan istilah EAL-typable menggunakan kotak logika linier elementer, yang lebih sederhana (mereka disebut kotak functorial$\lambda$). Namun, saya tidak percaya bahwa penyederhanaan ini akan berdampak penting pada implementasi kombinator interaksi. Ini karena kotak adalah fitur global (mereka mengidentifikasi subnet besar yang sewenang-wenang untuk diduplikasi / dihapus), sedangkan kombinator interaksi (seperti sistem jaring interaksi) sepenuhnya lokal (reduksi hanya memodifikasi subnet yang dibatasi), sehingga tantangannya adalah untuk mewakili fitur global secara lokal. Sekarang, duplikasi / penghapusan global dalam EAL identik dengan logika linear penuh, itu sebabnya saya tidak berharap bahwa implementasi kombinator interaksi EAL akan secara radikal berbeda dari yang diusulkan oleh Mackie dan Pinto.