diff options
Diffstat (limited to 'spec')
| -rw-r--r-- | spec/README.md | 16 | ||||
| -rw-r--r-- | spec/inferred.md | 8 |
2 files changed, 18 insertions, 6 deletions
diff --git a/spec/README.md b/spec/README.md index 4d3bb5f6..e536b5fd 100644 --- a/spec/README.md +++ b/spec/README.md @@ -2,11 +2,11 @@ # BQN specification -This directory gives a specification for BQN. The specification differs from the [documentation](../doc/README.md) in that its purpose is only to describe the exact details of BQN's operation in the most quickly accessible way, rather than to explain the core ideas of BQN functionality and how it might be used. +This document, and the others in this directory (linked in the list below) make up the pre-versioning BQN specification. The specification differs from the [documentation](../doc/README.md) in that its purpose is only to describe the exact details of BQN's operation in the most quickly accessible way, rather than to explain the central ideas of BQN functionality and how it might be used. The core of BQN, which excludes system-provided values, is now almost completely specified. Three planned features—syntax for system-provided values, inferred property function headers, and an extension to allow low-rank elements in the argument to Join—have not yet been added, and the spec will continue to be edited further to improve clarity and cover any edge cases that have been missed. -The core of BQN, which excludes system-provided values, is now completely specified, although the spec will continue to be edited further to improve clarity and cover edge cases that were missed initially. +Under this specification, a language implementation is a **BQN pre-version implementation** if it behaves as specified for all input programs. It is a **BQN pre-version implementation with extensions** if it behaves as specified in all cases where the specification does not require an error, but behaves differently in at least one case where it requires an error. It is a **partial** version of either of these if it doesn't conform to the description but differs from a conforming implementation only by rejecting with an error some programs that the conforming implementation accepts. As the specification is not yet versioned, other instances of the specification define these terms in different ways. An implementation can use one of these term if it conforms to any instance of the pre-versioning BQN specifications that defines them. When versioning is begun, there will be only one specification for each version. -The BQN specification consists of the following documents: +The following documents are included in the BQN specification. A BQN program is a sequence of [Unicode](https://en.wikipedia.org/wiki/Unicode) code points: to evaluate it, it is converted into a sequence of tokens using the token formation rules, then these tokens are arranged in a syntax tree according to the grammar, and then this tree is evaluated according to the evaluation semantics. The program may be evaluated in the presence of additional context such as a filesystem or command-line arguments; this context is presented to the program and manipulated through the system-provided values. - [Types](types.md) - [Token formation](token.md) - [Literals](literal.md) @@ -16,3 +16,13 @@ The BQN specification consists of the following documents: - [Primitives](primitive.md): [reference implementations](reference.bqn) - [Inferred properties](inferred.md) (identities, fills, Undo, and Under) - [System-provided values](system.md) (`•`) + +In several cases, an implementation can choose between more than one possible behavior. +- An implementation chooses its number system, which must be an approximation of the real or complex numbers but has no specific requirements. Results of basic numeric operations must be deterministic but are not specified. +- Minimum (`⌊`) and Maximum (`⌈`) may give an error if either argument is a character. +- Other than the required cases, attempting to use an inferred property can either fail or give a result consistent with the constraints on that property. +- In some cases there are multiple valid results for Undo. Any of these results, or an error, can be given; if there is no obvious choice of result an error is recommended. The choice must depend only on the inputs to Undo. +- If the specification does not identify the fill element for an array, then any or no fill can be deterministically chosen. +- If an expression in a program cannot be evaluated without error (that is, there is no context that would cause the program, or a caller with access to its result, to evaluate the expression but not eventually fail with an error), then the implementation may reject this program, giving an error before evaluating any code and regardless of context—in this case, it must not accept the program in any context. This "compiler clause" modifies the behavior described above. +- The way the program's output (either a result or an error) is displayed to the user is not specified. +- Any system values can be implemented, and they may act in an arbitrary way including modifying the behavior of the rest of the program. If system values with names given in this specification are implemented, however, then they must conform with the specified behavior. diff --git a/spec/inferred.md b/spec/inferred.md index 8d5693a6..18cd67dc 100644 --- a/spec/inferred.md +++ b/spec/inferred.md @@ -2,7 +2,7 @@ # 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⊑∧‿∨)⁼`. @@ -10,7 +10,7 @@ Failing to compute an inferred property for a function or array as it's created ## 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. @@ -34,7 +34,7 @@ Additionally, the identity of `∾˝` must be recognized: if `0=≠𝕩` and `1< 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 `' '`. @@ -65,6 +65,8 @@ The Undo 1-modifier `⁼`, given an operand `𝔽` and argument `𝕩`, and poss 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. |