Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

van Brügge, Jan; Popescu, Andrei; Traytel, Dmitriy

doi:10.4230/LIPIcs.ITP.2025.11

Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

Jan van Brügge

Heriot-Watt University, Edinburgh, UK Andrei Popescu

University of Sheffield, UK Dmitriy Traytel

University of Copenhagen, Denmark

Abstract

Nominal Isabelle provides powerful tools for meta-theoretic reasoning about syntax of logics or programming languages, in which variables are bound. It has been instrumental to major verification successes, such as Gödel’s incompleteness theorems. However, the existing tooling is not compositional. In particular, it does not support nested recursion, linear binding patterns, or infinitely branching syntax. These limitations are fundamental in the way nominal datatypes and functions on them are constructed within Nominal Isabelle. Taking advantage of recent theoretical advancements that overcome these limitations through a modular approach using the concept of map-restricted bounded natural functor (MRBNF), we develop and implement a new definitional package for binding-aware datatypes in Isabelle/HOL, called MrBNF. We describe the journey from the user specification to the end-product types, constants and theorems the tool generates. We validate MrBNF in two formalization case studies that so far were out of reach of nominal approaches: (1) Mazza’s isomorphism between the finitary and the infinitary affine $\lambda$ -calculus, and (2) the POPLmark 2B challenge, which involves non-free binders for linear pattern matching.

Keywords and phrases:

syntax with bindings, datatypes, inductive predicates, Isabelle/HOL

Funding:

Andrei Popescu: Acknowledges support from the EPSRC grants EP/V039156/1 (Security of Digital Twins in Manufacturing) and and EP/X015114/1 Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT).

Dmitriy Traytel: Acknowledges support from the Novo Nordisk Foundation (start package grant NNF20OC0063462) and the Independent Research Fund Denmark (Sapere Aude grant 3120-00057B, titled DISCOVER: Distributed Streaming Computations Verified).

Copyright and License:

2012 ACM Subject Classification:

Security and privacy

\rightarrow

Logic and verification

Supplementary Material:

Software: https://doi.org/10.5281/zenodo.15756655

Acknowledgements:

We thank the ITP reviewers for their insightful comments. Martin Elsman challenged MrBNF with advanced syntaxes, which overall resulted in our tool becoming more robust. The authors are listed alphabetically regardless of individual contributions or seniority.

DOI:

10.4230/LIPIcs.ITP.2025.11

Event:

16th International Conference on Interactive Theorem Proving (ITP 2025)

Editors:

Yannick Forster and Chantal Keller

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Most programming languages involve variable-binding constructs, or simply binders, such as the lambda abstraction or the recursive and non-recursive let operators. For the study of these languages’ metatheory, the specific choice of bound variable names in a language expression is immaterial. For example, it is customary to treat the lambda calculus expressions $\lambda x.\;x$ and $\lambda y.\;y$ as being syntactically equal and to choose bound variables in a way that avoids name clashes with surrounding free variables – this is known as Barendregt’s variable convention [6].

The mechanization of programming language metatheory in proof assistants struggles to keep up with this informal convention. The POPLmark challenge [4] initiated a flurry of approaches to mechanized binders, each with its own strengths and weaknesses (§2). The used approaches can be categorized into three main paradigms: (1) the nameless representation that replaces bound variables in terms with pointers to the binding position [17, 23]; (2) the nameful or nominal representation that includes bound variable names but identifies terms modulo alpha-equivalence, i.e., up to bound variable renaming [18]; and (3) the reductive representation that embeds the programming language’s binders into the metalogic’s binders [19, 30, 28].

The nominal representation faithfully encodes Barendregt’s variable convention in that the accompanying reasoning principles (e.g., nominal induction) allow their users to assume that bound variables do not clash with surrounding free variables whenever bound variables are introduced. Nominal Isabelle [21] implements the nominal representation in the Isabelle/HOL proof assistant with successful applications ranging from Gödel’s incompleteness theorems [29] to verifying the correctness of Haskell’s compiler optimizations [13] and the security of authenticated data structures [14]. All these developments use the expected binder constructs: lambda abstractions, existential quantifiers, and (parallel) recursive let constructs.

Nominal Isabelle is fundamentally restricted to syntaxes with finite support, i.e., expressions may only contain finitely many free and bound variables. This rules out applications like Mazza’s infinitary affine lambda calculus [22]. Moreover, nested recursion, which e.g., is needed to model function applications to multiple arguments, is not directly supported. Sometimes this limitation can be overcome by using mutual recursion instead, but this workaround is limited to cases where the nesting type is a datatype itself. Nesting through coinductive datatypes such as streams or lazy lists or non-free structures such as finite or countable sets remains problematic. Also nominal datatypes, even in their flexible variant provided by Nominal 2 [42], cannot directly incorporate linear patterns, which are required in most of the complex binder structures including those of POPLmark 2B.

Blanchette et al. [10] have proposed map-restricted bounded natural functors (MRBNFs) as a new modular foundation for binding-aware datatypes that overcomes the above limitations. MRBNFs generalize bounded natural functors (BNFs) [41], which underly Isabelle’s datatypes and codatatypes [11]. In this paper, we present the journey from the theoretical MRBNF framework to a practical package in Isabelle/HOL, called MrBNF (pronounced “Mister BNF”).

MrBNF’s heart is the binder_datatype command for declaring binding-aware datatypes. Behind the scenes, the command composes and takes least fixed points of MRBNFs, defines the new type as the quotient of a raw nameful datatype by alpha-equivalence, lifts the raw constructors to the quotient, and proves nominal induction principles as well as a wealth of constructor properties (§3). The command also provides a nominal recursor infrastructure, which is crucial for defining recursive functions. All constructions are carried out foundationally in Isabelle/HOL: no axioms have been introduced (§4). Our main contributions are twofold:

$\blacksquare$

We extend Isabelle/HOL with a foundational package for defining binding-aware datatypes that supports nested recursion, complex inductive binders, and types that may have infinitely many free or bound variables. This involves proving that MRBNFs, the key notion underlying our approach, are closed under composition and least fixed points. We design and automate these mechanized proofs as Isabelle/ML tactics. Our implementation includes a user-friendly proof method for applying the nominal induction principles and a nominal recursor for defining binding-aware primitive recursive functions on datatypes with binders.
$\blacksquare$

Two case studies illustrate our tool’s usefulness. First, we prove Mazza’s result [22] that the $\lambda$ -calculus is isomorphic to an infinitary affine $\lambda$ -calculus (§5). Second, we formalize the POPLmark challenge [4], i.e., type soundness of System F_<:, including parts 1B and 2B, which extend the language with records and pattern matching (§6). To the best of our knowledge, this is the first formalization of these extensions using a nominal approach.

Our implementation and case studies are publicly available [44].

2 Related Work

We refer to Blanchette et al. [10, Section 9] for a broad overview of syntax with bindings approaches in programming languages and proof assistants. Here, we focus our attention on how these approaches manifest themselves in proof assistants and discuss strength and weaknesses.

The representation of variables as de Bruijn indices [17] is widely popular in proof assistants [8, 45, 37, 20, 16, 35, 40, 25] because it is readily available via standard datatypes. Thereby bound variables point to the respective binders using a simple indexing scheme: a number indicates how many binders to skip when traversing the syntax tree towards its root. Binders such as $\lambda$ -abstractions do not need to mention the bound variable. Free variables are numbers, too, namely those larger than the number of binders above them. For example, $\mathsf{{Lm}}\;(\mathsf{{Lm}}\;(\mathsf{{Ap}}\;(\mathsf{{Ap}}\;1\;0)\;2))$ is the de Bruijn version of the $\lambda$ -calculus term $\lambda x.\;\lambda y.\;((y\;x)\;z)$ . Working with indices frequently requires shifting when a term is moved under a binder, e.g., during substitution. Good automation as provided by Autosubst in Coq [36, 39] can eliminate much of the tedium of index shifting. Nonetheless the internal representation occasionally leaks: index shifts may pop up in induction proofs and sometimes even lemma statements.

The related locally nameless representation [15, 33] combines de Bruijn indices for bound variables with the named representation for free variables, which allows to use readable names for the free variables. Locally nameless replaces shifting by opening terms such that bound variables are turned into free ones. One downside of the locally nameless approach is that terms with loose bounds are malformed and need to be ruled out using a predicate (or a subtype).

Nominal Logic [18] provides a nameful alternative to the two above approaches: binders carry explicit bound variable names, but the syntax is quotiented by a notion of alpha-equivalence which makes the name choice immaterial. Still the explicit mention of the bound meta-variable in the binders allows us to refer to it explicitly and choose it to avoid other surrounding variables, which enforces Barendregt’s variable convention. Nominal Isabelle is the Isabelle/HOL implementation of nominal logic [21, 42], which has been used in several substantial formalizations efforts [7, 29, 14, 13]. Our contribution follows the nominal approach, while generalizing the support for nested recursion and allowing infinitely many variables in terms.

Higher-order abstract syntax (HOAS) [30] uses binding primitives available in the meta-logic to represent binders of the object of study. For example, abstraction in the $\lambda$ -calculus becomes $\mathsf{{Lm}}:(\text{var}\rightarrow\text{term})\rightarrow\text{term}$ under weak HOAS and $\mathsf{{Lm}}:(\text{term}\rightarrow\text{term})\rightarrow\text{term}$ under HOAS, reusing the $\lambda$ -abstraction available in the language when writing specific lambda terms, e.g., $\mathsf{{Lm}}\;(\lambda x.\;\mathsf{{Lm}}\;(\lambda y.\;\mathsf{{Ap}}\;(% \mathsf{{Ap}}\;y\;x)\;(\mathsf{{Vr}}\;z)))$ . A challenge with (weak) HOAS are so-called exotic terms, i.e., terms that do not constitute valid $\lambda$ -calculus terms because they observe aspects of the meta-language that the object language should not see. HOAS is popular in logical frameworks pioneered by Twelf [31] and refined and extended in Beluga [32] and Abella [5].

Berghofer and Urban [9] provide a detailed comparison between the de Bruijn and nominal approaches; Momigliano et al. [24] perform a similar exercise for de Bruijn and (weak) HOAS. Ambal et al. [2] compare all above approaches in the context of a higher-order $\pi$ -calculus. Norrish and Vestergaard [27] establish a formal connection between de Bruijn and nominal terms.

Solutions using different above techniques [1] target the POPLmark challenge [4]. However, only four cover all proof-related parts, in particular including complex binders for linear pattern matching: three using de Bruijn indices in Isabelle [8] and Coq [45, 38] and one using HOAS in Twelf [3]. We provide the first complete solution following the nominal approach.

3 MrBNF in Action

As users, what do we want to be the effect of specifying a datatype with bindings, such as those of $\lambda$ - or $\pi$ -calculus syntax? We want the following: (1) a type capturing the syntax fully abstractly, i.e., not distinguishing between alpha-equivalent terms and not including “junk”, i.e., invalid terms; (2) constants corresponding to the syntactic constructors and other syntactic operators such as renaming and free-variables; (3) propositions describing the basic properties of non-binding constructors), and quasi-injectivity for the binder constructors; (4) propositions describing the basic properties concerning the interaction of constructors and the renaming and free-variable operators; (5) a proposition stating a binding-aware structural induction principle; and (6) a proposition stating the characteristic equations of a binding-aware structural recursion principle.

Importantly, we would not care how such a type and constants have been defined internally, because (a subset of) the above properties characterize the type uniquely up to an isomorphism. This ensures that these internal definitions, however they proceed, give us the correct result.

In the remainder of this section, using a sequence of increasingly sophisticated syntaxes with bindings we will illustrate how our MrBNF definitional package achieves these goals.

3.1 Preliminaries on cardinals and permutations

Isabelle has a well-developed theory of ordinals and cardinals [12]. In a nutshell: an ordinal is just a well-order, while a cardinal is an ordinal that is minimal under the preorder relation $\leq_{o}$ on ordinals defined as follows: $r\leq_{o}r^{\prime}$ iff there exists a well-order embedding between $r$ and $r^{\prime}$ ; we also write $<_{o}$ for the strict counterpart of this preorder, and also $=_{o}$ for its induced equivalence relation. Given any set $A:{{}^{\prime}a}\;\text{set}$ , we define $|A|$ to be its cardinality; technically, this is a (necessarily unique up to an order isomorphism) choice of a cardinal on ${}^{\prime}a$ whose domain is $A$ and that forms a well-order on $A$ . Instead of $|\mathsf{{UNIV}}:{{}^{\prime}a\;\text{set}}|$ , the cardinality of the set of all elements of type ${}^{\prime}a$ , we will simply write $|^{\prime}a|$ , and refer to it as the cardinality of the type ${}^{\prime}a$ .

For a function $\sigma:{{}^{\prime}a}\rightarrow{{}^{\prime}a}$ , we write $\mathsf{{supp}}\;\sigma$ for its support, defined as the set of elements that $\sigma$ modifies, $\{x\mid\sigma\;x\not=x\}$ . We call permutation any such function that (1) is bijective and (2) has the cardinality of its support strictly smaller than that of its underlying type. Formally, the (polymorphic) predicate $\mathsf{{perm}}:({{}^{\prime}a}\rightarrow{{}^{\prime}a})\rightarrow\text{bool}$ reflects this as $\mathsf{{perm}}\;\sigma\,\longleftrightarrow\,\mathsf{bij}\;\sigma\;\wedge\;|% \mathsf{{supp}}\;\sigma|<_{o}|^{\prime}a|$ . When ${}^{\prime}a$ is countably infinite, being a permutation amounts to being a bijection of finite support, so this generalizes the standard nominal logic assumption. We let $\sigma$ range over permutations and write $\sigma^{-1}$ for the inverse of $\sigma$ . We let $a\!\leftrightarrow\!b$ denote the swapping permutation, which takes $a$ to $b$ , takes $b$ to $a$ , and leaves everything else unchanged.

3.2 $\lambda$ -calculus terms

Let us start with the paradigmatic example of syntax with bindings, that of untyped $\lambda$ -calculus. Using our package, this can be declared as the following datatype lterm of $\lambda$ -terms, which is polymorphic in the type of variables, i.e., depends on the Isabelle type-variable ${}^{\prime}\mathit{var}$ :

⬇

binder_datatype ’var lterm = Vr ’var | Ap "’var lterm" "’var lterm"

| Lm x::’var t::"’var lterm" binds x in t

When using the type ${}^{\prime}\mathit{var}\;\text{{lterm\>}}$ , we will always implicitly assume that ${}^{\prime}\mathit{var}$ has at least countably infinite cardinality. (This is achieved in practice via a type class $\mathsf{large}_{\text{{lterm\>}}}$ , i.e., being “large enough”, which means having cardinality at least as large as $\mathsf{bound}_{\text{{lterm\>}}}$ , and $\mathsf{bound}_{\text{{lterm\>}}}$ is a cardinal bound specific to each datatype – here, for lterm , it is a countable cardinal, i.e., $\mathsf{bound}_{\text{{lterm\>}}}=\aleph_{0}$ , so smallness means “at least countably infinite” – see §4 for more details.)

The command produces the following constants, all polymorphic in ${}^{\prime}\mathit{var}$ :

$\blacksquare$

the constructors $\mathsf{{Vr}}:{{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}\;% \text{{lterm\>}}$ , $\mathsf{{Ap}}:{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow{{}^{% \prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow{{}^{\prime}\mathit{var}}\;% \text{{lterm\>}}$ and $\mathsf{{Lm}}:{{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}\;% \text{{lterm\>}}\rightarrow{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}$ ;
$\blacksquare$

the free-variable operator $\mathsf{{FV}}_{\text{{lterm\>}}}:{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}% \rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ ;
$\blacksquare$

the permutation operator $\mathsf{{PERM}}_{\text{{lterm\>}}}:({{}^{\prime}\mathit{var}}\rightarrow{{}^{% \prime}\mathit{var}})\rightarrow{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}% \rightarrow{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}$ , where we write $t[\sigma]_{\text{{lterm\>}}}$ instead of $\mathsf{{PERM}}_{\text{{lterm\>}}}\;\sigma\;t$ ;
$\blacksquare$

a cardinal bound, $\mathsf{bound}_{\text{{lterm\>}}}$ (which, as explained above, in this case it is $\aleph_{0}$ );

\blacksquare

a binding-aware recursion combinator

\begin{array}[]{@{}rcll@{}}\mathsf{{rec}}_{\text{{lterm\>}}}&:&(({{}^{\prime}% \mathit{var}}\rightarrow{{}^{\prime}\mathit{var}})\rightarrow({{}^{\prime}p}% \rightarrow{{}^{\prime}p}))\;\rightarrow&({{}^{\prime}p}\rightarrow{{}^{\prime% }\mathit{var}}\;\text{set})\;\rightarrow\\ &&(({{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}})\rightarrow(% {{}^{\prime}a}\rightarrow{{}^{\prime}a}))\;\rightarrow&({{}^{\prime}a}% \rightarrow{{}^{\prime}\mathit{var}}\;\text{set})\;\rightarrow\\ &&({{}^{\prime}\mathit{var}}\rightarrow({{}^{\prime}p}\rightarrow{{}^{\prime}a% }))\;\rightarrow\\ &&\lx@intercol(({{}^{\prime}p}\rightarrow{{}^{\prime}a})\rightarrow({{}^{% \prime}p}\rightarrow{{}^{\prime}a})\rightarrow({{}^{\prime}p}\rightarrow{{}^{% \prime}a}))\;\rightarrow\hfil\lx@intercol\\ &&\lx@intercol({{}^{\prime}\mathit{var}}\rightarrow({{}^{\prime}p}\rightarrow{% {}^{\prime}a})\rightarrow({{}^{\prime}p}\rightarrow{{}^{\prime}a}))\;% \rightarrow\hfil\lx@intercol\\ &&{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow({{}^{\prime}p}% \rightarrow{{}^{\prime}a})\;.\end{array}

We write $\mathsf{{FV}}$ and $\_[\_]$ instead of $\mathsf{{FV}}_{\text{{lterm\>}}}$ and $\_[\_]_{\text{{lterm\>}}}$ (and similarly for other examples).

The following properties are generated (stated and proved) by our command:

Prop 1.

(I)

Distinctness and (quasi-)injectivity of the constructors:
(1) $\mathsf{{Vr}}\;x\not=\mathsf{{Ap}}\;t_{1}\;t_{2}$ ; (2) $\mathsf{{Vr}}\;x\not=\mathsf{{Lm}}\;x^{\prime}\;t$ ; (3) $\mathsf{{Ap}}\;t_{1}\;t_{2}\not=\mathsf{{Lm}}\;x\;t$ ;
(4) $\mathsf{{Vr}}\;x=\mathsf{{Vr}}\;x^{\prime}\,\longleftrightarrow\,x=x^{\prime}$ ; (5) $\mathsf{{Ap}}\;t_{1}\;t_{2}=\mathsf{{Ap}}\;t_{1}^{\prime}\;t_{2}^{\prime}\,% \longleftrightarrow\,t_{1}=t_{1}^{\prime}\wedge t_{2}=t_{2}^{\prime}$ ;
(6) $\mathsf{{Lm}}\;x\;t=\mathsf{{Lm}}\;x^{\prime}\;t^{\prime}\,\longleftrightarrow% \,(x^{\prime}\notin\mathsf{{FV}}\;t\lor x=x^{\prime})\land t=t^{\prime}[x\!% \leftrightarrow\!x^{\prime}]$ ;
(II)

Equivariance of the constructors:
(1) $\mathsf{{perm}}\;\sigma\longrightarrow(\mathsf{{Vr}}\;x)[\sigma]=\mathsf{{Vr}}% \,(\sigma\;x)$ ; (2) $\mathsf{{perm}}\;\sigma\longrightarrow(\mathsf{{Ap}}\;t_{1}\;t_{2})[\sigma]=% \mathsf{{Ap}}\;(t_{1}[\sigma])\;(t_{2}[\sigma])$ ;
(3) $\mathsf{{perm}}\;\sigma\longrightarrow(\mathsf{{Lm}}\;x\;t)[\sigma]=\mathsf{{% Lm}}\,(\sigma\;x)\,(t[\sigma])$ ;
(III)

Smallness (here, equivalently, finiteness) of the set of free variables:
(1) $|\mathsf{{FV}}\;t|<_{o}\mathsf{bound}_{\text{{lterm\>}}}$ ;
(IV)

Interaction between free variables and constructors:
(1) $\mathsf{{FV}}\,(\mathsf{{Vr}}\;x)=\{x\}$ ; (2) $\mathsf{{FV}}\,(\mathsf{{Ap}}\;t_{1}\;t_{2})=\mathsf{{FV}}\;t_{1}\cup\mathsf{{% FV}}\;t_{2}$ ; (3) $\mathsf{{FV}}\,(\mathsf{{Lm}}\;x\;t)=\mathsf{{FV}}\;t\,\smallsetminus\,\{x\}$ .
(V)

Permutation identity and compositionality:
(1) $t[\mathsf{{id}}]=t$ ; (2) $\mathsf{{perm}}\;\sigma\wedge\mathsf{{perm}}\;\sigma^{\prime}\longrightarrow t% [\sigma][\sigma^{\prime}]=t[\sigma^{\prime}\circ\sigma]$ ;
(VI)

Interaction between free variables and permutation (infix $\mathrel{\text{\textasciigrave}}$ denotes image):
(1) $\mathsf{{perm}}\;\sigma\longrightarrow\mathsf{{FV}}\;(t[\sigma])=\sigma% \mathrel{\text{\textasciigrave}}\mathsf{{FV}}\;t$ ; (2) $\mathsf{{perm}}\;\sigma\wedge(\forall x\in\mathsf{{FV}}\;t.\;\sigma\;x=x)% \longrightarrow t[\sigma]=t$ .

Note that the constructors $\mathsf{{Vr}}$ and $\mathsf{{Ap}}$ are free, hence injective (points (4) and (5) in the above proposition). On the other hand, the $\lambda$ -constructor $\mathsf{{Lm}}$ is not free, since it introduces bindings – for example, $\mathsf{{Lm}}\;x\;(\mathsf{{Vr}}\;x)=\mathsf{{Lm}}\;y\;(\mathsf{{Vr}}\;y)$ for any variables $x, y$ . Therefore, only a quasi-injectivity, i.e., injectivity up to a renaming, property holds for it (point (6)).

Points (I.6), (IV.3) and (VI.2) all reflect the fact that we work not with entirely free terms but with terms quotiented to alpha-equivalence. And so does the following proposition, expressing a strong version of structural induction, which is also generated by the binder_datatype command:

Prop 2 (Binding-aware structural induction).

Assume $\mathsf{Pvars}:{{}^{\prime}p}\rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ and $\varphi:{{}^{\prime}p}\rightarrow{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}% \rightarrow\text{bool}$ are such that (1) $\forall p.\;|\mathsf{Pvars}\;p|<_{o}\mathsf{bound}_{\text{{lterm\>}}}$ , i.e., $\forall p.\;\mathsf{finite}\,(\mathsf{Pvars}\;p)$ ; (2) $\forall p,x.\;\varphi\;p\;(\mathsf{{Vr}}\;x)$ ; (3) $\forall p,t_{1},t_{2}.\;(\forall q.\;\varphi\;q\;t_{1})\,\wedge\,(\forall q.\;% \varphi\;q\;t_{2})\longrightarrow\varphi\;p\;\allowbreak(\mathsf{{Ap}}\;% \allowbreak t_{1}\;t_{2})$ ; and (4) $\forall p.\;\forall x,t.\;{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle x\notin\mathsf{Pvars}\;p$}}{\hbox{\pagecolor{light-gray}$% \textstyle x\notin\mathsf{Pvars}\;p$}}{\hbox{\pagecolor{light-gray}$% \scriptstyle x\notin\mathsf{Pvars}\;p$}}{\hbox{\pagecolor{light-gray}$% \scriptscriptstyle x\notin\mathsf{Pvars}\;p$}}}}\wedge\,(\forall q.\;\varphi\;% q\;t)\longrightarrow\varphi\;p\;(\mathsf{{Lm}}\;x\;t)$ . Then $\forall p,t.\;\varphi\;p\;t$ .

The above resembles standard structural induction (as available for the standard datatypes), except for the highlighted part, which allows one to assume during the induction process that the bound variables are disjoint from the variables coming from a designated type ${}^{\prime}p$ of parameters – this enables the rigorous application of Barendregt’s variable convention [6]. Taking ${}^{\prime}p$ to be the unit type and $\mathsf{Pvars}\;p=\varnothing$ , we obtain standard structural induction.

Given a type ${}^{\prime}a$ together with operators resembling the free-variable and permutation operators, namely $\mathit{{afv}}:{{}^{\prime}a}\rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ and $\mathit{{aprm}}:({{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}% )\rightarrow{{}^{\prime}a}\rightarrow^{\prime}a$ , we say that they form a loosely-supported pre-nominal structure, written $\mathsf{lspnom}\;\mathit{{afv}}\;\mathit{{aprm}}$ , when the following holds:

$\blacksquare$

Compositionality (Prop. 1, V.2): $\mathsf{{perm}}\,\sigma\wedge\mathsf{{perm}}\,\sigma^{\prime}\,{% \longrightarrow}\,\mathit{{aprm}}\,\sigma\,(\mathit{{aprm}}\,\sigma^{\prime}\,% a)\,{=}\,\mathit{{aprm}}\,(\sigma\circ\sigma^{\prime})\,a$ .
$\blacksquare$

Congruence (Prop. 1, VI.2): $\mathsf{{perm}}\;\sigma\land(\forall x\in\mathit{{afv}}\;a.\;\sigma\;x=x)% \longrightarrow\mathit{{aprm}}\;\sigma\;a=a$ .

Moreover, for any cardinal $\kappa$ , we say that they form a $\kappa$ -loosely-supported nominal structure, written $\mathsf{lsnom}_{\kappa}\;\mathit{{afv}}\;\mathit{{aprm}}$ , when $\mathsf{lspnom}\;\mathit{{afv}}\;\mathit{{aprm}}$ holds and additionally the following holds:

$\blacksquare$

Smallness (Prop. 1, III.1 in case $\kappa=\mathsf{bound}_{\text{{lterm\>}}}$ ): $|\mathsf{{FV}}\;a|<_{o}\kappa$ .

Finally, given two types ${}^{\prime}p$ and ${}^{\prime}a$ and operators on them

$\blacksquare$

$\mathit{{pfv}}:{{}^{\prime}p}\rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ , $\mathit{{pprm}}:({{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}% )\rightarrow{{}^{\prime}p}\rightarrow{{}^{\prime}p}$ ,
$\blacksquare$

$\mathit{{afv}}:{{}^{\prime}a}\rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ , $\mathit{{aprm}}:({{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}% )\rightarrow{{}^{\prime}a}\rightarrow{{}^{\prime}a}$ ,
$\blacksquare$

$\mathit{{vr}}:{{}^{\prime}\mathit{var}}\rightarrow({{}^{\prime}p}\rightarrow{{% }^{\prime}a})$ , $\mathit{{ap}}:{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow({{}^{% \prime}p}\rightarrow{{}^{\prime}a})\rightarrow{{}^{\prime}\mathit{var}}\;\text% {{lterm\>}}\rightarrow({{}^{\prime}p}\rightarrow{{}^{\prime}a})\rightarrow({{}% ^{\prime}p}\rightarrow{{}^{\prime}a})$ , $\mathit{{lm}}:{{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{var}}\;% \text{{lterm\>}}\rightarrow({{}^{\prime}p}\rightarrow{{}^{\prime}a})% \rightarrow({{}^{\prime}p}\rightarrow{{}^{\prime}a})$

(where $\mathit{{vr}}$ , $\mathit{{ap}}$ , $\mathit{{lm}}$ have types resembling those of lterm ’s constructors $\mathsf{{Vr}}$ , $\mathsf{{Ap}}$ and $\mathsf{{Lm}}$ ), we say that they form an lterm -model, written $\mathsf{{model}}_{\text{{lterm\>}}}\,\mathit{{pfv}}\,\mathit{{pprm}}\,\mathit{% {afv}}\,\mathit{{aprm}}\,\mathit{{vr}}\,\mathit{{ap}}\,\mathit{{lm}}$ , provided that: (1) $\mathsf{lsnom}_{\mathsf{bound}_{\text{{lterm\>}}}}\;\mathit{{pfv}}\;\mathit{{% pprm}}$ holds; (2) $\mathsf{lspnom}\;\mathit{{afv}}\;\mathit{{aprm}}$ holds; and (3) the following properties, corresponding to properties of lterm , hold, where $\mathit{{paprm}}\;\sigma\;f=\mathit{{aprm}}\;\sigma\circ f\circ\mathit{{pprm}}% \;(\sigma^{-1})$ :

1.
equivariance of the constructors (Prop 1, II.1, II.2, II.3):
- $\blacksquare$
  
  $\mathsf{{perm}}\;\sigma\longrightarrow\mathit{{paprm}}\;\sigma\;(\mathit{{vr}}% \;x)=\mathit{{vr}}\,(\sigma\;x)$ ;
- $\blacksquare$
  
  $\mathsf{{perm}}\;\sigma\longrightarrow\mathit{{paprm}}\;\sigma\;(\mathit{{ap}}% \;t_{1}\;f_{1}\;t_{2}\;f_{2})=\mathit{{ap}}\;(t_{1}[\sigma])\;(\mathit{{paprm}% }\;\sigma\;f_{1})\;(t_{2}[\sigma])\;(\mathit{{paprm}}\;\sigma\;f_{2})$ ;
- $\blacksquare$
  
  $\mathsf{{perm}}\;\sigma\longrightarrow\mathit{{paprm}}\;\sigma\;(\mathit{{lm}}% \;x\;t\;f)=\mathit{{lm}}\;(\sigma\;x)\;(t[\sigma])\;(\mathit{{paprm}}\;\sigma% \;f)$ ;
2.
free-variables sub-distributing under constructors (weaker versions of Prop 1, IV.1, IV.2, IV.3, with inclusions instead of equalities):
- $\blacksquare$
  
  $\mathit{{afv}}\,(\mathit{{vr}}\;x\;p)\subseteq\{x\}\cup\mathit{{pfv}}\;p$ ;
- $\blacksquare$
  
  $\mathit{{afv}}\,(f_{1}\;p)\subseteq\mathit{{afv}}\;t_{1}\,\cup\,\mathit{{pfv}}% \;p\;\wedge\;\mathit{{afv}}\,(f_{2}\;p)\subseteq\mathit{{afv}}\;t_{2}\,\cup\,% \mathit{{pfv}}\;p\longrightarrow\\ \mathit{{afv}}\,(\mathit{{ap}}\;t_{1}\;f_{1}\;t_{2}\;f_{2}\;p)\subseteq\mathit% {{afv}}\;t_{1}\,\cup\,\mathit{{afv}}\;t_{2}\,\cup\,\mathit{{pfv}}\;p$ ;
- $\blacksquare$
  
  $x\notin\mathit{{pfv}}\;p\,\wedge\,\mathit{{afv}}\,(f\;p)\subseteq\mathit{{afv}% }\;t\smallsetminus\{x\}\,\cup\,\mathit{{pfv}}\;p\;\longrightarrow\;\mathit{{% afv}}\,(\mathit{{lm}}\;x\;t\;f\;p)\subseteq\mathit{{afv}}\;t\,\smallsetminus\,% \{x\}\,\cup\,\mathit{{pfv}}\;p$ .

We refer to the types ${}^{\prime}p$ and ${}^{\prime}a$ above as the parameter type and the carrier type of the lterm -model, respectively. Our binding-aware recursor operates on lterm -models, in that, given any lterm -model it returns a function from terms and parameters to carrier elements that (1) commutes with the constructors and permutation operators; and (2) preserves the free-variable operators. Moreover, commutation with the binding constructor happens in a binding-aware fashion, that is, avoiding clashes between the bound variables and the parameter variables – i.e., again obeying Barendregt’s variable convention. This is expressed in the following proposition:

Prop 3 (Binding-aware recursion).

Assume $\mathsf{{model}}_{\text{{lterm\>}}}\;\mathit{{pfv}}\;\mathit{{pprm}}\;\mathit{% {afv}}\;\mathit{{aprm}}\;\mathit{{vr}}\;\mathit{{ap}}\;\mathit{{lm}}$ holds and let $\mathit{g}:{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow{{}^{\prime}p% }\rightarrow{{}^{\prime}a}$ denote $\mathsf{{rec}}_{\text{{lterm\>}}}\;\mathit{{pfv}}\;\mathit{{pprm}}\;\mathit{{% afv}}\;\mathit{{aprm}}\;\mathit{{vr}}\;\mathit{{ap}}\;\mathit{{lm}}$ . The following properties hold: (1) $\mathit{g}\;(\mathsf{{Vr}}\;x)\;p=\mathit{{vr}}\;x\;p$ ; (2) $\mathit{g}\;(\mathsf{{Ap}}\;t_{1}\;t_{2})\;p=\mathit{{ap}}\;t_{1}\;(\mathit{g}% \;t_{1})\;t_{2}\;(\mathit{g}\;t_{2})\;p$ ; (3) ${\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle x\notin% \mathit{{pfv}}\;p$}}{\hbox{\pagecolor{light-gray}$\textstyle x\notin\mathit{{% pfv}}\;p$}}{\hbox{\pagecolor{light-gray}$\scriptstyle x\notin\mathit{{pfv}}\;p% $}}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle x\notin\mathit{{pfv}}\;p$}% }}}\longrightarrow\mathit{g}\;(\mathsf{{Lm}}\;x\;t)\;p=\mathit{{lm}}\;x\;t\;(% \mathit{g}\;t)\;p$ ; (4) $\mathsf{{perm}}\;\sigma\longrightarrow\mathit{g}\;(a[\sigma])\;p=\mathit{{% paprm}}\;\sigma\;(\mathit{g}\;a)\;p$ ; and (5) $\mathit{{afv}}\;(\mathit{g}\;t\;p)\subseteq\mathsf{{FV}}\;t\,\cup\,\mathit{{% pfv}}\;p$ .

In the current implementation, we do not get a single recursor constant and the above recursion theorem, but rather given a model we define $\mathit{g}$ and derive its properties on the fly. Our recursor definition follows Blanchette et al.’s design [10], which generalizes Norrish’s nominal recursor [26] and removes one of the unnecessary assumptions [34].

Here is an example of applying the recursor. For any $\rho:{{}^{\prime}var}\rightarrow{{}^{\prime}var}\;\text{{lterm\>}}$ , we let its support $\mathsf{Supp}\;\rho$ be $\{x:{{}^{\prime}var}\mid\rho\;x\not=\mathsf{{Vr}}\;x\}$ , and its image-support $\mathsf{ImSupp}\;\rho$ be $\mathsf{Supp}\;\rho\cup\bigcup_{t\in\mathsf{Supp}\;\rho}\mathsf{{FV}}\;t$ . We let the type of substitution-functions ${{}^{\prime}var}\;\mathsf{substFun}$ be the type of all functions $\rho$ such that $|\mathsf{Supp}\;\rho|<_{o}\mathsf{bound}_{\text{{lterm\>}}}$ (obtained as a subtype of $\rho:{{}^{\prime}var}\rightarrow{{}^{\prime}var}\;\text{{lterm\>}}$ ); function application and composition are inherited to ${{}^{\prime}var}\;\mathsf{substFun}$ from the function type and are denoted the same. To define term-for-variable substitution operator $\mathsf{{subst}}:{{}^{\prime}\mathit{var}}\;\text{{lterm\>}}\rightarrow{{}^{% \prime}var}\;\mathsf{substFun}\rightarrow{{}^{\prime}var}\;\text{{lterm\>}}$ , we take ${{}^{\prime}p}={{}^{\prime}var}\;\mathsf{substFun}$ and ${{}^{\prime}a}={{}^{\prime}var}\;\text{{lterm\>}}$ , and determine the model from the desired recursive clauses for the constructors and the desired behavior of substitution w.r.t. free variables and permutation:

(1)

$\mathsf{{subst}}\;(\mathsf{{Vr}}\;x)\;\rho=\rho\;x$ ;
(2)

$\mathsf{{subst}}\;(\mathsf{{Ap}}\;t_{1}\;t_{2})\;\rho=\mathsf{{Ap}}\;(\mathsf{% {subst}}\;t_{1}\;\rho)\;(\mathsf{{subst}}\;t_{2}\;\rho)$ ;
(3)

$x\notin\mathsf{ImSupp}\;\rho\longrightarrow\mathsf{{subst}}\;(\mathsf{{Lm}}\;x% \;t)\;\rho=\mathsf{{Lm}}\;x\;(\mathsf{{subst}}\;t\;\rho)$ ;
(4)

$\mathsf{{subst}}\;(t[\sigma])\;\rho=\mathsf{{subst}}\;t\;((\_[\sigma])\circ\rho)$ ;
(5)

$\mathsf{{FV}}\;(\mathsf{{subst}}\;t\;\rho)\subseteq\mathsf{{FV}}\;t\cup\mathsf% {ImSupp}\;\rho$ .

Namely, here is the lterm -model structure $(\mathit{{pfv}},\mathit{{pprm}},\mathit{{afv}},\mathit{{aprm}},\mathit{{vr}},% \mathit{{ap}},\mathit{{lm}})$ corresponding to (and unambiguously determined from) the above:

(M1): $\mathit{{vr}}\;x\;\rho=\rho\;x$ ;
(M2): $\mathit{{ap}}\;t_{1}\;f_{1}\;t_{2}\;f_{2}\;\rho=\mathsf{{Ap}}\;(f_{1}\;\rho)\;% (f_{2}\;\rho)$ ;
(M3): $\mathit{{lm}}\;x\;t\;f\;\rho=\mathsf{{Lm}}\;x\;(f\;\rho)$ ;
(M4): $\mathit{{aprm}}\;t\;\sigma=t[\sigma$ ] and $\mathit{{pprm}}\;\rho\;\sigma=(\_[\sigma])\circ\rho$ ;
(M5): $\mathit{{afv}}\;t=\mathsf{{FV}}\;t$ and $\mathit{{pfv}}\;\rho=\mathsf{ImSupp}\;\rho$ .

Indeed, the (M $i$ ) definitions are obtained by “fishing” the codomain operator behind the ( $i$ ) recursive clause – e.g., (M2) turns (2) into $\mathsf{{subst}}\;(\mathsf{{Ap}}\;t_{1}\;t_{2})\;\rho=\mathit{{ap}}\;t_{1}\;(% \mathsf{{subst}}\;\rho\;t_{1})\;t_{2}\;(\mathsf{{subst}}\;\rho\;t_{2})\;\rho$ . Currently this fishing process is not implemented in our package, so the user has to explicitly indicate these operators and then infer (1)–(5) from the recursion theorem.

3.3 Infinitary $\lambda$ -calculus terms

Let ${}^{\prime}a\;\text{stream\>}$ and ${}^{\prime}a\;\text{dstream\>}$ be the polymorphic types of streams (i.e., countable sequences) and distinct (i.e., non-repetitive) streams, respectively. While streams exist in Isabelle’s standard library, we introduce distinct streams as a subtype of streams that ensures that stream elements do not repeat. To simplify the exposition, we pretend that making a type non-repetitive (or linear) is performed automatically using the following command, while for now we are executing manually a uniform construction sketched by Blanchette et al. [10, §4].

linear_type

{}^{\prime}a\;\text{dstream\>}

=

{}^{\prime}a\;\text{stream\>}

on

{{}^{\prime}a}

The type of infinitary $\lambda$ -terms [22], where $\lambda$ -abstraction binds a distinct stream of variables and application applies a term to a stream of terms, is introduced by the following command:

⬇

binder_datatype ’var iterm = iVr ’var | iAp "’var iterm" "’var iterm stream"

| iLm "(xs::’var) dstream" t::"’var iterm" binds xs in t

This time (employing the same type-class mechanism explained in §3.2) when using the type ${}^{\prime}\mathit{var}\;\text{{iterm}}$ we will implicitly assume that ${}^{\prime}\mathit{var}$ has cardinality at least $\aleph_{1}$ , i.e., is more than countable. Indeed, to accommodate the countable branching syntax while ensuring that no term can exhaust the entire supply of variables, we now have $\mathsf{bound}_{\text{{iterm}}}=\aleph_{1}$ .

Our command produces again the familiar constants: the constructors $\mathsf{{iVr}}$ , $\mathsf{{iAp}}$ and $\mathsf{{iLm}}$ , free-variable operator $\mathsf{{iFV}}$ , permutation operator $\mathsf{{iPERM}}$ (written $\_[\_]$ ), a cardinal bound $\mathsf{bound}_{\text{{iterm}}}$ (here, $\aleph_{1}$ ), and a binding-aware recursion combinator $\mathsf{{rec}}_{\text{{iterm}}}$ . Moreover, it generates similar properties as for lterm . We only show properties that differ in a major way from the lterm case (while keeping the numbering). We use an auxiliary predicate for a function that behaves as identity on a given set: $\mathsf{id\_on}\>A\>f\mathrel{=}\forall x\in A.\;f\>x=x$ .

Prop 4.

(I)

Distinctness and (quasi-)injectivity of the constructors: (6) $\mathsf{{iLm}}\;\mathit{xs}\;t=\mathsf{{iLm}}\;\mathit{xs}^{\prime}\;t^{\prime% }\,\longleftrightarrow\,{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle(\exists\sigma.\;\mathsf{{perm}}\;\sigma\land\mathsf{id\_on}\;(% \mathsf{{iFV}}\;t\smallsetminus\mathsf{{dsset}}\;\mathit{xs})\;\sigma\land% \mathsf{{dsmap}}\;\sigma\;\mathit{xs}=\mathit{xs}^{\prime}\land t[\sigma]=t^{% \prime})$}}{\hbox{\pagecolor{light-gray}$\textstyle(\exists\sigma.\;\mathsf{{% perm}}\;\sigma\land\mathsf{id\_on}\;(\mathsf{{iFV}}\;t\smallsetminus\mathsf{{% dsset}}\;\mathit{xs})\;\sigma\land\mathsf{{dsmap}}\;\sigma\;\mathit{xs}=% \mathit{xs}^{\prime}\land t[\sigma]=t^{\prime})$}}{\hbox{\pagecolor{light-gray% }$\scriptstyle(\exists\sigma.\;\mathsf{{perm}}\;\sigma\land\mathsf{id\_on}\;(% \mathsf{{iFV}}\;t\smallsetminus\mathsf{{dsset}}\;\mathit{xs})\;\sigma\land% \mathsf{{dsmap}}\;\sigma\;\mathit{xs}=\mathit{xs}^{\prime}\land t[\sigma]=t^{% \prime})$}}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle(\exists\sigma.\;% \mathsf{{perm}}\;\sigma\land\mathsf{id\_on}\;(\mathsf{{iFV}}\;t\smallsetminus% \mathsf{{dsset}}\;\mathit{xs})\;\sigma\land\mathsf{{dsmap}}\;\sigma\;\mathit{% xs}=\mathit{xs}^{\prime}\land t[\sigma]=t^{\prime})$}}}}$ ;
(II)

Equivariance of the constructors:
(2) $\mathsf{{perm}}\;\sigma\longrightarrow(\mathsf{{iAp}}\;t\;\mathit{ts})[\sigma]% =\mathsf{{iAp}}\;(t[\sigma])\;({\mathord{\mathchoice{\hbox{\pagecolor{light-% gray}$\displaystyle\mathsf{{smap}}$}}{\hbox{\pagecolor{light-gray}$\textstyle% \mathsf{{smap}}$}}{\hbox{\pagecolor{light-gray}$\scriptstyle\mathsf{{smap}}$}}% {\hbox{\pagecolor{light-gray}$\scriptscriptstyle\mathsf{{smap}}$}}}}\;(\lambda t% ^{\prime}.\;t^{\prime}[\sigma])\;\mathit{ts})$ ;
(3) $\mathsf{{perm}}\;\sigma\longrightarrow(\mathsf{{iLm}}\;\mathit{xs}\;t)[\sigma]% =\mathsf{{iLm}}\,({\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle\mathsf{{dsmap}}$}}{\hbox{\pagecolor{light-gray}$\textstyle% \mathsf{{dsmap}}$}}{\hbox{\pagecolor{light-gray}$\scriptstyle\mathsf{{dsmap}}$% }}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle\mathsf{{dsmap}}$}}}}\;% \sigma\;\mathit{xs})\,(t[\sigma])$ ;
(III)

Smallness (here, equivalently, at most countability) of the set of free variables:
(1) $|\mathsf{{iFV}}\;t|<_{o}\mathsf{bound}_{\smash{{\mathord{\mathchoice{\hbox{% \pagecolor{light-gray}$\displaystyle\text{{iterm}}$}}{\hbox{\pagecolor{light-% gray}$\textstyle\text{{iterm}}$}}{\hbox{\pagecolor{light-gray}$\scriptstyle% \text{{iterm}}$}}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle\text{{iterm}% }$}}}}}}$ ;
(IV)

Interaction between free variables and constructors:
(2) $\mathsf{{iFV}}\,(\mathsf{{iAp}}\;t\;\mathit{ts})=\mathsf{{iFV}}\;t\cup\bigcup_% {t^{\prime}\in\smash{{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle\scriptsize\mathsf{{sset}}$}}{\hbox{\pagecolor{light-gray}$% \textstyle\scriptsize\mathsf{{sset}}$}}{\hbox{\pagecolor{light-gray}$% \scriptstyle\scriptsize\mathsf{{sset}}$}}{\hbox{\pagecolor{light-gray}$% \scriptscriptstyle\scriptsize\mathsf{{sset}}$}}}}}\;\mathit{ts}}\mathsf{{iFV}}% \;t^{\prime}$ ; (3) $\mathsf{{iFV}}\,(\mathsf{{iLm}}\;\mathit{xs}\;t)=\mathsf{{iFV}}\;t\,% \smallsetminus\,{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle\mathsf{{dsset}}$}}{\hbox{\pagecolor{light-gray}$\textstyle% \mathsf{{dsset}}$}}{\hbox{\pagecolor{light-gray}$\scriptstyle\mathsf{{dsset}}$% }}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle\mathsf{{dsset}}$}}}}\;% \mathit{xs}$ ;
(V)

Permutation identity and compositionality;
(VI)

Interaction between free variables and permutation.

Again, $\mathsf{{iVr}}$ and $\mathsf{{iAp}}$ are free constructors, hence injective, whereas the binding constructor $\mathsf{{iLm}}$ only satisfies quasi-injectivity, i.e., injectivity up to a permutation of the bound variables which leaves the term’s free variables untouched (I.6) – note that the latter property uses the dstream -specific free variables ( $\mathsf{{dsset}}$ ) and permutation operators ( $\mathsf{{dsmap}}$ ). Similarly the recursive occurrences of iterm nested under stream in the $\mathsf{{iAp}}$ constructor are accessed via the stream’s $\mathsf{{smap}}$ and $\mathsf{{sset}}$ functions in II.2 and IV.2, respectively. We obtain binding-aware structural induction and recursion principles, too, and highlight the main differences to Props. 2 and 3 (for a corresponding notion of iterm-model):

Prop 5 (Binding-aware structural induction).

Assume $\mathsf{Pvars}:{{}^{\prime}p}\rightarrow{{}^{\prime}\mathit{var}}\;\text{set}$ and $\varphi:{{}^{\prime}p}\rightarrow{{}^{\prime}\mathit{var}}\;\text{{iterm}}% \rightarrow\text{bool}$ are such that (1) $\forall p.\;|\mathsf{Pvars}\;p|<_{o}\mathsf{bound}_{\smash{{\mathord{% \mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle\text{{iterm}}$}}{\hbox{% \pagecolor{light-gray}$\textstyle\text{{iterm}}$}}{\hbox{\pagecolor{light-gray% }$\scriptstyle\text{{iterm}}$}}{\hbox{\pagecolor{light-gray}$% \scriptscriptstyle\text{{iterm}}$}}}}}}$ , i.e., $\forall p.\;{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle% \mathsf{countable}$}}{\hbox{\pagecolor{light-gray}$\textstyle\mathsf{countable% }$}}{\hbox{\pagecolor{light-gray}$\scriptstyle\mathsf{countable}$}}{\hbox{% \pagecolor{light-gray}$\scriptscriptstyle\mathsf{countable}$}}}}\,(\mathsf{% Pvars}\;p)$ ; (2) $\forall p,x.\;\varphi\;p\;(\mathsf{{iVr}}\;x)$ ; (3) $\forall p,t,\mathit{ts}.\;(\forall q.\;\varphi\;q\;t)\,\wedge\,{\mathord{% \mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle(\forall t^{\prime}\in% \mathsf{{sset}}\;\mathit{ts}.\;\forall q.\;\varphi\;q\;t^{\prime})$}}{\hbox{% \pagecolor{light-gray}$\textstyle(\forall t^{\prime}\in\mathsf{{sset}}\;% \mathit{ts}.\;\forall q.\;\varphi\;q\;t^{\prime})$}}{\hbox{\pagecolor{light-% gray}$\scriptstyle(\forall t^{\prime}\in\mathsf{{sset}}\;\mathit{ts}.\;\forall q% .\;\varphi\;q\;t^{\prime})$}}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle(% \forall t^{\prime}\in\mathsf{{sset}}\;\mathit{ts}.\;\forall q.\;\varphi\;q\;t^% {\prime})$}}}}\longrightarrow\varphi\;p\;\allowbreak(\mathsf{{iAp}}\;% \allowbreak t\;\mathit{ts})$ ; and (4) $\forall p,\mathit{xs},t.\;{\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$% \displaystyle\mathsf{{dsset}}\;\mathit{xs}\cap\mathsf{Pvars}\;p=\varnothing$}}% {\hbox{\pagecolor{light-gray}$\textstyle\mathsf{{dsset}}\;\mathit{xs}\cap% \mathsf{Pvars}\;p=\varnothing$}}{\hbox{\pagecolor{light-gray}$\scriptstyle% \mathsf{{dsset}}\;\mathit{xs}\cap\mathsf{Pvars}\;p=\varnothing$}}{\hbox{% \pagecolor{light-gray}$\scriptscriptstyle\mathsf{{dsset}}\;\mathit{xs}\cap% \mathsf{Pvars}\;p=\varnothing$}}}}\wedge\,(\forall q.\;\varphi\;q\;t)% \longrightarrow\varphi\;p\;(\mathsf{{iLm}}\;\mathit{xs}\;t)$ . Then $\forall p,t.\;\varphi\;p\;t$ .

Prop 6 (Binding-aware recursion).

Assume $\mathsf{{model}}_{\text{{iterm}}}\;\mathit{{pfv}}\;\mathit{{pprm}}\;\mathit{{% afv}}\;\mathit{{aprm}}\;\mathit{{ivr}}\;\mathit{{iap}}\;\mathit{{ilm}}$ holds, and let $g:{{}^{\prime}\mathit{var}}\;\text{{iterm}}\rightarrow{{}^{\prime}p}% \rightarrow{{}^{\prime}a}$ denote $\mathsf{{rec}}_{\text{{iterm}}}\;\mathit{{pfv}}\;\mathit{{pprm}}\;\mathit{{afv% }}\;\mathit{{aprm}}\;\mathit{{ivr}}\;\mathit{{iap}}\;\mathit{{ilm}}$ . Further let $\mathit{{paprm}}\;\sigma\;f=\mathit{{aprm}}\;\sigma\circ f\circ\mathit{{pprm}}% \;(\sigma^{-1})$ . The following hold: (1) $g\;(\mathsf{{iVr}}\;x)\;p=\mathit{{ivr}}\;x\;p$ ; (2) $g\;(\mathsf{{iAp}}\;t\;\mathit{ts})\;p=\mathit{{iap}}\;t\;(g\;t)\;\mathit{ts}% \;({\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle\mathsf{{% smap}}$}}{\hbox{\pagecolor{light-gray}$\textstyle\mathsf{{smap}}$}}{\hbox{% \pagecolor{light-gray}$\scriptstyle\mathsf{{smap}}$}}{\hbox{\pagecolor{light-% gray}$\scriptscriptstyle\mathsf{{smap}}$}}}}\;g\;\mathit{ts})\;p$ ; (3) ${\mathord{\mathchoice{\hbox{\pagecolor{light-gray}$\displaystyle\mathsf{{dsset% }}\;xs\cap\mathit{{pfv}}\;p=\varnothing$}}{\hbox{\pagecolor{light-gray}$% \textstyle\mathsf{{dsset}}\;xs\cap\mathit{{pfv}}\;p=\varnothing$}}{\hbox{% \pagecolor{light-gray}$\scriptstyle\mathsf{{dsset}}\;xs\cap\mathit{{pfv}}\;p=% \varnothing$}}{\hbox{\pagecolor{light-gray}$\scriptscriptstyle\mathsf{{dsset}}% \;xs\cap\mathit{{pfv}}\;p=\varnothing$}}}}\longrightarrow g\;(\mathsf{{iLm}}\;% \mathit{xs}\;t)\;p=\mathit{{ilm}}\;\mathit{xs}\;t\;(g\;t)\;p$ ; (4) $\mathsf{{perm}}\;\sigma\longrightarrow g\;(a[\sigma])\;p=\mathit{{paprm}}\;% \sigma\;(g\;a)\;p$ ; and (5) $\mathit{{afv}}\;(g\;t\;p)\subseteq\mathsf{{iFV}}\;t\,\cup\,\mathit{{pfv}}\;p$ .

3.4 Types and terms for System F_<:

We define the types and terms of System F_<:, which we will use in our solution to the POPLmark challenge (§6). Because we aim for the challenge 2B, we directly introduce the syntax that incorporates nested types and pattern matching. Compared to the previous subsections we will be much briefer regarding the output of our binder_datatype commands: the previous examples already cover many of the arising ingredients and phenomena.

We start by introducing a non-repetitive (in the keys) type of finite sets of key-value pairs that will be used to represent records (where we use strings as keys).

type_synonym label

=

string

linear_type

(^{\prime}a,^{\prime}b)\;\text{{lfset}}

=

(^{\prime}a\times^{\prime}b)\;\text{fset}

on

{{}^{\prime}a}

The challenge description and all existing solutions favor ordered collections for records, and it would be easy for us to adjust our entire formalization to use lists instead of finite sets (fset). We chose to use fset as the basis for our records because in practical languages like Standard ML or JSON records are considered to be unordered collections. We also chose it because it displays the flexibility of our approach to work with nested recursion through non-datatypes:

⬇

binder_datatype ’tvar type = TVr ’tvar | Top | Arr "’tvar type" "’tvar type"

| All X::’tvar "’tvar type" T::"’tvar type" binds X in T

| TRec "(label, ’tvar type) lfset"

The above command defines POPLmark types. The only binding constructor is $\mathsf{All}$ and we obtain the following quasi-injectivity property for it (where $\mathsf{{TFV}}:{{}^{\prime}\mathit{tvar}}\;\text{{type}}\to{{}^{\prime}\mathit% {tvar}}\;\text{set}$ ): $\mathsf{All}\;X\;T_{1}\;T_{2}=\mathsf{All}\;X^{\prime}\;T_{1}^{\prime}\;T_{2}^% {\prime}\,\longleftrightarrow\,(T_{1}=T_{1}^{\prime}\wedge(X^{\prime}\notin% \mathsf{{TFV}}\;T_{2}\lor X=X^{\prime})\wedge T_{2}=T_{2}^{\prime}[X\!% \leftrightarrow\!X^{\prime}])$ . Naturally, we also obtain binding-aware induction and recursion principles.

We continue with defining terms. For that purpose we introduce patterns as the non-repetitive subtype of the (non-binding) “pre-pattern” datatype that recurses through lfset.

datatype

({{}^{\prime}\mathit{tvar}},{{}^{\prime}\mathit{var}})\;\text{{ppat}}

=

\mathsf{{PPVr}}\;{{}^{\prime}\mathit{var}}\;({{}^{\prime}\mathit{tvar}}\;\text% {{type}})

\mid

\mathsf{PPRec}\;(\text{{label}},({{}^{\prime}\mathit{tvar}},{{}^{\prime}% \mathit{var}})\;\text{{ppat}})\;\text{{lfset}}

linear_type

({{}^{\prime}\mathit{tvar}},{{}^{\prime}\mathit{var}})\;\text{{pat}}

=

({{}^{\prime}\mathit{var}},{{}^{\prime}\mathit{tvar}})\;\text{{ppat}}

on

{{}^{\prime}\mathit{var}}

We lift the pre-pattern constructors $\mathsf{{PPVr}}$ and $\mathsf{PPRec}$ to the pattern type as $\mathsf{{PVr}}:{{}^{\prime}\mathit{var}}\rightarrow{{}^{\prime}\mathit{tvar}}% \;\text{{type}}\rightarrow({{}^{\prime}\mathit{tvar}},{{}^{\prime}\mathit{var}% })\,\text{{pat}}$ and $\mathsf{PRec}\,{:}\,(\text{{label}},({{}^{\prime}\mathit{tvar}},{{}^{\prime}% \mathit{var}})\,\text{{pat}})\;\text{{lfset}}\rightarrow({{}^{\prime}\mathit{% tvar}},{{}^{\prime}\mathit{var}})\,\text{{pat}}$ . The latter operator is not a free constructor: its argument must satisfy a non-repetitiveness predicate ( $\textsf{nonrep}_{\mathsf{PRec}}:(\text{{label}},({{}^{\prime}\mathit{tvar}},{{% }^{\prime}\mathit{var}})\;\text{{pat}})\;\text{{lfset}}\rightarrow\text{bool}$ ). We are ready to define terms:

⬇

binder_datatype (’tvar, ’var) term = Vr ’var

| Ap "(’tvar, ’var) term" "(’tvar, ’var) term"

| Lm x::’var "’tvar typ" t::"(’tvar, ’var) term" binds x in t

| ApT "(’tvar, ’var) term" "’tvar typ"

| LmT X::’tvar "’tvar typ" t::"(’tvar, ’var) term" binds X in t

| Rec "(label, (’tvar, ’var) term) lfset" | Proj "(’tvar, ’var) term" label

| Let "(’tvar, P::’var) pat" "(’tvar, ’var) term" t::"(’tvar, ’var) term" binds P in t

Of the eight constructors, three are binding. We show their quasi-injectivity properties:

\begin{array}[]{@{}l@{}}\mathsf{{Lm}}\;x\;T\;t=\mathsf{{Lm}}\;x^{\prime}\;T^{% \prime}\;t^{\prime}\,\longleftrightarrow\,(T=T^{\prime}\wedge(x^{\prime}\notin% \mathsf{{FV}}\;t\lor x=x^{\prime})\wedge t=t^{\prime}[x\!\leftrightarrow\!x^{% \prime}])\\ \mathsf{{LmT}}\;X\;T\;t=\mathsf{{LmT}}\;X^{\prime}\;T^{\prime}\;t^{\prime}\,% \longleftrightarrow\,(T=T^{\prime}\wedge(X^{\prime}\notin\mathsf{{FTV}}\;t\lor x% =x^{\prime})\wedge t=t^{\prime}[X\!\leftrightarrow\!X^{\prime}])\\ \mathsf{{Let}}\;P\;t_{1}\;t_{2}=\mathsf{{Let}}\;P^{\prime}\;t_{1}^{\prime}\;t_% {2}^{\prime}\,\longleftrightarrow\,(t_{1}=t_{1}^{\prime}\wedge\\ \phantom{\mathsf{{Let}}}(\exists\sigma.\;\mathsf{{perm}}\;\sigma\wedge\mathsf{% id\_on}\;(\mathsf{{FV}}\;t\smallsetminus\mathsf{{PV}}\;P)\;\sigma\wedge P[% \sigma]=P^{\prime}\wedge t_{2}[\sigma]=t_{2}^{\prime}))\end{array}

These hinge on our ability to refer to a term’s free variables ( $\mathsf{{FV}}$ ) and its free type variables ( $\mathsf{{FTV}}$ ), as well as a pattern’s free type variables ( $\mathsf{{PV}}$ ). Similarly, we obtain and make use of infrastructure to permute a pattern’s variables, a term’s variables, and a term’s type variables. Again, we also obtain binding-aware induction and recursion principles, where e.g., the parameter $p$ avoids a pattern $P$ ’s free variables in the $\mathsf{{Let}}$ case of the induction by providing the assumption $\mathsf{{P\hskip-0.88887ptVars}}\;p\cap\mathsf{{PV}}\;P=\varnothing$ to the user.

4 MrBNF’s Internals: Construction of Datatypes with Bindings

Isabelle’s definitional package for standard (co)datatypes [12], sometimes referred to as the BNF package, is based on bounded natural functors (BNFs) [41] – which are comprised of meta-information associated with well-behaved type constructors and are closed under composition and fixpoints (datatype and codatatype construction). The meta-information consists of a few constants and relations between them. Specifically, a BNF is an $n$ -ary type constructor $\overline{\vphantom{\gamma^{\prime}}\alpha}\;T$ (here we use the overlined notation as a shorthand for $(\alpha_{1},\ldots,\alpha_{n})\;T$ and similarly in the following for other types and terms) along with a mapper $\mathsf{map}_{T}:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\beta)}% \rightarrow\overline{\vphantom{\gamma^{\prime}}\alpha}\;T\rightarrow\overline{% \vphantom{\gamma^{\prime}}\beta}\;T$ , the relator $\mathsf{rel}_{T}:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\beta% \rightarrow\text{bool})}\rightarrow\overline{\vphantom{\gamma^{\prime}}\alpha}% \;T\rightarrow\overline{\vphantom{\gamma^{\prime}}\beta}\;T\rightarrow\text{bool}$ , several setters $\mathsf{set}^{i}_{T}:\overline{\vphantom{\gamma^{\prime}}\alpha}\;T\rightarrow% \alpha_{i}\;\text{set}$ , and the cardinal bound $\mathsf{bound}_{T}$ satisfying a number of properties, e.g., $\mathsf{map}_{T}\;\overline{\vphantom{\gamma^{\prime}}\mathsf{{id}}}=\mathsf{{% id}}$ or $\mathsf{set}^{i}_{T}\;(\mathsf{map}\;\overline{\vphantom{\gamma^{\prime}}f}\;x% )=f_{i}\mathrel{\text{\textasciigrave}}\mathsf{set}^{i}_{T}\;x$ . For example, standard lists form a BNF with the standard $\mathsf{map}$ function, the relator $\mathsf{list\_all2}$ , which relates two lists of the same length provided that lists’ elements satisfy the given relation when zipped pair-wise, the $\mathsf{set}$ function that returns all the list’s elements and the cardinality bound $\aleph_{0}$ . Standard datatypes are least fixpoints of BNFs.

The BNF properties require $\mathsf{map}_{T}$ to behave well when applied to arbitrary functions. Blanchette et al. [10] observed that this is too restrictive when dealing with syntax with bindings and generalized BNFs to map-restricted bounded natural functions (MRBNFs). MRBNFs thus resemble BNFs but distinguish between three modes of type arguments: bound variables which can be mapped by permutations, free variables which can be mapped by small-support (endo)functions, and live variables which correspond to BNF’s variables and can be mapped by arbitrary functions. (Both BNFs and MRBNFs also support variables that are ignored by $\mathsf{map}_{T}$ , which are called dead.) We write $(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{% \prime}}\beta})\;T$ for the MRBNF with $m=|\overline{\vphantom{\gamma^{\prime}}\alpha}|$ free and bound variables and $|\overline{\vphantom{\gamma^{\prime}}\beta}|$ live variables (dead variables are left implicit) with the mapper $\mathsf{map}_{T}:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\alpha)% }\rightarrow\overline{\vphantom{\gamma^{\prime}}(\beta\rightarrow\gamma)}% \rightarrow(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{% \gamma^{\prime}}\beta})\;T\rightarrow(\overline{\vphantom{\gamma^{\prime}}% \alpha},\overline{\vphantom{\gamma^{\prime}}\gamma})\;T$ , the relator $\mathsf{rel}_{T}:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\alpha)% }\rightarrow\overline{\vphantom{\gamma^{\prime}}(\beta\rightarrow\gamma% \rightarrow\text{bool})}\rightarrow(\overline{\vphantom{\gamma^{\prime}}\alpha% },\overline{\vphantom{\gamma^{\prime}}\beta})\;T\rightarrow(\overline{% \vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{\prime}}\gamma})% \;T\rightarrow\text{bool}$ , several setters $\mathsf{set}^{i}_{T}:(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{% \vphantom{\gamma^{\prime}}\beta})\;T\rightarrow\gamma_{i}\;\text{set}$ where $\gamma_{i}=\alpha_{i}$ if $i<m$ and $\gamma_{i}=\beta_{i-m}$ otherwise, and the cardinal bound $\mathsf{bound}_{T}$ . Note that $\mathsf{rel}_{T}$ only acts on the bound and free variables using permutations or small-support functions, respectively. The MRBNF properties clarify which of the $\overline{\vphantom{\gamma^{\prime}}\alpha}$ are bound or free. For example, distinct streams ${{}^{\prime}a}\;\text{dstream\>}$ are an MRBNF with bound variable ${}^{\prime}a$ . Our MrBNF package implements Blanchette et al.’s [10] construction of binding-aware datatypes as least fixpoints of MRBNF type equations, and also customizes it to the high-level operators and theorems required by the users. In this section, we describe the construction’s main milestones.

4.1 From User-Specifications to Fixpoint Equations

The binder_datatype command’s syntax is inspired by Isabelle’s standard datatype command. Bound and free variables in binder datatypes are always left polymorphic. A custom name can be provided for the free variable operators. A type class on the type argument ensures that the type chosen is large enough for the size of the binder datatype, e.g., that it is at least countably infinite for finite syntax like lterm and at least uncountably infinite for iterm. The “at least” makes nesting binder datatypes in other potentially larger (e.g. uncountable) types easier as the variable type can be increased to match the size of the surrounding type.

The other major addition to the command’s syntax compared with standard datatypes are the binding annotations (inspired by Nominal Isabelle) and the subterm selectors. Normal datatypes allow to automatically define accessor functions using the fun_name::type syntax. For binder datatypes this syntax is repurposed and generalized to define the binding structure. A selector can not only appear on the top level (i.e. on a field of a constructor as in the $\mathsf{{Lm}}$ constructor in term) but also nested within other types (as in the $\mathsf{{Let}}$ constructor in term). Valid targets for the selectors are variable positions and (potentially mutually) recursive positions.

MrBNF translates the user specification into the pre-datatype, a non-recursive sum of products. Thereby, variable and recursive positions are separated based on whether they appear in a binding clause. Next to the free variables visible in the syntax (’var), the pre-datatype also has a bound variable position, and two recursive positions for recursive occurrences under a binder and not under a binder respectively. The iterm type’s pre-datatype is:

⬇

type_synonym (’var, ’bvar, ’rec, ’brec) pre_iterm = ’var (* free occurrence *)

+ (’rec * ’rec stream) (* recursive non-binding occurrences *)

+ (’bbar dstream * ’brec) (* bound and recursive bound occurrence *)

Next, MrBNF defines a “raw” standard datatype with a single constructor (which is completely free, i.e., not yet quotiented to $\alpha$ -equivalence):

⬇

datatype ’var raw_iterm =

ctor

{}_{\texttt{raw\_iterm}}

"(’var, ’var, ’var raw_iterm, ’var raw_iterm) pre_iterm"

For the above step as well as to prepare for the next steps in the construction of the binder datatype, the pre-datatype must form an MRBNF with free ${}^{\prime}\mathit{var}$ (setter $\mathsf{set}^{1}_{\texttt{pre\_iterm}}$ ), bound ${}^{\prime}\mathit{bvar}$ (setter $\mathsf{set}^{2}_{\texttt{pre\_iterm}}$ ), and live ${}^{\prime}\mathit{rec}$ (setter $\mathsf{set}^{3}_{\texttt{pre\_iterm}}$ ) and ${}^{\prime}\mathit{brec}$ (setter $\mathsf{set}^{4}_{\texttt{pre\_iterm}}$ ) positions – this is ensured by tracking the registered MRBNFs and automating their composition.

4.2 Composition of MRBNFs

The proof that a given type forms an MRBNF proceeds recursively via composition. For the individual components there are three cases to consider. If the type is a type-variable then return the identity MRBNF (live ${}^{\prime}a$ , $\mathit{T}_{\text{ID}}:={{}^{\prime}a}$ , $\mathsf{map}_{\text{ID}}:=\mathsf{{id}}:({{}^{\prime}a}\rightarrow{{}^{\prime}% a})\rightarrow{{}^{\prime}a}\rightarrow{{}^{\prime}a}$ , $\mathsf{rel}_{\text{ID}}:=\mathsf{{id}}:({{}^{\prime}a}\rightarrow{{}^{\prime}% a}\rightarrow\text{bool})\rightarrow{{}^{\prime}a}\rightarrow{{}^{\prime}a}% \rightarrow\text{bool}$ , and $\mathsf{set}_{\text{ID}}:=\lambda x.\;\{x\}:\rightarrow{{}^{\prime}a}% \rightarrow{{}^{\prime}a}\;\text{set}$ ). If the topmost type constructor is not known to be a (MR)BNF then return the constant MRBNF (dead ${}^{\prime}d$ , $\mathit{T}_{\text{CST}}:={{}^{\prime}d}$ , $\mathsf{map}_{\text{CST}}:=\mathsf{{id}}:{{}^{\prime}d}\rightarrow{{}^{\prime}d}$ , $\mathsf{rel}_{\text{CST}}:=(=):{{}^{\prime}d}\rightarrow{{}^{\prime}d}% \rightarrow\text{bool}$ ). Otherwise (i.e., the topmost type constructor is a MRBNF) recursively prove that its arguments are MRBNFs. Then do a composition step between the outer MRBNF and the inner MRBNFs.

Inspired by BNF composition [12], MRBNF composition is split into several phases. First step is demoting. All type-variables shared between the involved MRBNFs are demoted to the same mode. Given that modes can only become more specific (live > free > bound > dead), this will result in the lowest mode a variable is used at in any of the MRBNFs. If a type-variable appears under a type constructor that is not a (MR)BNF, it must be demoted to dead (using the constant MRBNF). The second step is lifting: new dummy type-variables are added to all MRBNFs to ensure that all involved MRBNFs have the same (modulo reordering) bound and free type-variables and all the inner MRBNFs have the same live type-variables (again modulo reordering). The third step is permuting: bring shared type variables into the same order in all involved MRBNFs. Finally, composition proceeds along the following definition:

Definition 1.

Given an outer MRBNF $\>(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{% \prime}}\beta})\>G$ where $|\overline{\vphantom{\gamma^{\prime}}\alpha}|=m$ and $|\overline{\vphantom{\gamma^{\prime}}\beta}|=n$ and inner MRBNFs $(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{% \prime}}\gamma})\>F_{1}\dots(\overline{\vphantom{\gamma^{\prime}}\alpha},% \overline{\vphantom{\gamma^{\prime}}\gamma})\>F_{n}$ where $|\overline{\vphantom{\gamma^{\prime}}\gamma}|=k$ , the composed MRBNF $(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{% \prime}}\gamma})\>H$ is given by:

\begin{array}[]{lcll}(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{% \vphantom{\gamma^{\prime}}\gamma})\>\text{T}_{\text{H}}&=&(\overline{\vphantom% {\gamma^{\prime}}\alpha},(\overline{\vphantom{\gamma^{\prime}}\alpha},% \overline{\vphantom{\gamma^{\prime}}\gamma})\>F_{1},\dots,(\overline{\vphantom% {\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{\prime}}\gamma})\>F_{n})% \>G\\ \mathsf{map}_{\text{H}}&=&\lambda\overline{\vphantom{\gamma^{\prime}}f}\>% \overline{\vphantom{\gamma^{\prime}}g}.\>\mathsf{map}_{G}\>\overline{\vphantom% {\gamma^{\prime}}f}\>(\mathsf{map}_{F_{1}}\>\overline{\vphantom{\gamma^{\prime% }}f}\>\overline{\vphantom{\gamma^{\prime}}g})\dots(\mathsf{map}_{F_{n}}\>% \overline{\vphantom{\gamma^{\prime}}f}\>\overline{\vphantom{\gamma^{\prime}}g}% )\\ &&\qquad:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\alpha)}% \rightarrow\overline{\vphantom{\gamma^{\prime}}(\gamma\rightarrow\gamma^{% \prime})}\rightarrow(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{% \vphantom{\gamma^{\prime}}\gamma})\>T_{H}\rightarrow(\overline{\vphantom{% \gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{\prime}}\gamma^{\prime}})% \>T_{H}\\ \mathsf{set}^{i\leq m}_{\text{H}}&=&\lambda x.\>\mathsf{set}^{i}_{G}\>x\cup% \bigcup\left(y\in\mathsf{set}^{m+1}_{G}\>x.\>\mathsf{set}^{i}_{F_{1}}\>y\right% )\cup\dots\cup\bigcup\left(y\in\mathsf{set}^{m+n}_{G}.\>\mathsf{set}^{i}_{F_{n% }}\>y\right)\\ &&\qquad:(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{% \gamma^{\prime}}\gamma})\>T_{H}\rightarrow\alpha_{i}\>\mathsf{set}\\ \mathsf{set}^{i>m}_{\text{H}}&=&\lambda x.\>\bigcup\left(y\in\mathsf{set}^{m+1% }_{G}\>x.\>\mathsf{set}^{i}_{F_{1}}\>y\right)\cup\dots\cup\bigcup\left(y\in% \mathsf{set}^{m+n}_{G}.\>\mathsf{set}^{i}_{F_{n}}\>y\right)\\ &&\qquad:(\overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{% \gamma^{\prime}}\gamma})\>T_{H}\rightarrow\gamma_{i-m}\>\mathsf{set}\\ \mathsf{rel}_{\text{H}}&=&\lambda\overline{\vphantom{\gamma^{\prime}}f}\>% \overline{\vphantom{\gamma^{\prime}}R}.\>\mathsf{rel}_{G}\>\overline{\vphantom% {\gamma^{\prime}}f}\>(\mathsf{rel}_{F_{1}}\>\overline{\vphantom{\gamma^{\prime% }}f}\>\overline{\vphantom{\gamma^{\prime}}R})\dots(\mathsf{rel}_{F_{n}}\>% \overline{\vphantom{\gamma^{\prime}}f}\>\overline{\vphantom{\gamma^{\prime}}R}% )\\ &&\qquad:\overline{\vphantom{\gamma^{\prime}}(\alpha\rightarrow\alpha)}% \rightarrow\overline{\vphantom{\gamma^{\prime}}(\gamma\rightarrow\gamma^{% \prime}\rightarrow\text{bool})}\rightarrow(\overline{\vphantom{\gamma^{\prime}% }\alpha},\overline{\vphantom{\gamma^{\prime}}\gamma})\>T_{H}\rightarrow(% \overline{\vphantom{\gamma^{\prime}}\alpha},\overline{\vphantom{\gamma^{\prime% }}\gamma^{\prime}})\>T_{H}\rightarrow\text{bool}\\ \end{array}

4.3 Fixpoint and Quotienting Constructions

Next, MrBNF automates Blanchette et al. [10] definition of free variables, permutation and $\alpha$ -equivalence on the raw datatype. Free variables are defined via an inductive predicate $\mathsf{free}$ that specifies if a variable $x$ is free in a term $t$ , here shown on our running example iterm.

The $\mathsf{FV}_{\texttt{raw\_iterm}}$ function is then defined as $\lambda t.\>\{a.\;\mathsf{free}\>a\>x\}$ . One also defines a primitive recursive function $\mathsf{permute}$ that takes an permutation on the variable position and applies it to all variables (bound and free). This function uses the map function of the pre-datatype: $\mathsf{permute}\>\sigma\>(\mathsf{ctor}_{\texttt{raw\_iterm}}\>x)=\mathsf{% ctor}_{\texttt{raw\_iterm}}\>(\mathsf{map}_{\texttt{pre\_iterm}}\;\sigma\;% \sigma\;(\mathsf{permute}\>\sigma)\;(\mathsf{permute}\>\sigma)\;x)$ . Equipped with these two functions, alpha-equivalence is defined inductively as follows:

MrBNF proves $\mathsf{alpha}_{\texttt{iterm}}$ to be an equivalence relation and uses it to define a quotient of the raw datatype. The constructor, free variable and permutation operators are lifted from the raw datatype to the quotient. The lifted constructor $\mathsf{ctor}_{\texttt{iterm}}$ is used to define the high-level constructors $\mathsf{{iVr}}$ , $\mathsf{{iAp}}$ , and $\mathsf{{iLm}}$ , and to prove all the high-level theorems illustrated in §3.

MrBNF actually implements a mild generalization of Blanchette et al. [10]’s fixpoint construction, which only allows to bind variables in recursive subterms. However, sometimes it is necessary to bind variables that appear free in another (non-recursive) type occurrence. To solve this issue in the pre-datatype, instead of just having positions for free and bound type-variables, we also introduce a hybrid called bfree type-variables. Then, alpha-equivalence ensures that the portion of bfree variables that appear bound is appropriately renamed.

4.4 Recursion

MrBNF also implements Blanchette et al.’s binding-aware recursion principle [10]. To define a recursive function from a binding-aware datatype $\overline{\alpha}\;T$ of free type-variables $\overline{\alpha}$ to some other $\overline{\alpha}$ -type $\overline{\alpha}\>U$ , one needs: (1) a parameter structure consisting of a type $\overline{\alpha}\;P$ , a permutation $\textit{Pmap}:\overline{\alpha\rightarrow\alpha}\rightarrow\overline{\alpha}\;% P\rightarrow\overline{\alpha}\;P$ and support operators $\textit{PVars}_{i}:\overline{\alpha}\;P\rightarrow\alpha_{i}\;\mathsf{set}$ , and (2) a model consisting of a type $\overline{\alpha}\;U$ , permutation, and support operators similar to the parameter structure as well as an algebra structure encoding the recursive behavior of the all the constructors, $\textit{Uctor}:\left(\overline{\alpha},\overline{\overline{\alpha}\>T\times(% \overline{\alpha}\>P\rightarrow\overline{\alpha}\>U)}\right)\,\textit{pre\_T}% \rightarrow\overline{\alpha}\>P\rightarrow\overline{\alpha}\>U$ , where pre_T is the pre-datatype of $T$ .

We introduce a precursor of our recursor on raw terms, which applies Uctor recursively while suitably permuting bound variables “out of the way” with regard to the parameter structure. Suitably means that the “out of the way” function $f$ returns a permutation that does not change the frees and makes bounds disjoint from the frees. For iterm, suitable is defined as:

\begin{array}[]{l}\mathsf{suitable}_{\texttt{iterm}}\>f\mathrel{=}\forall x\>p% .\>\mathsf{{perm}}\>(f\>x\>p)\>\wedge\\ \qquad\mathsf{imsupp}\>(f\>x\>p)\cap\left((\mathsf{FV}_{\texttt{iterm}}\>(% \mathsf{ctor}_{\texttt{iterm}}\>x)\cup\mathsf{PVars}\>p)\setminus\mathsf{set}^% {2}_{\texttt{pre\_iterm}}\>x\right)=\varnothing\>\wedge\\ \qquad f\>x\>p\mathrel{\text{\textasciigrave}}\mathsf{set}^{2}_{\texttt{pre\_% iterm}}\>x\cap(\mathsf{FV}_{\texttt{iterm}}\>(\mathsf{ctor}_{\texttt{iterm}}\>% x)\cup\mathsf{PVars}\>p)=\varnothing\end{array}

Here, $\mathsf{imsupp}\;f=\mathsf{{supp}}\;f\cup f\mathrel{\text{\textasciigrave}}% \mathsf{{supp}}\;f$ . As the precursor must permute the bound variables, it is not possible to define it using primitive recursion. Instead, we use well-founded recursion via an auxiliary $\mathsf{subshape}$ relation, which provides the necessary wiggle room:

We obtain the definition of the precursor $\mathsf{rec}_{U}$ for a suitable “out of the way” function $f$ :

\begin{array}[]{@{}l@{}}\mathsf{rec}_{U}\>f\>(\mathsf{ctor}_{\texttt{raw\_% iterm}}\>x)\>p=\text{if}\;\lnot\mathsf{suitable}_{\texttt{iterm}}\>f\>\text{% then}\>\mathsf{undefined}\>\text{else}\>\mathit{Uctor}\\ \quad(\mathsf{map}_{\texttt{pre\_iterm}}\>\text{id}\>(f\>x\>p)\>((\lambda t.\>% (t,\mathsf{rec}_{U}\>f\>t))\circ\mathsf{permute}_{\texttt{raw\_iterm}}\>(f\>x% \>p))\>(\lambda t.\>(t,\mathsf{rec}_{U}\>f\>t))\>x)\>p\end{array}

The main lemma that the package proves is that the precursor commutes with permutation, it returns the same result for alpha-equivalent terms, and that the specific choice of the “out of the way” function is irrelevant. These properties must be proved simultaneously by induction on the binder datatype using the induction scheme associated with the subshape relation:

\begin{array}[]{@{}l@{}}\mathsf{suitable}_{\texttt{iterm}}\>f\Longrightarrow% \mathsf{suitable}_{\texttt{iterm}}\>f^{\prime}\Longrightarrow\mathsf{{perm}}\>% \sigma\Longrightarrow\mathsf{alpha}_{\texttt{iterm}}\>t\>t^{\prime}% \Longrightarrow\\ \mathsf{rec}_{U}\>f\>(\mathsf{permute}_{\texttt{raw\_iterm}}\>\sigma\>t)\>p=% \mathit{Umap}\>\sigma\>\left(\mathsf{rec}_{U}\>f\>t\>(\mathsf{Pmap}\>\sigma^{-% 1}\>p)\right)\wedge\mathsf{rec}_{U}\>f\>t\>p=\mathsf{rec}_{U}\>f^{\prime}\>t^{% \prime}\>p\end{array}

To move towards the binding-aware recursor, we use Hilbert Choice to hide the “out of the way” function by choosing an arbitrary suitable one $\mathsf{rrec}_{U}\mathrel{=}\mathsf{rec}_{U}\>(\varepsilon f.\>\mathsf{% suitable}_{\texttt{iterm}}\>f)$ .

The invariance of the precursor under alpha is needed to lift it from the raw type to the quotient type. The definition of the precursor is used to derive a better simplification rule that hides the permuting function. This rule requires that the top-level bound variables are disjoint from the parameter structure and from the free variables. We then use identity as the “out of the way” function on the top level and an arbitrary suitable function in the recursion.

\begin{array}[]{@{}l@{}}\mathsf{set}^{2}_{\texttt{pre\_iterm}}\>x\cap\left(% \mathsf{set}^{1}_{\texttt{pre\_iterm}}\>x\cup(\textstyle\bigcup_{z\in\mathsf{% set}^{3}_{\texttt{pre\_iterm}}\>x}\mathsf{FV}_{\texttt{iterm}}\>z)\cup\mathsf{% PVars}\>p\right)=\varnothing\Longrightarrow\\ \mathsf{rrec}_{U}\>(\mathsf{ctor}_{\texttt{raw\_iterm}}\>x)\>p=\mathsf{Uctor}% \>\left(\mathsf{map}_{\texttt{pre\_iterm}}\>\mathsf{{id}}\>\mathsf{{id}}\>(% \lambda t.\>(t,\mathsf{rrec}_{U}\>t))\>(\lambda t.\>(t,\mathsf{rrec}_{U}\>t))% \>x\right)\>p\end{array}

Relativized Recursion.

The above is a slightly simplified version of our recursion facilities. To accommodate situations where the domain of parameters or the target domain for the intended recursion function do not make up the entire types but only certain subsets, MrBNF allows the user to optionally provide predicates $\mathsf{valid}_{P}:\overline{\alpha}\;P\rightarrow\text{bool}$ and $\mathsf{valid}_{U}:\overline{\alpha}\;U\rightarrow\text{bool}$ that restrict these domains – while producing proof obligations that the user-provided parameter-structure and recursor-model operators preserve these predicates, and producing recursor clauses relativized to these predicates. For normal datatypes such a feature would be useless, as there are no proof obligations incurred for recursion. But for binding datatypes this is useful, since organizing the entire type as a parameter structure or a recursor model (so that the proof obligations can be discharged) is often difficult or awkward. An example of leveraging the $\mathsf{valid}_{P}$ flexibility is if the user prefers to define substitution using actual functions subject to the small-support requirement, as opposed to defining a subtype corresponding to this requirement ( $\mathsf{substFun}$ at the end of §3.2). In §5, we show an example that leverages the $\mathsf{valid}_{U}$ flexibility.

5 Application I: Mazza’s Isomorphism

In his work on connecting the meta-theory of $\lambda$ -calculus with the notion of metric completion, Mazza [22] establishes an isomorphic translation between standard $\lambda$ -calculus (using the lterm syntax in §3.2) and a (uniform affine) infinitary $\lambda$ -calculus (the iterm syntax from §3.3). We show our formalization using MrBNF of some key constructions in his development.

Recall that the type-variable for the lterm type constructor must be infinite (since $\mathsf{bound}_{\text{{lterm\>}}}=\aleph_{0}$ ), and the one for iterm must be uncountably infinite (since $\mathsf{bound}_{\text{{iterm}}}=\aleph_{1}$ ). In what follows, we fix these type-variables, namely fix a countable type var (a copy of nat) and an uncountable type ivar; we will refer to the elements of ivar as ivariables. We will simply write lterm instead of var lterm and iterm instead of ivar iterm.

Following Mazza, we choose a countable set $\mathsf{Spr}:(\text{var}\;\text{dstream\>})\;\text{set}$ of distinct streams of variables called supervariables, having the property that any two are mutually disjoint: $\forall\mathit{xs},\mathit{ys}\in\mathsf{Spr}.\;\mathsf{{sset}}\;\mathit{xs}\,% \cap\,\mathsf{{sset}}\;\mathit{ys}=\emptyset$ . The intention is restricting the $\lambda$ -iterms to only use these as bindings. Moreover, we choose a function $\mathsf{spr}:\text{var}\rightarrow(\text{var}\;\text{dstream\>})\;\text{set}$ for which $\mathsf{bij\_betw}\;\mathsf{spr}\;(\mathsf{{UNIV}}:\text{var}\;\text{set})\;% \mathsf{Spr}$ holds, i.e., $\mathsf{spr}$ is a bijection between variables and supervariables; we write $\mathsf{spr}^{-1}:(\text{var}\;\text{dstream\>})\;\text{set}\rightarrow\text{var}$ for its inverse. We refer to the elements of nat list as positions, and choose a bijection $\mathsf{natOf}:\text{{nat}}\;\text{list}\rightarrow\text{{nat}}$ . For $p:\text{{nat}}\;\text{list}$ and $n:\text{{nat}}$ , $p\cdot n$ denotes the concatenation of $p$ and $[n]$ . According to Mazza’s definition, the finitary-to-infinitary translation should be a function $\llbracket\_\rrbracket_{\_}:\text{{lterm\>}}\rightarrow\text{{nat}}\;\text{% list}\rightarrow\text{{iterm}}$ given by: (1) $\llbracket\mathsf{{Vr}}\;x\rrbracket_{p}=\mathsf{{iVr}}\;((\mathsf{spr}\;x)_{% \mathsf{natOf}\;p})$ ; (2) $\llbracket\mathsf{{Lm}}\;x\;t\rrbracket_{p}=\mathsf{{iLm}}\;(\mathsf{spr}\;x)% \;\llbracket t\rrbracket_{p}$ ; and (3) $\llbracket\mathsf{{Ap}}\;t_{1}\;t_{2}\rrbracket_{p}=\mathsf{{iAp}}\;\llbracket t% _{1}\rrbracket_{p\cdot 0}\,(\llbracket t_{2}\rrbracket_{p\cdot 1},\llbracket t% _{2}\rrbracket_{p\cdot 2},\llbracket t_{2}\rrbracket_{p\cdot 3},\ldots)$ .

The intuition is that every variable $x$ in the original term is duplicated in the translation into countably many ivariable “copies” of it sourced from its corresponding supervariable, $\mathsf{spr}\;x$ . The positions make sure that the copies located in different parts of the resulting iterm are distinct, thus ensuring that the iterm is affine. Indeed, in the recursive case for application, we see that the position $p$ grows with different numbers appended to the arguments of infinitary application, which ensures disjointness in conjunction with choosing the particular “copy” based on this position counter ( $\mathsf{natOf}\;p$ ) when reaching the $\mathsf{{Vr}}$ -leaves. Correspondingly, abstraction over a variable is translated to abstraction over its supervariable, i.e., over all its “copies”.

Moreover, to describe the image of this translation, Mazza defines the notion of renaming equivalence expressed as the relation $\approx\;:\text{{iterm}}\rightarrow\text{{iterm}}\rightarrow\text{bool}$ defined inductively in Fig. 1. It relates two $\lambda$ -iterms $t$ and $t^{\prime}$ just in case they (i) have the same $(\mathsf{{iVr}},\mathsf{{iLm}},\mathsf{{iAp}})$ -structure (as trees), (ii) only use supervariables in binders, (iii) at the leaves have variables appearing in the same supervariable, and (iv) for both $t$ and $t^{\prime}$ all the subterms that form the righthand side of an application are mutually renaming equivalent. Then uniformity of an iterm, which will characterize the translation’s image, is self-renaming-equivalence: $\mathsf{uniform}\;t=(t\approx t)$ .

$\displaystyle\frac{\mathit{xs}\in\mathsf{Spr}\hskip 8.61108pt\{x,x^{\prime}\}% \subseteq\mathsf{{sset}}\;\mathit{xs}}{\mathsf{{iVr}}\;x\,\approx\,\mathsf{{% iVr}}\;x^{\prime}}$ iVr $\displaystyle\frac{\mathit{xs}\in\mathsf{Spr}\hskip 17.22217ptt\approx t^{% \prime}}{\mathsf{{iLm}}\;xs\;t\,\approx\,\mathsf{{iLm}}\;xs\;t^{\prime}}$ iLm

$\displaystyle\frac{\begin{array}[]{c}t\approx t^{\prime}\hskip 25.83325pt% \forall t_{1},t_{2}.\;\{t_{1},t_{2}\}\subseteq\mathsf{{sset}}\;\mathit{ts}\cup% \mathsf{{sset}}\;\mathit{ts}^{\prime}\longrightarrow t_{1}\approx t_{2}\end{% array}}{\mathsf{{iAp}}\;t\;\mathit{ts}\,\approx\,\mathsf{{iAp}}\;t^{\prime}\;% \mathit{ts}^{\prime}}$ iAp

Figure 1: Renaming equivalence relation.

We aim to define a function satisfying clauses (1)–(3) above, with (2) formally written as $\mathsf{{iAp}}\;\llbracket t_{1}\rrbracket_{p\cdot 0}\,(\mathsf{{smap}}\;% \llbracket t_{2}\rrbracket_{p\cdot\_}\;(\mathsf{natsFrom}\;1))$ where, for any $n$ , $\mathsf{natsFrom}\;n$ denotes the stream of naturals starting from $n$ . To turn these clauses into a formal definition, we deploy our recursor for lterm , which requires also indicating the desired interaction between the to-be-defined function with permutation and free-variables. Upon analysis, we converge to (4) $\llbracket t[\sigma]\rrbracket_{p}=\llbracket t\rrbracket_{p}[\mathsf{{v2iv}}% \,\sigma]$ and (5) $\mathsf{spr}^{-1}\mathrel{\text{\textasciigrave}}\mathsf{touched}\;\llbracket t% \rrbracket_{p}\subseteq\mathsf{{FV}}\;t$ , where $\mathsf{{v2iv}}\,\sigma$ (read “variable to ivariable”) converts $\sigma:\mathit{var}\rightarrow\mathit{var}$ , via $\mathsf{spr}$ , into a supervariable-preserving function; namely, for any $y\in\mathit{ivar}$ such that $y$ appears in some (necessarily unique) supervariable $\mathit{xs}$ , we define $\mathsf{{v2iv}}\,\sigma\;y:\mathit{ivar}$ as $(\mathsf{spr}\;(\sigma\;(\mathsf{spr}^{-1}\,\mathit{xs})))_{i}$ for the unique $i$ such that $\mathit{xs}_{i}=y$ ; and $\mathsf{touched}\;t$ is the set of all supervariables that are touched by (the free variables of) $t$ , namely $\{\mathit{xs}\in\mathsf{Spr}\mid\mathsf{{sset}}\;\mathit{xs}\,\cap\,\mathsf{{% FV}}\;t\not=\emptyset\}$ .

Equation (4) above is seen to be intuitive if we remember that the translation sends variables to supervariables, which means that bijections $\sigma$ between variables naturally correspond to bijections between supervariables, hence (thanks to the supervariables being mutually disjoint) to supervariable-structure preserving bijections between ivariables; therefore indeed (A) applying a bijection on variables and then translating should be the same as (B) first translating and then applying this corresponding bijection of its ivariable “copies” in the translation. As for the above inclusion (5), we obtained it by adjunction from $\mathsf{touched}\;\llbracket t\rrbracket_{p}\subseteq\mathsf{spr}\mathrel{% \text{\textasciigrave}}\mathsf{{FV}}\;t$ , which is again intuitive if we think in terms of the variable-supervariable correspondence.

Clauses (1)–(5) give us a structure on the intended codomain of $\llbracket\_\rrbracket_{\_}$ , $\text{{nat}}\;\text{list}\rightarrow\text{{iterm}}$ , using the recipe sketched at the end of §3.2. However, for these to give us an lterm -model, we must restrict the codomain to include only those functions $f:\text{{nat}}\;\text{list}\rightarrow\text{{iterm}}\,$ whose image consists of renaming-equivalent items only – otherwise the model properties do not hold; this is not suprising, since Mazza’s translation’s goal is to produce uniform iterms. We therefore employ the codomain-relativized recursion discussed at the end of §4.4, obtaining:

Prop 7.

There exists a unique function $\llbracket\_\rrbracket_{\_}:\text{{lterm\>}}\rightarrow\text{{nat}}\;\text{% list}\rightarrow\text{{iterm}}$ such that clauses (1)–(5) hold, and in addition $\forall p,q.\;\llbracket t\rrbracket_{p}\approx\llbracket t\rrbracket_{q}$ ; in particular, $\forall p.\;\mathsf{uniform}\;\llbracket t\rrbracket_{p}$ .

For the opposite translation $\llparenthesis\hskip 0.86108pt\_\hskip 0.86108pt\rrparenthesis$ (from infinitary back to finitary terms), Mazza writes equations that in our notation look as follows, restricting the domain to uniform iterms:
(1) $\llparenthesis\hskip 0.86108pt\mathsf{{iVr}}\;\mathit{xs}_{i}\hskip 0.86108pt% \rrparenthesis=\mathsf{{Vr}}\,(\mathsf{spr}^{-1}\,\mathit{xs})$ ; (2) $\llparenthesis\hskip 0.86108pt\mathsf{{iLm}}\;\mathit{xs}\;t\hskip 0.86108pt% \rrparenthesis=\mathsf{{Lm}}\;(\mathsf{spr}^{-1}\,\mathit{xs})\;\llparenthesis% \hskip 0.86108ptt\hskip 0.86108pt\rrparenthesis$ ; (3) $\llparenthesis\hskip 0.86108pt\mathsf{{iAp}}\;t\;\mathit{ts}\hskip 0.86108pt% \rrparenthesis=\mathsf{{Ap}}\;\llparenthesis\hskip 0.86108ptt\hskip 0.86108pt% \rrparenthesis\;\llparenthesis\hskip 0.86108pt\mathit{ts}_{0}\hskip 0.86108pt\rrparenthesis$ .

With the help of a custom recursor for a suitable superset of the uniform iterms, again adding clauses for permuation and free variables, we are able to prove:

Prop 8.

There exists a function $\llparenthesis\hskip 0.86108pt\_\hskip 0.86108pt\rrparenthesis:\text{{iterm}}% \rightarrow\text{{lterm\>}}$ satisfying the above clauses (1)–(3) when resticted to uniform iterms (i.e., assuming $\mathsf{{iVr}}\;\mathit{xs}_{i}$ , $\mathsf{{iLm}}\;\mathit{xs}\;t$ and $\mathsf{{iAp}}\;t\;\mathit{ts}$ are uniform), and such that $\llbracket\_\rrbracket$ ’s restriction to uniform iterms is uniquely determined by these properties.

Mazza’s main result consists of a sequence of five statements, three of which refer to the syntactic component of the finitary-infinitary isomorphism.

Prop 9.

The following hold: (1) (Lemma 16 from [22]) $t\approx t\longrightarrow\llparenthesis\hskip 0.86108ptt\hskip 0.86108pt% \rrparenthesis=\llparenthesis\hskip 0.86108ptt^{\prime}\hskip 0.86108pt\rrparenthesis$ .
(2) (Thm. 19(1) from [22]) $\llparenthesis\hskip 0.86108pt\llbracket s\rrbracket_{p}\hskip 0.86108pt% \rrparenthesis=s$ . (3) (Thm. 19(2) from [22]) $\mathsf{uniform}\;t\longrightarrow\llbracket\llparenthesis\hskip 0.86108ptt% \hskip 0.86108pt\rrparenthesis\rrbracket_{p}\approx t$ .

The theorem states that, for any position $p$ , $\llbracket\_\rrbracket$ and $\llparenthesis\hskip 0.86108pt\_\hskip 0.86108pt\rrparenthesis_{p}$ give mutually inverse bijections between terms and equivalence classes of uniform iterms w.r.t. renaming equivalence. An additional lemma (omitted here) shows that the $\approx$ -representative produced by $\llparenthesis\hskip 0.86108pt\_\hskip 0.86108pt\rrparenthesis_{p}$ is affine (i.e., has no repeated variables). Thus the result establishes a syntactic isomorphism, up to renaming equivalence, between terms and uniform affine iterms. Mazza’s isomorphism also has an operational-semantics component, given by a theorem stating that $\llbracket\_\rrbracket$ and $\llparenthesis\hskip 0.86108pt\_\hskip 0.86108pt\rrparenthesis_{p}$ preserve $\beta$ -reduction in both calculi in a manner that matches the number of reduction steps [22, Thm. 19(3,4)]. We omit this result here, but details can be found in our formalization [44].

6 Application II: POPLmark Challenge

We report on our solution to the Part 2 of the POPLmark challenge [4], which is concerned with the type soundness of System F_<:; our formalization also solves Part 1, which is concerned with subtyping. We work with the System F_<: types and terms we have introduced in §3.4. With our setup that enforces the variable convention in all induction proofs, the formalization becomes a routine exercise: we can follow the formalization document and transcribe auxiliary lemmas and their proofs. We show our core definitions of Part 2. Naturally, they rely on some definitions of Part 1 (notably the subtyping relation) and other basic infrastructure (notably contexts modeled as lists); we refer to our formalization for full details [44].

We start with the typing judgments for patterns and terms:

⬇

inductive pat_typing ("

\vdash

_ : _

\rightarrow

_" [30,29,30] 30) where

PTPVr: "

\vdash

PVr x T : T

\rightarrow

\varnothing

, Inr x <: T"

| PTPRec: "nonrep_PRec PP

\Longrightarrow

labels PP = labels TT

\Longrightarrow

(

\forall

l P T. (l, P)

\in\in

PP

\longrightarrow

(l, T)

\in\in

TT

\longrightarrow

\vdash

P : T

\rightarrow

\Delta

l)

\Longrightarrow

\vdash

PRec PP : TRec TT

\rightarrow

concat (map

\Delta

(labelist TT))"

inductive typing ("_

\vdash

_ : _" [30,29,30] 30) where

TVr: "

\vdash

\Gamma

OK

\Longrightarrow

(Inr x, T)

\in

set

\Gamma

\Longrightarrow

\Gamma

\vdash

Vr x : T"

| TLm: "

\Gamma

, Inr x <: T1

\vdash

t : T2

\Longrightarrow

\Gamma

\vdash

Lm x T1 t : Arr T1 T2"

| TAp: "

\Gamma

\vdash

t1 : Arr T11 T12

\Longrightarrow

\Gamma

\vdash

t2 : T11

\Longrightarrow

\Gamma

\vdash

App t1 t2 : T12"

| TLmT: "

\Gamma

, Inl X <: T1

\vdash

t : T2

\Longrightarrow

\Gamma

\vdash

LmT X T1 t : All X T1 T2"

| TApT: "

\Gamma

\vdash

t1 : All X T11 T12

\Longrightarrow

proj_ctxt

\Gamma

\vdash

T2 <: T11

\Longrightarrow

\Gamma

\vdash

ApT t1 T2 : substT (TVr(X := T2)) T12"

| TSub: "

\Gamma

\vdash

t : S

\Longrightarrow

proj_ctxt

\Gamma

\vdash

S <: T

\Longrightarrow

\Gamma

\vdash

t : T"

| TRec: "

\vdash

\Gamma

OK

\Longrightarrow

rel_lfset id (

\lambda

t T.

\Gamma

\vdash

t : T) XX TT

\Longrightarrow

\Gamma

\vdash

Rec XX : TRec TT"

| TProj: "

\Gamma

\vdash

t : TRec TT

\Longrightarrow

(l, T)

\in\in

TT

\Longrightarrow

\Gamma

\vdash

Proj t l : T"

| TLet: "

\Gamma

\vdash

t : T

\Longrightarrow

\vdash

P : T

\rightarrow

\Delta

\Longrightarrow

\Gamma

,

\Delta

\vdash

u : U

\Longrightarrow

\Gamma

\vdash

Let P t u : U"

All rules follow closely the challenge description [4]. A few rules deserve some explanation. Rules TVr and TRec assume that the context is well-scoped ( $\vdash\nobreak\ \Gamma\nobreak\ \mathtt{OK}$ ); other rules preserve this invariant inductively. Rule TRec uses the relator rel_lfset to relate the values in two lfsets pairwise grouped by label. Rule TApT uses the parallel substitution function on System F_<: types (substT), which we define using our recursor. Rule PTPRec assumes that the destructed record pattern is nonrepetitive (nonrep_PRec); it also writes $\in\in$ for membership in lfset and constructs the resulting context by sorting the finite set of labels lexicographically (labelist).

We next define matching and the evaluation function for the terms.

⬇

inductive match for

\sigma

where

MPVr: "

\sigma

X = v

\Longrightarrow

match

\sigma

(PVr X T) v"

| MPRec: "nonrep_PRec PP

\Longrightarrow

labels PP

\subseteq

labels VV

\Longrightarrow

(

\forall

l P v. (l, P)

\in\in

PP

\longrightarrow

(l, v)

\in\in

VV

\longrightarrow

match

\sigma

P v)

\Longrightarrow

match

\sigma

(PRec PP) (Rec VV)"

definition "restrict

\sigma

A x = (if x

\in

A then

\sigma

x else Vr x)"

inductive step where

ApLm: "value v

\Longrightarrow

step (Ap (Lm x T t) v) (subst (Vr(x := v)) TVr t)"

| ApTLmT: "step (ApT (LmT X T t) T2) (subst Vr (TVr(X := T2)) t)"

| LetV: "value v

\Longrightarrow

match

\sigma

P v

\Longrightarrow

step (Let P v u) (subst (restrict

\sigma\!

(PV p)) TVr u)"

| ProjRec: "

\forall

v

\in

values VV. value v

\Longrightarrow

(l, v)

\in\in

VV

\Longrightarrow

step (Proj (Rec VV) l) v"

| ApCong1: "step t t’

\Longrightarrow

step (Ap t u) (Ap t’ u)"

| ApCong2: "value v

\Longrightarrow

step t t’

\Longrightarrow

step (Ap v t) (Ap v t’)"

| ApTCong: "step t t’

\Longrightarrow

step (ApT t T) (ApT t’ T)"

| ProjCong: "step t t’

\Longrightarrow

step (Proj t l) (Proj t’ l)"

| RecCong: "step t t’

\Longrightarrow

(l, t)

\in\in

XX

\Longrightarrow

step (Rec XX) (Rec (XX

\langle

l := t’

\rangle

))"

| LetCong: "step t t’

\Longrightarrow

step (Let P t u) (Let P t’ u)"

Similar to Berghofer’s solution [8], we use a matching predicate rather than a (partial) function that computes the matching substitution. The rules ApLm, ApTLmT, LetV, and ProjRec implement actual transitions; the remaining rules of step are congruence rules navigating to allowed redexes. We prefer this formulation over an equivalent context-based one, because the congruence steps are in all cases the easy cases of the involved induction proofs. The rules ApLm, ApTLmT, LetV use the parallel substitution subst, which we again define using our recursor. This substitution function acts both on term variables (first argument) and type variables (second argument). We then prove the main results: progress and preservation.

⬇

lemma progress: "

\varnothing

\vdash

t : T

\Longrightarrow

value t

\lor

(

\exists

t’. step t t’)"

lemma preservation: : "

\Gamma

\vdash

t : T

\Longrightarrow

step t t’

\Longrightarrow

\Gamma

\vdash

t’ : T"

The proofs are canonical following the challenge description [4]. We pervasively use binding-aware induction on our datatypes but also on the shown inductive predicates, which has recently been developed in Isabelle by van Brügge et al. [43]. Occasionally we use induction even in places where a case distinction would have sufficed: this is because our tool lacks case distinction theorems following the variable convention. One omission in the challenge’s pen-and-paper proof, which has been also noted by Berghofer [8], is the following lemma, crucial for progress, about the existence of matching substitutions for well-typed patterns.

⬇

lemma pat_typing_ex_match:

\vdash

P : T

\rightarrow

\Delta

\Longrightarrow

\varnothing

\vdash

v : T

\Longrightarrow

value v

\Longrightarrow

\exists\sigma

. match

\sigma

P v

7 Conclusion

MrBNF is a new definitional package in Isabelle/HOL for defining binding-aware datatypes. It follows a modular approach to datatypes relying on the notion of MRBNF as infrastructure to refer to free, bound, and recursive occurrences in a syntax declaration. It comprises 20 000 lines of Standard ML. While some of its usability edges are still rough, our case studies suggest that MrBNF can be a cornerstone in mechanized developments, pushing the boundaries of nominal techniques. We are currently proceeding to polish MrBNF’s rough edges, which involves providing a high-level interface to the recursor, automating the non-repetitiveness construction (linear_type), and providing variable-avoiding case distinction rules and a proof method to apply them effectively. At the same time, we are extending MrBNF’s scope to binding-aware codatatypes, which will have applications such as Böhm trees [6].

References

[1] Submitted solutions to the POPLmark challenge. https://www.seas.upenn.edu/˜plclub/poplmark/, accessed March 22, 2025, 2005.
[2] Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt. HO $\pi$ in Coq. J. Autom. Reason., 65(1):75–124, 2021. doi:10.1007/S10817-020-09553-0.
[3] Michael Ashley-Rollman, Karl Crary, and Robert Harper. Group from CMU’s solution to the POPLmark challenge. https://www.seas.upenn.edu/˜plclub/poplmark/cmu.html, accessed March 22, 2025, 2005.
[4] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLMark challenge. In Joe Hurd and Thomas F. Melham, editors, TPHOLs 2005, volume 3603 of LNCS, pages 50–65. Springer, 2005. doi:10.1007/11541868_4.
[5] David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. J. Formaliz. Reason., 7(2):1–89, 2014. doi:10.6092/ISSN.1972-5787/4650.
[6] Hendrik Pieter Barendregt. The lambda calculus – its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.
[7] Jesper Bengtson and Joachim Parrow. Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci., 5(2), 2009. URL: http://arxiv.org/abs/0809.3960.
[8] Stefan Berghofer. A solution to the POPLMark challenge using de Bruijn indices in Isabelle/HOL. J. Autom. Reason., 49(3):303–326, 2012. doi:10.1007/S10817-011-9231-4.
[9] Stefan Berghofer and Christian Urban. A head-to-head comparison of de Bruijn indices and names. In Alberto Momigliano and Brigitte Pientka, editors, LFMTP 2006, volume 174 of ENTCS, pages 53–67. Elsevier, 2006. doi:10.1016/J.ENTCS.2007.01.018.
[10] Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. Proc. ACM Program. Lang., 3(POPL):22:1–22:34, 2019. doi:10.1145/3290335.
[11] Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 93–110. Springer, 2014. doi:10.1007/978-3-319-08970-6_7.
[12] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 111–127. Springer, 2014. doi:10.1007/978-3-319-08970-6_8.
[13] Joachim Breitner. Formally proving a compiler transformation safe. In Ben Lippmeier, editor, Haskell Symposium 2015, pages 35–46. ACM, 2015. doi:10.1145/2804302.2804312.
[14] Matthias Brun and Dmitriy Traytel. Generic authenticated data structures, formally. In John Harrison, John O’Leary, and Andrew Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 10:1–10:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPICS.ITP.2019.10.
[15] Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363–408, 2012. doi:10.1007/s10817-011-9225-2.
[16] Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Nachum Dershowitz and Andrei Voronkov, editors, LPAR 2007, volume 4790 of LNCS, pages 211–225. Springer, 2007. doi:10.1007/978-3-540-75560-9_17.
[17] N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381–392, 1972. doi:10.1016/1385-7258(72)90034-0.
[18] Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341–363, 2002. doi:10.1007/s001650200016.
[19] Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. In LICS 1987, pages 194–204. IEEE Computer Society, 1987.
[20] Gérard P. Huet. Residual theory in lambda-calculus: A formal development. J. Funct. Program., 4(3):371–394, 1994. doi:10.1017/S0956796800001106.
[21] Brian Huffman and Christian Urban. A new foundation for Nominal Isabelle. In Matt Kaufmann and Lawrence C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 35–50. Springer, 2010. doi:10.1007/978-3-642-14052-5_5.
[22] Damiano Mazza. An infinitary affine lambda-calculus isomorphic to the full lambda-calculus. In LICS 2012, pages 471–480. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.57.
[23] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Henrik Nilsson, editor, Haskell Workshop 2004, pages 1–9. ACM, 2004. doi:10.1145/1017472.1017477.
[24] Alberto Momigliano, S.J. Ambler, and R.L. Crole. A comparison of formalizations of the meta-theory of a language with variable bindings in Isabelle. In TPHOLs 2001, Supplemental Proceedings, pages 267–282, 2001. URL: https://www.inf.ed.ac.uk/publications/online/0046/b267.pdf.
[25] Tobias Nipkow. More Church-Rosser proofs. J. Autom. Reason., 26(1):51–66, 2001. doi:10.1023/A:1006496715975.
[26] Michael Norrish. Recursive function definition for types with binders. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, TPHOLs 2004, volume 3223 of LNCS, pages 241–256. Springer, 2004. doi:10.1007/978-3-540-30142-4_18.
[27] Michael Norrish and René Vestergaard. Proof pearl: De Bruijn terms really do work. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, volume 4732 of LNCS, pages 207–222. Springer, 2007. doi:10.1007/978-3-540-74591-4_16.
[28] Lawrence C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363–397, 1989. doi:10.1007/BF00248324.
[29] Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reason., 55(1):1–37, 2015. doi:10.1007/s10817-015-9322-8.
[30] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Richard L. Wexelblat, editor, PLDI 1988, pages 199–208. ACM, 1988. doi:10.1145/53990.54010.
[31] Frank Pfenning and Carsten Schürmann. System description: Twelf – A meta-logical framework for deductive systems. In Harald Ganzinger, editor, CADE 1999, volume 1632 of LNCS, pages 202–206. Springer, 1999. doi:10.1007/3-540-48660-7_14.
[32] Brigitte Pientka and Jana Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Jürgen Giesl and Reiner Hähnle, editors, IJCAR 2010, volume 6173 of LNCS, pages 15–21. Springer, 2010. doi:10.1007/978-3-642-14203-1_2.
[33] Andrew M. Pitts. Locally nameless sets. Proc. ACM Program. Lang., 7(POPL):488–514, 2023. doi:10.1145/3571210.
[34] Andrei Popescu. Nominal recursors as epi-recursors. Proc. ACM Program. Lang., 8(POPL):425–456, 2024. doi:10.1145/3632857.
[35] Tom Ridge and James Margetson. A mechanically verified, sound and complete theorem prover for first order logic. In Joe Hurd and Thomas F. Melham, editors, TPHOLs 2005, volume 3603 of LNCS, pages 294–309. Springer, 2005. doi:10.1007/11541868_19.
[36] Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In Christian Urban and Xingyuan Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 359–374. Springer, 2015. doi:10.1007/978-3-319-22102-1_24.
[37] Natarajan Shankar. A mechanical proof of the Church-Rosser theorem. J. ACM, 35(3):475–522, 1988. doi:10.1145/44483.44484.
[38] Kathrin Stark. Mechanising syntax with binders in Coq. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28822.
[39] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, CPP 2019, pages 166–180. ACM, 2019. doi:10.1145/3293880.3294101.
[40] Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. A sound and complete projection for global types. In Adam Naumowicz and René Thiemann, editors, ITP 2023, volume 268 of LIPIcs, pages 28:1–28:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITP.2023.28.
[41] Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In LICS 2012, pages 596–605. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.75.
[42] Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. Log. Methods Comput. Sci., 8(2), 2012. doi:10.2168/LMCS-8(2:14)2012.
[43] Jan van Brügge, James McKinna, Andrei Popescu, and Dmitriy Traytel. Barendregt convenes with Knaster and Tarski: Strong rule induction for syntax with bindings. Proc. ACM Program. Lang., 9(POPL):57:1–57:32, 2025. doi:10.1145/3704893.
[44] Jan van Brügge, Andrei Popescu, and Dmitriy Traytel. Implementation of MrBNF and case studies presented in this paper, 2025. doi:10.5281/zenodo.15756655.
[45] Jérôme Vouillon. A solution to the POPLMark challenge based on de Bruijn indices. J. Autom. Reason., 49(3):327–362, 2012. doi:10.1007/S10817-011-9230-5.

[bib.bib1] [1] Submitted solutions to the POPLmark challenge. https://www.seas.upenn.edu/˜plclub/poplmark/, accessed March 22, 2025, 2005.

[bib.bib2] [2] Guillaume Ambal, Sergueï Lenglet, and Alan Schmitt. HO $\pi$ in Coq. J. Autom. Reason., 65(1):75–124, 2021. doi:10.1007/S10817-020-09553-0.

[bib.bib3] [3] Michael Ashley-Rollman, Karl Crary, and Robert Harper. Group from CMU’s solution to the POPLmark challenge. https://www.seas.upenn.edu/˜plclub/poplmark/cmu.html, accessed March 22, 2025, 2005.

[bib.bib4] [4] Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLMark challenge. In Joe Hurd and Thomas F. Melham, editors, TPHOLs 2005, volume 3603 of LNCS, pages 50–65. Springer, 2005. doi:10.1007/11541868_4.

[bib.bib5] [5] David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. J. Formaliz. Reason., 7(2):1–89, 2014. doi:10.6092/ISSN.1972-5787/4650.

[bib.bib6] [6] Hendrik Pieter Barendregt. The lambda calculus – its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.

[bib.bib7] [7] Jesper Bengtson and Joachim Parrow. Formalising the pi-calculus using nominal logic. Log. Methods Comput. Sci., 5(2), 2009. URL: http://arxiv.org/abs/0809.3960.

[bib.bib8] [8] Stefan Berghofer. A solution to the POPLMark challenge using de Bruijn indices in Isabelle/HOL. J. Autom. Reason., 49(3):303–326, 2012. doi:10.1007/S10817-011-9231-4.

[bib.bib9] [9] Stefan Berghofer and Christian Urban. A head-to-head comparison of de Bruijn indices and names. In Alberto Momigliano and Brigitte Pientka, editors, LFMTP 2006, volume 174 of ENTCS, pages 53–67. Elsevier, 2006. doi:10.1016/J.ENTCS.2007.01.018.

[bib.bib10] [10] Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, and Dmitriy Traytel. Bindings as bounded natural functors. Proc. ACM Program. Lang., 3(POPL):22:1–22:34, 2019. doi:10.1145/3290335.

[bib.bib11] [11] Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 93–110. Springer, 2014. doi:10.1007/978-3-319-08970-6_7.

[bib.bib12] [12] Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel. Cardinals in Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 111–127. Springer, 2014. doi:10.1007/978-3-319-08970-6_8.

[bib.bib13] [13] Joachim Breitner. Formally proving a compiler transformation safe. In Ben Lippmeier, editor, Haskell Symposium 2015, pages 35–46. ACM, 2015. doi:10.1145/2804302.2804312.

[bib.bib14] [14] Matthias Brun and Dmitriy Traytel. Generic authenticated data structures, formally. In John Harrison, John O’Leary, and Andrew Tolmach, editors, ITP 2019, volume 141 of LIPIcs, pages 10:1–10:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019. doi:10.4230/LIPICS.ITP.2019.10.

[bib.bib15] [15] Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363–408, 2012. doi:10.1007/s10817-011-9225-2.

[bib.bib16] [16] Zaynah Dargaye and Xavier Leroy. Mechanized verification of CPS transformations. In Nachum Dershowitz and Andrei Voronkov, editors, LPAR 2007, volume 4790 of LNCS, pages 211–225. Springer, 2007. doi:10.1007/978-3-540-75560-9_17.

[bib.bib17] [17] N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381–392, 1972. doi:10.1016/1385-7258(72)90034-0.

[bib.bib18] [18] Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341–363, 2002. doi:10.1007/s001650200016.

[bib.bib19] [19] Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. In LICS 1987, pages 194–204. IEEE Computer Society, 1987.

[bib.bib20] [20] Gérard P. Huet. Residual theory in lambda-calculus: A formal development. J. Funct. Program., 4(3):371–394, 1994. doi:10.1017/S0956796800001106.

[bib.bib21] [21] Brian Huffman and Christian Urban. A new foundation for Nominal Isabelle. In Matt Kaufmann and Lawrence C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 35–50. Springer, 2010. doi:10.1007/978-3-642-14052-5_5.

[bib.bib22] [22] Damiano Mazza. An infinitary affine lambda-calculus isomorphic to the full lambda-calculus. In LICS 2012, pages 471–480. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.57.

[bib.bib23] [23] Conor McBride and James McKinna. Functional pearl: I am not a number—I am a free variable. In Henrik Nilsson, editor, Haskell Workshop 2004, pages 1–9. ACM, 2004. doi:10.1145/1017472.1017477.

[bib.bib24] [24] Alberto Momigliano, S.J. Ambler, and R.L. Crole. A comparison of formalizations of the meta-theory of a language with variable bindings in Isabelle. In TPHOLs 2001, Supplemental Proceedings, pages 267–282, 2001. URL: https://www.inf.ed.ac.uk/publications/online/0046/b267.pdf.

[bib.bib25] [25] Tobias Nipkow. More Church-Rosser proofs. J. Autom. Reason., 26(1):51–66, 2001. doi:10.1023/A:1006496715975.

[bib.bib26] [26] Michael Norrish. Recursive function definition for types with binders. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, TPHOLs 2004, volume 3223 of LNCS, pages 241–256. Springer, 2004. doi:10.1007/978-3-540-30142-4_18.

[bib.bib27] [27] Michael Norrish and René Vestergaard. Proof pearl: De Bruijn terms really do work. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, volume 4732 of LNCS, pages 207–222. Springer, 2007. doi:10.1007/978-3-540-74591-4_16.

[bib.bib28] [28] Lawrence C. Paulson. The foundation of a generic theorem prover. J. Autom. Reason., 5(3):363–397, 1989. doi:10.1007/BF00248324.

[bib.bib29] [29] Lawrence C. Paulson. A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. J. Autom. Reason., 55(1):1–37, 2015. doi:10.1007/s10817-015-9322-8.

[bib.bib30] [30] Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Richard L. Wexelblat, editor, PLDI 1988, pages 199–208. ACM, 1988. doi:10.1145/53990.54010.

[bib.bib31] [31] Frank Pfenning and Carsten Schürmann. System description: Twelf – A meta-logical framework for deductive systems. In Harald Ganzinger, editor, CADE 1999, volume 1632 of LNCS, pages 202–206. Springer, 1999. doi:10.1007/3-540-48660-7_14.

[bib.bib32] [32] Brigitte Pientka and Jana Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Jürgen Giesl and Reiner Hähnle, editors, IJCAR 2010, volume 6173 of LNCS, pages 15–21. Springer, 2010. doi:10.1007/978-3-642-14203-1_2.

[bib.bib33] [33] Andrew M. Pitts. Locally nameless sets. Proc. ACM Program. Lang., 7(POPL):488–514, 2023. doi:10.1145/3571210.

[bib.bib34] [34] Andrei Popescu. Nominal recursors as epi-recursors. Proc. ACM Program. Lang., 8(POPL):425–456, 2024. doi:10.1145/3632857.

[bib.bib35] [35] Tom Ridge and James Margetson. A mechanically verified, sound and complete theorem prover for first order logic. In Joe Hurd and Thomas F. Melham, editors, TPHOLs 2005, volume 3603 of LNCS, pages 294–309. Springer, 2005. doi:10.1007/11541868_19.

[bib.bib36] [36] Steven Schäfer, Tobias Tebbi, and Gert Smolka. Autosubst: Reasoning with de Bruijn terms and parallel substitutions. In Christian Urban and Xingyuan Zhang, editors, ITP 2015, volume 9236 of LNCS, pages 359–374. Springer, 2015. doi:10.1007/978-3-319-22102-1_24.

[bib.bib37] [37] Natarajan Shankar. A mechanical proof of the Church-Rosser theorem. J. ACM, 35(3):475–522, 1988. doi:10.1145/44483.44484.

[bib.bib38] [38] Kathrin Stark. Mechanising syntax with binders in Coq. PhD thesis, Saarland University, Saarbrücken, Germany, 2020. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28822.

[bib.bib39] [39] Kathrin Stark, Steven Schäfer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions. In Assia Mahboubi and Magnus O. Myreen, editors, CPP 2019, pages 166–180. ACM, 2019. doi:10.1145/3293880.3294101.

[bib.bib40] [40] Dawit Legesse Tirore, Jesper Bengtson, and Marco Carbone. A sound and complete projection for global types. In Adam Naumowicz and René Thiemann, editors, ITP 2023, volume 268 of LIPIcs, pages 28:1–28:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.ITP.2023.28.

[bib.bib41] [41] Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette. Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In LICS 2012, pages 596–605. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.75.

[bib.bib42] [42] Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. Log. Methods Comput. Sci., 8(2), 2012. doi:10.2168/LMCS-8(2:14)2012.

[bib.bib43] [43] Jan van Brügge, James McKinna, Andrei Popescu, and Dmitriy Traytel. Barendregt convenes with Knaster and Tarski: Strong rule induction for syntax with bindings. Proc. ACM Program. Lang., 9(POPL):57:1–57:32, 2025. doi:10.1145/3704893.

[bib.bib44] [44] Jan van Brügge, Andrei Popescu, and Dmitriy Traytel. Implementation of MrBNF and case studies presented in this paper, 2025. doi:10.5281/zenodo.15756655.

[bib.bib45] [45] Jérôme Vouillon. A solution to the POPLMark challenge based on de Bruijn indices. J. Autom. Reason., 49(3):327–362, 2012. doi:10.1007/S10817-011-9230-5.

Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

Supplementary Material:

Acknowledgements:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Related Work

3 MrBNF in Action

3.1 Preliminaries on cardinals and permutations

3.2 𝝀-calculus terms

Prop 1.

Prop 2 (Binding-aware structural induction).

Prop 3 (Binding-aware recursion).

3.3 Infinitary 𝝀-calculus terms

Prop 4.

Prop 5 (Binding-aware structural induction).

Prop 6 (Binding-aware recursion).

3.4 Types and terms for System F<:

4 MrBNF’s Internals: Construction of Datatypes with Bindings

4.1 From User-Specifications to Fixpoint Equations

4.2 Composition of MRBNFs

Definition 1.

4.3 Fixpoint and Quotienting Constructions

4.4 Recursion

Relativized Recursion.

5 Application I: Mazza’s Isomorphism

Prop 7.

Prop 8.

Prop 9.

6 Application II: POPLmark Challenge

7 Conclusion

References

3.2 $\lambda$ -calculus terms

3.3 Infinitary $\lambda$ -calculus terms

3.4 Types and terms for System F_<: