Church Booleans in Joy

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:

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:

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

For example (allowing integers and strings):

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:

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:

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:

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:

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:

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).

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 in stead 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

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 (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 current predicate that we rely on in our protein programs 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.