Framing for specification, and discussion of implementation-defined aspects

4 files changed, 36 insertions, 12 deletions

diff --git a/docs/spec/index.html b/docs/spec/index.html
index 71d7c6f6..5c2017e1 100644
--- a/docs/spec/index.html
+++ b/docs/spec/index.html
@@ -5,9 +5,9 @@
 </head>
 <div class="nav"><a href="https://github.com/mlochbaum/BQN">BQN</a> / <a href="../index.html">main</a></div>
 <h1 id="bqn-specification">BQN specification</h1>
-<p>This directory gives a specification for BQN. The specification differs from the <a href="../doc/index.html">documentation</a> 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.</p>
-<p>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.</p>
-<p>The BQN specification consists of the following documents:</p>
+<p>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 <a href="../doc/index.html">documentation</a> 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.</p>
+<p>Under this specification, a language implementation is a <strong>BQN pre-version implementation</strong> if it behaves as specified for all input programs. It is a <strong>BQN pre-version implementation with extensions</strong> 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 <strong>partial</strong> 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.</p>
+<p>The following documents are included in the BQN specification. A BQN program is a sequence of <a href="https://en.wikipedia.org/wiki/Unicode">Unicode</a> 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.</p>
 <ul>
 <li><a href="types.html">Types</a></li>
 <li><a href="token.html">Token formation</a></li>
@@ -19,3 +19,14 @@
 <li><a href="inferred.html">Inferred properties</a> (identities, fills, Undo, and Under)</li>
 <li><a href="system.html">System-provided values</a> (<code><span class='Value'>•</span></code>)</li>
 </ul>
+<p>In several cases, an implementation can choose between more than one possible behavior.</p>
+<ul>
+<li>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.</li>
+<li>Minimum (<code><span class='Function'>⌊</span></code>) and Maximum (<code><span class='Function'>⌈</span></code>) may give an error if either argument is a character.</li>
+<li>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.</li>
+<li>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.</li>
+<li>If the specification does not identify the fill element for an array, then any or no fill can be deterministically chosen.</li>
+<li>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 &quot;compiler clause&quot; modifies the behavior described above.</li>
+<li>The way the program's output (either a result or an error) is displayed to the user is not specified.</li>
+<li>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.</li>
+</ul>
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 @@
 </head>
 <div class="nav"><a href="https://github.com/mlochbaum/BQN">BQN</a> / <a href="../index.html">main</a> / <a href="index.html">spec</a></div>
 <h1 id="specification-bqn-inferred-properties">Specification: BQN inferred properties</h1>
-<p>BQN includes some simple deductive capabilities: detecting the type of empty array elements, and the Undo (<code><span class='Modifier'>⁼</span></code>) and Under (<code><span class='Modifier2'>⌾</span></code>) 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.</p>
+<p>BQN includes some simple deductive capabilities: detecting the type of empty array elements, the result of an empty reduction, and the Undo (<code><span class='Modifier'>⁼</span></code>) and Under (<code><span class='Modifier2'>⌾</span></code>) 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.</p>
 <p>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 <code><span class='Paren'>(</span><span class='Function'>+-×</span><span class='Paren'>)</span><span class='Modifier'>⁼</span></code> to <code><span class='Function'>∨</span><span class='Modifier'>⁼</span></code>. However, it is necessary to identify computed functions and modifiers: for example <code><span class='Function'>F</span><span class='Modifier'>⁼</span></code> when the value of <code><span class='Function'>F</span></code> in the expression is <code><span class='Function'>∨</span></code>, or <code><span class='Paren'>(</span><span class='Number'>1</span><span class='Function'>⊑∧</span><span class='Ligature'>‿</span><span class='Function'>∨</span><span class='Paren'>)</span><span class='Modifier'>⁼</span></code>.</p>
 <p>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.</p>
 <h2 id="identities">Identities</h2>
-<p>When monadic Fold (<code><span class='Modifier'>´</span></code>) or Insert (<code><span class='Modifier'>˝</span></code>) 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 <code><span class='Function'>𝔽</span></code> is a value <code><span class='Value'>r</span></code> such that <code><span class='Value'>e</span><span class='Function'>≡</span><span class='Value'>e</span><span class='Function'>𝔽</span><span class='Value'>r</span></code> for any element <code><span class='Value'>e</span></code> in the domain. For such a value <code><span class='Value'>r</span></code>, the reduction <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> is equivalent to <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for a non-empty list <code><span class='Value'>l</span></code>, because the first application <code><span class='Paren'>(</span><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span><span class='Paren'>)</span> <span class='Function'>𝔽</span> <span class='Value'>r</span></code> gives <code><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span></code>, which is the starting point when no initial value is given. It's thus reasonable to define <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> to be <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for an empty list <code><span class='Value'>l</span></code> as well, giving a result <code><span class='Value'>r</span></code>.</p>
+<p>When monadic Fold (<code><span class='Modifier'>´</span></code>) or Insert (<code><span class='Modifier'>˝</span></code>) 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 <code><span class='Function'>𝔽</span></code> is a value <code><span class='Value'>r</span></code> such that <code><span class='Value'>e</span><span class='Function'>≡</span><span class='Value'>e</span><span class='Function'>𝔽</span><span class='Value'>r</span></code> for any element <code><span class='Value'>e</span></code> in the domain. For such a value <code><span class='Value'>r</span></code>, the fold <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> is equivalent to <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for a non-empty list <code><span class='Value'>l</span></code>, because the first application <code><span class='Paren'>(</span><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span><span class='Paren'>)</span> <span class='Function'>𝔽</span> <span class='Value'>r</span></code> gives <code><span class='Number'>¯1</span><span class='Function'>⊑</span><span class='Value'>l</span></code>, which is the starting point when no initial value is given. It's thus reasonable to define <code><span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> to be <code><span class='Value'>r</span> <span class='Function'>𝔽</span><span class='Modifier'>´</span> <span class='Value'>l</span></code> for an empty list <code><span class='Value'>l</span></code> as well, giving a result <code><span class='Value'>r</span></code>.</p>
 <p>For Fold, the result of <code><span class='Function'>𝔽</span><span class='Modifier'>´</span></code> on an empty list is defined to be a right identity value for the <em>range</em> of <code><span class='Function'>𝔽</span></code>, if exactly one such value exists. If an identity can't be proven to uniquely exist, then an error results.</p>
 <p>For Insert, <code><span class='Function'>𝔽</span><span class='Modifier'>˝</span></code> on an array of length 0 is defined similarly, but also depends on the cell shape <code><span class='Number'>1</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span></code>. The required domain is the arrays of that shape that also lie in the range of <code><span class='Function'>𝔽</span></code> (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 <code><span class='Number'>1</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span></code> and be unique among arrays with that shape. For example, with cell shape <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span></code>, all of <code><span class='Number'>0</span></code>, <code><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code>, and <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code> are identities for <code><span class='Function'>+</span></code>, but <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span><span class='Function'>⥊</span><span class='Number'>0</span></code> can be used because it is the only indentity with shape <code><span class='Number'>3</span><span class='Ligature'>‿</span><span class='Number'>2</span></code>, while the other identities aren't unique and can't be used.</p>
 <p>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.</p>
@@ -70,7 +70,7 @@
 <p>Additionally, the identity of <code><span class='Function'>∾</span><span class='Modifier'>˝</span></code> must be recognized: if <code><span class='Number'>0</span><span class='Function'>=≠</span><span class='Value'>𝕩</span></code> and <code><span class='Number'>1</span><span class='Function'>&lt;=</span><span class='Value'>𝕩</span></code>, then <code><span class='Function'>∾</span><span class='Modifier'>˝</span><span class='Value'>𝕩</span></code> is <code><span class='Paren'>(</span><span class='Number'>0</span><span class='Function'>∾</span><span class='Number'>2</span><span class='Function'>↓≢</span><span class='Value'>𝕩</span><span class='Paren'>)</span><span class='Function'>⥊</span><span class='Value'>𝕩</span></code>. If <code><span class='Number'>1</span><span class='Function'>==</span><span class='Value'>𝕩</span></code>, then there is no identity element, as the result of <code><span class='Function'>∾</span></code> always has rank at least 1, but the cell rank is 0.</p>
 <h2 id="fill-elements">Fill elements</h2>
 <p>Any BQN array can have a <em>fill element</em>, which is a sort of &quot;default&quot; value for the array. The reference implementations use <code><span class='Function'>Fill</span></code> to access this element, and it is used primarily for Take (<code><span class='Function'>↑</span></code>), First (<code><span class='Function'>⊑</span></code>), and Nudge (<code><span class='Function'>«</span></code>, <code><span class='Function'>»</span></code>). One way to extract the fill element of an array <code><span class='Value'>a</span></code> in BQN is <code><span class='Function'>⊑</span><span class='Number'>0</span><span class='Function'>⥊</span><span class='Value'>a</span></code>.</p>
-<p>A fill element can be either <code><span class='Number'>0</span></code>, <code><span class='String'>' '</span></code>, 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 <code><span class='Number'>0</span></code>, while the fill element for an array of variable-length lists should probably be <code><span class='Bracket'>⟨⟩</span></code>. However, the fill element, unlike other inferred properties, does not satisfy any particular constraints that relate it to its array.</p>
+<p>A fill element can be either <code><span class='Number'>0</span></code>, <code><span class='String'>' '</span></code>, 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 <code><span class='Number'>0</span></code>, while the fill element for an array of variable-length lists should probably be <code><span class='Bracket'>⟨⟩</span></code>. 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.</p>
 <p>In addition to the requirements below, the fill element for the value of a string literal is <code><span class='String'>' '</span></code>.</p>
 <h3 id="required-functions">Required functions</h3>
 <p>Combinators <code><span class='Function'>⊣⊢!</span><span class='Modifier'>˙˜´˝</span><span class='Modifier2'>∘○⊸⟜⊘◶⍟</span></code> 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. <code><span class='Modifier2'>⍟</span></code> constructs arrays if its right operand is or contains arrays, and the fill elements of these arrays are not specified; converting <code><span class='Value'>𝕩</span></code> to a fill element is a reasonable choice in some cases but not others.</p>
@@ -129,6 +129,7 @@
 <h2 id="undo">Undo</h2>
 <p>The Undo 1-modifier <code><span class='Modifier'>⁼</span></code>, given an operand <code><span class='Function'>𝔽</span></code> and argument <code><span class='Value'>𝕩</span></code>, and possibly a left argument <code><span class='Value'>𝕨</span></code>, finds a value <code><span class='Value'>y</span></code> such that <code><span class='Value'>𝕩</span><span class='Function'>≡</span><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Value'>y</span></code>, that is, an element of the pre-image of <code><span class='Value'>𝕩</span></code> under <code><span class='Function'>𝔽</span></code> or <code><span class='Value'>𝕨</span><span class='Function'>𝔽⊢</span></code>. Thus it satisfies the constraint <code><span class='Value'>𝕩</span> <span class='Function'>≡</span> <span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier'>⁼</span><span class='Value'>𝕩</span></code> (<code><span class='Value'>𝕨</span><span class='Function'>𝔽</span><span class='Modifier'>⁼</span><span class='Function'>⊢</span></code> is a <em>right inverse</em> of <code><span class='Value'>𝕨</span><span class='Function'>𝔽⊢</span></code>) provided <code><span class='Function'>𝔽</span><span class='Modifier'>⁼</span></code> and <code><span class='Function'>𝔽</span></code> both complete without error. <code><span class='Function'>𝔽</span><span class='Modifier'>⁼</span></code> 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 <code><span class='Function'>𝔽</span><span class='Modifier'>⁼</span></code> to give an error if there are many choices of inverse with no clear way to choose one of them: for example, <code><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Function'>⍉</span><span class='Value'>m</span></code> returns the diagonal of matrix <code><span class='Value'>m</span></code>; <code><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Function'>⍉</span><span class='Modifier'>⁼</span><span class='Number'>2</span><span class='Ligature'>‿</span><span class='Number'>3</span></code> 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 <code><span class='Number'>2</span><span class='Ligature'>‿</span><span class='Number'>3</span><span class='Modifier2'>⌾</span><span class='Paren'>(</span><span class='Number'>0</span><span class='Ligature'>‿</span><span class='Number'>0</span><span class='Modifier2'>⊸</span><span class='Function'>⍉</span><span class='Paren'>)</span></code> applied to a matrix of initial elements, than to return a result that could be very different from other implementations.</p>
 <p>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 <code><span class='Function'>𝔽</span></code> 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.</p>
+<p>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 <code><span class='Function'>𝔽</span></code>, <code><span class='Value'>𝕩</span></code>, and (if present) <code><span class='Value'>𝕨</span></code>.</p>
 <h3 id="required-functions">Required functions</h3>
 <p>Function inverses are given for one or two arguments, with cases where inverse support is not required left blank.</p>
 <p>For arithmetic functions the implementations below may in some cases not give the closest inverse (that is, there may be some other <code><span class='Value'>y</span></code> so that <code><span class='Function'>F</span> <span class='Value'>y</span></code> is closer to <code><span class='Value'>x</span></code> than <code><span class='Function'>F</span> <span class='Function'>F</span><span class='Modifier'>⁼</span><span class='Value'>x</span></code>). Even in these cases the exact functions given below must be used.</p>
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.