Partial Evaluation of Call-by-value lambda-calculus with Side-effects
We present a framework of an online partial evaluator for a
call-by-value lambda-calculus with destructive updates of data
structures. It properly and correctly specializes expressions that
contain side-effects, while preserving pointer equality, which is an
important property for programs using updates. Our partial evaluator
uses a side-effect analysis to extract immutable data structures and
then performs an online specialization using preactions. Once mutable
and immutable data structures are separated, partial evaluation is
done in such a way that accesses to immutable ones are performed at
specialization time, while accesses to mutable ones are residualized.
For the correct residualization of side-effecting operations,
preactions are used to solve various issues, including code
elimination, code duplication, and execution order preservation. The
preaction mechanism also enables us to reduce expressions that were
residualized when the conventional let-expression approach of Similix
was used. The resulting partial evaluator is simple enough to prove
its correctness. Based on the framework, we have constructed a
partial evaluator for Scheme, which is powerful enough to specialize
fairly complicated programs with side-effects, such as an interpreter.