Ł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
    Fundings :
      Source : OpenAIRE Research Graph
    • Infinitary Rewriting for Type Systems; Funder: European Commission; Code: 704111

    Linked data

    Source : ScholeXplorer HasVersion DOI 10.48550/arxiv.1808.05059
    • 10.48550/arxiv.1808.05059
    An operational interpretation of coinductive types
    Czajka, Łukasz ;

    Share

    Consultation statistics

    This page has been seen 300 times.
    This article's PDF has been downloaded 811 times.