Coinductive types model infinite structures unfolded on demand, like politicians' excuses: for each attack, there is a defence but no likelihood of resolution. Representing such evolving processes coinductively is often more attractive than representing them as functions from a set of permitted observations, such as projections or finite approximants, as it can be tricky to ensure that observations are meaningful and consistent. As programmers and reasoners, we need coinductive definitions in our toolbox, equipped with appropriate computational and logical machinery.
|Title of host publication||Algebra and Coalgebra in Computer Science|
|Number of pages||13|
|Publication status||Published - Sep 2009|
|Name||Lecture Notes in Computer Science|
- information systems
- information applications
- theoretical computer science
McBride, C., Kurz, A. (Ed.), Lenisa, M. (Ed.), & Tarlecki, A. (Ed.) (2009). Let's see how things unfold.: reconciling the infinite with the intensional (extended abstract). In Algebra and Coalgebra in Computer Science (5728 ed., pp. 113-126). (Lecture Notes in Computer Science). Springer.