zbMATH — the first resource for mathematics

Bisimilarity as a theory of functional programming. (English) Zbl 0910.68118
Brookes, Steve (ed.) et al., Mathematical foundations of programming semantics. Proceedings of the 11th conference (MFPS), Tulane Univ., New Orleans, LA, USA, March 29 - April 1, 1995. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 1, 21 p. (1995).
Summary: Morris-style contextual-equivalence invariance of termination under any context of ground type – is the usual notion of operational equivalence for deterministic functional languages such as FPC (PCF plus sums, products and recursive types). Contextual equivalence is hard to establish directly. Instead we define a labelled transition system for call-by-name FPC (and variants) and prove that CCS-style bisimilarity equals contextual equivalence – a form of operational extensionality. Using co-induction we establish equational laws for FPC. By considering variations of Milner’s ‘bisimulations up to \(\sim\)’ we obtain a second co-inductive characterisation of contextual equivalence in terms of reduction behaviour and production of values. Hence we use co-inductive proofs to establish contextual equivalence in a series of stream-processing examples. Finally, we consider a form of Milner’s original context lemma for FPC, but conclude that our form of bisimilarity supports simpler co-inductive proofs.
For the entire collection see [Zbl 0903.00064].

68Q55 Semantics in the theory of computing
Full Text: Link