Well-formedness and its preservation in a PIEO tree context

[anshumanmohan]

#16 discussed PIEO trees, and #17 goes a long way towards formalizing these and fleshing out an OCaml implementation. This issue is to track a remaining piece of the formalism, which is well-formedness.

Formal Abstractions defines well-formedness in §3.3. Intuitively, we need well-formedness to ensure that a pop operation on the tree will never "get stuck". That is, we'll pop the root, get some value i, and recursively pop the ith child of the root until we hit a leaf; we'll always have something to pop as we walk our way down the tree.

We need an analogue of well-formedness for PEIO trees. @polybeandip has an attempt in Definition 1.6 of his notes. It's a little brief (in particular it skips a definition of

which I think is meant to be read as "the number of instances of i in p, such that those instances of i satisfy f) but basically I believe this attempt is solid. Note that the definitions is in two parts: first, well-formedness with regard to a given f, and then well-formedness in general using an existential f.

We need to prove that well-formedness will be preserved in our PIEO trees when we push or pop. Formal Abstractions does a quick little proof sketch of these properties for PIFO trees, but the property will be a little trickier for us in PIEO tree land because the property will depend on the possible choices of f. In fact I think doing this proof will illuminate the ways in which we'll need to restrict F, the collection of permissible predicates.

[anshumanmohan]

@KabirSamsi this is yours if you want it. It's the thing that @polybeandip, @sampsyo and I discussed briefly at the top of the meeting today. You mentioned wanting a piece of the math action, and I think this could be fun for you! While it indeed has not been important for @polybeandip's compilation proofs, well-formedness is an important property as I explain in the topmatter.

As you know, this stuff has proved tricky in the past. I encourage you to discuss this frequently, surface your progress often, and to ask lots of questions!

[polybeandip]

I like the writeup here!

One minor nitpick: the definition for $|p|_{i, f}$ wasn't skipped. It's at the bottom of Definition 1.1.

Other than this, I agree with everything else.

To help make this issue more concrete, I've added a bit of scaffolding to the notes with d200333: namely, the statement of the PIEO tree analogue of Lemma 3.9 from Formal Abstactions (without proof). In writing this down, I noticed a bug in Definition 1.6 (PIEO tree well-formedness) and patched it with this same commit. @anshumanmohan what do you think of this change?

@KabirSamsi feel free to branch off pieo-trees and add to pieo-trees/notes.tex if you'd like.

[anshumanmohan]

Aha thanks! And sorry about the slander haha

[KabirSamsi]

My work on this led me to re-consult the proof sketch for PIFO Tree Well-Formedness in Formal Abstractions. While it's left to the reader in the paper, I'm completing the proof in a new branch.
Here's my work so far.

Two notable things:

1. The relationships between $push$, $pop$, $| \cdot | : \text{PIFOTree(t)} \rightarrow \mathbb{N}$ and $\text{PUSH, POP, } |\cdot| : \text{PIFO } \rightarrow \mathbb{N}$ needed to be clearer in order to formally define (and by extension, prove) the preservation of well-formedness. I've added a few new definitions for how these function on PIFOs, and two new lemmas (with proofs) clarifying that $| \cdot |$ and $| \cdot |_i$ increment and decrement with pushes and pops, respectively.

2. Formal Abstractions suggest inducting over the topology of a tree. I feel that it's more intuitive to induct over the definitions of $push$ and $pop$. This is what I've done so far (albeit it would be great if someone could skim the logic once it's fully done, before I move to the meatier PIEO Tree proofs).

This leaves us in a good place though! The fact that $push$ functions the same for PIFO Trees and PIEO Trees (minus the few key differences) means that half of the proof for well-formedness translates over easily. The other half will require more work, but formally proving preservation of well-formedness for pops in PIFO Trees will help us there.

[anshumanmohan]

Cool! I'll add this to my stack. But just FYI, there is a version of the paper with a few of the proofs fleshed out. Just pointing you to it in case it is ever helpful! https://arxiv.org/pdf/2211.11659

[polybeandip]

Heads up: the arXiv version doesn't have full proofs, but the one @anshumanmohan sent on slack here does.

Even this one doesn't have full proofs from section 3.3 (well-formedness) though.

[anshumanmohan]

Eek, thanks for the catch! That's totally a snafu; the arXiv version's raison d'etre is to be an extended version haha. I will alert Tobias, who owns push rights to the arXiv version

[KabirSamsi]

I consulted the paper that Anshuman linked on Slack yesterday actually! The proof I'm working on for now, though, is for Section 3.3, which isn't covered there (proofs from 4 & 5 are covered). So hopefully this isn't a waste!

At any rate, I think that the new definitions that I'm working through will help us in the pursuit of proving well-formedness in PIEO Trees, as they are applicable for both.

[polybeandip]

Apologies, I've noticed another bug with the well-formedness definition and theorem in the notes; just pushed a fix with bba1bf2.