Łukasz Czajka - An operational interpretation of coinductive types

lmcs:4758 - Logical Methods in Computer Science, February 13, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:11)2020
An operational interpretation of coinductive types

Authors: Łukasz Czajka

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.

Volume: Volume 16, Issue 1
Published on: February 13, 2020
Accepted on: February 13, 2020
Submitted on: August 17, 2018
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 286 times.
This article's PDF has been downloaded 594 times.