Formal P-Category Theory and Normalization by Evaluation in Rocq
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910938936901632 |
|---|---|
| author | Berry, David G. Fiore, Marcelo P. |
| author_facet | Berry, David G. Fiore, Marcelo P. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_07780 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal P-Category Theory and Normalization by Evaluation in Rocq Berry, David G. Fiore, Marcelo P. Logic in Computer Science Category Theory 03B40, 03B38, 68N18 F.3.2; F.4.1 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. |
| title | Formal P-Category Theory and Normalization by Evaluation in Rocq |
| topic | Logic in Computer Science Category Theory 03B40, 03B38, 68N18 F.3.2; F.4.1 |
| url | https://arxiv.org/abs/2505.07780 |