Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal P-Category Theory and Normalization by Evaluation in Rocq

David G. Berry, Marcelo P. Fiore

TL;DR

This work formalizes a Rocq library for p-category theory with subsetoid homs and applies it to normalization by evaluation (NbE) for simply typed lambda calculus, achieving a categorical proof of strong completeness and enabling extraction of normalization programs. It introduces a full universal property for the free Cartesian-closed p-category and a novel universal property for unquotiented syntax, then uses gluing in a presheaf setting to synthesize a final, sound and strongly complete normalization procedure. The results unify computation and category theory within a constructive framework and provide concrete Rocq implementations that derive long βη-normal forms, illustrating how high-level universal properties yield practical algorithms. The approach promises broader applicability to other type theories and future work on extending the framework to polymorphic or dependent systems, while deepening connections to gluing techniques in categorical semantics.

Abstract

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our work reconsiders a third approach - P-category theory - from Čubrić et al. (1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of P-category theory - where homs become subsetoids - and apply it to formalizing algorithms for normalization by evaluation which are purely categorical but, surprisingly, do not use neutral and normal terms. Čubrić et al. (1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed lambda-calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long) beta-eta-normal forms of simply typed lambda-terms together with a derivation of beta-eta-conversion.

Formal P-Category Theory and Normalization by Evaluation in Rocq

TL;DR

This work formalizes a Rocq library for p-category theory with subsetoid homs and applies it to normalization by evaluation (NbE) for simply typed lambda calculus, achieving a categorical proof of strong completeness and enabling extraction of normalization programs. It introduces a full universal property for the free Cartesian-closed p-category and a novel universal property for unquotiented syntax, then uses gluing in a presheaf setting to synthesize a final, sound and strongly complete normalization procedure. The results unify computation and category theory within a constructive framework and provide concrete Rocq implementations that derive long βη-normal forms, illustrating how high-level universal properties yield practical algorithms. The approach promises broader applicability to other type theories and future work on extending the framework to polymorphic or dependent systems, while deepening connections to gluing techniques in categorical semantics.

Abstract

Traditional category theory is typically based on set-theoretic principles and ideas, which are often non-constructive. An alternative approach to formalizing category theory is to use E-category theory, where hom sets become setoids. Our work reconsiders a third approach - P-category theory - from Čubrić et al. (1998) emphasizing a computational standpoint. We formalize in Rocq a modest library of P-category theory - where homs become subsetoids - and apply it to formalizing algorithms for normalization by evaluation which are purely categorical but, surprisingly, do not use neutral and normal terms. Čubrić et al. (1998) establish only a soundness correctness property by categorical means; here, we extend their work by providing a categorical proof also for a strong completeness property. For this we formalize the full universal property of the free Cartesian-closed category, which is not known to have been performed before. We further formalize a novel universal property of unquotiented simply typed lambda-calculus syntax and apply this to a proof of correctness of a categorical normalization by evaluation algorithm. We pair the overall mathematical development with a formalization in the Rocq proof assistant, following the principle that the formalization exists for practical computation. Indeed, it permits extraction of synthesized normalization programs that compute (long) beta-eta-normal forms of simply typed lambda-terms together with a derivation of beta-eta-conversion.
Paper Structure (33 sections, 21 theorems, 46 equations, 7 figures)

This paper contains 33 sections, 21 theorems, 46 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related Work
  4. Category Theory
  5. Normalization
  6. Organization
  7. p-Category Theory
  8. p-Sets
  9. Basic p-Categorical Definitions
  10. p-Functor Categories
  11. p-Comma Categories
  12. p-Set-Valued (Co)Ends
  13. p-Categorical Structure
  14. Finite p-Limits
  15. p-Cartesian-Closed Structure
  16. ...and 18 more sections

Key Result

Lemma 3.1.5

Comma p-categories, $(F \downarrow G)$, where $F : \mathbb{B} \rightarrow \mathbb{D}$ and $G : \mathbb{C} \rightarrow \mathbb{D}$, are p-Cartesian whenever $\mathbb{B}$, $\mathbb{C}$, $\mathbb{D}$ are Cartesian p-categories, and $G$ is a Cartesian p-functor.

Figures (7)

  • Figure 3.3.1: Lifting of Cartesian-Pre-Closure to Induced p-Functors into Comma p-Categories
  • Figure 5.2.1: Freeness Property for a Free Cartesian-Closed p-Category
  • Figure 5.2.2: Universal Property for Substα relative to Substβη
  • Figure 6.1.1: Interpretation of Substβη into its p-Category of Presheaves
  • Figure 6.1.2: Interpretation of Substβη into the p-Category of Presheaves over Substα
  • ...and 2 more figures

Theorems & Definitions (79)

  • Definition 2.1.1: PER
  • Definition 2.1.2: PType
  • Remark
  • Definition 2.2.1: PCat
  • Definition 2.2.5: IsPIso
  • Definition 2.2.6: PFun
  • Definition 2.2.7
  • Definition 2.2.9: IsPNatural
  • Definition 2.2.10: PNatTrans
  • Definition 2.3.1: p-Functor Categories
  • ...and 69 more