Apakah ada strategi pengurangan normalisasi (atau abadi) untuk kombinator yang tidak diketik?

Terinspirasi oleh pertanyaan ini , saya ingin tahu apakah ada strategi pengurangan untuk kombinator SKI yang tidak dikenal yang dikenal sebagai normalisasi atau abadi.

Seperti dijelaskan di sini (Twelfed here ), aturan nondeterminstic dari kalkulus combinator adalah sebagai berikut:

$Ix \rightarrow x$

$Kxy \rightarrow x$

$Sxyz \rightarrow xz(yz)$

x → x $xy \rightarrow x'y$ jika$x \rightarrow x'$

y → y $xy \rightarrow xy'$ if$y \rightarrow y'$

Combinator SKI digunakan sebagai teknik implementasi untuk Miranda, bahasa fungsional malas yang dikembangkan oleh David Turner. Strategi reduksi yang Anda kejar hanyalah melakukan reduksi dari kiri ke kanan (alias urutan normal atau pengurangan panggilan-dengan-nama). Ini disebut pengurangan combinator SKI , dan itu secara alami malas. Jika ada urutan reduksi normalisasi, maka strategi reduksi ini akan menemukannya.

Satu masalah dengan kombinator SKI adalah bahwa mereka memiliki properti yang tidak menguntungkan sehingga menghasilkan ledakan eksponensial dalam ukuran kode selama pengurangan.

Lihat:

• DA Turner. Teknik implementasi baru untuk bahasa aplikatif. Lembut. Praktik dan Exper., 9, hlm. 31-49, 1979.

• Lambda-Calculus and Combinators: An Introduction, Edisi Kedua oleh JR Hindley dan JP Seldin