diff options
Diffstat (limited to 'spec')
| -rw-r--r-- | spec/inferred.md | 4 |
1 files changed, 2 insertions, 2 deletions
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 |