Nominal Recursors as Epi-Recursors

on YouTube ↗21m

" summary

Identifies nominal recursion schemes as instances of an abstract epi-recursors pattern and builds a categorical framework that compares expressiveness by extending constructor algebras with auxiliary operators (permutations, freshness, renaming, substitution). Instantiates the framework to existing nominal recursors, creates new mixed variants by cross‑pollination, produces hierarchies for recursion and corecursion over alpha‑quotiented syntax, and validates all results mechanized in Isabelle/HOL with reusable artifacts.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 3:16Nominal Lambda calculus syntax
3. 6:49Free variable counting in Lambda terms
4. 9:39Recursion on pre-terms vs Alpha-equivalent terms
5. 12:54Extending standard recursion
6. 14:01Nominal recursors as Epi-Recursors
7. 15:48Summary
8. 16:30Q&A: Quotient Inductive Types
9. 17:52Q&A: Category-theoretic view
10. 19:14Q&A: Proof assistant use