Loading...
Proving the correctness of unfold/fold program transformations using bisimulation
Date
2012
Abstract
This paper shows that a bisimulation approach can be used to prove the correctness of unfold/fold program transformation algorithms. As an illustration, we show how our approach can be use to prove the correctness of positive supercompilation (due to S rensen et al). Traditional program equivalence proofs show the original and transformed programs are contextually equivalent, i.e., have the same termination behaviour in all closed contexts. Contextual equivalence can, however, be di cult to establish directly. Gordon and Howe use an alternative approach: to represent a program's behaviour by a labelled transition system whose bisimilarity relation is a congruence that coincides with contextual equivalence. Labelled transition systems are well-suited to represent global program behaviour. On the other hand, unfold/fold program transformations use generalization and folding, and neither is easy to describe contextually, due to use of non-local information.We show that weak bisimulation on labelled transition systems gives an elegant framework to prove contextual equivalence of original and transformed programs. One reason is that folds can be seen in the context of corresponding unfolds.
Supervisor
Description
peer-reviewed
Publisher
Springer
Citation
Perspectives of Systems Informatics: Lecture Notes in Computer Science;7162 pp. 153-169
Files
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)