Sorted Labelled Trees

I've recently opened my copy of Sørensen-Urzyczyn's Lectures on the Curry-Howard Isomorphism again and noted that I've never been completely happy with the formalities around the definitions of $\lambda$-pre-terms and $\lambda$-terms. E.g. the definition of an occurence of a variable in Definition 1.2.3 is not very precise. Harper's Practical Foundations for Programming Languages is a bit more precise (talking about trees) but the definition of trees is still not completely formal. I also find the definition of abstract binding trees very hard to understand and I think that it might have some small issues. So I decided to formulate the definitions of abstract binding trees and $\alpha$-equivalence between them (of which $\lambda$-(pre-)terms should be a special case) in a way that I personally am happy with, even though, as Sørensen-Urzyczyn put it, these things are »rather dull, but necessary to make [the] formalism precise«.

In this first blog post of a small series I want to give a definition of sorted labelled trees and prove the principle of structural induction for them. The approach is inspired by Harper's book, Section 5.3 of the Homotopy Type Theory Book and the nlab page on W-types. There will hopefully be follow-ups on abstract syntax trees and abstract binding trees (and maybe $\lambda$-terms).

Definition

Let $S$ be a finite set of sorts and let $O$ be a sets of labels. Let $\sigma \from O \to S$ be a map which assigns to each label $o \in O$ a sort $\sigma(o) \in S$, called the sort of $o$ and let $\alpha \from S \to \List(S)$ a map which assigns to each label $o \in O$ a list $\alpha(o) = [s_0, \dots, s_{r-1}]$ called the arity of $S$.

We define by strong induction for $n \in \IN$ a family of sets $\Tree^{(n)} = \{\Tree^{(n)}_s\}_{s \in S}$. For this, we introduce the notation $$ \succ \from \IN^r \to \IN, \qquad (k_0, \dots, k_{r-1}) \mapsto \min\{n \in \IN \mid k_0, \dots, k_{r-1} < n\}. $$

Assuming that $\Tree^{(k)}_s$ is already defined for all $k < n$ and all $s \in S$, we set $$ \Tree^{(n)}_s \defby \coprod_{\substack{o \in O \\ \sigma(o) = s \\ [s_0, \dots, s_{r-1}] \defby \alpha(o)}} \coprod_{\substack{(k_0, \dots, k_{r-1}) \in \IN^r \\ \succ(k_0, \dots, k_{r-1}) = n}} \Tree^{(k_0)}_{s_0} \times \dots \times \Tree^{(k_{r-1})}_{s_{r-1}}. $$ Finally, we set $\Tree_s \defby \coprod_{n \in \IN} \Tree^{(n)}_s$ and call $\Tree_s$ the set of trees of sort $s$ (with labels in $O$, sorted in $S$).

We have a map $$ \sup \from \coprod_{\substack{o \in O \\ \sigma(o) = s \\ [s_0, \dots, s_{r-1}] \defby \alpha(o)}} \Tree_{s_0} \times \dots \times \Tree_{s_{r-1}} \to \Tree_s $$ which is defined as follows:

Let $o \in O$ with $\sigma(o) = s$ and $\alpha(o) = [s_0, \dots, s_{r-1}]$ and let $(t_0, \dots, t_{r-1}) \in \Tree_{s_0} \times \dots \times \Tree_{s_{r-1}}$. Write $t_i = \langle k_i, \widetilde{t_i}\rangle$ with $k_i \in \IN$ and $\widetilde{t_i} \in \Tree^{(k_i)}_{s_i}$. Set $n \defby \succ(k_0, \dots, k_{r-1})$. Then $\widetilde{t} \defby \langle o, \langle (k_0, \dots, k_{r-1}), (\widetilde{t_0}, \dots, \widetilde{t_{r-1}})\rangle\rangle \in \Tree^{(n)}_s$ and we set $$ \sup(o, (t_0, \dots, t_{r-1})) \defby \langle n, \widetilde{t}\rangle. $$ We also write $o(t_0, \dots, t_{r-1}) \defby \sup(o, (t_0, \dots, t_{r-1}))$.

Principle of Structural Induction

Theorem. Let $(X^{(s)}_t)_{s \in S, t \in \Tree_s}$ be a family of sets. Assume that there is for each $o \in O$ with $s \defby \sigma(o)$ and $[s_0, \dots, s_{r-1}] \defby \alpha(o)$ a family of maps $$ f^{(o)} = \{f^{(o)}_{(t_0, \dots, t_{r-1}), t} \from X^{(s_0)}_{t_0} \times \dots \times X^{(s_{r-1})}_{t_{r-1}} \to X^{(s)}_t\} _{(t_0, \dots, t_{r-1}) \in \Tree_{\alpha(o)}, t \in \Tree_{\sigma(o)}}. $$ Then there exists a unique family $$ (x^{(s)}(t))_{s \in S, t \in \Tree_s} \in \prod_{s \in S} \prod_{t \in \Tree_s} X_t^{(s)} $$ such that for every $o \in O$ with $s \defby \sigma(o)$ and $[s_0, \dots, s_{r-1}] \defby \alpha(o)$ and every $(t_0, \dots, t_{r-1})$ with $t_i \in \Tree_{s_i}$ we have $$ x^{(s)}(o(t_0, \dots, t_{r-1})) = f^{(o)}_{(t_0, \dots, t_{r-1}), t}(x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1})). $$ Proof. By (strong) induction on $n \in \IN$ we define for each $n \in \IN$ a family $$ (\widetilde{x}^{(s)}_n(\widetilde{t}))_{s \in S, \widetilde{t} \in \Tree^{(n)}_{s}} \in \prod_{s \in S} \prod_{t \in \Tree_s} X_t^{(s)}. $$ Indeed, assuming that $$ (\widetilde{x}^{(s)}_k(\widetilde{t}))_{s \in S, \widetilde{t} \in \Tree^{(k)}_{s}} \in \prod_{s \in S} \prod_{t \in \Tree_s} X_t^{(s)} $$ is already defined for all $k < n$, we define $(\widetilde{x}^{(s)}_n(\widetilde{t}))_{s \in S, \widetilde{t} \in \Tree^{(n)}_{s}}$ as follows: Let $s \in S$ and $\widetilde{t} \in \Tree_s^{(n)}$. Write $\widetilde{t} = \langle o, \langle (k_0, \dots, k_{r-1}), (\widetilde{t_0}, \dots, \widetilde{t_{r-1}})\rangle\rangle$ with $o \in O$, $s = \sigma(o)$, $[s_0, \dots, s_{r-1}] = \alpha(o)$, $(k_0, \dots, k_{r-1}) \in \IN^r$ and $\widetilde{t_i} \in \Tree^{(k_i)}_{s_i}$. Setting $t_i \defby \langle k_i, \widetilde{t_i}\rangle \in \Tree_{s_i}$, let $\widetilde{x}_n^{(s)}(\widetilde{t}) \defby f^{(o)}_{(t_0, \dots, t_{r-1}), t}(x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1}))$.

Now we can define the family $(x^{(s)}(t))_{s \in S, t \in \Tree_s}$ as follows: Let $s \in S$ and $t \in \Tree_{s}$. Write $t = \langle n, \widetilde{t}\rangle$ with $n \in \IN$ and $\widetilde{t} \in \Tree^{(n)}_s$. Then define $x^{(s)}(t) \defby \widetilde{x}_n^{(s)}(\widetilde{t})$.

Now let $o \in O$ with $s \defby \sigma(s)$ and $[s_0, \dots, s_{r-1}] \defby \alpha(o)$ and let $(t_0, \dots, t_{r-1})$ be trees with $t_i \in \Tree_{s_i}$. We want to prove $x^{(s)}(o(t_0, \dots, t_{r-1}) = f^{(o)}_{(t_0, \dots, t_{r-1}), t}(x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1}))$. We recall the definition of $o(t_0, \dots, t_{r-1})$: Write $t_i = \langle k_i, \widetilde{t_i} \rangle$ with $k_i \in \IN$ and $\widetilde{t_i} \in \Tree^{(k_i)}_{s_i}$. Set $n \defby \succ(k_0, \dots, k_{r-1})$. Then $o(t_0, \dots, t_{r-1}) = \langle n, \widetilde{t} \rangle$ where $\widetilde{t} = \langle o, \langle (k_0, \dots, k_{r-1}), (\widetilde{t_0}, \dots, \widetilde{t_{r-1}})\rangle \rangle$. Then we have $$ x^{(s)}(o(t_0, \dots, t_{r-1})) = \widetilde{x}_n^{(s)}(\widetilde{t}) = f^{(o)}_{(t_0, \dots, t_{r-1}), t} (x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1})) $$ by definition.

To show uniqueness, assume that $(x^{(s)}(t))_{s \in S, t \in \Tree_s}$ and $(y^{(s)}(t))_{s \in S, t \in \Tree_s}$ are two families satisfying $$ x^{(s)}(o(t_0, \dots, t_{r-1})) = f^{(o)}_{(t_0, \dots, t_{r-1}), t}(x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1})) $$ and $$ y^{(s)}(o(t_0, \dots, t_{r-1})) = f^{(o)}_{(t_0, \dots, t_{r-1}), t}(y^{(s_0)}(t_0), \dots, y^{(s_{r-1})}(t_{r-1})). $$ We prove by strong induction on $n \in \IN$ that if $t \in \Tree_s$ has the form $\langle n, \widetilde{t} \rangle$ with $\widetilde{t} \in \Tree^{(n)}_s$, then $x^{(s)}(t) = y^{(s)}(t)$. Suppose the claim has been shown for all $k < n$. Now let $t = \langle n, \widetilde{t}\rangle \in \Tree_s$. We can write $\widetilde{t} = \langle o, \langle (k_0, \dots, k_{r-1}), (\widetilde{t_0}, \dots, \widetilde{t_{r-1}})\rangle \rangle$ with $o \in O$, $s = \sigma(o)$, $[s_0, \dots, s_{r-1}] = \alpha(o)$, $(k_0, \dots, k_{r-1}) \in \IN^r$ such that $\succ(k_0, \dots, k_{r-1}) = n$ and $\widetilde{t_i} \in \Tree_{s_i}^{(k_i)}$. Note that we have $k_i < n$ and we have $t = o(t_0, \dots, t_{r-1})$ where $t_i \defby \langle k_i, \widetilde{t_i} \rangle$. Using the induction hypothesis we have $$ \begin{split} x^{(s)}(t) &= x^{(s)}(o(t_0, \dots, t_{r-1})) \\ &= f^{(o)}_{(t_0, \dots, t_{r-1}), t}(x^{(s_0)}(t_0), \dots, x^{(s_{r-1})}(t_{r-1})) \\ &= f^{(o)}_{(t_0, \dots, t_{r-1}), t}(y^{(s_0)}(t_0), \dots, y^{(s_{r-1})}(t_{r-1})) \\ &= y^{(s)}(o(t_0, \dots, t_{r-1})) \\ &= y^{(s)}(t). \end{split} $$ This finishes the proof. ∎

Remarks

In the unsorted case ($S$ = $\{s\}$), we have shown that our construction is a construction of the W-type $W_{o \in O} A(o)$ where $A(o) = \{0, \dots, r-1\}$ if $\alpha(o)$ has length $r$. We have not really used that $S$ is finite (it is required in Harper's PFPL though). The case of general $S$ probably fits into the framework of dependent W-types. What we have used is that $\alpha(o)$ is a finite list (i.e. a map $\{0, \dots, r - 1\} \to S$) where $r$ is a natural number depending on $o$. One can replace $\{1, \dots, r-1\}$ by an arbitray set depending on $o$. As far as I understand, ZFC still proves the existence of these more general W-types, but one needs transfinite recursion (i.e. the axiom of choice) to prove the existence. Alternatively, one can require existence of W-types as an axiom, this is what is done in Homotopy Type Theory.