Ask HN: Where's good to ask questions about language papers?
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 ] threadNo comments yet.