From ddde54a778b9cbf5503fdf7ec0a9ed02d8a075e0 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Sat, 12 Dec 2020 11:06:36 -0500 Subject: Actually finish the structural Under well-definedness proof --- docs/spec/inferred.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs') diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html index 44bba9ff..617dcfd5 100644 --- a/docs/spec/inferred.html +++ b/docs/spec/inferred.html @@ -359,8 +359,8 @@

A structural function decomposition is a possibly infinite family of structure transformations such that any possible BQN value is captured by at most one of these transformations. It can be applied to any value: if some transformation captures the value, then apply that transformation, and otherwise give an error. A function is a structural function if there is a structural function decomposition that matches it: that is, for any input either both functions give an error or the results match.

For a structural function 𝔾, the structural inverse of 𝔾 on v into 𝕩 is the inverse of G on v into 𝕩, where G is the structure transformation that captures 𝕩 from some structural function decomposition Gd matching 𝔾. If no decomposition has an initial structural matching 𝕩 then the structural inverse does not exist.

Well-definedness

-

In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given 𝕩, if G and H are structure transformations from different decompositions of 𝔾 both capturing 𝕩, then the structural inverse of G on v into 𝕩 matches that of H on v into 𝕩. Call these inverses y and z. Now begin by supposing that H captures y and G captures z; we will show this later. From the definition of a structural inverse, v≑G y, so that v≑𝔾 y, and because H captures y we have v≑H y as well. Let S w indicate the set of all functions F such that w ≑○F 𝕩 (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of z we know that S z is a strict superset of S w for any w other than z with v≑H w. It follows that either y≑z or S y is a strict subset of S z. By symmetry the same relation holds exchanging y and z, but it's not possible for S y to be a strict subset of S z and vice-versa. The only remaining possibility is that y≑z.

-

We now need to show that H captures y (the proof that G captures z is of course the same as H and G are symmetric). To do this we must show that any array in the initial structure of H corresponds to a matching array in y. Choose the position of an array in H, and assume by induction that each array containing it already has the desired property; this implies that this position exists in y as well although we know nothing about its contents. G captures y, so G's initial structure is Β· at this position or some parent position. There are now two cases: either G makes use of this postionβ€”at least one position in its final structure corresponds to itβ€”or it doesn't. If not, then the contents of y at this position are the same as those of 𝕩. Since H captures 𝕩, its initial structure matches 𝕩 and hence y as well at this position. If it does, then instead y matches a part of v.

+

In order to show that the structural inverse of a structural function is well-defined, we must show that it does not depend on the choice of structural function decomposition. That is, for a given 𝕩, if G and H are structure transformations from different decompositions of 𝔾 both capturing 𝕩, then the structural inverse of G on v into 𝕩 matches that of H on v into 𝕩. Call these inverses y and z. Now begin by supposing that H captures y and G captures z; we will show this later. From the definition of a structural inverse, v≑G y, so that v≑𝔾 y, and because H captures y we know that 𝔾 y is H y, so we have v≑H y as well. Let S w indicate the set of all functions F such that w ≑○F 𝕩 (this is not a BQN value, both because it is a set and because it's usually infinite): from the definition of z we know that S z is a strict superset of S w for any w other than z with v≑H w. It follows that either y≑z or S y is a strict subset of S z. By symmetry the same relation holds exchanging y and z, but it's not possible for S y to be a strict subset of S z and vice-versa. The only remaining possibility is that y≑z.

+

We now need to show that H captures y (the proof that G captures z is of course the same as H and G are symmetric). To do this we must show that any array in the initial structure of H corresponds to a matching array in y. For convenience, we will call the initial structures of the two transformations iG and iH, and the final structures fG and fH, and use the notation pβŠ‘a to indicate the value of array a at position p. Choose the position of an array in H, and assume by induction that each array containing it already has the desired property; this implies that this position exists in y as well although we know nothing about its contents. G captures y, so iG is Β· at this position or some parent position; call this position in iG p. There are now two cases: either G makes use of this pβ€”at least one position in fG corresponds to itβ€”or it doesn't. If it doesn't, then the contents of y at p are the same as those of 𝕩. Since H captures 𝕩, iH matches 𝕩 and hence y as well at p. If it does, then let s be a position in fG that corresponds to p (if there are multiple possibilities, choose one). From v≑G y, we know that sβŠ‘v matches pβŠ‘y. We know that fH captures v, so that sβŠ‘fH captures sβŠ‘v, or pβŠ‘y. But we can show that the value of sβŠ‘fH is the same as pβŠ‘iH, which would prove that H captures y at p. To show this, construct an array xp by replacing the value of 𝕩 at p with pβŠ‘iH (to be more careful in our handling of types, we might replace every Β· with some value that never appears in 𝕩). Both H and G capture xp: clearly they capture it outside p, while at p itself, iG is Β· and iH is equal to pβŠ‘xp. Now (H xp)≑(G xp) because both functions match 𝔾 on their domains. Therefore sβŠ‘H xp matches sβŠ‘G xp, which by the definition of s matches pβŠ‘xp, which matches pβŠ‘iH. But sβŠ‘H xp comes from replacing each atom in sβŠ‘fH with an atom in xp that's captured by a Β· in iH. Because it matches pβŠ‘iH, every atom in sβŠ‘H xp is Β·, but the only instances of Β· in xp come from our inserted copy of pβŠ‘iH and each is immediately captured by the corresponding Β· in iH. It follows that sβŠ‘H xp, and consequently sβŠ‘fH, is exactly pβŠ‘iH, completing the proof.

Required structural inverses

The following primitive functions be fully supported by structural Under. Each manipulates its right argument structurally.

-- cgit v1.2.3