A BRICS Mini-Course
March 22 and 23, 1995
Andrew D. Gordon
Computer Laboratory, Cambridge University
Co-induction is an important tool for reasoning about unbounded structures. This tutorial explains the foundations of co-induction, and shows how it justifies intuitive arguments about lazy streams, of central importance to lazy functional programmers (Hughes 1989). Our theory is based on a new formulation of bisimilarity for functional programs. Our main contribution is to answer Turner's (1990, Preface) concern that Abramsky's (1993) formulation of applicative bisimulation was too intensional for lazy languages such as Haskell or Miranda. Our bisimilarity coincides with Morris-style contextual equivalence. In particular it identifies Omega and lambdax. Omega, which are distinguished by applicative bisimulation. We explain from first principles an operational theory of functional programming based on bisimilarity and co-induction. We show how to prove properties of lazy streams by co-induction and derive the 'Take Lemma' of Bird and Wadler(1988), a well-known proof technique for lazy streams.