Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Abstract clones for abstract syntax

Nathanael Arkor, Dylan McDermott

TL;DR

This work develops a syntax-independent framework for simple type theories by using multisorted second-order abstract clones and their algebras. It introduces second-order presentations to encode binding operations like $\mathsf{abs}$ and $\mathsf{app}$, constructs free algebras to capture the syntax modulo $β$-$η$-equality, and derives an induction principle that supports rigorous proofs via logical relations, including adequacy and normalization results. The approach accommodates STLC and even STLC with global state by forming appropriate free algebras (e.g., on $\mathbf{GS}_{V}$), while avoiding the complexities of presheaf-based semantics. Overall, cloning-theoretic methods provide a streamlined, syntax-driven foundation that connects to existing categorical frameworks (presheaves, cartesian multicategories, algebraic theories) and highlights their applicability to simple type theories.

Abstract

We give a formal treatment of simple type theories, such as the simply-typed $λ$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $λ$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $β$- and $η$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.

Abstract clones for abstract syntax

TL;DR

This work develops a syntax-independent framework for simple type theories by using multisorted second-order abstract clones and their algebras. It introduces second-order presentations to encode binding operations like and , constructs free algebras to capture the syntax modulo --equality, and derives an induction principle that supports rigorous proofs via logical relations, including adequacy and normalization results. The approach accommodates STLC and even STLC with global state by forming appropriate free algebras (e.g., on ), while avoiding the complexities of presheaf-based semantics. Overall, cloning-theoretic methods provide a streamlined, syntax-driven foundation that connects to existing categorical frameworks (presheaves, cartesian multicategories, algebraic theories) and highlights their applicability to simple type theories.

Abstract

We give a formal treatment of simple type theories, such as the simply-typed -calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed -calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as - and -equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.

Paper Structure

This paper contains 14 sections, 7 theorems, 35 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Abstract clones and first-order presentations
  3. Substitution and context extension
  4. First-order presentations
  5. Second-order presentations
  6. Algebras
  7. Free algebras
  8. Induction over second-order syntax
  9. Logical relations
  10. Closed terms and adequacy
  11. Open terms and normalization
  12. Comparison to other approaches
  13. Conclusion
  14. Normalization with global state

Key Result

Lemma 8

For each clone homomorphism $f : \mathbf{X} \to \mathbf{Y}$ and substitution $\boldsymbol\sigma \in Y(\diamond; \Xi)$, there is a unique homomorphism $g : {\Uparrow^{\Xi}} \mathbf{X} \to \mathbf{Y}$ such that $g \circ \mathsf{weaken}^{\IfNoValueF{\Xi}{(\Xi)}}_{\mathbf{X}} = f$ and $g_{\diamond; \Xi}

Figures (1)

  • Figure 1: Construction of the free $(\Sigma, E)$-algebra on a clone $\mathbf{X} = (X, \mathsf{var}^{\IfNoValueF{-NoValue-}{(-NoValue-)}}, \mathsf{subst}_{})$.

Theorems & Definitions (29)

  • Definition 2
  • Example 3
  • Example 4
  • Example 5
  • Remark 6
  • Remark 7
  • Lemma 8
  • Definition 9
  • Remark 10
  • Definition 11
  • ...and 19 more