Well-definedness and observational equivalence for inductive–coinductive programs. (8th July 2019)

• Record Type: Journal Article
• Authors: Basold, Henning; Hansen, Helle Hvid
• Is Part Of: Journal of logic and computation. Volume 29:Number 4(2019)
• Page Start: 419
• Page End: 468
• Publication Date: 2019-07-08
• Subjects: Inductive types -- coinductive types -- termination -- productivity -- observational equivalence -- testing logic; Logic programming -- Periodicals; Logic, Symbolic and mathematical -- Periodicals; Computational complexity -- Periodicals; 005.115
• DOI: 10.1093/logcom/exv091
• Languages: English
• ISSNs: 0955-792X

Abstract

Abstract: We define notions of well-definedness and observational equivalence for programs of mixed inductive and coinductive types. These notions are defined by means of tests formulas which combine structural congruence for inductive types and modal logic for coinductive types. Tests also correspond to certain evaluation contexts. We define a program to be well-defined if it is strongly normalizing under all tests, and two programs are observationally equivalent if they satisfy the same tests. We show that observational equivalence is sufficiently coarse to ensure that least and greatest fixed point types are initial algebras and final coalgebras, respectively. This yields inductive and coinductive proof principles for reasoning about program behaviour. On the other hand, we argue that observational equivalence does not identify too many terms, by showing that tests induce a topology that, on streams, coincides with usual topology induced by the prefix metric. As one would expect, observational equivalence is, in general, undecidable, but in order to develop some practically useful heuristics we provide coinductive techniques for establishing observational normalization and observational equivalence, along with up-to techniques for enhancing these methods.