Ł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 typesArticle

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: October 25, 2019
    Submitted on: August 17, 2018
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Infinitary Rewriting for Type Systems; Funder: European Commission; Code: 704111

    Consultation statistics

    This page has been seen 1002 times.
    This article's PDF has been downloaded 1045 times.