## 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

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’?

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