etiamz

Joined 1 year ago

Karma

Submissions

Member since

May 5

Recent submissions

> Again, as a "proof of research" take a look at : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.

Yes, it doesn't look like a paper at all. I can see the idea, and it's an interesting idea, but no proofs that it works, no measurements, and no proper citations.

Nobody claims Victor hasn't done a lot of research. But academically inclined people typically expect claims to be substantiated either formally or empirically or both.

Comment · 1 month ago

Then you might be interested in Marc Thatcher's recent PhD thesis dedicated to interaction nets [1]. A great exposition of interaction nets through multiplicative linear logic's proof nets, and several novel contributions like productivity analysis for interaction nets.

[1] https://hdl.handle.net/10779/uos.32024301

Comment · 11 months 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.