Well-definedness and observational equivalence for inductive-coinductive programs

Well-definedness and observational equivalence for inductive-coinductive programs

Basold, Henning (Radboud Universiteit Nijmegen)
Hansen, H.H. (TU Delft Energie and Industrie)

2019

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.

coinductive types
Inductive types
observational equivalence
productivity
termination
testing logic

http://resolver.tudelft.nl/uuid:d03656f1-6eb9-4d33-b91a-67187f3559c1

https://doi.org/10.1093/logcom/exv091

2020-08-01

0955-792X

Journal of Logic and Computation, 29 (4), 419-468

Institutional Repository

journal article

© 2019 Henning Basold, H.H. Hansen