Church Booleans in Joy
Tags: joy, elixir
Published: 2020-10-24 12:21:04

*Update: I've since extended the post such that the composed `ifte` function is now semantically identical to the built-in primitive `ifte` function.*

In some of the preceding posts of this series on an artificial life system in the Joy programming language, we have programmed a number of proteins. Conditional execution has been a crucial component of these protein programs. The need for branching logic has surfaced mostly in the recursive sections of our programs: if the base case is met then terminate else recurse.

Nevertheless, the use of the `ifte` (if-then-else) and `true` and `false` Joy functions isn't as pure as it could be for our purposes. First, I would like to limit the data types to only functions and quotations (lists of functions). We have already banished numbers and sets, but had to hold on to Booleans. Second, the `ifte` function strikes me as being too high-level to be implemented as a primitive.

To be fair, "high-level primitives", numbers, sets, booleans, and strings are perfectly acceptable in Joy proper. For our purposes of constructing an artificial life system, however, we are looking for a minimal but useful subset of Joy.

## Interdependence of Joy primitives

The small set of functions/combinators `dup`, `pop`, `swap`, `cons`, `uncons`, `i`, `dip`, `cat`, `unit` that we have encountered so far is enough to render Joy Turing-complete. It's actually more than enough because it turns out that a set of only two appropriately defined combinators will suffice. Take for instance the Ess-Kay (SK) system or some of the more exotic systems invented by Brent Kirby in his Theory of Concatenative Combinators. As such, it is not surprizing that many of these primitive combinators can be expressed in terms of some of the others:

```
cat  == [[i] dip i] cons cons
unit == [] cons
cons == [unit] dip cat
swap == unit dip
dip  == swap unit cat i
i    == [[]] dip dip pop
```

Could it also be possible to express `ifte`, `true`, and `false` in terms of these combinators?

## `ifte` as a primitive

We have treated `ifte` as a primitive function so far. This means that it isn't a composite of other Joy functions. It is instead considered to be a given of the language, implemented in Elixir, the language in which we have implemented the Joy interpreter. Here is the implementation in Elixir:

``` elixir
def ifte(stack) do
  [else_quot, then_quot, if_quot | rest] = stack
  [result | _] = __execute(rest, if_quot)

  quot =
    if result !== false do
      then_quot
    else
      else_quot
    end

  __execute(rest, quot)
end
```

It expects three quotations on the stack. At the top it expects the quoted else-block, below it the quoted then-block and below that the quoted if-block (the predicate). After having popped these quotations from the stack, it executes the if-block against the remainder of the stack. It then pops the resulting (usually boolean) value from the stack, checks that it is not equal to  `false`, in which case it executes the then-block against the stack as if the if-block was never executed. That is, before executing the then-block the stack is restored to the state in which is was prior to executing the if-block. If, on the other hand, the if-block leaves a `false` on the stack, the else-block is executed, also against a restored stack.

This implementation allows us to call `ifte` like this:

``` joy
[if-block] [then-block] [else-block] ifte
```

For example (allowing integers and strings):

``` joy
2 3 [<] ["the first value is smaller"] ["the second value is smaller"] ifte
```

Which would leave `2 3 "the first value is smaller"` on the stack. There are two things to notice. All three of the quotations (if, then and else), when executed, only see `2 3` on the stack. In addition, if the if-block is executed and leaves anything other than `false` on the stack, the then-block will be executed.

## `true` and `false` as primitives

Our Elixir implementation of Joy treats all functions that don't have explicit definitions as if they simply place themselves on the stack. This means that the boolean `true` and `false`, which are actually functions, would simply place themselves on the stack when executed. However, we could also explicitly implement `true` and `false` in Elixir like this:

``` elixir
def unquote(true)(stack) do
  [true | stack]
end

def unquote(false)(stack) do
  [false | stack]
end
```

The `unquote` macro is required, because `true` and `false` are something like reserved words in Elixir. In fact, `true` and `false` are not strictly speaking booleans, but rather atoms:

``` elixir
iex(1)> true == :true
true
iex(2)> false == :false
true
```

Their boolean semantics comes from the functions and macros (`if`, `not`, `and`, etc.) that act on them. This is also true for our Joy implementation. The fact that the `true` Joy function acts in the way that one would expect from the boolean `true` can be entirely ascribed to the implementation of the `ifte` function that acts on it.

This is good news because it means that we can make (compositions) of other Joy functions to assume the behaviour and meaning of booleans simply by how we implement `ifte` and other functions that act on booleans. Let's take a short detour to the land of Church encoding, before we attempt to eliminate `ifte`, `true` and `false` as Joy primitives.

## Church encoding

Functions are the only primitive data types in untyped lambda calculus. It is nevertheless possible to represent numerals, booleans, lists, sets, characters and strings as higher order functions in untyped lambda calculus using Church encoding (named after Alonzo Church).

Similarly, everything in Joy is either a function or a quotation (list of functions). Some functions look like numerals, for instance the function `2` looks like the numeral `2`, but it is still strictly speaking only a function. However, because of the Church-Turing thesis we can go one step further and eliminate even these literal-mimicking functions and replace them with compositions of a minimal base of primitive functions.

Church booleans are representations of the boolean true and false data types in terms of higher order functions (functions and quotations in Joy). Church booleans revolve around the concept of choice. Given `a` and `b`, selecting `a` represents truth, whereas selecting `b` represents falsity:

```
true == λa.λb.a
false == λa.λb.b
```

In case the lambda calculus notation is not all that clear, here are the same definitions as anonymous functions in Elixir:

``` elixir
true = fn a, b do a end
false = fn a, b do b end
```

Let's turn to Joy to help us understand these definitions a bit better.

## `ifte`, `true`, and `false` as composites

The two definitions of true and false as seen above can be represented in Joy as follows:

``` joy
A B true == A
A B false == B
```

That is, supposing that A is below B on the stack, then the function `true` effectively *pops* B off the stack. Whereas, for an identical stack, the function `false` would first *swap* A and B, then *pop* A off the stack. While these definitions agree with their counterparts in lambda calculus, they are still treated here as primitives. Let's see if we can change that.

We have already hinted at the solution.

```
true == [pop i]
false == [swap pop i]
```

In what way do these definitions confer the semantics of boolean data types on the `true` and `false` functions? There is nothing in these definitions that inherently make them boolean. Instead, the boolean semantics comes from how we define other functions such as `ifte` that act on `true` and `false`.

Suppose that `then` is a function that we would like to execute if a certain program `pred` evaluates to true and that `else` is a function that we would like to execute if `pred` evaluates to false. We could make use of the primitive `ifte`, which would expect `[else]` to be on top of the stack, with `[then]` just below it, and `[pred]` below that. `ifte` first executes `[pred]` which evaluates (hopefully) to a boolean. If false, `[else]` is executed, otherwise `[then]` is executed.

In other words, we'd like `[true] [then] [else] ifte` to evaluate to `then` and `[false] [then] [else] ifte` to `else`. But we are in search of a pure Joy implementation. Here is a first attempt:

``` joy
ifte == dig2 i i
```

where `dig2 == [] cons cons dip` digs out the element that is two positions below the top of the stack and places it on top of the stack. Let's see how it pans out:

```
[true] [then] [else] ifte
[true] [then] [else] dig2 i i    (definition of ifte)
[then] [else] [true] i i         (dig2)
[then] [else] true i             (i)
[then] [else] [pop i] i          (definition of true)
[then] [else] pop i              (i)
[then] i                         (pop)
then                             (i)
```

Similarly, for when `[pred]` evaluates to `false`.

```
[false] [then] [else] ifte
[false] [then] [else] dig2 i i     (definition of ifte)
[then] [else] [false] i i          (dig2)
[then] [else] false i              (i)
[then] [else] [swap pop i] i       (definition of false)
[then] [else] swap pop i           (i)
[else] [then] pop i                (swap)
[else]                             (pop)
else                               (i)
```

However, this definition of `ifte` is only sufficient if `pred` doesn't have to perform operations on the stack. If `pred` needs to operate on the stack, it would need to dig below `[then] [else]` in order to get to the stack. While that is an option, we can get around this problem with a more robust definition of `ifte`:

```
ifte == unit cons unit cat i swap cat i
```

Let's see it in action (again permitting the numeral-like functions `2` and `3`, and the comparison function `<`):

```
2 3 [<] [then] [else] ifte
2 3 [<] [then] [else] unit cons unit cat i swap cat i  (definition of ifte)
2 3 [<] [then] [[else]] cons unit cat i swap cat i     (unit)
2 3 [<] [[then] [else]] unit cat i swap cat i          (cons)
2 3 [<] [[[then] [else]]] cat i swap cat i             (unit)
2 3 [< [[then] [else]]] i swap cat i                   (cat)
2 3 < [[then] [else]] swap cat i                       (i)
true [[then] [else]] swap cat i                        (<)
[pop i] [[then] [else]] swap cat i                     (definition of true)
[[then] [else]] [pop i] cat i                          (swap)
[[then] [else] pop i] i                                (cat)
[then] [else] pop i                                    (i)
[then] i                                               (pop)
then                                                   (i)
```

The corresponding evaluation with `>` instead of `<` is left as an exercise to the reader. This definition of `ifte` essentially ensures that `[pred]` is evaluated against the stack that is below `[then] [else]` and assumes that the result is a quoted boolean. It then brings the boolean to the top of the stack and executes it, which in turn conditionally executes either the `[then]` or the `[else]` quotations. It only works as expected if `[pred]` evaluates to exactly `true` or `false`.

Finally, after executing `[pred]`, the `ifte` *primitive* restored the stack to what it was before executing `[pred]`. This allows `[then]` and `[else]` to operate on the data that `[pred]` used to make a decision. Our composite definition of `ifte` doesn't have this property (yet -- see two sections down).

## Boolean operators

We can now also define `or`, `and`, `not` and `xor`.

First we define the function `branch`. It is similar to `ifte`, but expects a boolean instead of a predicate:

```
true [then] [else] branch == then

false [then] [else] branch == else
```

`branch` is roughly the composition of `dig2` and `dip`. We can define it as:

```
branch == unit cons swap cat i
```

`branch` turns out to be very useful in the definitions of the boolean operators `or`, `and`, `not`, and `xor`. First up, here is `or`.

```
or == [pop true] [] branch
```

We expect that the following holds:

```
true true or == true

true false or == true

false true or == true

false false or == false
```

Here are some worked examples.

```
false true or
false true [pop true] [] unit cons swap cat i  (definition of or and branch)
false true [pop true] [[]] cons swap cat i     (unit)
false true [[pop true] []] swap cat i          (cons)
false [[pop true] []] true cat i               (swap)
false [[pop true] []] [pop i] cat i            (definition of true)
false [[pop true] [] pop i] i                  (cat)
false [pop true] [] pop i                      (i)
false [pop true] i                             (pop)
true                                           (i pop true)
```

```
true false or
true false [pop true] [] branch
true false [pop true] [] unit cons swap cat i
true false [pop true] [[]] cons swap cat i
true false [[pop true] []] swap cat i
true [[pop true][]] false cat i
true [[pop true][]] [swap pop i] cat i
true [[pop true][] swap pop i] i
true [pop true][] swap pop i
true [][pop true] pop i
true [] i
true
```

The definition of `and` uses the same line of logic:

```
and == [] [pop false] branch
```

A worked example:

```
true true and
true true [] [pop false] branch
true true [] [pop false] unit cons swap cat i
true true [] [[pop false]] cons swap cat i
true true [[] [pop false]] swap cat i
true [[] [pop false]] true cat i
true [[] [pop false]] [pop i] cat i
true [[] [pop false] pop i] i
true [] [pop false] pop i
true [] i
true
```

The function `not` essentially replaces `true` with `false` and the other way around:

```
not == [false] [true] branch
```

Here are worked examples for the only two cases that we have to consider:

```
false not
false [false] [true] branch
false [false] [true] unit cons swap cat i
false [false] [[true]] cons swap cat i
false [[false] [true]] swap cat i
[[false] [true]] false cat i
[[false] [true]] [swap pop i] cat i
[[false] [true] swap pop i] i
[[true] [false] pop i] i
[true] [false] pop i
[true] i
true
```

```
true not
true [false] [true] branch
true [false] [true] unit cons swap cat i
true [[false] [true]] swap cat i
[[false] [true]] true cat i
[[false] [true]] [pop i] cat i
[[false] [true] pop i] i
[false] [true] pop i
[false] i
false
```

Finally, we can define `xor` in terms of `not`:

```
xor == [[false] [true] branch] [] branch

xor == [not] [] branch
```

And here are worked examples for all the possible cases:

```
true true xor
true true [not] [] branch
true true [not] [] unit cons swap cat i
true true [[not] []] swap cat i
true [[not] []] true cat i
true [[not] []] [pop i] cat i
true [[not] [] pop i] i
true [not] [] pop i
true [not] i
true not
false
```

```
false false xor
false false [not] [] branch
false false [not] [] unit cons swap cat i
false false [[not] []] swap cat i
false [[not] []] false cat i
false [[not] []] [swap pop i] cat i
false [[not] [] swap pop i] i
false [] [not] pop i
false [] i
false
```

```
true false xor
true false [not] [] branch
true false [not] [] unit cons swap cat i
true false [[not] []] swap cat i
true [[not] []] false  cat i
true [[not] []] [swap pop i]  cat i
true [[not] [] swap pop i] i
true [not] [] swap pop i
true [] i
true
```

```
false true xor
false true [not] [] branch
false true [not] [] unit cons swap cat i
false true [[not] []] swap cat i
false [[not] []] true cat i
false [[not] []] [pop i]  cat i
false [[not] [] pop i] i
false [not] [] pop i
false [not] i
false not
true
```

## A composed `ifte` with identical semantics to the built-in Joy `ifte` combinator

So far, we've developed a composite implementation of `ifte` that comes close to the built-in `ifte` primitive of standard Joy:

```
ifte == unit cons unit cat i swap cat i
```

But in order to get semantics that are identical to the built-in Joy primitive, the stack should be restored after the predicate is evaluated to the state in which it was before the predicate was executed. This makes it possible the `then` and `else` clauses to potentially make use of data on the stack that would otherwise be consumed by the predicate.

A viable remedy looks like this:

```
ifte == unit cons [[stack] swap unit cat i infra uncons pop] swap unit cat i swap cat i
```

In this definition, `stack` is a function that puts the stack itself as a quotation on the top of the stack; and `infra` is a function that executes the quotation on top of the stack while treating another quotation below it as a temporary stack. Let's see how it works:


```
2 3 [<] [then] [else] ifte
2 3 [<] [then] [else] unit cons [[stack] swap unit cat i infra uncons pop] swap unit cat i swap cat i
2 3 [<] [then] [else] unit cons [[stack] dip infra uncons pop] dip swap cat i
2 3 [<] [[then] [else]] [[stack] dip infra uncons pop] dip swap cat i
2 3 [<] [stack] dip infra uncons pop [[then] [else]] swap cat i
2 3 stack [<] infra uncons pop [[then] [else]] swap cat i
2 3 [3 2] [<] infra uncons pop [[then] [else]] swap cat i
2 3 [true] uncons pop [[then] [else]] swap cat i
2 3 true [] pop [[then] [else]] swap cat i
2 3 true [[then] [else]] swap cat i
2 3 [pop i] [[then] [else]] swap cat i
2 3 [[then] [else]] [pop i] cat i
2 3 [[then] [else] pop i] i
2 3 [then] [else] pop i
2 3 [then] i
2 3 then
2 3 +         # treating `then` as the addition function
5
```

As before, for illustration purposes, we allow integers and arithmetic and predicates like `<`. In this case we see that, since 2 is smaller than 3, the `then` clause is executed, which we arbitrarily choose to be addition. Note that the predicate and the `then` clause operated on the same data. I.e. the 2 and 3 were available to both.

While this definitions works, I find the following one more elegant in that the two functions that have to be introduced are inverses of one another:

```
ifte == unit cons [[stack] dip dip] dip dig2 cat [unstack] dip i
```

Here `unstack` replaces the current stack with the quotation that is on top of it. This means that `stack` followed by `unstack` is the identity function: `stack unstack == id`. Let's see how it works:

```
2 3 [<] [then] [else] ifte
2 3 [<] [then] [else] unit cons [[stack] dip dip] dip dig2 cat [unstack] dip i
2 3 [<] [[then] [[else]] cons [[stack] dip dip] dip dig2 cat [unstack] dip i
2 3 [<] [[then] [else]] [[stack] dip dip] dip dig2 cat [unstack] dip i
2 3 [<] [stack] dip dip [[then] [else]] dig2 cat [unstack] dip i
2 3 stack [<] dip [[then] [else]] dig2 cat [unstack] dip i
2 3 stack [<] dip [[then] [else]] dig2 cat [unstack] dip i
2 3 [3 2] [<] dip [[then] [else]] dig2 cat [unstack] dip i
2 3 true [3 2] [[then] [else]] dig2 cat [unstack] dip i
2 3 [3 2] [[then] [else]] true cat [unstack] dip i
2 3 [3 2] [[then] [else]] [pop i] cat [unstack] dip i
2 3 [3 2] [[then] [else] pop i] [unstack] dip i  
2 3 [[then] [else] pop i] i
2 3 [then] [else] pop i
2 3 [then] i
2 3 then
2 3 +
5
```

So what's the big deal? We were able to drop `ifte`, `true`, and `false`, but had to introduce `stack` and `unstack`. That is not a big win in terms of the number of functions we have to deal with, but it does free us from a pre-imposed notion of what conditional program flow should look like. While the compositional form of `ifte` that we've developed here helps us to reason about and write programs, our artificial cell is not required in any way to make use of this exact compositional definition of `ifte`. There are multiple ways in which the same semantics can be achieved, some even without `stack` and `unstack`. The important bit is that we equip our system with a strong enough base to evolve on.

Suddenly there is also no real reason to require the strict predicate-then-else ordering. A protein in our artificial life system could contain these components at different locations
and still end up with the same overall outcome. For instance, a program that looks like this:

```
2 3 stack [<] dip [[then] [else]] dig2 cat [unstack] dip i
```

is equivalent to one that looks like this:

```
2 3 [<] [then] [else] unit cons [[stack] dip dip] dip dig2 cat [unstack] dip i
```

with less "dipping" and could be employed by a cell to the same effect. Ultimately, this is a matter of personal preference, and sticking to the built-in primitive `ifte` would not have prevented us from reaching our goal.

## Conclusion

By defining `ifte`, `true` and `false` in some of the more low-level Joy primitives, we have eliminated the need to treat them as amino acids in our artificial life system. Doing so is mostly a matter of personal preference. The goal is not to minimize the number of required amino acids to the bare minimum, but rather to arrive at a pleasing middle ground.

One aspect that we have neglected in this post is the requirement of a predicate function that will actually yield `[pop i]` for true and `[swap pop i]` for false. In our example we used the primitive `<`, which isn't actually part of our artificial life system. While it is trivial to come up with a function (or function composition) that will yield either one of these booleans, such a function would still have to know when to yield the one or the other in some meaningful way that is arbitrary yet deterministic.

Knowing that 2 is less than 3 was built into the definition of `<`, which is therefore primitive. Therefore, in order to use `ifte`, or rather `unit cons unit cat i swap cat i` in a way that makes it mean what the primitive `ifte` meant, we still need a predicate function of sorts. The predicate that we have relied on in our protein programs up to know has been `equal`, a function that checks if the two top elements of the stack are equal. We'll see how we can replace that with something more fuzzy. Life loves fuzzy.