Source-linked AI summary
Heterogeneous substitution systems revisited
Benedikt Ahrens, Ralph Matthes
TL;DR
The paper studies how categorical structure can be added to heterogeneous substitution systems for syntax with binding, while formalizing the theory in UniMath. It organizes substitution systems into a category, extends the associated monad construction to morphisms, proves initiality results, and formalizes most of these developments. The results include substitution systems for both initial algebras and inverses of final coalgebras, with performance limitations in the formal library.
Problem
Existing heterogeneous substitution systems support syntax with binding across least and greatest fixed-point settings, but their categorical organization and formalized proofs require further development.
Method
The paper defines morphisms and a category of heterogeneous substitution systems, proves categorical and initiality properties, and formalizes the developments in UniMath using Coq.
Results
Substitution systems yield monads, the construction extends functorially to morphisms, and initial algebras produce initial substitution systems; the framework also covers inverses of final coalgebras.
Takeaways & Limitations
The framework supports categorical treatment of binding syntax across wellfounded and non-wellfounded cases, including explicit-substitution flattening as an initial morphism.
Takeaways & Limitations
The UniMath library can compile slowly because rank-2 functors generate large proof terms, and some constructions make typechecking unfeasibly slow.
Abstract
from arXiv · showhide
Matthes and Uustalu (TCS 327(1-2):155-174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.
1. Introduction
The paper extends heterogeneous substitution systems with categorical structure and formalizes the resulting mathematics in UniMath. It builds on a framework that supports both wellfounded and non-wellfounded syntax involving binding.
- Prior framework: Heterogeneous substitution systems axiomatize substitution for signatures that can include variable binding and explicit substitution.They use rank-2 functors with an explicitly added monadic unit for variables.
- Prior framework: The framework applies to both initial algebras and inverses of final coalgebras, covering wellfounded and non-wellfounded syntax.Existing examples include lambda calculus, languages with typing, and infinite terms.
- Contributions: The paper introduces morphisms of heterogeneous substitution systems, organizes them into a category, and extends monad construction functorially to those morphisms.It also proves initiality results for substitution systems obtained from initial algebras.
- Formalization: Most results are formalized in UniMath, a library of univalent mathematics implemented using the Coq proof assistant.The formalization includes the cited results and the paper’s new results, with stated exceptions.
- Contributions: A worked example expresses explicit-substitution flattening in the lambda calculus as an initial morphism of substitution systems.The paper constructs a substitution system for the extended signature on the ordinary lambda-calculus carrier.
2. Univalent mathematics
The paper develops its categorical results in univalent foundations, where equivalence principles support extensional reasoning about types, structures, and categories. It uses these foundations to define and study categories whose objects are identified up to isomorphism.
- Univalent foundations: The formal development uses intensional Martin-Löf type theory augmented by Voevodsky’s univalence axiom.The original work used purely categorical methods without specifying a mathematical foundation.
- Type theory: In this setting, dependent sums, dependent functions, products, function types, and identity types provide the basic type-theoretic constructions used by the formalization.These constructions support the dependent type theory underlying the development.
- Univalent foundations: Univalence makes constructions invariant under equivalence of types and yields extensionality principles for functions, mathematical structures, and categories.The equivalence principle is presented as the corresponding invariance of mathematical reasoning.
- Categories: A univalent category requires set-valued hom-types and an equivalence between object identity types and isomorphism types.The second condition means that isomorphic objects cannot be distinguished.
- Categories: The paper proves that its main category is univalent when the starting category is univalent, while noting that this condition is not essential for the other results.The category of sets, algebraic-structure categories, functor categories over univalent targets, and full subcategories provide examples of univalent categories.
- UniMath: UniMath supplies computer-checked mathematics in univalent foundations, with Coq used as an approximation because no prover directly implements the described foundations.The formalization relies on extensional features and restricted use of Coq’s language.
3. Preliminaries
The preliminaries introduce categories, functors, natural transformations, pointed endofunctors, algebras, and monads needed for the substitution-system development. They also make explicit the compositional and non-strict categorical structure used later.
- Notation: The notation distinguishes composition of functors and natural transformations from morphisms and type-theoretic functions, although the same arrow symbol is used in several contexts.The intended meaning is determined from context.
- Pointed functors: Pointed endofunctors pair an endofunctor with a natural transformation from the identity, and morphisms must preserve the chosen points.They form the category Ptd(C), with a forgetful functor to the endofunctor category.
- Functor categories: Composition gives the endofunctor category and pointed-functor category monoidal structures, with associativity and unit isomorphisms made explicit.The formalization does not treat these structures as strict under definitional equality.
- Algebras: An algebra for an endofunctor F consists of a carrier X and a morphism F X → X, with algebra morphisms commuting with the structure maps.This supplies the algebraic setting for substitution systems.
- Monads: A monad consists of an endofunctor, a unit natural transformation Id → T, and a multiplication natural transformation T · T → T satisfying the monad laws.The paper follows prior work in taking multiplication, rather than a binding operation, as the monad’s third component.
4. Generalized Iteration in Mendler-style and fusion law
The section presents generalized iteration in Mendler-style together with a fusion law used later to construct substitution systems from initial algebras. The fusion law combines two stages of calculation into one iteration.
- Generalized iteration in Mendler-style: Generalized iteration in Mendler-style yields a unique morphism from the initial algebra, given an adjunction and a suitable natural transformation.The formulation assumes an initial algebra (µF, in), an adjunction L ⊣ R, an object X, and a natural transformation Ψ.
- Generalized iteration in Mendler-style: The displayed iterator equation specifies the unique morphism characterized by the commuting diagram.The paper notes that the functors in Ψ’s type are, strictly speaking, opposites of L and F.
- Generalized iteration in Mendler-style: The right adjoint is a technical convenience that can instead be replaced by preservation conditions for chains, colimits, and initiality.The paper does not pursue this alternative in its formalization.
- Generalized iteration in Mendler-style: The paper uses a more general Mendler-style formulation even though Sections 7 and 8 require only its generalized-fold specialization.The broader formulation makes the subsequent fusion law more natural, especially because morphisms of substitution systems are considered.
- Fusion law: The fusion law relates two iterator applications by fusing the subsequent calculation of ΦµF with the iteration over µF into one iteration.Its generalized form permits the objects X and X′ to be chosen separately; the paper uses the generalized-fold instance later.
5. The category of heterogeneous substitution systems
This section makes signatures explicit, defines heterogeneous substitution systems and their morphisms, and organizes them into a category. It then establishes that this category is replete and univalent when the base category is univalent.
- Signatures: A signature consists of an endofunctor H on [C,C] and a natural transformation θ relating H applied before and after composition with the underlying functor of a pointed endofunctor.The definition is adapted to non-strict monoidal structures on endofunctors.
- Signatures: The signature notion is modular: constructing signatures from arities corresponds to taking an amalgamated sum, and it includes explicit-flattening arities beyond polynomial signatures.The framework assumes specified coproducts from Convention 11, although the abstract signature definition itself does not require them.
- Heterogeneous substitution systems: A heterogeneous substitution system is an (Id + H)-algebra equipped with a unique bracket operation assigning each pointed morphism into the carrier a compatible morphism T · Z → T.The carrier is the functor T; the bracket is treated operationally rather than through a universal property, which is important for obtaining a monad.
- Category structure: A morphism of substitution systems is an algebra morphism whose natural transformation also commutes with the bracket operations on both sides.Compatibility with substitution is a proposition on algebra morphisms, and the category can be represented as a subcategory of (Id + H)-algebras.
- Properties: The category hss(H, θ) is a replete subcategory of (Id + H)-algebras and is univalent whenever the base category C is univalent.The univalence result follows from closure under functor categories, algebra categories, and replete subcategories.
6. From substitution systems to monads
The section recalls that every heterogeneous substitution system induces a monad, then extends this construction from objects to morphisms. The resulting functor is faithful but not full.
- Monad construction: Every (Id + H)-algebra that forms a heterogeneous substitution system induces a monad with carrier T and multiplication given by the bracket at the identity.This is the principal monad-construction result recalled from Matthes and Uustalu.
- Functorial extension: The assignment from heterogeneous substitution systems to monads extends to a functor hss(H, θ) → Mon(C).A substitution-system morphism preserves the monad multiplication because it is compatible with the bracket operations.
- Faithfulness and fullness: The functor is not full because monad morphism axioms constrain mappings at variables, not compatibility with the inner nodes of expressions.A concrete initial-system example gives a monad morphism that is not a substitution-system morphism.
- Faithfulness and fullness: The resulting functor is faithful: parallel morphisms are determined by their underlying natural transformations.The proof reduces equality of monad morphisms and substitution-system morphisms to equality of their underlying transformations.
7. Lifting initiality through a fusion law
The paper uses generalized iteration in Mendler-style to construct substitution systems from initial algebras, then uses a fusion law to prove that the constructed system is itself initial.
- Construction: Under suitable conditions, an initial (Id + H)-algebra yields a substitution system via generalized iteration in Mendler-style.The construction assumes an initial algebra and right adjoints for reduction functors −·Z.
- Generalized iteration: The method abstracts a morphism problem from the fixed point µF to an arbitrary parameter X and extends solutions naturally from X to FX.Naturality lets the iteration lemma provide a unique solution at the least fixed point.
- Generalized iteration: Mendler-style iteration supplies the general scheme, while the paper specializes it using an algebra structure on the target to guide the required natural transformation.The specialization is identified with a form of generalized iteration from Matthes and Uustalu.
- Fusion proof: The constructed bracket operation is defined through the transformation Ψf and the fusion law, whose defining equations establish compatibility with substitution operations.The proof compares both sides of the required compatibility equation by identifying them with an iterator.
- Initiality: The resulting substitution system is initial in the category hss(H, θ) of heterogeneous substitution systems.This extends the earlier construction by establishing initiality, not merely existence of a substitution system.
8. A worked example: flattening of explicit substitution
The worked example combines application, abstraction, and explicit-flattening signatures to represent λ-calculus with explicit flattening, then maps that syntax into ordinary λ-terms.
- Signature construction: The example combines application, abstraction, and explicit-flattening arities into signatures Λ and Λµ.Λ represents λ-calculus, while Λµ extends it with explicit flattening.
- Abstraction: Abstraction uses option(X) := 1 + X to model context extension by one distinguished element, with a strength implementing the lifting needed for de Bruijn substitution.The strength maps terms over X(1 + ZA) to terms over X(Z(1 + A)).
- Explicit flattening: Explicit flattening is represented by the self-composition signature HFlatten(T) := T · T, with the pointed functor unit inserted into the strength.This signature captures a nested datatype pattern not expressible with a fixed enumeration of variable names.
- Representation on Lam: The carrier Lam is equipped with an Id + Λµ-algebra by adding a natural transformation µLam : HFlatten(Lam) → Lam to the ordinary λ-calculus algebra.The resulting algebra satisfies the substitution-system compatibility requirements.
- Evaluation: Initiality yields a morphism from Lamµ to Lam that maps the explicit flattening constructor to ordinary substitution or its flattened-term evaluation.The morphism also induces a monad morphism through functoriality of the monad construction.
9. About the formalization
The formalization packages most results in UniMath and documents their organization, size, and performance trade-offs. Transparent constructions support manageable proofs, but large proof terms make compilation costly.
- About the formalization: Most results are formalized in UniMath, except Theorem 20 and Lemmas 23 and 19.
- About the formalization: The SubstitutionSystems package is organized into files corresponding roughly to the article’s sections and includes a summary interface for important formalized theorems.
- Statistics: The library contains a bit more than 4400 lines of code plus 600 lines of comments, compared with about 37000 lines for all of UniMath at the same commit.
- Statistics: Definitional equality makes pointwise functor-category constructions compute directly, which was crucial for keeping proof complexity manageable.
- Statistics: The formalization keeps many category-theoretic constructions transparent, using Defined instead of Qed in Coq.
- About performance: transparency vs. opacity: Opacification reduces machine costs but is feasible only for small subproofs when implemented with abstract blocks.
- About performance: transparency vs. opacity: The library compiles slowly because rank 2 functors generate large proof terms, and some Qed commands take a long time to check.
- About performance: transparency vs. opacity: Manual lifting of products and coproducts into functor categories was used because the general colimit construction made typechecking unfeasibly slow.
10. Conclusions
The paper formalizes new results on heterogeneous substitution systems in a univalent foundation and derives initial substitution systems from initial algebras using generalized Mendler-style iteration. It also identifies initial-algebra construction in univalent foundations as future work.
- The paper presents new results about heterogeneous substitution systems in a univalent foundation.
- Initial substitution systems, including lambda calculi, can be obtained from initial algebras using generalized iteration in Mendler-style.
- The construction of initial algebras in univalent foundations remains for forthcoming work.