| ▲ | etiamz 4 hours ago | |
Note that, in the interaction net literature, it is pretty common to introduce graphical notation without corresponding textual counterparts. See the works of Lafont, Lamping, Asperti, Guerrini, and many others [1]. (However, the textual calculus can be absolutely crucial for formal proof.) The absence of proofs and benchmarks undermines the paper for me as well. I find it absolutely critical to demonstrate how the approach works in comparison with already established software, such as BOHM [2]. Parallel beta reduction not being elementarily recursive is not a thing to address, nor a thing one can address. Lamping's abstract algorithm already performs the minimal amount of work to reduce a term -- one cannot improve it further. From my understanding, the paper aims to optimize the bookkeeping overhead present in earlier implementations of optimal reduction. However, as I said, the absence of formal/empirical evidence of correctness and extensive benchmarks makes the contributions of the paper debatable. | ||