English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

An operational interpretation of coinductive types