Howe's method

There are many ways to define the notion of program equivalence. One of them involves the construction of (bi)simulations between programs. The idea is that two programs P and Q are related by a simulation if every behaviour of P is a behaviour of Q.

Simulations are better known for their use in process calculi, where there are natural definitons of observable behaviour (e.g. sending a message). But it is no less natural to consider certain behaviours of ordinary functional programs as observable. For example, the termination of an evaluation to a \lambda-abstraction \lambda x. M can be considered as an observable event. Moreover, in an untyped setting the lambda can be considered as a request by the program to be given an argument. This perspective is due to Abramsky 1990.

This leads to various notions of program equivalence that are based on bisimilarity, observable behaviour, etc. Unlike contextual equivalence it is surprisingly hard to argue that these program equivalences are congruences, i.e. that they preserve all the constructs of the language. For example, if M \simeq N we would like to conclude that \lambda x. M \simeq \lambda x. N. This key property of congruence is what enables equational reasoning: we must be able to replace any part of a program by one that we already know is equivalent, and thus obtain equivalent programs again.

Howe's method is a technique for proving that such notions of applicative bisimilarity are in fact congruences Howe 1996.

Howe's method has been used to prove congruence properties of bimilarities for

untyped functional languages Howe 1996, Pitts 2011
typed higher-order languages, like PCF Pitts 1997, Gordon 1999
languages with objects Gordon 1998
languages with local state Jeffrey and Rathke 1999
languages with concurrent communication

References

A comprehensive tutorial on Howe's method can be found in

Pitts, A. M. 2011. ‘Howe’s Method for Higher-Order Languages’. In Advanced Topics in Bisimulation and Coinduction, edited by D. Sangiorgi and J. Rutten, 52:197–232. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. pdf

@incollection{pitts_howes_2011,
	series = {Cambridge {Tracts} in {Theoretical} {Computer} {Science}},
	title = {Howe's {Method} for {Higher}-{Order} {Languages}},
	volume = {52},
	isbn = {978-1-107-00497-9},
	booktitle = {Advanced {Topics} in {Bisimulation} and {Coinduction}},
	publisher = {Cambridge University Press},
	author = {Pitts, A. M.},
	editor = {Sangiorgi, D. and Rutten, J.},
	year = {2011},
	pages = {197--232}
}

Howe's method itself was introduced by Howe in a LICS 1989 paper. A journal version appeared in 1996.

Howe, D.J. 1989. ‘Equality in Lazy Computation Systems’. In 1989 Proceedings. Fourth Annual Symposium on Logic in Computer Science, 198–203. Pacific Grove, CA, USA: IEEE Comput. Soc. Press. https://doi.org/10.1109/LICS.1989.39174.

@inproceedings{howe_equality_1989,
	address = {Pacific Grove, CA, USA},
	title = {Equality in lazy computation systems},
	doi = {10.1109/LICS.1989.39174},
	booktitle = {[1989] {Proceedings}. {Fourth} {Annual} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE Comput. Soc. Press},
	author = {Howe, D.J.},
	year = {1989},
	pages = {198--203}
}

Howe, Douglas J. 1996. ‘Proving Congruence of Bisimulation in Functional Programming Languages’. Information and Computation 124 (2): 103–12. https://doi.org/10.1006/inco.1996.0008.

@article{howe_proving_1996,
	title = {Proving {Congruence} of {Bisimulation} in {Functional} {Programming} {Languages}},
	volume = {124},
	issn = {08905401},
	url = {https://linkinghub.elsevier.com/retrieve/pii/S0890540196900085},
	doi = {10.1006/inco.1996.0008},
	number = {2},
	journal = {Information and Computation},
	author = {Howe, Douglas J.},
	year = {1996},
	pages = {103--112}
}

A use of Howe's method for proving congruence of bisimilarity in PCF with lists can be found in

Pitts, A. M. ‘Operationally-Based Theories of Program Equivalence’. In Semantics and Logics of Computation, edited by A. M. Pitts and P. Dybjer, 241–98. Publications of the Newton Institute. Cambridge University Press, 1997. pdf

@incollection{pitts_1997,
	title = {Operationally-Based Theories of Program Equivalence},
	isbn = {978-0-521-11846-0},
	url = {https://www.cl.cam.ac.uk/~amp12/papers/opebtp/opebtp.pdf},
	series = {Publications of the Newton Institute},
	pages = {241--298},
	booktitle = {Semantics and Logics of Computation},
	publisher = {Cambridge University Press},
	author = {Pitts, A. M.},
	editor = {Pitts, A. M. and Dybjer, P.},
	date = {1997},
}

Gordon, Andrew D. ‘Bisimilarity as a Theory of Functional Programming’. Theoretical Computer Science 228, no. 1–2 (1999): 5–47. https://doi.org/10.1016/S0304-3975(98)00353-3.

@article{gordon_1999,
	title = {Bisimilarity as a theory of functional programming},
	volume = {228},
	doi = {10.1016/S0304-3975(98)00353-3},
	pages = {5--47},
	number = {1},
	journaltitle = {Theoretical Computer Science},
	shortjournal = {Theoretical Computer Science},
	author = {Gordon, Andrew D.},
	date = {1999},
}

A use of Howe's method for proving congruence of bisimilarity in object calculi can be found in

Gordon, Andrew D. ‘Operational Equivalences for Untyped and Polymorphic Object Calculi’. In Higher Order Operational Techniques in Semantics, edited by A. D. Gordon and A. M. Pitts, 9–54. Publications of the Newton Institute. Cambridge University Press, 1998.

@incollection{gordon_operational_1998,
	title = {Operational equivalences for untyped and polymorphic object calculi},
	series = {Publications of the Newton Institute},
	pages = {9--54},
	booktitle = {Higher Order Operational Techniques in Semantics},
	publisher = {Cambridge University Press},
	author = {Gordon, Andrew D.},
	editor = {Gordon, A. D. and Pitts, A. M.},
	date = {1998},
}

A use of Howe's method for proving congruence of bisimilarity in a language with local names can be found in

Jeffrey, A., and J. Rathke. ‘Towards a Theory of Bisimulation for Local Names’. In Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 56–66. IEEE, 1999. https://doi.org/10.1109/LICS.1999.782586.

@inproceedings{jeffrey_towards_1999,
	title = {Towards a theory of bisimulation for local names},
	doi = {10.1109/LICS.1999.782586},
	pages = {56--66},
	booktitle = {Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. {PR}00158)},
	publisher = {{IEEE}},
	author = {Jeffrey, A. and Rathke, J.},
	date = {1999},
}

The notion of applicative bisimilarity was introduced in

Abramsky, Samson. 1990. ‘The Lazy Lambda Calculus’. In Research Topics in Functional Programming, 65–117. Addison Wesley. pdf

@incollection{abramsky_lazy_1990,
	title = {The {Lazy} {Lambda} {Calculus}},
	url = {https://www.cs.ox.ac.uk/files/293/lazy.pdf},
	booktitle = {Research {Topics} in {Functional} {Programming}},
	publisher = {Addison Wesley},
	author = {Abramsky, Samson},
	year = {1990},
	pages = {65--117}
}