Ask HN: Where's good to ask questions about language papers?

1 points by mrobot ↗ HN
Where is a good place to ask questions about language papers? I am having trouble with a little proof that i guess should be obvious as part of a paper and thought i wanted to ask someone, but i don't know where people talk about such things. Are there any good language theory IRC channels?

I wanted to understand "evlis tail recursion" so I am studying the paper Wand 1980, "Continuation-based program transformation strategies" -- https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.8567&rep=rep1&type=pdf

I am on page 167 and i am trying to prove that "If REV terminates (which it always does), then so does REVC".

It says to consider the performance specification "psi-Revc(X, gamma; Z) -- if y occurs as a first argument to REVC during the computation of REVC(x, gamma), then y occurs as a first argument to REV during the computation of REV(x)."

Then it says if you consider the operational semantics of recursion equations in, say, call-by-value, this spec is inconsistent with nontermination.

First question is how do you say that the performance specification is true for a correct REVC? I think i see it but was having trouble formalizing it.

Second is how to say that REVC definitely terminates?

I am new to proving correctness so sorry if this is obvious.

0 comments

[ 4.7 ms ] story [ 8.2 ms ] thread

No comments yet.