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 that target infinitary non-well-founded terms (known in the literature as Böhm trees). Our results are validated with the Isabelle/HOL theorem prover.

Current position: Senior Lecturer at the University of Sheffield

Ph.D. in computer science in 2010 from the University of Illinois at Urbana-Champaign

Ph.D. in mathematics in 2006 from the University of Bucharest