From 37a18f37aeb44152f3a2f79a6304c99d995153c8 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Mon, 26 Jul 2021 21:34:41 -0400 Subject: Editing --- docs/spec/inferred.html | 6 +++--- spec/inferred.md | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html index ef7bb6e1..433a65c5 100644 --- a/docs/spec/inferred.html +++ b/docs/spec/inferred.html @@ -477,9 +477,9 @@

When implementing, there is no need to implement invertable Under specially: it can be handled as part of the structural and computation cases.

Mathematical definition of structural Under

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: