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 ++-- spec/inferred.md | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) 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.

diff --git a/spec/inferred.md b/spec/inferred.md index bb52e5b4..9a171396 100644 --- a/spec/inferred.md +++ b/spec/inferred.md @@ -134,9 +134,9 @@ For a structural function `𝔾`, the *structural inverse* of `𝔾` on `v` into #### 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`. +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`. 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`. +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 -- cgit v1.2.3