BRICS · Contents · Programme · Lecture Notes

A Tutorial on Co-Induction and Functional Programming

A BRICS Mini-Course
March 22 and 23, 1995

Lectures by
Andrew D. Gordon
Computer Laboratory, Cambridge University


Course Contents

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.

Programme

Wednesday March 22, 1995, 13:15-15:15 in Auditorium D2

Thursday March 23, 1995, 14:15-16:15 in Auditorium D1

Lecture Notes

BRICS-NS-95-3