Formalize PIEO Tree Compilation

[polybeandip]

This PR closes #17 by formalizing PIEO tree compilation!

[polybeandip]

I have a few notes on this write-up I'd like to record here.

Tweaks to Formal Abstractions

Given an embedding $f$, the construction of $\widehat{f}$ is underspecified when $f$ is not surjective on leaves. In particular, the phrase

For all $1 \leq j \leq m$, $\alpha \cdot j$ is a prefix of some $f(i)$

from Definition 5.4 in Formal Abstractions is false for such $f$.

There's a couple ways to patch this bug. @anshumanmohan's updated paper simply asserts $f$ must be "leaf-surjective" in Definition 5.4. There's good and bad sides to this choice.

• Good: none of the proofs for results from Section 5 need to be tweaked since they too implicity assume Leaf-surjective $f$!

  The section 5 Lemmas use a common strategy: two nested inductions, where the inner one is over prefixes $\alpha$ of $f(i)$. In the inner inductive step, while showing the inductive hypothesis for $\widehat{f}(q)_\alpha$, they assume the IH for all its children. This isn't legal when $f$ isn't leaf-surjective since some children might not be prefixes of any $f(i)$.

• Bad: the embedding algorithms from Section 6 don't always produce leaf-surjective embeddings.

  In particular, for $t_1 = \mathrm{Node}(\ast, \ast)$ and $d=3$, the algorithm from Theorem 6.1 yields $d$-ary topology $t_2 = \mathrm{Node}(\ast, \ast, \ast)$. No embedding from $t_1$ to $t_2$ can be leaf-surjective.

Alternatively, we could alter the construction for $\widehat{f}$. Replace the second sentence of the inverse recursion in Definition 5.4 with

For $1 \leq j \leq m$ such that $\alpha \cdot j$ is not a prefix of some $f(i)$, define $\widehat{f}(q)_{\alpha \cdot j}$ to be the PIFO tree with topology $t_2/(\alpha \cdot j)$ and empty PIFOs on all leaves and internal nodes. With this and recursion, we know $\widehat{f}(q)_{\alpha \cdot j} \in \mathrm{PIFOTree}(t_2/(\alpha \cdot j))$ for all $j \in [1, m]$.

All other parts of this step stay as is.

As previously mentioned, this change would cascade into changes for Lemmas 5.x ($x \in {5, 6, 7, 9}$). Thankfully, showing the IH holds on $\widehat{f}(q)_{\alpha \cdot j}$, when $\alpha \cdot j$ isn't a prefix of any $f(i)$, should be easy to handle since our altered construction guarantees $\widehat{f}(q)_{\alpha \cdot j}$ must have empty PIFOs on all nodes.

These notes

1. assume this slight extension to the construction of $\widehat{f}$ and Lemmas 5.x ($x \in {5, 6, 7, 9}$)
2. construct $\overline{f}$ to handle non-leaf-surjective embeddings in the same way

Mixing proof techniques

We hoped the PIEO tree analogue of Theorem 5.10 from Formal Abstractions (Theorem 4.8 in the notes) would die quickly to this commutative diagram.

This way, we wouldn't have proofs identical to Lemmas 5.x from Formal Abstractions. We'd simply use those results to prove our PIEO tree analogues by clever routing through this diagram.

Commit 06e752f tries for this style of proof but ultimately falls short: we couldn't show
$$\mathrm{pop}(q, g) = (\mathrm{pkt}, q^{\prime}) \implies \mathrm{pop}(\overline{f}(q), g) = (\mathrm{pkt}, \overline{f}(q^\prime))$$

Using notation from the notes, the issue is that there's a link between $q_1^\prime$ and $g$ since $q_1^\prime$ was made by popping $q_1$ with $g$. For this reason, it's tricky to show equation (†) holds for all $g$. To sidestep this, the proof for Lemma 4.6 from the notes doesn't use our commutative diagram. Instead, we write a proof near identical to Lemma 5.7, doing the two nested inductions a la Formal Abstractions.

It's not pretty, but it gets the job done (for now).

[anshumanmohan]

Thanks for flagging the points of divergence! Hoping to have this reviewed tomorrow :)

[polybeandip]

@KabirSamsi heads up on a weird quirk of TeX: when you recompile notes.tex, remember to do it twice! If you do it only once, all the \refs aren't registered and the pdf will show question marks instead

[anshumanmohan]

Yes TeX is annoying in general and infuriating when it comes to references. You could try to remember to do the double-compile thing, or also consider a modern engine like https://tectonic-typesetting.github.io/