💾 Archived View for dcreager.net › concatenative › reduction.gmi captured on 2024-06-16 at 12:32:47. Gemini links have been rewritten to link to archived content
⬅️ Previous capture (2024-03-21)
-=-=-=-=-=-=-
Starting with the natural basis:
[B] [A] cat ≜ [B A]
[A] drop ≜
[A] dup ≜ [A] [A]
[A] i ≜ A
[B] [A] swap ≜ [A] [B]
[A] unit ≜ [[A]]
The natural normal concatenative basis
Some examples using reduction instead of stacks:
[B] [A] cons ≜ [B] [A] [unit] swap unit cat i cat
^^^^^^^^^^^^^^^
= [B] [unit] [A] unit cat i cat
^^^^^^^^
= [B] [unit] [[A]] cat i cat
^^^^^^^^^^^^^^^^
= [B] [unit [A]] i cat
^^^^^^^^^^^^
= [B] unit [A] cat
^^^^^^^^
= [[B]] [A] cat
^^^^^^^^^^^^^
= [[B] A]
[B] [A] cons ≜ [B] [A] swap unit swap cat
^^^^^^^^^^^^
= [A] [B] unit swap cat
^^^^^^^^
= [A] [[B]] swap cat
^^^^^^^^^^^^^^
= [[B]] [A] cat
^^^^^^^^^^^^^
= [[B] A]
[B] [A] k ≜ [B] [A] swap drop i
^^^^^^^^^^^^
= [A] [B] drop i
^^^^^^^^
= [A] i
^^^^^
= A
false ≜ [drop]
true ≜ [swap drop]
or ≜ dup i
false true or ≜ [drop] [swap drop] dup i
^^^^^^^^^^^^^^^
= [drop] [swap drop] [swap drop] i
^^^^^^^^^^^^^
= [drop] [swap drop] swap drop
^^^^^^^^^^^^^^^^^^^^^^^
= [swap drop] [drop] drop
^^^^^^^^^^^
= [swap drop]
= true
false false or ≜ [drop] [drop] dup i
^^^^^^^^^^
= [drop] [drop] [drop] i
^^^^^^^^
= [drop] [drop] drop
^^^^^^^^^^^
= [drop]
= false
All of these have a single sequence of reductions that is possible, because they do not require reducing anything nested in a quotation. Here's an example from Kerby that does have multiple reduction paths:
[B] [A] cat ≜ [B] [A] [[i] dip i] cons cons
^^^^^^^^^^^^^^^^^^^^
= [B] [[A] [i] dip i] cons
^^^^^^^^^^^^^^^^^^^^^^^^
= [[B] [A] [i] dip i]
^^^^^^^^^^^
= [[B] i [A] i]
^^^^^
= [B [A] i]
^^^^^
= [B A]
Aiming for
[B] [A] ℕ₀ == B
[B] [A] ℕ₁ == [B] A
[B] [A] ℕ₂ == [[B] A] A
[B] [A] ℕ₃ == [[[B] A] A] A
…
Definitions
[B] [A] ℕ₀ ≜ [B] [A] drop i
^^^^^^^^
= [B] i
^^^^^
= B
[B] [A] ℕ₁ ≜ [B] [A] i
^^^^^
= [B] A
[ℕ] succ ≜ [ℕ] [ℕ₁] +
= [ℕ] [i] [cons b] cons s
^^^^^^^^^^^^^^^^^
= [ℕ] [[i] cons b] s
[B] [A] ℕ₂ ≜ [B] [A] [ℕ₁] succ
= [B] [A] [i] [[i] cons b] s
^^^^^^^^^^^^^^^^^^^^^^
= [B] [[A] i] [A] [i] cons b
^^^^^^^^^^^^
= [B] [[A] i] [[A] i] b
^^^^^^^^^^^^^^^^^^^^^
= [[B] [A] i] [A] i
^^^^^
= [[B] [A] i] A
^^^^^
= [[B] A] A