β Scribed by Andrew D. Gordon
No coin nor oath required. For personal study only.
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 PCF. Contextual equivalence is hard to establish directly. Instead, we deΓΏne a labelled transition system for call-by-name PCF (and variants) and prove that CCS-style bisimilarity equals contextual equivalence. Using co-induction we establish equational laws. By considering variations of Milner's 'bisimulations up to βΌ' we obtain a second co-inductive characterisation of contextual equivalence in terms of reduction behaviour and production of values. Hence we use co-induction to establish contextual equivalence in a series of stream-processing examples. We show that Milner's context lemma may be extended to our variants of PCF, but in fact our form of bisimilarity supports simpler co-inductive proofs. We sketch how these results extend to variants, including eager evaluation and the addition of sums, pairs and recursive types.
π SIMILAR VOLUMES