Defining ‘cons’ with only empty quotations

2023-11-07

In Swanson, I'm currently treating stack values and quotations separately, similar to how CBPV and FMC have a clear distinction between values and computations. Concretely, that means that my original definition of ‘cons’ in the natural linear basis (shown below) won't work, since ‘[unit]’ would be a stack value containing an instruction. I need a different definition of ‘cons’, which uses only the instructions in the natural basis, and which only uses empty quotations (i.e. S₀'s ‘nil’ instruction).

=> The natural linear concatenative basis | Call By Push Value (CBPV) | Functional Machine Calculus (FMC)

cons ≜ swap unit swap cat

          ┃ [B] [A] cons
          ┃ [B] [A] swap unit swap cat
      [B] ┃ [A] swap unit swap cat
  [B] [A] ┃ swap unit swap cat
  [A] [B] ┃ unit swap cat
[A] [[B]] ┃ swap cat
[[B]] [A] ┃ cat
  [[B] A] ┃

Turns out that's a better definition not only because it doesn't depend on quoted programs; it's just simpler overall! Can we do the same with ‘sap’?

=> A simpler definition of ‘sap’

Original definition

For reference, here is the original definition that used a quoted program:

cons ≜ [unit] swap unit cat i cat

                 ┃ [B] [A] cons
                 ┃ [B] [A] [unit] swap unit cat i cat
             [B] ┃ [A] [unit] swap unit cat i cat
         [B] [A] ┃ [unit] swap unit cat i cat
  [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] ┃ cat
         [[B] A] ┃