2.4 Position functions

Definition 2.17 position function

✓

Let \( \tau \) be a type. A position function for \( \tau \) is an injection \( \iota : \tau \to \mu \). This is a typeclass.

Proposition 2.18 injective functions from denied sets

✓

Let \( \tau \) be a type such that \( \# \tau \leq \# \mu \). Let \( D : \tau \to \operatorname {\mathsf{Set}}(\mu ) \) be a function such that for each \( x : \tau \), the set \( D(x) \), called the denied set of \( x \), has size less than \( \operatorname {\mathsf{cof}}(\operatorname {\mathsf{ord}}(\# \mu )) \). Then there is an injective function \( f : \tau \to \mu \) such that if \( \nu \in D(x) \), then \( \nu {\lt} f(x) \).

Proof ▶

Pick a well-ordering \( \prec \) of \( \tau \) of length at most \( \operatorname {\mathsf{ord}}(\# \mu ) \). Define \( f \) by well-founded recursion on \( \prec \). Suppose that we have already defined \( f \) for all \( y \prec x \). Then let

\[ X = \{ f(y) \mid y \prec x \} \cup \{ \nu \mid \exists \nu ' \in D(x),\, \nu \leq \nu ' \} \]

This set has size strictly less than \( \mu \), so there is some \( \nu : \mu \) not contained in it. Set \( f(x) = \nu \).

Proposition 2.19 base positions

✓

There are position functions on \( {\mathcal A}, {\mathcal N}\) that are jointly injective and satisfy

\( \iota (\operatorname {\mathsf{NL}}(a^\circ )) {\lt} \iota (a) \) for every atom \( a \);
\( \iota (\operatorname {\mathsf{NL}}(N^\circ )) \leq \iota (N) \) for every near-litter \( N \);
\( \iota (a) {\lt} \iota (N) \) for every near-litter \( N \) and atom \( a \in N \mathrel {\triangle }\operatorname {\mathsf{LS}}(N^\circ ) \). ¹

We register these position functions as instances for use in typeclass inference. We also define \( \iota (L) = \iota (\operatorname {\mathsf{NL}}(L)) \) for litters.

Proof ▶

First, establish an equivalence \( f_{\mathcal L}: {\mathcal L}\simeq \mu \). Use proposition 2.18 to obtain an injective map \( f_{\mathcal A}: {\mathcal N}\to \mu \) such that \( f_{\mathcal L}(a^\circ ) {\lt} f_{\mathcal A}(a) \) for each atom \( a \). Now use proposition 2.18 again to obtain an injective map \( f_{\mathcal N}: {\mathcal N}\to \mu \) such that

\[ f_{\mathcal L}(N^\circ ) {\lt} f_{\mathcal N}(N);\quad f_{\mathcal A}(a) {\lt} f_{\mathcal N}(N) \text{ for } a \in N \mathrel {\triangle }\operatorname {\mathsf{LS}}(N^\circ ) \]

Endow \( 3 \times \mu \) with its lexicographic order, of order type \( \operatorname {\mathsf{ord}}(\# \mu ) \), giving an order isomorphism \( e : 3 \times \mu \simeq \mu \). Finally, we define

\[ \iota (a) = e(1, f_{\mathcal A}(a));\quad \iota (N) = \begin{cases} e(0, f_{\mathcal L}(N^\circ )) & \text{if } N = \operatorname {\mathsf{NL}}(N^\circ ) \\ e(2, f_{\mathcal N}(N)) & \text{otherwise} \end{cases} \]