The AMEN architecture.

Peter Hancock

Abandoned draft of Jan 99

Abstract There are many combinatorially complete sets of combinators. The most famous are {S, K } and {B, W, I, C, K }. Several authors have observed that there is a set of ‘arithmetic’ combinators arising from the Church numerals, to which λ-expressions can be compiled. However their sets of combinators are not absolutely perfect. The perfect set of combinators is {A, M, E, N }, ( {(+), (×), (ˆ ), 0} in section-notation), defined herein.

We show how to make these combinators into a 4-instruction machine, with opcodes {Add, Mul, Exp, Nop}. It may be that there is more to this machine than entertainment, as the garbage collector can execute the whole instruction set except addition.

As with all machine codes, no-one should actually write in it. Fortunately, it is next to impossible to manually write such programs as they resemble the symptoms of a severe eye disease. All the same, they have a strange iconic logic.

Suppose we write application backwards, with the function after the argument, as mathematicians sometimes do. The notation is usually called ‘algebraic notation’, but I will refer to it as ‘exponential notation’, for reasons that will soon be clear. Perhaps it is congenial if you visualise data as starting on the left and flowing through successive functions towards the right.

Let us use … ˆ … as an infix notation for application written backwards. (Juxtaposition (. . . . . .) is more often used in real life, but in most functional languages, juxtaposition is already in use for the reverse operator.) The symbol is chosen to evoke ‘exponential’ associations, as we shall shortly introduce the familiar arithmetic operators ×, 1, +, 0. We take all binary operators to be right associative, so that for example a ˆ b ˆ c is bracketed a ˆ (b ˆ c), corresponding to the left associativity of the normal juxtaposition operator.

In connection with the normal application notation it is supremely natural to introduce the normal composition notation, and something like 1 for the identity. In connection with exponential notation, for mirror-image reasons it is natural to introduce a multiplication operator … × …, which is the reverse of composition.

\begin{aligned}(f · g) a & = & f (g a) & a ˆ (g × f) & = & (a ˆ g) ˆ f \\ 1 a & = & a & a ˆ 1 & = & a \end{aligned}

What is more, on the arithmetic side there is good use for the … + … operator and 0. I do not know of any common notation for their counterparts in the normal column, so I shall use the operator … ˜+ …, and constant ˜0 :

\begin{aligned}(f ˜+ g) a & = & f a · g a & a ˆ (g + f) & = & a ˆ g × a ˆ f \\ ˜0 a & = & 1 & a ˆ 0 & = & 1 \end{aligned}

Let us take the ‘ζ’ rule for granted:

\frac{x ˆ a = x ˆ b}{a = b} where x is fresh to a and b

This is a harmless form of mild extensionality, or perhaps exponentiality. Using it, we can prove from the definitions the following algebraic facts:

• (… × …, 1) forms a monoid: i.e. … × … is associative, and has 1 as a left and right neutral element.

• (… + …, 0) forms a monoid.

• … × … distributes over … + … from the left:

\begin{aligned}a × (b + c) & = & a × b + a × c \\ a × 0 & = & 0 \end{aligned}

Curiously, these laws are (roughly) the main ones that continue to hold when arithmetic is extended to arbitrary orderings (well-founded or not). Other laws that hold only in finite arithmetic fail. For example, the commutativity of multiplication fails because it says that order of composition does not matter. (I have no explanation of this coincidence.)

It is simple to translate arithmetic notation into a Haskell style functional program, without using recursion:

       -- `take over' operators
       import Prelude hiding ((*),(^),(+))
       -- usual precedence
       infixr 8 ^
       infixr 7 *
       infixr 6 +
       m + n       = \f -> f ^m * f ^n
       m * n       = \f -> (f ^m) ^n
       m ^n       = n m
       nop f z     = z

(Perhaps it is an anomaly that one cannot ‘take over’ 0 and the other digits in the same way – isn’t there some way that could work?) However, by doing so, we have given ourselves the possibility of using (+), (*), and (^) as if they were ‘numbers’, that represent the arithmetical operations in the sense that the following laws hold:

b ˆ a ˆ (ˆ ) = a ˆ b
b ˆ a ˆ (×) = a × b
b ˆ a ˆ (+) = a + b

These are the ‘arithmetic combinators’ of Stenlund, Schwichtenberg, Burge, Barendregt, Rosenbloom, Church?, Shoenfinkel?, Curry?, Turing? .. . , except for a quibble. Almost everyone defines the multiplication combinator to be the mirror of (×), namely (·), which equals the classic ‘B’ combinator. Their usual addition combinator is correspondingly different. (It is … ˜+ . . ..) My definitions have the authority of Cantor, who appreciated exponential notation, and said (after working with them for a while) that laws such as:

a ˆ (f × g) = (a ˆ g) ˆ f

were ‘repulsive’ (abstoßende in German)^{1} ^{2}.

1 Completeness

That the arithmetic combinators are functionally complete, means that we can introduce λ-abstraction as a façon-de-parler, and compile untyped lambda terms into equivalent applicative terms (‘code’) with only the arithmetic combinators. Because of the arithmetic setting, it is natural to use logarithmic notation ‘log_{x} b’ instead of ‘λx.b’ .)

To compile into arithmetic combinators, first consider affine λ-abstraction log_{x} b, where the bound variable x may have at most one occurrence in the body b. The following cases are typical. I have used ‘section notation’, replacing a ˆ (ˆ ) by (aˆ ), etc. .

• log_{x} x = 1. (1 can be defined as Junk ˆ 0, where Junk is anything, eg 0.)

• log_{x}(x ˆ f) = f, if x does not occur in f.

• log_{x}(a ˆ x) = log_{x}(x ˆ (aˆ )) = (aˆ ), if x does not occur in a.

• log_{x}(a_{k} ˆ ⋯ ˆ a_{1} ˆ M ˆ a) = (log_{x} M) × a × (a_{1}ˆ ) × ⋯ × (a_{k}ˆ ), if x does not occur in a_{1}, …, a_{k}, a.

• log_{x} a = 0 × (aˆ ), if x does not occur in a.

1I learnt this from p 120 of ‘Sets, An Introduction’, by Michael D. Potter, Oxford Science Publications, Clarendon Press 1990.

2I suggest that a correct definition of the multiplication combinator can be read into Wittgenstein’s Tractatus. (See 6.241, 6.02, 6.021.) Wittgenstein used exponential notation in connection with iteration of operations, and thought of numbers à la Church. I have not yet looked in the book of Leviticus …

Here is the arithmetical code for the classical combinators C, B and K.

\begin{aligned}C & = & (×) × ((ˆ )×) \\ B & = & (ˆ ) × ((×)×) \\ K & = & (ˆ ) × (0×) \end{aligned}

For full λ-abstraction, we have to use addition, which is the only arithmetic combinator to duplicate an argument. It is sufficient to consider the case log_{x}(x ˆ x ˆ a), where x has no occurrence in a. By manipulation, we obtain:

x ˆ x ˆ a
= (Junk ˆ x ˆ K) ˆ x ˆ a
= Junk ˆ x ˆ (K + a)
= (x ˆ (K + a)) ˆ (Junkˆ )
= x ˆ ((K + a) × (Junkˆ ))

and so take (K + a) × (0ˆ ) to be the code for log_{x}(x ˆ x ˆ a).

One can compile logarithmic expressions to arithmetical code by ‘brute force’, meaning first translation to affine form by introducing W combinators and then compiling the affine term. However, one can also sometimes exploit laws such as log_{x}(a × b) = (log_{x} a) + (log_{x} b), log_{x}(a ˆ 0) = 0 (even if x is free in a), and (1×) = (0+) = 1 to produce tighter code.

An interesting form of term is the following:

l(n) = K × n

It acts as a conditional. We have:

c ˆ b ˆ l(0)  = c
c ˆ b ˆ l(1)  = b
c ˆ b ˆ l(1 + 1)  = b
c ˆ b ˆ l(1 + 1 + 1) = b
…

Another miscellaneous thing: the usual pairing combinator log_{c}(c a b) comes out as (aˆ )×(bˆ ), with projections (Kˆ ) and (0ˆ ), which seems to make a weird kind of sense.

One can also take familiar formulas, such as for polynomials and their roots, and look at them in a new light. How do the formulas behave as λ-terms? More speculatively, perhaps there is some way to think of power-series in this connection. (For this one would probably have to consider lazy streams of some kind.)

It is also interesting to think about the inverses of the arithmetic operations. To what extent can we express subtraction, and division? What about change of base in logarithms, or primes and unique factorisation, or Diophantine equations, or having an ordered structure, or factorials and Stirling’s approximation, or algebraic numbers versus transcendentals, or differentiation, or … ?

2 The AMEN machine

In this section we sketch in general terms the Arithmetical Logical Unit, or ALU as it is called in computer architecture. Intellectual property considerations dictate that we should restrict ourselves tightly to giving only cryptic hints.

The machine works by graph rewriting. There are 5 ‘leaf’ nodes (+),0,(*),1,(^) and 3 forms of inner node. All inner nodes are binary, and there is one for each of the binary functions +,*,^. The three different kinds of node help conserve space.

The general idea is much as with a combinator machine such as the ‘SKI’- machine (Turner,Fairburn?), or a supercombinator machine (Hughes, Johnsonn-Augustsonn, Peyton-Jones). One ‘unwinds’ the graph in pursuit of the combinator at its head, building up a stack of intermediate nodes. When the combinator is found, if there are sufficient arguments, the graph is rewritten so that the node that formerly held an instance of the left-hand-side of its definition now holds the corresponding instance of the right-hand-side.

However, here there are three levels of arithmetic, and so we have an additive stack, a multiplicative stack, and an exponential stack. It is the ordinary thing, but in 3 dimensions. One can think of the machine as being in 3 modes: exponential (the E-axis), multiplicative (the M-axis), and additive (the A-axis).

(I haven’t really worked this out, as must be obvious.)

Perhaps one could express this mechanism in the form of an interpreter. In Haskell there might be a state monad, with 3 stacks. Garbage collection could be represented by an operation to ‘canonicalise’ the graph to the part of potential interest (accessible from a stack), as in breadth-first copying. However, garbage collection should do affine reductions.

An observation of Conor McBride: we have a machine which spends practically all of its time performing garbage reduction, except once in a while when it gets round to performing an addition. Truely the blame for all forms of garbage may be laid at the feet of addition.

We should have ‘varargs’ versions of the binary addition and multiplication nodes, as with finite sums and products. Zero and one would be the degenerate, 0-place versions. If a right field in a product is a sum, then expanding will introduce sharing of the left field. This is a typical optimisation.

Wadler, how to fix leaks with a garbage collector. He remarks that certain functions (paradigmatically projections) can safely be evaluated by a garbage collector, as they need no new storage. He probably knew that this holds good for all affine functions.

Purely exponential stack: figure 1

The usual combinators: fig 2.

Exponential:

\begin{matrix}… & ˆ … & ˆ … & ˆ … & ˆ (bˆ a) ⟶ & … & ˆ b & ˆ a \\ c & ˆ b & ˆ a & ˆ f & ˆ (+) ⟶ & (cˆ bˆ f) & ˆ b & ˆ a \\ … & ˆ b & ˆ a & ˆ f & ˆ (×) ⟶ & … & ˆ (bˆ f) & ˆ a \\ … & ˆ … & ˆ a & ˆ f & ˆ (ˆ ) ⟶ & … & ˆ f & ˆ a \\ … & ˆ … & ˆ a & ˆ f & ˆ 0 ⟶ & … & ˆ … & ˆ a \end{matrix}

Applicative (other way round):

\begin{matrix}(a b) & … & … & … & … ⟶ & a & b & … \\ (+) & f & a & b & c ⟶ & a & b & (f b c) \\ (×) & f & a & b & … ⟶ & a & (f b) & … \\ (ˆ ) & f & a & … & … ⟶ & a & f & … \\ 0 & f & a & … & … ⟶ & a & … & … \end{matrix}

Figure 1: Stack transitions for the (exponential part of the) arithmetic machine.

(f a) . . . . . . . . .  ⟶  f a …
B  f a b  ⟶  f (a b) …  (.)
C  f a b  ⟶  f b  a  swap
W  f a …  ⟶  f a  a  dupl
K  f a …  ⟶  f . . . . . .  pop
I  f . . . . . .  ⟶  f . . . . . .  no-op

Figure 2: Usual combinators

  a + b = \ l s z -> b l s (a l s z)
  a * b = \ l s z -> b l (a l s) z
  a ^b = \ l s z -> b l' (a l) s z
                     where l' xi x = l (\ n -> xi n x)
  0 = \ l s z -> z
  1 = \ l s z -> s z

Figure 3: Arithmetic with a limit operation

3 Typeful programming (rough notes)

The exponential function entails a certain shift in type. You can see this if you think of numbers as iterating operations – for example, handing another coin to a shopkeeper. Doing such a thing n + m times is just doing it n times, and then m more. Doing a thing n × m times is doing m blocks in each of which it it is done n times. Doing a thing n^{m} times also involves doing something m times, but now the operation is higher order. It is the operation on a concrete operation which iterates it n times. (To be sure, there is also a ‘up-shift’ involved in the step from addition to multiplication, since we have to think of the operation as something that can be replaced by blocks or multiples of itself.)

The Haskell ‘program’ \ x -> x ^x is ill-typed, while the simplest type

 \ x y -> y ^x has is

α′′

where

α′ = α → α

The type α′′ is the type of Church-numerals with ground-type α.

It is to be suspected that in order to get a class of functions which is closed under identification of different arguments (i.e. under the W combinator), some kind of polymorphism is involved.

You can see this shift in another way, if you consider what happens when the notion of number is extended (as in figure 3) to include ‘limit’ numbers of some kind, such as limits of countable sequences. We can extend the arithmetic combinators to commute with taking limits in the appropriate sense. (The domain of the type of sequences plays no rôle.)

The things to remark here:

• See how the brackets creep to the left.

• Look at how b is taken to be a 4 place function in the equation for exponentiation.

• We need some notion of limit structure.

That affine terms are always well-typed. It is some restriction on W, or +, or S (or other ‘repetitor’) that enforces a typing discipline.

4 Streams (rought notes)

I suspect that proof-theorists (with the honourable exception of Peter Aczel) have been unduly obsessed with well-foundedness, or in more modern jargon, initiality. If, in 1998, in a computer-science department, one reads the original papers by Tait, Martin-Löf, Howard, .. about infinite terms, or indeed (from a Curry-Howard perspective) infinite proofs, it seems reasonable to ask “should this really be expressed in terms of streams?”.

What is the ‘strength’, in any reasonable sense, of (some simple) principles of co-induction (say, as on streams, which seems somehow dual to induction on the natural numbers)? I have no idea! On the other hand, from programming in lazy functional languages, I know that coinduction is an enormously useful form of recursion. (It seems to arise whenever you want to deal with something ‘stateful’.)

Addition, multiplication (perhaps), exponentiation, and zero are 4 of the 5 ingredients of Cantor normal form. What could be ω?

a ˆ (b : bs) ˆ ω = a : (a ˆ b) ˆ bs ˆ ω
ω × hd  = 0
ω × tl  = hd + tl × ω

Maybe. (: is an infix cons.) Something else that seems to crop up is bang – a kind of infinite repetition.

a ˆ bang = a : a ˆ bang
bang × hd = 1
bang × tl = bang

And then, there are pointwise operations (zipWith).

How to make something precise of this.