NOT.4:5 - Archetypal Grounding

NOT.4:5.1 - Name a repeated construction without capturing another input

A reader wants to see and change the repeated construction in (x + 1) * (x + 1). The expression denotes ordinary integer arithmetic with a fixed input x. Introduce a local definition: let v = x + 1 in v * v. Here let gives v the value of its defining expression within the following body.

At x = 3 the original expression gives 4 * 4 = 16; the new one first obtains v = 4 and then the same result. For any integer x, substitution of v’s definition recovers the original expression, establishing the general equality under this interpretation. To change the repeated construction to x + 2, change the one definition. The new value at x = 3 is 25, and expansion shows both occurrences received that change.

Now use a larger expression u + (x + 1) * (x + 1) with external inputs u = 10 and x = 3. Introducing let u = x + 1 in u + u * u is wrong: it turns the external u into a local reference and produces 20 instead of 26. A fresh v gives let v = x + 1 in u + v * v, which produces 26. The repair changes the binding choice, not the arithmetic law.

The rule applies to the pure arithmetic interpretation supplied here. If each occurrence instead instructs a fresh observation, sharing their results changes the operation. For example, two sensor reads may return 4 and 5, whose product is 20; one read returning 4 reused twice gives 16. Retain two observations unless their consolidation is justified for the intended use.

NOT.4:5.2 - Compress a sequence while preserving its order

A notation describes ordered cues A and B. The sequence A; B; A; B is to be shortened without changing the order of cues. Define repeat 2 { E } to expand into two copies of the entire finite sequence E, preserving its order. Then:

A; B; A; B  ->  repeat 2 { A; B }

Expansion returns A, B, A, B. The third cue remains A. A reader changing B in every repeated unit can now change it once in the repeated body. If only the final B must change to C, expand or separate that occurrence: A; B; A; C. The earlier abbreviation no longer expresses the intended two identical units.

The tempting form repeat 2 { A }; repeat 2 { B } expands to A, A, B, B. It preserves counts but changes the third cue to B. Counts are insufficient for the selected ordered reading. No rule for exchanging cues was supplied.

This notation states cue order. If intervals, accents or bodily actions distinguish the repetitions, retain those distinctions in E or choose a different abbreviation. The order-preservation result alone supplies no claim about those further observations.

NOT.4:5.3 - Keep a cancellation inside the condition that permits it

For real x, consider if x != 0 then x/x else 0. Only the selected branch is evaluated. Within the first branch, division is defined and the quotient is 1, so the expression can become if x != 0 then 1 else 0.

At x = 2 both expressions return 1; at x = 0 both return 0 without evaluating the quotient. More generally, the two branches cover all real inputs and give the same result in each. Replacing the whole expression by 1 would fail at zero. Replacing an unrelated occurrence of x/x outside that guarded branch would also need its own domain condition. The useful transformation follows the local assumption through its scope.

NOT.4:5.4 - Reconnect an ordered pair after removing two swaps

A diagram carries an ordered pair of integer values on two wires: port 1 carries a and port 2 carries b. A swap exchanges the two values. Its output is (b, a); a second swap restores (a, b). Replace the two swaps by straight connections preserving port numbers. This argument holds for every integer pair.

The enclosing operation subtracts port 2 from port 1. In compact diagram notation:

(1:a, 2:b) -> swap -> swap -> subtract(1, 2)
(1:a, 2:b) -> straight     -> subtract(1, 2)

Both forms return a - b. The replacement makes the source of each subtraction input directly traceable. If the replacement’s outgoing wires are accidentally crossed, the enclosing operation instead receives (b, a) and returns b - a. Inputs (5, 2) then give -3 instead of 3; inputs (2, 5) give 3 instead of -3. Retaining two ports without retaining their correspondence loses the required use.

The diagram describes pure value operations, and the enclosing operation consumes only the ordered pair. That interpretation justifies this replacement in its context. Physical wire length or signal delay would be additional observations requiring a different preservation argument.