diff options
Diffstat (limited to 'spec')
| -rw-r--r-- | spec/inferred.md | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/spec/inferred.md b/spec/inferred.md index be2bab67..bb52e5b4 100644 --- a/spec/inferred.md +++ b/spec/inferred.md @@ -137,3 +137,60 @@ For a structural function `πΎ`, the *structural inverse* of `πΎ` on `v` into 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`. + +### Required structural inverses + +The following primitive functions be fully supported by structural Under. Each manipulates its right argument structurally. + +| Type | Primitives +|---------|----------- +| Monad | `β£β’<>βΎβ₯ββββ½βββ` +| Dyad | `β’β₯ββββ½β/βββ` + +The following combinations must also be supported, where `S` and `T` are structural functions and `k` is a constant function (data type, or function derived from `Λ`): + +| Expression | Remarks +|------------|-------- +| `SβT` | +| `S T` | +| `Β·S T` | +| `SβT` | +| `kβΈT` | +| `k T β’` | +| `Sβk` | `k` a natural number +| `SΒ¨` | +| `Sβk` | `k` contains only negative numbers +| `Sβ` | +| `SΛ` | +| `Sβk` | + +### A structural Under algorithm + +This section offers the outline for a procedure that computes most structural inverses that a programmer would typically use. The concept is to build a special result array whose elements are not BQN values but instead indicate positions within the initial argument. This structural array is applied to the initial argument by replacing its elements with the values at those positions, and inverted by placing elements back in the original array at these indices, checking for any conflicts. If operations like dyadic `βΎ` are allowed, then a structural array might have some indices that are prefixes or parents of others, making it slightly different from a structural transformation as defined above (although it could be represented as a structural transformation by expanding some of these). This requires additional checking to ensure that elements of previously inserted elements can't be modified. + +Structural functions can be applied to structural arrays directly, after ensuring that they have the necessary depth as given below. An array's depth can be increased by expanding each position in it into an array of child positions, or, if that position contains an atom and the structural function in question would tolerate an atom, enclosing it. + +| Level | Monads | Dyads | Modifiers +|:-----:|-----------------|-----------------|---------- +| 0 | `β’β£<` | `β’β£` | `ΛβββΈβββΆ` +| 1 | `=β β’β₯βββ»«β½βββ` | `β₯βΎββββ»«β½β/ββ` | `ΛΒ¨ββ` +| 2 | `>βΎ` | | +| n | | `β` | `β` + +Not all primitives in the table above are required. Of note are `=β β’`, which accept a structural array but return an ordinary value; this might be used as a left argument later. If the final result is not structural, then the function in question can't be structural, and the attempt to find a structural inverse can be aborted. + +### Non-structural case + +The behavior of invertible and computational Under is fully dependent on that of [Undo](#undo), and does not need to be repeated here. However, it is important to discuss when this definition can be applied: specifically, either +- When `πΎ` is exactly invertible, or +- When `πΎ` is provably not a structural function. + +A substantial class of functions that is easy to identify and always satisfies one of the above criteria is the functions that *never perform non-invertible structural manipulation*, or more colloquially *don't discard argument elements*. This class consists of functions made up of plain primitives that don't contain the following primitives: + +| Valence | Primitives +|---------|----------- +| Monad | `»«ββ` +| Dyad | `β₯ββ»«β/βββ` +| Modifer | `` βΌβΒ΄Λ` `` + +If a function of this class is a structural function, then it must be invertible, because the remaining primitives leave no way to retain some elements but discard others (an element's value can be ignored by replacing it by a constant, but a function that does this can't be structural). It can be extended to include some dyadic functions like `β₯ββ/` if it can be determined that the left argument never allows information to be discarded; for example if the left argument to `β` contains no duplicates or the left argument to `β₯` always has a product larger than its argument's bound. Inverses from `βΌ` or `β` might be allowed on a case-by-case basis, and `β` with a constant right operand that contains no negative numbers can also be allowed. |