From higher-order rewriting systems to higher-order categorial algebras and higher-order Curry-Howard isomorphisms

TL;DR

This work develops a comprehensive, multi-order framework relating higher-order rewriting systems to higher-order categorial algebras through Curry-Howard style isomorphisms, using towers indexed by $\mathbb{N}$ and a layered notion of morphisms. It builds foundational tools in Section 2 for many-sorted sets/algebras, subalgebras, congruences, and derivors, then extends to partial algebras in Section 3, and to zeroth-, first-, and second-order rewriting structures in Sections 1.1–1.4. The core contributions include defining first- and second-order path/Curry-Howard mappings, analyzing quotients and isomorphisms that realize Curry-Howard type correspondences, and developing a robust categorical/multilayered approach to morphisms and towers with the aim of a future category of towers. The work situates itself in relation to Hotz–Benson and Street–Burroni, contrasting semantic-syntactic and polygraphic viewpoints, and outlines a plan to formalize $\mathbb{N}$-indexed towers of higher-order structures with potential QE-variety and free-completion techniques. Overall, it provides a rigorous algebraic and categorical framework for higher-order rewriting and its Curry-Howard interpretations, setting the ground for future computational and theoretical developments in higher-order, multi-sorted settings.

Abstract

This ongoing project aims to define and investigate, from the standpoint of category theory, order theory and universal algebra, the notions of higher-order many-sorted rewriting system and of higher-order many-sorted categorial algebra and their relationships, via the higher-order Curry-Howard isomorphisms. The ultimate goal, to be developed in future versions of this work, is to define and investigate the category of towers, whose objects will consist of families, indexed by $\mathbb{N}$, of higher-order many-sorted rewriting systems and of higher-order many-sorted categorial algebras, including higher-order Curry-Howard type results for the latter, together with an additional structure that intertwines such $\mathbb{N}$-families; and whose morphism from a tower to another will be families, indexed by $\mathbb{N}$, of morphisms between its higher-order many-sorted rewriting systems and of higher-order many-sorted categorial algebras compatible with their structures. All feedback is appreciated.

Figures (110)

• Figure 1.1: Representation of the first two parts and their interrelationships.
• Figure 1.2: The tower associated to a rewriting system.
• Figure 1.3: Isomorphisms of $S$-sorted $n$-categorial $\Sigma$-algebras.
• Figure 1.4: A morphism of towers with the underlying Curry-Howard isomorphisms.
• Figure 1.5: A morphism from the tower $\mathbb{A}$ to the tower $\mathbb{B}$.

Theorems & Definitions (1443)

• Definition 2.1.1
• Definition 2.1.2
• Remark 2.1.3
• Proposition 2.1.4
• Proposition 2.1.5
• Definition 2.1.6
• Definition 2.1.7
• Definition 2.1.8
• Remark 2.1.9
• Proposition 2.1.10