Nominal Recursors as Epi-Recursors: Extended Technical Report

TL;DR

This paper introduces a new framework for comparing nominal recursors and corecursors as epi-recursors, providing a hierarchy of their expressiveness and validating the approach with theorem proving.

Contribution

It develops an abstract framework for analyzing nominal recursors as epi-recursors and applies it to establish expressiveness hierarchies, including for corecursors.

Findings

Nominal recursors can be viewed as epi-recursors, clarifying their structure.

Expressiveness hierarchies depend on comparison strictness.

Framework validated using Isabelle/HOL theorem prover.

Abstract

We study nominal recursors from the literature on syntax with bindings and compare them with respect to expressiveness. The term "nominal" refers to the fact that these recursors operate on a syntax representation where the names of bound variables appear explicitly, as in nominal logic. We argue that nominal recursors can be viewed as epi-recursors, a concept that captures abstractly the distinction between the constructors on which one actually recurses, and other operators and properties that further underpin recursion.We develop an abstract framework for comparing epi-recursors and instantiate it to the existing nominal recursors, and also to several recursors obtained from them by cross-pollination. The resulted expressiveness hierarchies depend on how strictly we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax. We also apply our methodology to produce an expressiveness hierarchy of nominal corecursors, which are principles for defining functions targeting infinitary non-well-founded terms (which underlie lambda-calculus semantics concepts such as B\"ohm trees). Our results are validated with the Isabelle/HOL theorem prover.