Editing

1 files changed, 3 insertions, 3 deletions

diff --git a/spec/inferred.md b/spec/inferred.md
index 0fe24442..d83461c7 100644
--- a/spec/inferred.md
+++ b/spec/inferred.md
@@ -180,11 +180,11 @@ When implementing, there is no need to implement invertable Under specially: it
 
 In general, structural Under requires information from the original right argument to be computed. Here we will define the *structural inverse of* structural function `𝔾` *on* `v` *into* `𝕩`, where `𝕩` gives this information. The value `𝕨𝔽⌾𝔾𝕩` is then the structural inverse of `𝔾` on `𝕨𝔽○𝔾𝕩` into `𝕩`.
 
-We define a *structure* to be either the value `·` or an array of structures (substitute `0` or any other specific value for `·` if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure `s` is a *captures* a BQN value or structure `𝕩` if it is `·`, or if `s` and `𝕩` are arrays of the same shape, and each element of `s` captures the corresponding element of `𝕩`. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.
+We define a *structure* to be either the value `·` or an array of structures (substitute `0` or any other specific value for `·` if you'd like structures to be a subset of BQN arrays; the value is irrelevant). A given structure `s` *captures* a BQN value or structure `𝕩` if it is `·`, or if `s` and `𝕩` are arrays of the same shape, and each element of `s` captures the corresponding element of `𝕩`. Thus a structure shares some or all of the structural information in arrays it captures, but none of the data.
 
 A *structure transformation* consists of an initial structure `s` and a result structure `t`, as well as a relation between the two: each instance of `·` in `t` is assigned the location of an instance of `·` in `s`. If `s` captures a value `𝕩`, we say that the structural transformation captures `𝕩` as well. Given such a value `𝕩`, the transformation is applied to `𝕩` by replacing each `·` in `t` with the corresponding value from `𝕩`, found by taking the same location in `𝕩` as the one in `s` given by the transformation.
 
-Given a structure transformation `G` and values `𝕩` and `v`, the *structural inverse* `z` of `G` on `v` into `𝕩`, if it exists, is the value such that `v≡G z`, and `𝕩 ≡○F z` for every structure transformation `F` as possible given the previous constraint. If `G` has initial structure `s` and final structure `t`, we know that `s` captures `𝕩` and `z` (it's required in order to apply `G` at all) while `t` captures `v`. For each instance of `·` in `s`, there are three possibilities:
+Given values `𝕩` and `v` and a structure transformation `G` capturing `𝕩`, the *structural inverse* `z` of `G` on `v` into `𝕩`, if it exists, is the value such that `v≡G z`, and `𝕩 ≡○F z` for every structure transformation `F` possible given the previous constraint. If `G` has initial structure `s` and final structure `t`, we know that `s` captures `𝕩` and `z` (it's required in order to apply `G` at all) while `t` captures `v`. For each instance of `·` in `s`, there are three possibilities:
 - No result location in `t` is assigned this location. This component of `z` must match `𝕩`, or `z` could be improved without breaking any constraints by replacing it.
 - Exactly one result location is assigned this location. The requirement `v≡G z` implies `z`'s value here is exactly `v`'s value at that result location.
 - More than one result location is assigned this location. Now `z`'s value there must match `v`'s value at each of these result leaves. If `v` has different values at the different leaves, there is no inverse.
@@ -196,7 +196,7 @@ 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 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`.
+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 structure transformations `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.