From 46e989035fa921a5a32169cc0a9b897ec313cc2e Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Wed, 24 Mar 2021 22:41:38 -0400 Subject: Specify function Undo headers --- docs/spec/inferred.html | 2 ++ 1 file changed, 2 insertions(+) (limited to 'docs/spec/inferred.html') diff --git a/docs/spec/inferred.html b/docs/spec/inferred.html index 2ff3ce0a..bda3e054 100644 --- a/docs/spec/inferred.html +++ b/docs/spec/inferred.html @@ -470,6 +470,8 @@ +

Undo headers

+

An UndoHead header specifies how a block function acts when undone. Like ordinary headers, undo headers are searched for a match when a block function F is undone, or when F˜ is undone with two arguments (including the two modifier cases 𝔽⟜k and 𝔽𝔾k from the previous section). An UndoHead without "˜" matches the F⁼ case while one with "˜" matches the F˜⁼ case. The left and right arguments are matched to headW and headX as with ordinary headers, and the first matching case is evaluated to give the result of the Undo-derived function.

Under

The Under 2-modifier ⌾ conceptually applies its left operand under the action of its right operand. Setting z←𝕨𝔽⌾𝔾𝕩, it satisfies (𝕨𝔽○𝔾𝕩) ≡ 𝔾z. We might say that 𝔾 transforms values to a new domain, and ⌾𝔾 lifts actions 𝔽 performed in this domain to the original domain of values. For example, addition in the logarithmic domain corresponds to multiplication in the linear domain: +⌾(⋆⁼) is × (but less precise if computed in floating point).

Let v←𝕨𝔽○𝔾𝕩, so that v≡𝔾z. v is of course well-defined, so the inference step is to find z based on v and possibly the original inputs. We distinguish three cases for Under:

-- cgit v1.2.3