aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/README.md1
-rw-r--r--doc/identity.md2
-rw-r--r--doc/primitive.md2
-rw-r--r--doc/repeat.md2
-rw-r--r--doc/transpose.md2
-rw-r--r--doc/undo.md56
-rw-r--r--docs/doc/identity.html2
-rw-r--r--docs/doc/index.html1
-rw-r--r--docs/doc/primitive.html2
-rw-r--r--docs/doc/repeat.html2
-rw-r--r--docs/doc/transpose.html2
-rw-r--r--docs/doc/undo.html53
12 files changed, 119 insertions, 8 deletions
diff --git a/doc/README.md b/doc/README.md
index 682edb92..74d70ef4 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -61,6 +61,7 @@ Primitives:
- [Solo, Couple, and Merge](couple.md) (`≍>`)
- [Take and Drop](take.md) (`↑`)
- [Transpose](transpose.md) (`⍉`)
+- [Undo](undo.md) (`⁼`)
- [Windows](windows.md) (`↕`)
Environment:
diff --git a/doc/identity.md b/doc/identity.md
index a9916bcb..fe9ad2e9 100644
--- a/doc/identity.md
+++ b/doc/identity.md
@@ -14,7 +14,7 @@ Here are the simplest functions in BQN: Right (`⊢`) always returns its right a
Depending on your past experiences, this could cause some confusion: built-in support for functions that do nothing? Documentation should say why a feature's there and how to use it, not just what it does, so we'll try to address this below. The most important single use is for tacit programming, but there are a variety of other uses as well.
-Of course, it's easy to write block functions `{𝕩}` and `{𝕨}` that return particular arguments. While I would already make `⊣` and `⊢` primitives just because they are common and important, there are also specific disadvantages to using blocks. They fail to indicate that there are no side effects, as primitives would, and they also need special casing for the interpreter to manipulate them when applying Undo (`⁼`) or making other inferences.
+Of course, it's easy to write block functions `{𝕩}` and `{𝕨}` that return particular arguments. While I would already make `⊣` and `⊢` primitives just because they are common and important, there are also specific disadvantages to using blocks. They fail to indicate that there are no side effects, as primitives would, and they also need special casing for the interpreter to manipulate them when applying [Undo](undo.md) (`⁼`) or making other inferences.
## Filling arrays
diff --git a/doc/primitive.md b/doc/primitive.md
index 9d4378c0..4cb8f13c 100644
--- a/doc/primitive.md
+++ b/doc/primitive.md
@@ -85,7 +85,7 @@ Other modifiers control array traversal and iteration. In three cases a simpler
`˘` | Cells | `⎉` | [Rank](https://aplwiki.com/wiki/Rank_(operator))
`¨` | [Each](map.md) | `⚇` | [Depth](depth.md#the-depth-modifier)
`⌜` | [Table](map.md) |
-`⁼` | Undo | `⍟` | [Repeat](repeat.md)
+`⁼` | [Undo](undo.md) | `⍟` | [Repeat](repeat.md)
`´` | [Fold](fold.md) |
`˝` | [Insert](fold.md) |
`` ` `` | [Scan](scan.md) |
diff --git a/doc/repeat.md b/doc/repeat.md
index 26afe7e9..bb7000ea 100644
--- a/doc/repeat.md
+++ b/doc/repeat.md
@@ -15,7 +15,7 @@ In mathematics (which unsurpisingly tends to use complicated terms to talk about
`F⍟0` repeats `F` zero times, that is, does nothing. Like `n⋆0` gives the multiplicative identity `1`, `F⍟0` is the compositional [identity](identity.md), `⊢`. Since `F⍟1` applies `F` and `F⍟0` doesn't, Repeat might be pronounced "if" or "conditional" when `𝔾` is boolean.
-BQN's Repeat modifier has some extra functionality relative to the mathematical version. It allows a left argument, and some extensions to the right operand `𝔾`. As usual for 2-modifiers, `𝔾` is actually a function that applies to the arguments to give a result. The result can be a natural number as shown above, or a negative number to Undo (`⁼`) `𝔽`, or an array of values.
+BQN's Repeat modifier has some extra functionality relative to the mathematical version. It allows a left argument, and some extensions to the right operand `𝔾`. As usual for 2-modifiers, `𝔾` is actually a function that applies to the arguments to give a result. The result can be a natural number as shown above, or a negative number to [Undo](undo.md) (`⁼`) `𝔽`, or an array of values.
## Left argument
diff --git a/doc/transpose.md b/doc/transpose.md
index c3d0807b..7f91ad2d 100644
--- a/doc/transpose.md
+++ b/doc/transpose.md
@@ -37,7 +37,7 @@ But, ignoring the whitespace and going in reading order, the argument and result
≍○<⟜⍉ ⥊˘ a322
-To exchange multiple axes, use the [Repeat](repeat.md) modifier. A negative power moves axes in the other direction, just like how [Rotate](reverse.md#rotate) handles negative left arguments. In particular, to move the last axis to the front, use Undo (as you might expect, this exactly inverts `⍉`).
+To exchange multiple axes, use the [Repeat](repeat.md) modifier. A negative power moves axes in the other direction, just like how [Rotate](reverse.md#rotate) handles negative left arguments. In particular, to move the last axis to the front, use [Undo](undo.md) (as you might expect, this exactly inverts `⍉`).
≢ ⍉⍟3 a23456
diff --git a/doc/undo.md b/doc/undo.md
new file mode 100644
index 00000000..e8f1605e
--- /dev/null
+++ b/doc/undo.md
@@ -0,0 +1,56 @@
+*View this file with results and syntax highlighting [here](https://mlochbaum.github.io/BQN/doc/undo.html).*
+
+# Undo
+
+Oh no, you've deleted a function after spending half an hour writing it! Well… hopefully your editor can help with that. But maybe you'll be interested to hear that BQN can reverse the action of some functions—ones that *don't* lose information. This capability is also used by [Repeat](repeat.md) (`⍟`) to repeat a negative number of times.
+
+ 2 ⌽ "abcde"
+
+ 2 ⌽⁼ 2 ⌽ "abcde"
+
+Above is one example of Undo (`⁼`) in action. [Rotate](reverse.md) shifts the elements of a list left, and undoing shifts them to the right. BQN's ability to undo functions covers a lot of cases and can seem somewhat magical:
+
+ (Fn ← -⟜1⌾(¯1⊸⊑)) "BQN"
+
+ Fn⁼ Fn "BQN"
+
+Here it undoes a function to decrement the last character by incrementing that character. In part this is enabled by the clean design of BQN primitives, because better-behaved functions like those using structural Under are easier to invert.
+
+## The rules
+
+If `𝔽` can be inverted exactly, then Undo just does that. However, there are also some other functions that BQN inverts. For example, the squaring function `ט` has both a positive and a negative inverse, and yet:
+
+ ט ¯3
+ ט⁼ ט ¯3 # It's not the same!
+
+Don't worry, this isn't 'nam. Undo doesn't always satisfy `𝕩 ≡ 𝔽⁼ 𝔽 𝕩`, but it *does* obey `𝕩 ≡ 𝔽 𝔽⁼ 𝕩`. That is, it gives one possible argument that could have been passed to `𝔽`, just not necessarily the one that actually was. BQN is conservative in how it uses this freedom, so that it won't for example make up new elements entirely to find an inverse. It's usually used when there's an obvious or standard way to pick which of the possible values should be returned.
+
+In a BQN with floating-point numbers, computations are approximate, so the inverse is allowed to be approximate as well (any error should still be very small though).
+
+ 6 - √⁼√6
+
+## What's supported?
+
+For the full list, see [the specification](../spec/inferred.md#undo). An individual implementation might support a lot more functionality than is required, so if you're not concerned about portability just try out whatever function you're interested in.
+
+Arithmetic and simple combinators are usually invertible. A compound function that refers to its argument just once, like `6+⌽∘⍉`, can typically be undone, but one that uses the argument in two different ways, such as `⊢+⋆`, probably can't.
+
+A few notable inverses are the [logarithm](arithmetic.md#basic-arithmetic) `⋆⁼`, [un-Transpose](transpose.md) `⍉⁼`, and [Indices inverse](replicate.md#inverse) `/⁼`. [Enclose](enclose.md) inverse, `<⁼`, is an alternative to [First](pick.md#first) that requires its argument to be a unit.
+
+Structural functions like [Take](take.md) and [shifts](shift.md) that remove elements from `𝕩` can't be inverted, because given the result there's no way to know what the elements should be. However, there are two special cases that have inverses defined despite losing data: these are `⊣⁼` and `k⁼` where `k` is a constant (a data type, or `k˙`). For these, `𝕩` is required to [match](match.md) the always returned value `𝕨` or `k`, and this value is also used for the result—even though any result would be valid, as these functions ignore `𝕩`.
+
+ 3 ⊣⁼ 4
+ 3 ⊣⁼ 3
+
+## Undo headers
+
+Undo headers are currently supported only by dzaima/BQN.
+
+Of course BQN will never be able to invert all the functions you could write (if it could you could earn a *lot* of bitcoins, among other feats). But it does recognize some [header](block.md#block-headers) forms that you can use to specify the inverse of a block function. BQN will trust you and won't verify the results your specified inverse gives.
+
+ {
+ 𝕊𝕩: 𝕩÷𝕩+1
+ 𝕊⁼𝕩: 𝕩÷𝕩-1
+ }
+
+The above function could also be defined with the automatically invertible `1⊸+⌾÷`, but maybe there's a numerical reason to use the definition above. Like a normal header, an undo header reflects the normal use, but it includes `⁼` and possibly `˜` addition to the function and arguments.
diff --git a/docs/doc/identity.html b/docs/doc/identity.html
index 196b219c..ec710ab6 100644
--- a/docs/doc/identity.html
+++ b/docs/doc/identity.html
@@ -19,7 +19,7 @@
"left"
</pre>
<p>Depending on your past experiences, this could cause some confusion: built-in support for functions that do nothing? Documentation should say why a feature's there and how to use it, not just what it does, so we'll try to address this below. The most important single use is for tacit programming, but there are a variety of other uses as well.</p>
-<p>Of course, it's easy to write block functions <code><span class='Brace'>{</span><span class='Value'>𝕩</span><span class='Brace'>}</span></code> and <code><span class='Brace'>{</span><span class='Value'>𝕨</span><span class='Brace'>}</span></code> that return particular arguments. While I would already make <code><span class='Function'>⊣</span></code> and <code><span class='Function'>⊢</span></code> primitives just because they are common and important, there are also specific disadvantages to using blocks. They fail to indicate that there are no side effects, as primitives would, and they also need special casing for the interpreter to manipulate them when applying Undo (<code><span class='Modifier'>⁼</span></code>) or making other inferences.</p>
+<p>Of course, it's easy to write block functions <code><span class='Brace'>{</span><span class='Value'>𝕩</span><span class='Brace'>}</span></code> and <code><span class='Brace'>{</span><span class='Value'>𝕨</span><span class='Brace'>}</span></code> that return particular arguments. While I would already make <code><span class='Function'>⊣</span></code> and <code><span class='Function'>⊢</span></code> primitives just because they are common and important, there are also specific disadvantages to using blocks. They fail to indicate that there are no side effects, as primitives would, and they also need special casing for the interpreter to manipulate them when applying <a href="undo.html">Undo</a> (<code><span class='Modifier'>⁼</span></code>) or making other inferences.</p>
<h2 id="filling-arrays">Filling arrays</h2>
<p>What's the easiest way to create a matrix with 0 on the first row, 1 on the second, and so on? Probably this one, with <a href="map.html#table">table</a>:</p>
<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=KOKGlTQpIOKKo+KMnCDihpU1">↗️</a><pre> <span class='Paren'>(</span><span class='Function'>↕</span><span class='Number'>4</span><span class='Paren'>)</span> <span class='Function'>⊣</span><span class='Modifier'>⌜</span> <span class='Function'>↕</span><span class='Number'>5</span>
diff --git a/docs/doc/index.html b/docs/doc/index.html
index 1c68347a..356773a9 100644
--- a/docs/doc/index.html
+++ b/docs/doc/index.html
@@ -67,6 +67,7 @@
<li><a href="couple.html">Solo, Couple, and Merge</a> (<code><span class='Function'>≍&gt;</span></code>)</li>
<li><a href="take.html">Take and Drop</a> (<code><span class='Function'>↑</span></code>)</li>
<li><a href="transpose.html">Transpose</a> (<code><span class='Function'>⍉</span></code>)</li>
+<li><a href="undo.html">Undo</a> (<code><span class='Modifier'>⁼</span></code>)</li>
<li><a href="windows.html">Windows</a> (<code><span class='Function'>↕</span></code>)</li>
</ul>
<p>Environment:</p>
diff --git a/docs/doc/primitive.html b/docs/doc/primitive.html
index 56b8a1a3..4c6ef8a8 100644
--- a/docs/doc/primitive.html
+++ b/docs/doc/primitive.html
@@ -506,7 +506,7 @@
</tr>
<tr>
<td><code><span class='Modifier'>⁼</span></code></td>
-<td>Undo</td>
+<td><a href="undo.html">Undo</a></td>
<td><code><span class='Modifier2'>⍟</span></code></td>
<td><a href="repeat.html">Repeat</a></td>
</tr>
diff --git a/docs/doc/repeat.html b/docs/doc/repeat.html
index 2de6fd6e..bfbe28e5 100644
--- a/docs/doc/repeat.html
+++ b/docs/doc/repeat.html
@@ -17,7 +17,7 @@
<span class='Function'>F</span><span class='Modifier2'>⍟</span><span class='Number'>4</span> <span class='Gets'>←→</span> <span class='Function'>F</span><span class='Modifier2'>∘</span><span class='Function'>F</span><span class='Modifier2'>∘</span><span class='Function'>F</span><span class='Modifier2'>∘</span><span class='Function'>F</span>
</pre>
<p><code><span class='Function'>F</span><span class='Modifier2'>⍟</span><span class='Number'>0</span></code> repeats <code><span class='Function'>F</span></code> zero times, that is, does nothing. Like <code><span class='Value'>n</span><span class='Function'>⋆</span><span class='Number'>0</span></code> gives the multiplicative identity <code><span class='Number'>1</span></code>, <code><span class='Function'>F</span><span class='Modifier2'>⍟</span><span class='Number'>0</span></code> is the compositional <a href="identity.html">identity</a>, <code><span class='Function'>⊢</span></code>. Since <code><span class='Function'>F</span><span class='Modifier2'>⍟</span><span class='Number'>1</span></code> applies <code><span class='Function'>F</span></code> and <code><span class='Function'>F</span><span class='Modifier2'>⍟</span><span class='Number'>0</span></code> doesn't, Repeat might be pronounced &quot;if&quot; or &quot;conditional&quot; when <code><span class='Function'>𝔾</span></code> is boolean.</p>
-<p>BQN's Repeat modifier has some extra functionality relative to the mathematical version. It allows a left argument, and some extensions to the right operand <code><span class='Function'>𝔾</span></code>. As usual for 2-modifiers, <code><span class='Function'>𝔾</span></code> is actually a function that applies to the arguments to give a result. The result can be a natural number as shown above, or a negative number to Undo (<code><span class='Modifier'>⁼</span></code>) <code><span class='Function'>𝔽</span></code>, or an array of values.</p>
+<p>BQN's Repeat modifier has some extra functionality relative to the mathematical version. It allows a left argument, and some extensions to the right operand <code><span class='Function'>𝔾</span></code>. As usual for 2-modifiers, <code><span class='Function'>𝔾</span></code> is actually a function that applies to the arguments to give a result. The result can be a natural number as shown above, or a negative number to <a href="undo.html">Undo</a> (<code><span class='Modifier'>⁼</span></code>) <code><span class='Function'>𝔽</span></code>, or an array of values.</p>
<h2 id="left-argument">Left argument</h2>
<p>If <code><span class='Value'>𝕨</span></code> is given, it's passed as the left argument to <code><span class='Function'>𝔽</span></code> for every invocation.</p>
<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=MyAr4o2fMiA3CjMgKyAzICsgNw==">↗️</a><pre> <span class='Number'>3</span> <span class='Function'>+</span><span class='Modifier2'>⍟</span><span class='Number'>2</span> <span class='Number'>7</span>
diff --git a/docs/doc/transpose.html b/docs/doc/transpose.html
index ee3e926c..e0cdf512 100644
--- a/docs/doc/transpose.html
+++ b/docs/doc/transpose.html
@@ -63,7 +63,7 @@
</pre>
-<p>To exchange multiple axes, use the <a href="repeat.html">Repeat</a> modifier. A negative power moves axes in the other direction, just like how <a href="reverse.html#rotate">Rotate</a> handles negative left arguments. In particular, to move the last axis to the front, use Undo (as you might expect, this exactly inverts <code><span class='Function'>⍉</span></code>).</p>
+<p>To exchange multiple axes, use the <a href="repeat.html">Repeat</a> modifier. A negative power moves axes in the other direction, just like how <a href="reverse.html#rotate">Rotate</a> handles negative left arguments. In particular, to move the last axis to the front, use <a href="undo.html">Undo</a> (as you might expect, this exactly inverts <code><span class='Function'>⍉</span></code>).</p>
<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=4omiIOKNieKNnzMgYTIzNDU2CgriiaIg4o2J4oG8IGEyMzQ1Ng==">↗️</a><pre> <span class='Function'>≢</span> <span class='Function'>⍉</span><span class='Modifier2'>⍟</span><span class='Number'>3</span> <span class='Value'>a23456</span>
⟨ 5 6 2 3 4 ⟩
diff --git a/docs/doc/undo.html b/docs/doc/undo.html
new file mode 100644
index 00000000..973a942a
--- /dev/null
+++ b/docs/doc/undo.html
@@ -0,0 +1,53 @@
+<head>
+ <link href="../favicon.ico" rel="shortcut icon" type="image/x-icon"/>
+ <link href="../style.css" rel="stylesheet"/>
+ <title>BQN: Undo</title>
+</head>
+<div class="nav"><a href="https://github.com/mlochbaum/BQN">BQN</a> / <a href="../index.html">main</a> / <a href="index.html">doc</a></div>
+<h1 id="undo">Undo</h1>
+<p>Oh no, you've deleted a function after spending half an hour writing it! Well… hopefully your editor can help with that. But maybe you'll be interested to hear that BQN can reverse the action of some functions—ones that <em>don't</em> lose information. This capability is also used by <a href="repeat.html">Repeat</a> (<code><span class='Modifier2'>⍟</span></code>) to repeat a negative number of times.</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=MiDijL0gImFiY2RlIgoKMiDijL3igbwgMiDijL0gImFiY2RlIg==">↗️</a><pre> <span class='Number'>2</span> <span class='Function'>⌽</span> <span class='String'>&quot;abcde&quot;</span>
+"cdeab"
+
+ <span class='Number'>2</span> <span class='Function'>⌽</span><span class='Modifier'>⁼</span> <span class='Number'>2</span> <span class='Function'>⌽</span> <span class='String'>&quot;abcde&quot;</span>
+"abcde"
+</pre>
+<p>Above is one example of Undo (<code><span class='Modifier'>⁼</span></code>) in action. <a href="reverse.html">Rotate</a> shifts the elements of a list left, and undoing shifts them to the right. BQN's ability to undo functions covers a lot of cases and can seem somewhat magical:</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=KEZuIOKGkCAt4p+cMeKMvijCrzHiirjiipEpKSAiQlFOIgoKRm7igbwgRm4gIkJRTiI=">↗️</a><pre> <span class='Paren'>(</span><span class='Function'>Fn</span> <span class='Gets'>←</span> <span class='Function'>-</span><span class='Modifier2'>⟜</span><span class='Number'>1</span><span class='Modifier2'>⌾</span><span class='Paren'>(</span><span class='Number'>¯1</span><span class='Modifier2'>⊸</span><span class='Function'>⊑</span><span class='Paren'>))</span> <span class='String'>&quot;BQN&quot;</span>
+"BQM"
+
+ <span class='Function'>Fn</span><span class='Modifier'>⁼</span> <span class='Function'>Fn</span> <span class='String'>&quot;BQN&quot;</span>
+"BQN"
+</pre>
+<p>Here it undoes a function to decrement the last character by incrementing that character. In part this is enabled by the clean design of BQN primitives, because better-behaved functions like those using structural Under are easier to invert.</p>
+<h2 id="the-rules">The rules</h2>
+<p>If <code><span class='Function'>𝔽</span></code> can be inverted exactly, then Undo just does that. However, there are also some other functions that BQN inverts. For example, the squaring function <code><span class='Function'>×</span><span class='Modifier'>˜</span></code> has both a positive and a negative inverse, and yet:</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=w5fLnCDCrzMKw5fLnOKBvCDDl8ucIMKvMyAgIyBJdCdzIG5vdCB0aGUgc2FtZSE=">↗️</a><pre> <span class='Function'>×</span><span class='Modifier'>˜</span> <span class='Number'>¯3</span>
+9
+ <span class='Function'>×</span><span class='Modifier'>˜⁼</span> <span class='Function'>×</span><span class='Modifier'>˜</span> <span class='Number'>¯3</span> <span class='Comment'># It's not the same!
+</span>3
+</pre>
+<p>Don't worry, this isn't 'nam. Undo doesn't always satisfy <code><span class='Value'>𝕩</span> <span class='Function'>≡</span> <span class='Function'>𝔽</span><span class='Modifier'>⁼</span> <span class='Function'>𝔽</span> <span class='Value'>𝕩</span></code>, but it <em>does</em> obey <code><span class='Value'>𝕩</span> <span class='Function'>≡</span> <span class='Function'>𝔽</span> <span class='Function'>𝔽</span><span class='Modifier'>⁼</span> <span class='Value'>𝕩</span></code>. That is, it gives one possible argument that could have been passed to <code><span class='Function'>𝔽</span></code>, just not necessarily the one that actually was. BQN is conservative in how it uses this freedom, so that it won't for example make up new elements entirely to find an inverse. It's usually used when there's an obvious or standard way to pick which of the possible values should be returned.</p>
+<p>In a BQN with floating-point numbers, computations are approximate, so the inverse is allowed to be approximate as well (any error should still be very small though).</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=NiAtIOKImuKBvOKImjY=">↗️</a><pre> <span class='Number'>6</span> <span class='Function'>-</span> <span class='Function'>√</span><span class='Modifier'>⁼</span><span class='Function'>√</span><span class='Number'>6</span>
+8.881784197001252e¯16
+</pre>
+<h2 id="whats-supported">What's supported?</h2>
+<p>For the full list, see <a href="../spec/inferred.html#undo">the specification</a>. An individual implementation might support a lot more functionality than is required, so if you're not concerned about portability just try out whatever function you're interested in.</p>
+<p>Arithmetic and simple combinators are usually invertible. A compound function that refers to its argument just once, like <code><span class='Number'>6</span><span class='Function'>+⌽</span><span class='Modifier2'>∘</span><span class='Function'>⍉</span></code>, can typically be undone, but one that uses the argument in two different ways, such as <code><span class='Function'>⊢+⋆</span></code>, probably can't.</p>
+<p>A few notable inverses are the <a href="arithmetic.html#basic-arithmetic">logarithm</a> <code><span class='Function'>⋆</span><span class='Modifier'>⁼</span></code>, <a href="transpose.html">un-Transpose</a> <code><span class='Function'>⍉</span><span class='Modifier'>⁼</span></code>, and <a href="replicate.html#inverse">Indices inverse</a> <code><span class='Function'>/</span><span class='Modifier'>⁼</span></code>. <a href="enclose.html">Enclose</a> inverse, <code><span class='Function'>&lt;</span><span class='Modifier'>⁼</span></code>, is an alternative to <a href="pick.html#first">First</a> that requires its argument to be a unit.</p>
+<p>Structural functions like <a href="take.html">Take</a> and <a href="shift.html">shifts</a> that remove elements from <code><span class='Value'>𝕩</span></code> can't be inverted, because given the result there's no way to know what the elements should be. However, there are two special cases that have inverses defined despite losing data: these are <code><span class='Function'>⊣</span><span class='Modifier'>⁼</span></code> and <code><span class='Value'>k</span><span class='Modifier'>⁼</span></code> where <code><span class='Value'>k</span></code> is a constant (a data type, or <code><span class='Value'>k</span><span class='Modifier'>˙</span></code>). For these, <code><span class='Value'>𝕩</span></code> is required to <a href="match.html">match</a> the always returned value <code><span class='Value'>𝕨</span></code> or <code><span class='Value'>k</span></code>, and this value is also used for the result—even though any result would be valid, as these functions ignore <code><span class='Value'>𝕩</span></code>.</p>
+<a class="replLink" title="Open in the REPL" target="_blank" href="https://mlochbaum.github.io/BQN/try.html#code=MyDiiqPigbwgNAozIOKKo+KBvCAz">↗️</a><pre> <span class='Number'>3</span> <span class='Function'>⊣</span><span class='Modifier'>⁼</span> <span class='Number'>4</span>
+ERROR
+ <span class='Number'>3</span> <span class='Function'>⊣</span><span class='Modifier'>⁼</span> <span class='Number'>3</span>
+3
+</pre>
+<h2 id="undo-headers">Undo headers</h2>
+<p>Undo headers are currently supported only by dzaima/BQN.</p>
+<p>Of course BQN will never be able to invert all the functions you could write (if it could you could earn a <em>lot</em> of bitcoins, among other feats). But it does recognize some <a href="block.html#block-headers">header</a> forms that you can use to specify the inverse of a block function. BQN will trust you and won't verify the results your specified inverse gives.</p>
+<pre><span class='Brace'>{</span>
+ <span class='Function'>𝕊</span><span class='Value'>𝕩:</span> <span class='Value'>𝕩</span><span class='Function'>÷</span><span class='Value'>𝕩</span><span class='Function'>+</span><span class='Number'>1</span>
+ <span class='Function'>𝕊</span><span class='Modifier'>⁼</span><span class='Value'>𝕩:</span> <span class='Value'>𝕩</span><span class='Function'>÷</span><span class='Value'>𝕩</span><span class='Function'>-</span><span class='Number'>1</span>
+<span class='Brace'>}</span>
+</pre>
+<p>The above function could also be defined with the automatically invertible <code><span class='Number'>1</span><span class='Modifier2'>⊸</span><span class='Function'>+</span><span class='Modifier2'>⌾</span><span class='Function'>÷</span></code>, but maybe there's a numerical reason to use the definition above. Like a normal header, an undo header reflects the normal use, but it includes <code><span class='Modifier'>⁼</span></code> and possibly <code><span class='Modifier'>˜</span></code> addition to the function and arguments.</p>