💾 Archived View for dcreager.net › concatenative › simpler-cons.gmi captured on 2024-02-05 at 09:32:57. Gemini links have been rewritten to link to archived content

View Raw

More Information

⬅️ Previous capture (2023-11-14)

-=-=-=-=-=-=-

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] ┃