Foundations of Dawn: The Untyped Concatenative Calculus

By Scott J Maddox.

First published 2021-11-19.

Updated on 2021-11-23 to address comments by lobste.rs user gasche.

Updated on 2022-11-01 to distinguish between sequence termination indices when composing two quotes. Thank you, Maja Kądziołka, for identifying this error and notifying me via email.

One of my long term goals for Dawn is to democratize formal software verification in order to make it much more feasible and realistic to write perfect software. In order for this goal to be achievable, it’s critical for Dawn to have a solid and sound theoretical foundation. In pursuit of this goal, in this Foundations of Dawn series, I will formalize the core of the language in a series of incremental steps, and for each step I will implement a toy programming language. In this first post in the series, I will formalize the untyped concatenative calculus, which is the tiny core calculus that Dawn is ultimately based on, and I will give some examples of how data types and computations can be encoded in it.

If you identify any errors or omissions in this post or in the associated toy programming language, I would greatly appreciate it if you would notify me. I would be happy to give attribution for any corrections or suggestions.

Note that while the untyped concatenative calculus can be embedded in the untyped lambda calculus (any Turing-complete system can be embedded in any other Turing-complete system), they are two distinct models of computation. There will inevitably be some computations which can be more compactly or efficiently expressed in the untyped concatenative calculus than in the untyped lambda calculus, and visa versa.

I chose to model Dawn on the concatenative calculus rather than on the lambda calculus or any other model of computation because 1) it naturally enforces linearity, in the sense of linear logic, and therefor maps more directly to actual hardware, 2) it is amenable to static analysis, including full type inference, 3) it simplifies factoring and refactoring, and 4) it has an extremely simple syntax and semantics.

Please note that while the theory described here is quite abstract and the associated toy programming language is inefficient, I am designing Dawn itself to be compiled to extremely efficient machine code. In the long run, I expect optimizing compilers for Dawn terms to consistently produce higher performing machine code than for all but the most highly tuned C procedures, thanks in no small part to Dawn’s extremely simple and highly analyzable core syntax and semantics.

Syntax

The syntax of the untyped concatenative calculus has just three basic forms, which are shown below. In contrast to the lambda calculus, there are no variables or lambda abstractions from which arbitrary combinators can be created. Instead, there are a finite number of intrinsic terms and two operations for combining those intrinsic terms into more complex terms: 1) quotation, which takes the place of lambda abstraction, and 2) composition, which takes the place of function application. In this embodiment, we consider six core intrinsics, $\text{swap}$, $\text{clone}$, $\text{drop}$, $\text{quote}$, $\text{compose}$, and $\text{apply}$, who’s semantics are defined in the next section, and we denote quotation by enclosing sub-expressions in square brackets and composition by juxtaposition of two or more sub-expressions.

$$\begin{array}{ l l r l l } \text{Expressions} & e & = & i & \text{intrinsic} \\ & & | & [e] & \text{quote} \\ & & | & e_1~e_2~...~e_n & \text{compose} \end{array}$$

Semantics

The semantics of this calculus are defined by the effects that expressions have on stacks of values. In this core calculus, all values take the form of quoted expressions, and value stacks are either empty or they are constructed by pushing single values on an existing value stack.

$$\begin{array}{ l l r l l } \text{Values} & v & = & [e] & \text{quoted expression} \\ \\ \text{Value Stacks} & \langle V\rangle & = & \langle \rangle & \text{empty} \\ & & | & \langle V~v\rangle & \text{push} \end{array}$$

Given this definition for value stacks, the semantics of this calculus are fully defined by the small step semantics for the six core intrinsics, by the small step semantics for quotations, and by the left-to-right evaluation of composed sub-expressions:

$$\begin{array}{ l l l l } \langle V~v~v'\rangle & \text{swap} & \longrightarrow & ~\langle V~v'~v\rangle \\ \langle V~v\rangle & \text{clone} & \longrightarrow & ~\langle V~v~v\rangle \\ \langle V~v\rangle & \text{drop} & \longrightarrow & ~\langle V\rangle \\ \langle V~v\rangle & \text{quote} & \longrightarrow & ~\langle V~[v]\rangle \\ \langle V~[e_1~...~e_n]~[e'_1~...~e'_m]\rangle & \text{compose} & \longrightarrow & ~\langle V~[e_1~...~e_n~e_1'~...~e'_m]\rangle \\ \langle V~[e]\rangle & \text{apply} & \longrightarrow & ~\langle V\rangle~e \\ \langle V\rangle & [e] & \longrightarrow & ~\langle V~[e]\rangle \\ \langle V\rangle & e_1~e_2~...~e_n & = & ~((((\langle V\rangle~e_1)~e_2)~...)~e_n) \end{array}$$

Perhaps surprisingly, this set of intrinsics is sufficient for Turing completeness. In fact, Turing completeness can be achieved with as few as two intrinsics, but this set of six is arguably the most orthogonal and intuitive. The first three intrinsics, $\text{swap}$, $\text{clone}$, and $\text{drop}$, directly correspond to the three common structural rules from proof theory:

By restricting the use of these intrinsics, we can cover the full range of substructural logics. This will become particularly important once we introduce types, and qualified types in particular, since it will provide the bases for a substructural type system that will allow us to both express and statically enforce a variety of constraints on resources. This will allow us, for example, to statically and automatically prove that files are not read from or written to after they are closed. The Rust programming language provides a particularly notable example of how useful substructural types can be, since they play a pivotal role in Rust’s static guarantees, such as memory safety and freedom from data races.

Encoding Data Types and Computations

In order to exercise this calculus a bit, in this section we’ll take a look at how we might perform some computations in it. Although this core concatenative calculus does not include any built-in data types, various data types can be encoded as quoted expressions in a way very similar to how data types can be encoded in the untyped lambda calculus. Since I do not ultimate intend to use these encodings in Dawn, we will not attempt to derive systematic encodings in the style of Boehm-Berarducci encodings. Instead, we will simply take inspiration from the Church encodings for booleans and natural numbers in the untyped lambda calculus.

Encoding Booleans

We will encode the boolean values $\text{false}$ and $\text{true}$ as quoted higher order terms with the following big-step semantics:

$\begin{array}{ l l l l } \qquad\langle V~v~v'\rangle & \text{false}~\text{apply} & \Downarrow & \langle V~v\rangle \\ \qquad\langle V~v~v'\rangle & \text{true}~\text{apply} & \Downarrow & \langle V~v'\rangle \end{array}$

Essentially, when applied, $\text{false}$ takes two values, retains the left-most value, and drops the right-most value, while $\text{true}$ does the exact opposite. This might seem backwards, but you’ll see later why I’ve chosen this encoding rather than the opposite encoding. These semantics are fulfilled by the following definitions:

$\begin{array}{ l l l } \qquad\text{false} & = & [\text{drop}] \\ \qquad\text{true} & = & [\text{swap}~\text{drop}] \end{array}$

Given these definitions, we can go on to define the various boolean operators, such as the disjunction operator, $\text{or}$, which has the following big-step semantics and definition:

$\begin{array}{ l l l l } \qquad\langle V~\text{false}~\text{false}\rangle & \text{or} & \Downarrow & ~\langle V~\text{false}\rangle \\ \qquad\langle V~\text{false}~\text{true}\rangle & \text{or} & \Downarrow & ~\langle V~\text{true}\rangle \\ \qquad\langle V~\text{true}~\text{false}\rangle & \text{or} & \Downarrow & ~\langle V~\text{true}\rangle \\ \qquad\langle V~\text{true}~\text{true}\rangle & \text{or} & \Downarrow & ~\langle V~\text{true}\rangle \end{array}$

$\qquad\text{or}=\text{clone}~\text{apply}$

The semantics and definitions for the other boolean operators are left as an exercise for the reader.

Useful Terms

In order to implement more complex operations, it is sometimes necessary to access values below the top two stack slots. This can be accomplished through the $\text{quote}_n$ and $\text{rotate}_n$ series of terms. To derive these, we will begin by defining the big-step semantics for the first two instances of each:

$\begin{array}{ l l l l } \qquad\langle V~v_1~v_2\rangle & \text{quote}_2 & \Downarrow & \langle V~[v_1~v_2]\rangle \\ \qquad\langle V~v_1~v_2~v_3\rangle & \text{quote}_3 & \Downarrow & \langle V~[v_1~v_2~v_3]\rangle \\ \\ \qquad\langle V~v_1~v_2~v_3\rangle & \text{rotate}_3 & \Downarrow & \langle V~v_2~v_3~v_1\rangle \\ \qquad\langle V~v_1~v_2~v_3~v_4\rangle & \text{rotate}_4 & \Downarrow & \langle V~v_2~v_3~v_4~v_1\rangle \end{array}$

These semantics are fulfilled by the following definitions:

$\begin{array}{ l l l } \qquad\text{quote}_2 & = & \text{quote}~\text{swap}~\text{quote}~\text{swap}~\text{compose} \\ \qquad\text{quote}_3 & = & \text{quote}_2~\text{swap}~\text{quote}~\text{swap}~\text{compose} \\ \\ \qquad\text{rotate}_3 & = & \text{quote}_2~\text{swap}~\text{quote}~\text{compose}~\text{apply} \\ \qquad\text{rotate}_4 & = & \text{quote}_3~\text{swap}~\text{quote}~\text{compose}~\text{apply} \end{array}$

This is enough to see the patterns and to generalize to arbitrary $N\gt2$:

$\qquad\langle V~v_1~...~v_N\rangle~\text{quote}_n\Downarrow\langle V~[v_1~...~v_N]\rangle$

$\qquad\langle V~v_1~...~v_N\rangle~\text{rotate}_n\Downarrow\langle V~v_2~...~v_{N-1}~v_1\rangle$

$\qquad\text{quote}_n=\text{quote}_{n-1}~\text{swap}~\text{quote}~\text{swap}~\text{compose}$

$\qquad\text{rotate}_n=\text{quote}_{n-1}~\text{swap}~\text{quote}~\text{compose}~\text{apply}$

Another useful series of terms is $\text{compose}_n$, which composes $n$ quoted expressions, for arbitrary $n \ge 2$:

$\qquad\langle V~[v_1]~...~[v_n]\rangle~\text{compose}_n\Downarrow\langle V~[v_1~...~v_n]\rangle$

$\qquad\text{compose}_2=\text{compose}$

$\qquad\text{compose}_n=\text{compose}~\text{compose}_{n-1}$

Encoding Natural Numbers

Taking inspiration from Church encodings, again, we can encode each natural number $n$ as a higher order term that, when applied to a given quote, applies that quote $n$ times. The first few natural numbers have the following big-step semantics, which are fulfilled by the following definitions:

$\begin{array}{ l l l } \qquad\langle V~[e]\rangle~\mathbb{N}_0~\text{apply} & \Downarrow & \langle V\rangle \\ \qquad\langle V~[e]\rangle~\mathbb{N}_1~\text{apply} & \Downarrow & \langle V\rangle~e \\ \qquad\langle V~[e]\rangle~\mathbb{N}_2~\text{apply} & \Downarrow & \langle V\rangle~e~e \\ \qquad\langle V~[e]\rangle~\mathbb{N}_3~\text{apply} & \Downarrow & \langle V\rangle~e~e~e \\ \qquad\langle V~[e]\rangle~\mathbb{N}_4~\text{apply} & \Downarrow & \langle V\rangle~e~e~e~e \end{array}$

$\begin{array}{ l l l } \qquad\mathbb{N}_0 & = & [\text{drop}] \\ \qquad\mathbb{N}_1 & = & [\text{apply}] \\ \qquad\mathbb{N}_2 & = & [\text{clone}~\text{compose}~\text{apply}] \\ \qquad\mathbb{N}_3 & = & [[\text{clone}]~\mathbb{N}_2~\text{apply}~[\text{compose}]~\mathbb{N}_2~\text{apply}~\text{apply}] \\ \qquad\mathbb{N}_4 & = & [[\text{clone}]~\mathbb{N}_3~\text{apply}~[\text{compose}]~\mathbb{N}_3~\text{apply}~\text{apply}] \end{array}$

Note that $\mathbb{N}_0$ has the same representation, $[\text{drop}]$, as $\text{false}$. This is why I chose this particular encoding for $\text{true}$ and $\text{false}$. It seems much more natural for $\mathbb{N}_0$ and $\text{false}$ to share the same representation than it does for $\mathbb{N}_0$ and $\text{true}$ to share the same representation.

Also note that $\mathbb{N}_3$ and $\mathbb{N}_4$ reveal a pattern that can be generalized and used as the definition for arbitrary $n\gt0$:

$\qquad\langle V~[e]\rangle~\mathbb{N}_n~\text{apply}\Downarrow\langle V\rangle~e^n$

$\qquad\mathbb{N}_n=[[\text{clone}]~\mathbb{N}_{n-1}~\text{apply}~[\text{compose}]~\mathbb{N}_{n-1}~\text{apply}~\text{apply}]$

Where:

$\qquad e^n= \underbrace{e~e~...~e}_{n~{\text{times}}}$

We can then define terms for succession, addition, and multiplication:

$\qquad\langle V~[e]~\mathbb{N}_n\rangle~\text{succ}~\text{apply}\Downarrow\langle V\rangle~e^{n+1}$

$\qquad\text{succ}=\text{quote}~[\text{apply}]~\text{compose}~[[\text{clone}]]~\text{swap}~\text{clone}~[[\text{compose}]]~\text{swap}~[\text{apply}]~\text{compose}_5$

$\qquad\langle V~[e]~\mathbb{N}_n~\mathbb{N}_m\rangle~\text{add}~\text{apply}\Downarrow\langle V\rangle~e^{n+m}$

$\qquad\text{add}=[\text{succ}]~\text{swap}~\text{apply}$

$\qquad\langle V~[e]~\mathbb{N}_n~\mathbb{N}_m\rangle~\text{mul}~\text{apply}\Downarrow\langle V\rangle~e^{n\times m}$

$\qquad\text{mul}=\mathbb{N}_0~\text{rotate}_3~\text{quote}~[\text{add}]~\text{compose}~\text{rotate}_3~\text{apply}$

It’s perhaps worth noting that this is not a particularly efficient encoding for the natural numbers. Since the definition for $\mathbb{N}_n$ contains $\mathbb{N}_{n-1}$ twice, the encodings grow exponentially in size with $n$. There is at least one other series of higher order functions that applies a quoted expression $n$ times and is more compact, but that series performs applications one at a time rather than all at once, and therefor does not strictly fulfill the big step semantics above. It’s unclear if this exact big step semantics is required or if there is a more compact encoding that fulfills this big step semantics. Since I do not intend to use these encodings in Dawn, we will leave such investigations to the interested reader.

Recursion

In this simple concatenative calculus, just as in the lambda calculus, it is not valid to recursively call a term from within its own definition. Nonetheless, recursion is possible by passing a copy of a quoted term to itself using higher order expressions such as $\text{clone}~\text{apply}$. The simplest recursive expression is perhaps $[\text{clone}~\text{apply}]~\text{clone}~\text{apply}$, which repeats in an infinite loop every other small step:

$\begin{array}{ l l } \qquad & \langle[\text{clone}~\text{apply}]\rangle~\text{clone}~\text{apply} \\ \qquad\longrightarrow & \langle[\text{clone}~\text{apply}]~[\text{clone}~\text{apply}]\rangle~\text{apply} \\ \qquad\longrightarrow & \langle[\text{clone}~\text{apply}]\rangle~\text{clone}~\text{apply} \end{array}$

When implementing this calculus as a programming language, though, it is very straightforward to allow direct recursion within term definitions, as in the implementation described below.

Implementation

In order to test and validate everything written above, I have implemented an interpreter for a toy programming language based on this calculus. The toy programming language extends the core calculus with user-defined terms, which can be directly or mutually recursive. The interpreter is available to try in your browser, and the source code is available on Github. All of the terms described above come predefined, but any and all terms can be redefined by the user. An example session is shown below:

Untyped Concatenative Calculus Interpreter (UCCI)
Type ":help" to see the available commands.

>>> false false or
⟨⟩ false false or
⇓ ⟨false⟩

>>> true or
⟨false⟩ true or
⇓ ⟨true⟩

>>> drop
⟨true⟩ drop
⇓ ⟨⟩

>>> n0 succ
⟨⟩ n0 succ
⇓ ⟨n1⟩

>>> n1 add
⟨n1⟩ n1 add
⇓ ⟨n2⟩

>>> n2 mul
⟨n2⟩ n2 mul
⇓ ⟨n4⟩

>>> drop
⟨n4⟩ drop
⇓ ⟨⟩

>>> :trace true false or
⟨⟩ true false or
⟶ ⟨true⟩ false or
⟶ ⟨true false⟩ or
⟶ ⟨true false⟩ clone apply
⟶ ⟨true false false⟩ apply
⟶ ⟨true false⟩ drop
⟶ ⟨true⟩

>>> {fn drop2 = drop drop}
Defined `drop2`.

>>> true
⟨true⟩ true
⇓ ⟨true true⟩

>>> drop2
⟨true true⟩ drop2
⇓ ⟨⟩

Conclusion

In this first Foundations of Dawn post, I have formally defined the untyped concatenative calculus that Dawn is ultimately based on, and I have given examples of how to encode booleans and natural numbers in this calculus. I have also provided an interpreter for a toy programming language based on this calculus, which I have used to test and validate everything written here.

In the next Foundations of Dawn post, I will formalize the untyped multistack concatenative calculus, which modifies the calculus described in this post to include an arbitrary number of arbitrarily named stacks. As I alluded to in Introducing Dawn (Part 1), multistacks alleviate the pain of stack shuffling and significantly improve readability and writability compared to other concatenative languages, while retaining the positive aspects of concatenative languages. As we’ll see later, multistacks also enable some other very interesting patterns such as something like global variables, but without the drawbacks, and something like a capability or effect system with full inference.

Additional References

The following additional references influenced this work:

• 2002 - Brent Kerby - The Theory of Concatenative Combinators
• 2008 - Diggins - Simple Type Inference for Higher-Order Stack-Oriented Languages
• 2012 - Jon Purdy - Why Concatenative Programming Matters
• 2017 - Robert Kleffner - A Foundation for Typed Concatenative Languages
• 2017 - Jon Purdy - Stanford Seminar - Concatenative Programming: From Ivory to Metal

Discuss this post on Hacker News or Lobsters.