¶Reduction semantics for CC

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]

[B] [A] ℕ₀ == B
[B] [A] ℕ₁ == [B] A
[B] [A] ℕ₂ == [[B] A] A
[B] [A] ℕ₃ == [[[B] A] A] A
           …

[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