Speaker:
Koko Muroya (Birmingham)
Title
A Graph-Rewriting Perspective of the Beta-Law
Abstract
This preliminary report studies a graphical version of Plotkin's
call-by-value equational theory, in particular its soundness with
respect to operational semantics. Although an equational theory is
useful in safe program transformation like compiler optimisation,
proving its soundness is not trivial, because it involves analysis
of interaction between evaluation flow and a particular sub-program
of interest. We observe that soundness can be proved in a direct
and generic way in the graphical setting, using small-step
semantics given by a graph-rewriting abstract machine previously
built for evaluation-cost analysis. This would open up
opportunities to think of a cost-sensitive equational theory for
compiler optimisation, and to prove contextual equivalence directly
in the presence of language extensions.