Proving the correctness of unfold/fold program transformations using bisimulation

TY - GEN

T1 - Proving the correctness of unfold/fold program transformations using bisimulation

AU - Hamilton, Geoff W.

AU - Jones, Neil

N1 - Conference code: 8

PY - 2012

Y1 - 2012

N2 - 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 difficult 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.

AB - 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 difficult 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.

UR - http://www.scopus.com/inward/record.url?scp=84862074469&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-29709-0_15

DO - 10.1007/978-3-642-29709-0_15

M3 - Article in proceedings

AN - SCOPUS:84862074469

SN - 978-3-642-29708-3

T3 - Lecture notes in computer science

SP - 153

EP - 169

BT - Perspectives of Systems Informatics

A2 - Clarke, Edmund

A2 - Virbitskaite, Irina

A2 - Voronkov, Andrei

PB - Springer

T2 - 8th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics

Y2 - 27 June 2011 through 1 July 2011

ER -