Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi

TL;DR

This paper extends nominal techniques to define mixed inductive-coinductive data types with variable binding, enabling a nominal description of infinitary lambda-terms and capture-avoiding substitution.

Contribution

It introduces mixed binding signatures and corresponding types, extending prior work to infinitary lambda-calculi with variable binding.

Findings

Nominal description of abc-infinitary lambda-terms.

Extension of corecursion principles to mixed inductive-coinductive types.

Formalization of capture-avoiding substitution on alpha-equivalence classes.

Abstract

Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in {0,1}) and of capture-avoiding substitution on alpha-equivalence classes of such terms.