Assume a functional language and a specialization operation (pulling out sub-expressions):

let f x y = (h 23 x) + (g 42 y)


(* h and g specialized, results might be mutually recursive *)
let rec h_23 = ... g_42 ...
and g_42 = ... h_23 ...
let f = (h_23 x) + (g_42 y)

for reasons, that do not matter, a syntactic category (e.g. the application of integers to functions) shall be evaluated by the compiler. The results might be mutually recursive (which is only detectable during specialization) and thus are bound using one big let-rec.

In such a scenario, how does one prove the correctness of the transformation (w.r.t. "normal" evaluation), when the evaluation is given as a big-step semantics?

A natural approach seems to be structural induction, but I am worried about using the induction hypothesis wrongly. The correctness property requires the explicit notion of the recursive group (say R), and evaluation of a transformed term will at some point refer to a term in that group, which is clearly not a sub-term. Can I apply the induction hypothesis on terms that appear anywhere in the premise Do I have to read up on co-induction or something completely different?

The structure of the correctness theorem looks (roughly) like this:

R is obtained via specialization
t => v        t specializes to t'
v specializes to v'
let rec R in t' => v'


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.