An operational interpretation of coinductive types

TL;DR

This paper develops an operational semantics for higher-order coinductive types using infinite reduction sequences, providing a refined understanding of productivity and infinite data structures in functional programming.

Contribution

It introduces a rewriting-based semantics for nested higher-order (co)inductive types, generalizing productivity notions to higher-order and nested data structures with an approximation theorem.

Findings

Proves that finite approximations lead to infinite objects in the semantics.

Establishes a type system ensuring well-defined interpretations of terms.

Provides a semantics that captures the limits of infinite reduction sequences.

Abstract

We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and generalization of the notion of productivity in term rewriting to a setting with higher-order functions and with data specified by nested higher-order inductive and coinductive definitions. Intuitively, we interpret lazy data structures in a higher-order functional language by potentially infinite terms corresponding to their complete unfoldings. We prove an approximation theorem which essentially states that if a term reduces to an arbitrarily large finite approximation of an infinite object in the interpretation of a coinductive type, then it infinitarily (i.e. in the "limit") reduces to an infinite object in the interpretation of this type. We introduce a sufficient syntactic correctness criterion, in the form of a type system, for finite terms decorated with type information. Using the approximation theorem, we show that each well-typed term has a well-defined interpretation in our semantics.