Global Utilities

You are here:  Mathematical foundations of Joy

TITLE>Mathematical foundations of Joy

# Mathematical foundations of Joy

by Manfred von Thun

Abstract: Joy is a functional programming language which is not based on the application of functions to arguments but on the composition of functions. This paper describes the theoretical basis of the language. The denotation of Joy programs maps a syntactic monoid of program concatenation to a semantic monoid of function composition. Instead of lambda abstraction Joy uses program quotation, and higher order functions can be simulated by first order functions which dequote quoted programs.

Keywords: functional programming, syntactic and semantic monoids, function composition, quotation and dequotation of programs, combinators, elimination of recursive definitions.

# Introduction

Joy programs are built from smaller programs by just two constructors: concatenation and quotation.

Concatenation is a binary constructor, and since it is associative it is best written in infix notation and hence no parentheses are required. Since concatenation is the only binary constructor of its kind, in Joy it is best written without an explicit symbol.

Quotation is a unary constructor which takes as its operand a program. In Joy the quotation of a program is written by enclosing it in square brackets. Ultimately all programs are built from atomic programs which do not have any parts.

The semantics of Joy has to explain what the atomic programs mean, how the meaning of a concatenated program depends on the meaning of its parts, and what the meaning of a quoted program is. Moreover, it has to explain under what conditions it is possible to replace a part by an equivalent part while retaining the meaning of the whole program.

Joy programs denote functions which take one argument and yield one value. The argument and the value are states consisting of at least three components. The principal component is a stack, and the other components are not needed here. Much of the detail of the semantics of Joy depends on specific properties of programs.

However, central to the semantics of Joy is the following:

The concatenation of two programs denotes the composition of the functions denoted by the two programs.
Function composition is associative, and hence denotation maps the associative syntactic operation of program concatenation onto the associative semantic operation of function composition. The quotation of a program denotes a function which takes any state as argument and yields as value the same state except that the quotation is pushed onto the stack.

One part of a concatenation may be replaced by another part denoting the same function while retaining the denotation of the whole concatenation.

One quoted program may be replaced by another denoting the same function only in a context where the quoted program will be dequoted by being executed. Such contexts are provided by the combinators of Joy. These denote functions which behave like higher order functions in other languages.

The above may be summarised as follows: Let `P`, `Q1`, `Q2` and `R` be programs, and let `C` be a combinator. Then this principle holds:

```        IF          Q1      ==      Q2
THEN     P  Q1  R   ==   P  Q2  R
AND        [Q1] C   ==     [Q2] C
```
The principle is the prime rule of inference for the algebra of Joy which deals with the equivalence of Joy programs, and hence with the identity of functions denoted by such programs. A few laws in the algebra can be expressed without combinators, but most require one or more combinators for their expression.

The remainder of this paper is organised as follows. The next sections deal with program concatenation and function composition. The first of these reviews certain algebras called monoids, and homomorphisms between them. In the following section the meaning of Joy programs is shown to be a homomorphism from a syntactic monoid to a semantic monoid. The last of these sections explains the semantic monoid in a little more detail, in particular function composition and the identity function.

The other sections deal with quotations and combinators. The first treats combinators that do not involve the stack, the second those that do. The next section illustrates how these very basic combinators can be used to emulate recursion without explicit definitions. The summary section recapitulates the main conclusions and hints at a connection with category theory.

# Monoids and homomorphisms

The design of Joy was motivated by {Backus78} who in quite different fields examine how variables of one kind or another can be eliminated and how their work can be done by combinators. In turn their work is based on the pioneers Schönfinkel and Curry. Backus has argued that concepts of programming languages should be selected on the basis of yielding strong and clean mathematical laws. In particular he favours concepts that allow simple algebraic manipulations, where possible replacing variables by combinators or higher order functions. With these goals in mind his research culminated in the language FP. The language Joy offers a very different solution to the same goals. Paulson {Paulson92} remarked that "Programming and pure mathematics are difficult to combine into one formal framework". Joy attempts this task.

Much of the elegance of Joy is due to the simple algebraic structure of its syntax and the simple algebraic structure of its semantics and to the fact that the two structures are so similar. In particular, the two structures are monoids and the meaning function which maps syntax into semantics is a homomorphism.

Monoids and homomorphisms are familiar from abstract algebra. A monoid `M` consists of a nonempty set ```{m, m1, m2 ...}``` including a special element `m`, and a binary operation, written, say, as infix period `"."`. The special element has to be a left and right unit element for the binary operation, and the binary operation has to be associative. In symbols, for all `x`, `y` and `z` from the set,

```        m . x   =   x   =   x . m
(x . y) . z   =   x . (y . z)
```
For example, these are monoids: the integers with `0` as the unit element and addition as the binary operation, or the integers with `1` as the unit element and multiplication as the binary operation. Two examples from logic are the truth values with falsity as the unit element and disjunction as the binary operation, or truth as the unit element and conjunction as the binary operation. Two examples from set theory are sets with the nullset as the unit element and set union as the binary operation, or the universal set as the unit element and set intersection as the binary operation. It so happens that in the preceding examples the binary operation is commutative, but this is not essential for monoids. Two other examples consists of lists with the empty list as the unit element and concatenation as the binary operation, or strings of characters with the empty string as the unit element and concatenation as the binary operation. Concatenation is not commutative.

Because of the associative law, parentheses are not needed. Also, if there are no other binary operations, the infix operator itself can be omitted and the operation indicated by juxtaposition. Unit elements are often called identity elements, but the word "identity" is already needed with a different meaning in Joy. Unit elements are sometimes called neutral elements, too.

Unit elements should be distinguished from zero elements, which behave the way the number `0` interacts with multiplication: a product containing a zero factor is equal to zero. In logic falsity is the zero element for conjunction, and truth is the zero element for disjunction. For sets the nullset is the zero element for intersection, and the universal set is the zero element for union. In commutative monoids there is always at most one zero element.

Let `M` over `{m m1 ..}` and `N` over `{n n1 ..}` be two monoids. A function `h` from `{m m1 ..}` to `{n n1 ..}` is called a homomorphism if and only if it maps unit elements onto unit elements and commutes with the binary operation:

```        h(m)  =  n                      h(x . y)  =  h(x) . h(y)
```
In the second equation, the binary operation on the left is that of `M`, and the one on the right is that of `N`. One example is the logarithm function which is a homomorphism from the multiplicative monoid onto the additive monoid. Another example of a homomorphism is the size (or length) function on lists which maps the list monoid onto the additive monoid: the size of the empty list is zero, and the size of the concatenation of two lists is the sum of the sizes of the two lists:
```        log(1)  =  0                    log(x * y)  =  log(x) + log(y)
size([])  =  0                  size(x ++ y)  =  size(x) + size(y)
```
(In the last two equations, the symbols `[]` and `++` are used for the empty list and for concatenation.) Other examples are the function which takes a list (or string) as argument and returns the set of its elements. So this function removes duplicates and forgets order. It maps the list monoid onto the set monoid with the nullset as the unit and union as the binary operation.

Homomorphisms can be defined over other algebras which are not monoids. Examples are groups, rings, fields and Boolean algebras. They are studied in universal algebra and in category theory. One particular homomorphism can only be described as mind-blowing: this is Gödel's arithmetisation of syntax - all syntactic operations on formulas of a theory are mapped onto corresponding arithmetic operations on their Gödel numbers. (See for example {Mendelson64}.)

In propositional logic the equivalence classes of formulas constitute a Boolean algebra of many elements. A valuation is a homomorphism from that algebra to the two element Boolean algebra of truth values. One can go further: the meaning of a formula is the set of valuations that make it true. The meaning function then is a homomorphism from the Boolean algebra of equivalence classes to the Boolean algebra of sets of valuations. This situation is typical in semantics: the meaning function is a homomorphism. The same holds for Joy - the meaning function is a homomorphism from Joy syntax to Joy semantics.

# A syntactic monoid and a semantic monoid

The syntax of Joy programs is very simple: the basic building blocks are atomic programs, and larger programs are formed by concatenation as one of the main modes of program construction. Concatenation is associative, and hence no parentheses are required. Also, concatenation is the only binary constructor, so no explicit symbol is required, and hence concatenation can be expressed by juxtaposition. It is useful to have a left and right unit element id. Collectively these constitute the syntactic monoid.

Now to the semantics. In the introduction it was said that Joy uses postfix notation for the evaluation of arithmetic expressions. To add two numbers they are pushed onto a stack and then replaced by their sum. This terminology is helpful but can be misleading in several ways. The phrasing suggest a procedural or imperative interpretation: Joy programs consist of commands such as push this, push that, pop these and push their sum. But there is nothing procedural about Joy, as described here it is a purely functional language.

However, the terminology of commands does suggest something useful. Commands, when executed, produce changes. Exactly what is changed depends on the nature of the command. But in the most general terms what changes is the state of a system. In particular the execution of a postfix expression produces changes in the state of a stack. For each change there is a before-state and an after-state. The after-state of one change is the before-state of the next change.

So, changes are essentially functions that take states as arguments and yield states as values. There is only one before-state, so they are functions of one argument. Therefore they can be composed. The composite of two functions can be applied to a state as argument and yields as value the state that is obtained by first applying the one function to the argument and then applying the other function to the resulting value. This is essentially the semantics of Joy: All programs denote functions from states to states.

The state does not have to be the state of a stack. It just so happens that evaluation of postfix expressions is so conveniently done on a stack. But evaluation of expressions is by no means everything. In what follows, the stack is an essential part of the state, but for many purposes it is useful to ignore the whole state altogether.

The operation of function composition is associative and there is a left and right unit element, the identity function. Collectively they comprise the semantic monoid. The meaning function maps a syntactic monoid onto a semantic monoid. The concatenation of two programs denotes the composition of the functions denoted by the two programs, and the unit element of concatenation denotes the unit element of composition.

# Function composition and the identity function

If the programs `P` and `Q` denote the same function, then the functions `P` and `Q` are identical. Two functions are identical if for all values in the intersection of their domains they yield the same value. This will be written
```        P   ==   Q
```
The symbol `==` will be used to denote the identity of Joy functions. The symbol does not belong to the language Joy but to its metalanguage. The identity relation between functions is clearly reflexive, symmetric and transitive. Furthermore, identicals are indiscernible in larger contexts such as compositions. Hence substitution of identicals can be used as a rule of inference:
```        IF             Q1      ==      Q2
THEN        P  Q1  R   ==   P  Q2  R
```
The symbol id will be used to denote the identity function. The fact that function composition is associative and that the identity function is a left and right unit is expressed by
```        (P  Q)  R   ==   P  (Q  R)
id  P   ==   P   ==   P  id
```
The notation can be used to express what look like identities of numbers; for example
```        2  3  +   ==   5
```
expresses that the composition of the three functions on the left is identical with the one function on the right. On the left, the first two functions push the numbers 2 and 3 onto the stack, and the third replaces them by their sum. On the right, the function pushes the number 5. The left and the right are defined for all stacks as arguments and yield the same stack as value. Hence the left and the right are identical.

But it is important to be quite clear what the equation says. Each of the four symbols `2`, `3`, `+` and `5` denotes a function which takes a stack as argument and yields a stack as value. The three numerals `2`, `3` and `5` denote functions which are defined for all argument stacks. They yield as values other stacks which are like the argument stacks except that a new number, 2, 3 and 5 has been pushed on top.

The symbol `+` does not denote a binary function of two numbers, but like all Joy functions it takes one argument only. That argument has to be a stack whose top two elements are numbers. The value returned is another stack which has the top two numbers replaced by their sum. It follows that the above equation does not express the identity of numbers but the identity of functions.

The associativity of composition has as a consequence about currying: that there is no difference between standard and curried operators. Consider the example

```        (2  3)  +   ==   2  (3  +)
```
On the left the `+` takes two parameters supplied by `(2 3)`. On the right `+` is given one parameter, `3`. The resulting function `(3 +)` expects one parameter to which it will add `3`. Because of associativity the two sides are identical and hence no parentheses are required.

Let `P` be a program which pushes m values onto the stack. Let `Q` be a program which expects n values on the stack, m <= n. Now consider their concatenation ```P Q```. Of the n expected by `Q`, n will be supplied by `P`. So the program `P Q` only expects n - m values on the stack.

+++HERE+++ assoc and curry

In the development of mathematics an explicit notation for the number `0` has been a rather recent innovation. The symbol enables one to say more than just that `0` is a unit element for addition. Similarly, in the algebra of functions an explicit symbol for the identity function makes it possible to state many laws. This is particularly true for the functions in Joy. The following are some examples:

In arithmetic `0` and `1` are unit elements for addition and multiplication, so adding `0` or multiplying by `1` have no effect. For lists the empty list is a unit element, so concatenation on the left or the right has no effect. Similarly in logic, falsity and truth are unit elements for disjunction and conjunction, so disjoining with falsity and conjoining with truth make no difference. Also in logic, disjunction and conjunction are idempotent, so disjoining or conjoining with a duplicate yields the original. For any stack it holds that swapping the top two elements twice has no net effect, and that duplicating the top element and then popping off the duplicate has no net effect.

There are many more laws: double negation has no net effect, reversing a sequence twice just leaves the original, and taking the successor and the predeccessor of a number - in either order - produces no net effect. In the algebra of Joy these are expressed by the following:

```        0  +   ==   id                  1  *   ==   id
[]  concat   ==   id            []  swap  concat   ==   id
false  or   ==   id             true  and   ==   id
dup  and   ==   id              dup  or   ==   id
swap  swap   ==   id            dup  pop   ==   id
not  not   ==   id              reverse  reverse   ==   id
succ  pred   ==   id            pred  succ   ==   id
```
Note that no variables were needed to express these laws.

The identity function is a left and right unit element with respect to function composition. It is appropriate to remark here that there is also a left zero element and there is a right zero element. Two such elements `l` and `r` satisfy the following for all programs `P`:

```        l  P   ==   l                   P  r   ==   r
```
Since function composition is not commutative, the two zero elements are not identical. In Joy the left zero `l` is the abort operator, it ignores any program following it. The right zero `r` is the clearstack operator, it empties the stack and hence ignores any calculations that might have been done before. The two operators have some theoretical interest, and they are occasionally useful.

# Quotation, dequotation and combinators

Any program enclosed in square brackets is called a quoted program or quotation. The length or `size` of the quotation `` is `1`, and the size of the quotation `[2 3 +]` is `3`. However, as noted earlier, the two programs inside the brackets denote the same function. What this shows is that we cannot substitute their quotations for each other:
```          size   =/=   [2 3 +]  size
```
What forbids the substitution is the quotation - by the square brackets. So quotations produce opaque contexts, quotation is an intensional constructor.

However, there are contexts where substitution is permissable across quotations. These are contexts where the content of the quote is not treated as a passive datum but as an active program. In Joy such treatment is due to combinators which in effect dequote one or more of their parameters.

The i combinator expects a quoted program on top of the stack. It pops that program and executes it. So, if the quoted program `[P]` has just been pushed onto the stack, then the `i` combinator will execute `P`:

```        [P]  i   ==   P
```
For example, each of the following four programs compute the same function - the one which takes any stack as argument and returns as value another stack which is like the argument stack but has the number `5` pushed on top.
```         2  3  +                         5
[2  3  +] i                      i
```
If the program `P` computes the identity function, then the effect of applying the `i` combinator is that of the identity function:
```        [id]  i   ==   id               []  i   ==   id
```
Another law is this:
```        i  ==  []  cons  i  i
```

Two programs `P` and `Q` may look very different - for example, they may differ in their sizes. But it could be that the compute the same function. In that case the dequotations of their quotations also compute the same function:

Hence

```        IF       P       ==    Q
THEN    [P]  i   ==   [Q]  i
```
Suppose now that a quoted program, `[P]`, is on top of the stack. It could then be executed with the `i` combinator. But it could also be manipulated as a passive data structure first. For example, one could push the quotation `[i]` and then use the cons operator to insert `[P]` into `[i]` to give `[[P] i]`. What happens if this is executed by the `i` combinator? The internal `[P]` quote is pushed, and then the internal `i` combinator is executed. So the net effect is that of executing `P`.

Hence

```        [i]  cons  i   ==   i
```
Note that it has been possible to state this law without reference to the quoted program `[P]`. But it may help to spell out a consequence:
```        [P]  [i]  cons  i   ==   [[P] i]  i   ==   [P]  i   ==   P
```

The `i` combinator is only one of many. Another is the b combinator which expects two quoted programs on top of the stack. It pops them both and then executes the program that was second on the stack and continues by executing the program that was on top of the stack. So, in the special case where two programs `[P]` and `[Q]` have just been pushed onto the stack, the `b` combinator will execute them in the order in which they have been pushed:

```        [P]  [Q]  b   ==   P  Q
```
It follows that the `b` combinator actually dequotes both of its parameters, and hence either or both can be replaced by an equivalent program:
```        IF       P1  ==  P2     AND    Q1  ==  Q2
THEN    [P1]  [Q1]  b   ==   [P2]  [Q2]  b
```
If both programs compute the identity function, then the effect of the `b` combinator is the identity function. If either of the two programs computes the identity function, then the effect is the same as that of executing the other, which is the same as applying the `i` combinator to the other:
```        []  []  b   ==   id
[]  b   ==   i
[]  swap  b   ==   i
```
The second equation could be reversed, and this shows that the `i` combinator could be defined in terms of the `b` combinator.

Quotations are sequences, and sequences can be concatenated. In Joy strings, lists and, more generally, quotations can be concatenated with the concat operator. If `[P]` and `[Q]` have just been pushed, then they can be concatenated to become `[P Q]`. The resultant concatenation can be executed by the `i` combinator. The net effect is that of executing the two programs, and that is also achieved by applying the `b` combinator:

```        [P]  [Q]  concat  i   ==   P  Q   ==   [P]  [Q]  b
```
But the two quoted programs do not have to be pushed immediately before the concatenation or the application of the `b` combinator. Instead they could have been constructed from smaller parts or extracted from some larger quotation. Hence the more general law:
```        concat  i   ==   b
```
The equation could be reversed, hence the `b` combinator could be defined in terms of the `i` combinator. The names `i` and `b` of the two combinators have been chosen because of their similarity to the I combinator and B combinator in combinatory logic. The standard text is {Curry58}, but good expositions are to be found in many other books, for example {Burge75}.

# Stack oriented combinators

The two previous combinators require one or two quoted programs as parameters, but the parameters merely have to be in an agreed place, they do not need to be on a stack. There are several combinators which only make sense if the data are located on a stack.

Sometimes it is necessary to manipulate the stack not at the top but just below the top. That is what the dip combinator is for. It is behaves like the `i` combinator by executing one quotation on top of the stack, except that it leaves the item just below the quotation unchanged. In detail, it expects a program `[P]` and below that another item `X`. It pops both, saves `X`, executes `P` and then restores `X`.

For example, in the following the saved and restored item is `4`:

```        2  3  4  [+]  dip  ==   5  4
```
If a program computes the identity function, then the effect of applying the `dip` combinator is to compute the identity function:
```        [id]  dip   ==   id             []  dip   ==   id
```
Suppose a program `[P]` is on top of the stack, and it is first duplicated and then the copy executed with `dip` just below the original `[P]`. Now the original has been restored, but suppose it is now popped explicitly. The net effect was the same as executing just the original `[P]` with the `i` combinator:
```        i   ==   dup  dip  pop
```
Suppose that there are two programs `[P]` and `[Q]` on top of the stack, with `[Q]` on top. It is required to execute `[P]` while saving `[Q]` above. One way to do that is this: First push `[i]`. Now `[Q]` is the second element. Executing `dip` will save `[Q]` and execute `[i]` on the stack which now has `[P]` on the top. That amounts to executing `[P]`, and after that `[Q]` is restored.

Suppose further that it is now required to execute `[Q]`, and that is easily done with the `i` combinator. The net effect of all this is the same as executing first `[P]` and then `[Q]`, which could have been done with the `b` combinator. Hence

```        b   ==   [i]  dip  i
```
The last two equations show that the `dip` combinator could be used to define both the `i` combinator and the `b` combinator. The reverse is not possible.

The last two equations also serve to illustrate algebraic manipulation of Joy programs. In the last equation the `i` combinator occurs twice, once quoted and once unquoted. Both occurrences can be replaced in accordance with the previous equation, and this yields

```        b   ==   [dup dip pop]  dip  dup  dip  pop
```
The substitution of the unquoted occurrence is unproblematic. But the other substitution requires comment. Quoted occurrences can be substituted only in a context of dequotation, and in this case such a context is given by the `dip` combinator.

Again suppose that there are two quoted programs `[P]` and `[Q]` on the stack. If the `dip` combinator is executed next, it will cause the topmost quotation `[Q]` to be executed while saving and later restoring `[P]` below. Suppose that the `i` combinator is executed next, this will cause the restored `[P]` to be executed. So the net effect of the two combinators is to execute first `P` and then `Q`. That same effect could have been achieved by first swapping `[P]` and `[Q]` around, so that `[P]` is on top, and then executing the `b` combinator. This is expressed in the left law below. The right law says the same thing, and it shows another way in which the `b` combinator could have been defined.

```        dip  i   ==   swap  b           b   ==   swap  dip  i
b   ==   swap  dip  dup  dip  pop
```

Function composition is associative, and hence the following holds:

```        [P]  [Q]  b  [R]  i   ==   [P]  i  [Q]  [R]  b
```
To eliminate the three quotations from this equation observe that they can be written on the left of both sides provided that the `b` combinator and the `i` combinator are applied appropriately. For the left side this is easy:
```        [P]  [Q]  b  [R]  i   ==   [P]  [Q]  [R]  [b] dip i
```
For the right side it is a little harder since the `i` combinator has to be applied to `[P]` which is obscured not by one but two other quotations. The `dip` combinator has to be used on itself in this case, as follows:
```        [P]  i  [Q]  [R]  b   ==   [P]  [Q]  [R]  [[i] dip]  dip  b
```
Combining the two right hand sides and cancelling the common three quotations we obtain the following to expressing the associativity of function composition:
```        [b]  dip  i   ==   [[i] dip]  dip  b
```
In this law we can even replace the `i` combinator and the `b` combinator in accordance with earlier definitions:
```        [swap  dip  dup  dip  pop]  dip  dup  dip  pop
==   [[dup  dip  pop]  dip]  dip  swap  dip  dup  dip  pop
```
It is possible to cancel the final `pop` on both sides, but it is not possible to cancel the prefinal `dip` on both sides. This unlikely law also expresses the associativity of function composition. But the most elegant way of expressing the associativity is by using a variant of the `dip` combinator, called dipd, which might be defined by
```        dipd   ==   [dip]  cons  dip
```
Then the associativity can be expressed by
```        [b]  dip  i   ==   [i]  dipd  b
```
({Henson87} criticises presentations of FP-systems, originally due to {Backus78} in that they give no law to this effect although they use it in proofs.)

The combination of the `dip` combinator immediately followed by the `i` combinator is sometimes useful for arranging the top few elements on the stack in a form that is suitable for executing a quoted program `[P]` that is at the top of the stack.

This is how it is done: first another quoted program `[Q]` is pushed, and executed using the `dip` combinator. This will save and restore the `[P]`, but arrange the stack in accordance with `[Q]`. Then the restored `[P]` is executed by the `i` combinator. Depending on the `[Q]` that is chosen, the three part combination of `[Q]`, the `dip` combinator and the `i` combinator will prepare the stack for the execution of `[P]`.

Since such a combination still requires the `[P]` on the stack, any such combination has the effect of a combinator. The following illustrate some simple choices of `[Q]` that are sometimes useful. The names of these combinators have been chosen because of their similarity to the K combinator, W combinator and the C combinator in combinatory logic.

```        k   ==   [pop]  dip  i
w   ==   [dup]  dip  i
c   ==   [swap] dip  i
```

# More general laws

Suppose that there is a quoted program `[P]` on top of the stack. This could now be executed by some combinator, say `C`. Alternatively, one could push the quotation `[C]` and then use the `cons` operator to insert the earlier `[P]` into the later quotation, and this produces `[[P] C]`. This of course may be executed by the `i` combinator. When that happens the inner `[P]` is pushed, thus partly undoing the `cons` operation. But then `C` will be executed. The net effect is the same as the earlier alternative. So we have: For all operators or combinators `C`
```        [C]  cons  i   ==   C
```
It should be remarked that this theorem also holds for operators, say `O`, instead of combinators `C`.

Again suppose that there is a quoted program `[P]` on top of the stack. It could be executed by some combinator `C`, or one could do this: push the quotation `[i]`, `cons` the earlier `[P]` into that and now execute `C`. The `cons` operation produced `[[P] i]` and when this is executed by `C`, the inner `[P]` is pushed partly undoing the `cons`. Then the `i` combinator actually executes this. The net effect is that of just executing `C`. Hence for all combinators `C`

```        [i]  cons  C   ==   C
```

The two laws above may be combined: for all combinators C

```        [i]  cons  C   ==   [C]  cons  i
```

So far we have only encountered one combinator which takes two quoted parameters - the `b` combinator. But Joy has a large number of combinators which take two, three or even four quoted parameters. The following concerns combinators which expect at least two quoted programs as parameters. For such combinators the first three laws holds unchanged, but these variations also hold:

```        [i]  cons  cons  C   ==   C
[C]  cons  cons  i   ==   C
[i]  cons  cons  C   ==   [C]  cons cons  i
```
The principle generalises to combinators with at least three quoted parameters, by allowing three `cons` operations to occur.

Finally, the second law generalises to all parameters of a combinator: any one parameter `[P]` can be replaced by ```[[P] i]```. The replacement can of course be constructed by `cons`ing `[P]` into `[i]`. That of course may be done for all quotation parameters. If there is just the one parameter `[P]`, then `cons`ing it into `[i]` to produce `[[P] i]` is easy enough, as in the second law.

If there are two parameters `[P]` and `[Q]` it already becomes tedious to change them to `[[P] i]` and `[[Q] i]`. If there are three or more quotation parameters, then the program to produce the three changes could be rather obscure.

Joy has a combinator which can use a function to map the elements of a list to a list of the same length containing the results of applying the function. Several special forms take as a parameter not an arbitrary list but a specified number of one, two, three and so on elements from the stack. These are the app1 combinator, the app2 combinator, the app3 combinator and so on. These are just the right combinators to produce the changes required for the parameters of a combinator. The following laws hold for combinators `C1`, `C2` and `C3` requiring one, two or three quotation parameters:

```        [[i] cons]  app1  C1   ==   C1
[[i] cons]  app2  C2   ==   C2
[[i] cons]  app3  C3   ==   C3
```
To illustrate for a combinator C3:
```         [P]      [Q]      [R]    [[i] cons]  app3  C3
==   [[P] i]  [[Q] i]  [[R] i]                   C3
==    [P]      [Q]      [R]                      C3
```
Computationally it is of course pointless to replace a quotation such as `[P]` by `[[P] i]` if the quotations are being used as parameters for a combinator. But the replacements are invaluable in a Joy interpreter written in Joy. This interpreter is essentially a complex combinator, appropriately called joy, and it has to behave just like the `i` combinator. In the definition of the `joy` combinator, the implementation of all combinators uses the above mapping combinators but with `[[joy] cons]` instead of `[[i] cons]`.

# Elimination of Definitions

One of the problems of large pieces of software concerns the complexity of interdependent parts and the need to make interfaces lean. To some extent this is a matter of information hiding, and programming languages achieve this in various ways. Most have local symbols such as formal parameters of functions and local program variables of procedures. Many have full block structure allowing declarations of functions and procedures to be nested and hence invisible from the outside. Some have modules or other compilation units which allow further information hiding in larger program components. Joy approaches the problem in a different way -- the information that needs to be hidden is minimised in the first place. Mostly the problem arises from declarations of named functions and procedures and their named formal parameters.

There are several reasons why one might want to declare a function, because

1. it requires recursion, or
2. it is needed in several seemingly unrelated places in a program, or
3. it makes the program clearer.

The third reason is always valid. In Joy the second reason is much less compelling, and the first has almost no force at all.

Joy has a large number of combinators which permit computation of anonymous functions which are normally defined recursively. It also has combinators that permit repeated calls of such functions in some related patterns. Joy programs which use suitable combinators to allow the computation of anonymous functions with anonymous formal parameters.

Consider the following recursive definition and use of the factorial function in a (fantasy) functional language:

```    LET  factorial(n)  =  if n = 0 then 1 else n * factorial(n - 1)
IN  factorial(5)
```
The call in the second line should return `120`. Joy has a number of ways of doing essentially the same computation without introducing the name `factorial` and without introducing the name of the formal parameter `n`. Several of these ways are still modelled on the recursive definition and have approximately the same length. Two of them are based on the fact that the definition has the pattern of linear recursion, indeed primitive recursion. As in all languages the use of accumulating parameters can avoid the recursion altogether, but that is not the point here.

The humble `i` and `dip` combinators were certainly not designed for recursion, so it will come as a surprise that they can be used to emulate recursion without naming the function or its formal parameter. To make the recursion possible, every call of the anonymous function must be able to access itself again, and this is done by giving it its own body as a quoted parameter on the top of the stack. This is achieved by always duplicating the quoted body first and then using the `i` combinator to execute the duplicate. The `dip` combinator can be used to access the stack below the quoted body. The only other combinator needed is the `ifte` combinator which achieves the same kind of two-way branching as the `if-then-else` in the conventional definition above.

This is the program:

```1           5
2           [  [pop  0  =]
3              [pop  pop  1]
4              [  [dup  1  -]  dip
5                 dip  i
6                 *  ]
7              ifte  ]
8           dup  i
```

The line numbers are only included for reference. Execution begins in line 1 by pushing the actual parameter `5` onto the stack. Then the long quotation extending from line 2 to line 7 is pushed onto the stack. This quotation is the body of the function, it corresponds to the right hand side of the conventional definition. Execution continues in line 8 where the long quotation is duplicated and the top copy is executed by the `i` combinator. This execution has the effect of pushing the two short quotations in lines 2 and 3 and also the longer quotation in lines 4 to 6. So at this point the stack contains the parameter `5` and above that four quotations.

But now the `ifte` combinator in line 7 executes. It pops the last three quotations and saves them elsewhere. Then it executes the if-part, the saved quotation from line 2. That will pop what is now the top of the stack, the body of the function from lines 2 to 7. This exposes the number which is the parameter, and it is compared with `0`.

The comparison will yield a truth value which the `ifte` combinator will use to determine whether to execute the saved then-part from line 3 or the saved else-part from lines 4 to 6. In either case the stack is first restored to what it was before the if-part was executed: the quoted body of the function is again on top of the stack and below it is the actual parameter for this particular call. If the most recent comparison by the if-part was true, then the saved then-part from line 3 is executed.

This results in the body and the actual parameter being popped off the stack and replaced by `1`, the factorial of `0`. On the other hand, if the most recent comparison was false, then the saved else-part from lines 4 to 6 is executed. For the later multiplication the parameter has to be duplicated and the top duplicate has to be decremented. Since the body of the function is in the way, the duplicating and decrementing is done via the `dip` combinator in line 4.

At this point the top three elements on the stack are the original parameter for this call, then the decremented duplicate, and right on top of that the quoted body of the function. It is now necessary to compute the factorial of the decremented duplicate, and this call may need access to the body again. So the body cannot be simply executed by the `i` combinator, but first the body is duplicated in line 5 and then the duplicate is executed by the `i` combinator. Execution of that duplicate body will eventually terminate, and then the top two elements will be the original parameter and the factorial of what was its decremented duplicate. The two numbers are now multiplied in line 6, yielding the required factorial of the parameter for this call. This completes the execution of the else-part from lines 4 to 6. Irrespective of whether the then-part or the else-part was executed, the execution of the `ifte` combinator is now complete.

This completes the execution of the body of the function in lines 2 to 7. It also completes the execution of whichever occurrence of the `i` combinator in lines 5 or 8 triggered this execution of the body. Ultimately the execution of the `i` combinator in line 8 will have completed, and at this point the parameter `5` from line 1 will have been replaced by its factorial `120` as required.

Two short comments are in order: Firstly, the description of the program was given in an imperative or procedural mode which is psychologically helpful. But this does not change the fact that all Joy programs and all their parts denote functions. Secondly, the program can be written using only the `dip` combinator and the `ifte` combinator by substituting ```dup dip pop``` for the two calls of the `i` combinator in lines 5 and 8.

Of course this program is a tour de force, it is ugly and inefficient. With more suitable combinators much crisper and more efficient programs can be written. In particular, the repeated pushing and saving of the quoted if-part, then-part and else-part is not necessary. Also, the repeated duplication of the quoted body is not necessary, and consequently the three parts do not have to work around the quoted body when it is in the way on the top. In fact, the essence of the if-part and most of the else-part are built into the primrec combinator for primitive recursion. The entire program then is

```        5    [*]  primrec
```
As mentioned before, even the use of recursion can be eliminated in favour of a more efficient loop combinator which uses an accumulating parameter.

# Summary

This paper has attempted to explain the theoretical foundations of the language Joy. Much of the semantics is summarised by observing that the following are true:
```        2  3  +   ==   7  2 -
dup  +   ==   2  *
dip  i   ==   swap  b
```
The first seems to express the identity of numbers. The second seems to express the identity of functions which both double a given number which they expect on the stack. The third seems to express the identity of functionals, or second order functions which take two first order functions as parameter and compose them.

While these readings are sometimes helpful, the unity of Joy semantics really forces a different interpretation. All three equations express identity of Joy functions which take one argument stack and yield one value stack.

The mathematical discipline of category theory deals with functions of one arguments. All Joy functions are of that kind, too. In fact all monoids are special cases of categories, so Joy's syntactic monoid of concatenation and Joy's semantic monoid of function composition are categories. So some fundamental connections should be expected. In particular, Joy is related to Cartesian closed categories, and to the "Combinatory Abstract Machine" CAM, see for example {Poigne92}.

The paper j00ovr contains an overview of Joy and references to other papers dealing with specific aspects of Joy.