From f3fcc2928931c8ec0ca0770f71c52f5567390b10 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Sun, 21 Mar 2021 15:11:37 -0400 Subject: Framing for specification, and discussion of implementation-defined aspects --- docs/spec/inferred.html | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'docs/spec/inferred.html') diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html index dd7de0f7..2ff3ce0a 100644 --- a/docs/spec/inferred.html +++ b/docs/spec/inferred.html @@ -5,11 +5,11 @@
BQN / main / spec

Specification: BQN inferred properties

-

BQN includes some simple deductive capabilities: detecting the type of empty array elements, and the Undo (⁼) and Under (⌾) modifiers. These tasks are a kind of proof-based or constraint programming, and can never be solved completely (some instances will be undecidable) but can be solved in more instances by ever-more sophisticated algorithms. To allow implementers to develop more advanced implementations while offering some stability and portability to programmers, two kinds of specification are given here. First, constraints are given on the behavior of inferred properties. These are not exact and require some judgment on the part of the implementer. Second, behavior for common or useful cases is specified more precisely. Non-normative suggestions are also given as a reference for implementers.

+

BQN includes some simple deductive capabilities: detecting the type of empty array elements, the result of an empty reduction, and the Undo (⁼) and Under (⌾) modifiers. These tasks are a kind of proof-based or constraint programming, and can never be solved completely (some instances will be undecidable) but can be solved in more instances by ever-more sophisticated algorithms. To allow implementers to develop more advanced implementations while offering some stability and portability to programmers, two kinds of specification are given here. First, constraints are given on the behavior of inferred properties. These are not exact and require some judgment on the part of the implementer. Second, behavior for common or useful cases is specified more precisely. Non-normative suggestions are also given as a reference for implementers.

For the specified cases, the given functions and modifiers refer to those particular representations. It is not necessary to detect equivalent representations, for example to reduce (+-×)⁼ to ∨⁼. However, it is necessary to identify computed functions and modifiers: for example F⁼ when the value of F in the expression is ∨, or (1⊑∧‿∨)⁼.

Failing to compute an inferred property for a function or array as it's created cannot cause an error. An error can only be caused when the missing inferred property is needed for a computation.

Identities

-

When monadic Fold (´) or Insert (˝) is called on an array of length 0, BQN attempts to infer a right identity value for the function in order to determine the result. A right identity value for a dyadic function 𝔽 is a value r such that e≡e𝔽r for any element e in the domain. For such a value r, the reduction r 𝔽´ l is equivalent to 𝔽´ l for a non-empty list l, because the first application (¯1⊑l) 𝔽 r gives ¯1⊑l, which is the starting point when no initial value is given. It's thus reasonable to define 𝔽´ l to be r 𝔽´ l for an empty list l as well, giving a result r.

+

When monadic Fold (´) or Insert (˝) is called on an array of length 0, BQN attempts to infer a right identity value for the function in order to determine the result. A right identity value for a dyadic function 𝔽 is a value r such that e≡e𝔽r for any element e in the domain. For such a value r, the fold r 𝔽´ l is equivalent to 𝔽´ l for a non-empty list l, because the first application (¯1⊑l) 𝔽 r gives ¯1⊑l, which is the starting point when no initial value is given. It's thus reasonable to define 𝔽´ l to be r 𝔽´ l for an empty list l as well, giving a result r.

For Fold, the result of 𝔽´ on an empty list is defined to be a right identity value for the range of 𝔽, if exactly one such value exists. If an identity can't be proven to uniquely exist, then an error results.

For Insert, 𝔽˝ on an array of length 0 is defined similarly, but also depends on the cell shape 1↓≢𝕩. The required domain is the arrays of that shape that also lie in the range of 𝔽 (over arbitrary arguments, not shape-restricted ones). Furthermore, an identity may be unique among all possible arguments as in the case of Fold, or it may be an array with shape 1↓≢𝕩 and be unique among arrays with that shape. For example, with cell shape 3‿2, all of 0, 2⥊0, and 3‿2⥊0 are identities for +, but 3‿2⥊0 can be used because it is the only indentity with shape 3‿2, while the other identities aren't unique and can't be used.

Identity values for the arithmetic primitives below must be recognized. Under Fold, the result is the given identity value, while under Insert, it is the identity value reshaped to the argument's cell shape.

@@ -70,7 +70,7 @@

Additionally, the identity of ∾˝ must be recognized: if 0=≠𝕩 and 1<=𝕩, then ∾˝𝕩 is (0∾2↓≢𝕩)⥊𝕩. If 1==𝕩, then there is no identity element, as the result of ∾ always has rank at least 1, but the cell rank is 0.

Fill elements

Any BQN array can have a fill element, which is a sort of "default" value for the array. The reference implementations use Fill to access this element, and it is used primarily for Take (↑), First (⊑), and Nudge («, »). One way to extract the fill element of an array a in BQN is ⊑0⥊a.

-

A fill element can be either 0, ' ', or an array of valid fill elements. If the fill element is an array, then it may also have a fill element (since it is an ordinary BQN array). The fill element is meant to describe the shared structure of the elements of an array: for example, the fill element of an array of numbers should be 0, while the fill element for an array of variable-length lists should probably be ⟨⟩. However, the fill element, unlike other inferred properties, does not satisfy any particular constraints that relate it to its array.

+

A fill element can be either 0, ' ', or an array of valid fill elements. If the fill element is an array, then it may also have a fill element (since it is an ordinary BQN array). The fill element is meant to describe the shared structure of the elements of an array: for example, the fill element of an array of numbers should be 0, while the fill element for an array of variable-length lists should probably be ⟨⟩. However, the fill element, unlike other inferred properties, does not satisfy any particular constraints that relate it to its array. The fill element of a primitive's result, including functions derived from primitive modifiers, must depend only on its inputs.

In addition to the requirements below, the fill element for the value of a string literal is ' '.

Required functions

Combinators ⊣⊢!˙˜´˝∘○⊸⟜⊘◶⍟ do not affect fill element computation: if the combinator calls a function that computes a fill element, then that fill element must be retained if the result is passed to other functions or returned. ⍟ constructs arrays if its right operand is or contains arrays, and the fill elements of these arrays are not specified; converting 𝕩 to a fill element is a reasonable choice in some cases but not others.

@@ -129,6 +129,7 @@

Undo

The Undo 1-modifier ⁼, given an operand 𝔽 and argument 𝕩, and possibly a left argument 𝕨, finds a value y such that 𝕩≡𝕨𝔽y, that is, an element of the pre-image of 𝕩 under 𝔽 or 𝕨𝔽⊢. Thus it satisfies the constraint 𝕩 ≡ 𝕨𝔽𝕨𝔽⁼𝕩 (𝕨𝔽⁼⊢ is a right inverse of 𝕨𝔽⊢) provided 𝔽⁼ and 𝔽 both complete without error. 𝔽⁼ should of course give an error if no inverse element exists, and can also fail if no inverse can be found. It is also preferred for 𝔽⁼ to give an error if there are many choices of inverse with no clear way to choose one of them: for example, 0‿0⍉m returns the diagonal of matrix m; 0‿0⍉⁼2‿3 requires values to be chosen for the off-diagonal elements in its result. It is better to give an error, encouraging the programmer to use a fully-specified approach like 2‿3⌾(0‿0⊸⍉) applied to a matrix of initial elements, than to return a result that could be very different from other implementations.

When working with limited-precision numbers, it may be difficult or impossible to exactly invert the operand function. Instead, it is generally acceptable to perform a computation that, if done with unlimited precision, would exactly invert 𝔽 computed with unlimited precision. This principle is the basis for the numeric inverses specified below. It is also acceptable to find an inverse by numeric methods, provided that the error in the inverse value found relative to an unlimited-precision inverse can be kept close to the inherent error in the implementation's number format.

+

Regardless of which cases for Undo are supported, the result of a call, and whether it is an error, must depend only on the values of the inputs 𝔽, 𝕩, and (if present) 𝕨.

Required functions

Function inverses are given for one or two arguments, with cases where inverse support is not required left blank.

For arithmetic functions the implementations below may in some cases not give the closest inverse (that is, there may be some other y so that F y is closer to x than F F⁼x). Even in these cases the exact functions given below must be used.

-- cgit v1.2.3