Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Rémy Cerda

TL;DR

This work extends nominal techniques to mixed inductive-coinductive data types with binding, enabling α-equivalence and capture-avoiding substitution on infinitary-term classes. It introduces mixed binding signatures, defines the corresponding bifunctor $\mathcal{F}_{\Sigma}(X,Y)$ and quotient $\mathcal{Q}_{\Sigma}$, and develops metric completion and nominal coalgebra foundations, demonstrating that mixed terms yield canonical coalgebras for both raw and α-equivalence classes. The paper also provides a Moss-corecursive substitution framework, with explicit rules for abc-infinitary lambda-terms and a detailed instance for $\Lambda^{001}_{ffv}/=_\alpha$. Collectively, these results establish a principled, canonical approach to binding, equivalence, and substitution in mixed infinitary term calculi, enabling rigorous formalization and potential tooling for infinitary lambda-calculi with binding.

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.

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

TL;DR

This work extends nominal techniques to mixed inductive-coinductive data types with binding, enabling α-equivalence and capture-avoiding substitution on infinitary-term classes. It introduces mixed binding signatures, defines the corresponding bifunctor and quotient , and develops metric completion and nominal coalgebra foundations, demonstrating that mixed terms yield canonical coalgebras for both raw and α-equivalence classes. The paper also provides a Moss-corecursive substitution framework, with explicit rules for abc-infinitary lambda-terms and a detailed instance for . Collectively, these results establish a principled, canonical approach to binding, equivalence, and substitution in mixed infinitary term calculi, enabling rigorous formalization and potential tooling for infinitary lambda-calculi with binding.

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.

Paper Structure

This paper contains 10 sections, 7 theorems, 20 equations, 2 figures.

Table of Contents

  1. Mixed binding signatures and mixed terms
  2. Nominal preliminaries
  3. Categorical preliminaries
  4. mbs and raw terms
  5. Metric completion
  6. α-equivalence
  7. Towards commutation (or not)
  8. The nominal coalgebra of α-equivalence classes of mixed terms
  9. Nominal mixed types
  10. Capture-avoiding substitution for mixed types

Key Result

Lemma 1

Given an $\omega$-cocontinuous functor $F : \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C}$, in the category of $F \Delta$-algebras, where $\Delta : X \mapsto (X,X)$ is the diagonal functor.

Figures (2)

  • Figure 1: Formal system defining $\mathcal{T}_{ \Sigma }^{\infty}$ for a mbs$(\Sigma, \mathsf{ar} )$. The simple rules are inductive, the double one is coinductive; for similar systems, see DalLago16CerdaVaux23.
  • Figure 2: A simplified mixed formal system defining $\Lambda^{ 001 }$.

Theorems & Definitions (19)

  • Lemma 1: diagonal identity
  • Definition 2: mixed binding signature
  • Definition 3: term functor of a mbs
  • Definition 4: raw terms on a mbs
  • Example 6: mixed infinitary λ-terms
  • Definition 7: truncation
  • Definition 8: Arnold-Nivat metric
  • Lemma 9
  • Example 10
  • Definition 11: quotient term functor of a mbs
  • ...and 9 more