\documentclass{article} \usepackage{graphicx} \usepackage{hyperref} \title{AMEN: The last word in combinators \\ (A Naperian meditation)} \author{Peter Hancock} \date{{DRAFT} of \today} \input{preamble.tex} %include polycode.fmt %format ^ = "\wedge" %format ** = "**" %format * = "\times" %format :^: = ":\wedge:" %format :*: = ":\times:" %format <^> = "\langle\wedge\rangle" %format <*> = "\langle\times\rangle" %format <+> = "\langle+\rangle" %format alpha = "\alpha" %format beta = "\beta" %format gamma = "\gamma" %%format "^" = "\"\wedge\"" %format LEQ = "\leq" %format <=> = "\iff" %format chipmul = "\mathop{\setminus}" %format chopmul = "\mathop{/}" %format chipadd = "\mathop{-\!\!<}" %format chopadd = "\mathop{>\!\!-}" %format <> = "\!" %format b0 = " b_0" %format b1 = " b_1" %format b2 = " b_2" %format bn = " b_n" %format k0 = " k_0" %format k1 = " k_1" %format k2 = " k_2" %format kn = " k_n" %%format c0 = " c_0" %format c1 = " c_1" %format c2 = " c_2" %format CW = " W^C " %format Omega = "\Omega" %format omega = "\omega" %format sum = "\mbox{$\sum$}" %format prod = "\mbox{$\prod$}" %%%%%%%%%%%%%%%%%%%%%%%\Usepackage{mathlig} \begin{document} \maketitle \begin{abstract} Delightfully, the arithmetical combinators for addition, multiplication, exponentiation and naught turn out to be combinatorially complete: we can compile the $\lambda$-calculus into a eerily arithmetical machine code. This fact, discovered over 30 years ago, deserves to be more widely known, if only for sheer entertainment. One can happily while away hours stuck in the British transport system figuring out the arithmetical forms of algorithms. It is in my opinion better than Sudoku. \textbf{I am trying to massage pieces of this into a publishable form. The contents page, and some of the appendices will disappear.} \end{abstract} \tableofcontents %%%%%%%%%%%%%%%%%%%%%%%\input{ligatures.tex} \section{Introduction} \paragraph{Recent attempt Thu May 24 09:28:24 BST 2007 to write an intro}\mbox{} What are numbers? More specifically, what are the numbers we use when we are counting off operations, like giving someone banknotes, or shearing sheep? They are fundamentally iterators, by which I mean they take an operation and a starting point, and perform that operation a certain number of times. The idea is as old as time, or at least Archimedes, who considered the problem of counting grains of sand, and devised a notation to express the number of grains that would fill the universe. One notation for iteration is the exponential, which expresses iteration with a superscript of the operation \[ o^n \] It is not an accident that we use the same notation for numerical exponentiation, with the base replacing the operator, and the exponent replacing the iteration \[ b^a = (\times b)^a(1) \] In this equation, the first superscription denotes numerical exponentiation, and the second denotes iteration. Superscripts can soon get out of hand at about 2 levels of nesting, so it is much more practical to use a infix binary operator such as |^|. What this paper is about is the use of exponential notation for function application itself, but with the function on the right. Hand in hand with exponential notation comes a useful algebraic calculus (`exponential calculus') involving the operators $\times$, |.|, $1$, $+$ and $0$ for working with exponential notation: \[ \begin{array}{llll} a^{b \times c} &= (a^b)^c & a^1 = a \\ a^{b + c} &= a^b \times a^c & a^0 = 1 \end{array} \] Together, these operators obey many (though not all) familiar arithmetical laws. Moreover, we can read the equations above as \emph{defining} combinators |(*)|,|1|,|(+)|,|0|, using the notation $a^f$ instead of mathematical $f(a)$ notation, or Haskell's juxtaposition |f a|. In this notation the binary operators are related to the combinators by the arithmetically bizarre laws: \begin{spec} b ^ c = c ^ b ^ (*) b * c = c ^ b ^ (*) b + c = c ^ b ^ (+) \end{spec} Remarkably, these combinators (minimally |(*)|,|(+)|,|(^)| and |0|) turn out to be combinatorially complete. Just like the fairly well-known pair |S, K|, or the less well-known set |C, B, K, W|, or indeed various other sets of combinators. they are a sufficient basis for introducing $\lambda$-abstraction |\ x -> e| as a meta-notation, where |e| is an exponential expression with one free variable |x|. Formally, this strongly resembles `logarithm to the base $x$'. This has to satisfy the so-called $\beta$-rule |a ^ (\ x -> b) = x<-a;b| where |a| is closed and |b| may contain occurrences of the free variable |x|. It also satisfies the so-called $\eta$-law |(\ x -> x ^ a) = a| where |a| is closed.) The logarithm fits well with this exponential calculus \[ \begin{array}{llll} (\log_c a) \times b &= \log_c (a^b) & 1 = \log_c c \\ (\log_c a) + (\log_c b) &= \log_c (a \times b) & 0 = \log_c 1 \end{array} \] If one thinks of application as a form of exponentiation, then surely some form of $\lambda$-abstraction should correspond to the logarithm. This turns out to hold at least for \emph{linear}\footnote{Technically, \emph{affine}.}lambda abstraction, where there may be at most one occurrence of the bound variable in the body. But, it holds even more generally, as shown by the equation above for the logarithm of a product. \paragraph{An older attempt to write an intro} If one represents natural numbers by Church numerals, there are natural definitions of the arithmetic operators |(+)|, |(*)|, and |(^)| that make sense as definitions of general combinators. Curiously, these combinators are combinatorially complete, in the sense, roughly, that they support untyped $\lambda$ abstraction. Another more logical way to describe combinatorial completeness is that there is a deduction theorem, for reducing a lambda-calculus or natural-deduction style presentation of a logic to a so-called Hilbert-style presentation in terms of axioms and the rule of modus ponens. The combinatorial completeness is not a new observation, but it deserves to be more widely known. It seems to have been published first by Stenlund in 1972 \cite{Ste:comltp}, and by B{\"o}hm in 1979 \cite{bohm:1979}. Other people must have have stumbled across the combinatorial completeness independently: according to Stenlund, some students of Fitch certainly knew of it. This paper aims to convey the sheer fun of it. If one looks at the $\lambda$-calculus with an arithmetical eye, it transpires that many common constructions have a natural arithmetical expression, which can manipulated according to some of the familiar laws of arithmetic. Agreeably, the arithmetical notation meshes well with notions of linearity. The fragment |(^), (*), (<>)| without addition characterises the affine lambda calculus, and if we also throw out naught~\footnote{ I use old-fashioned spelling ``naught'': the word is in fact etymologically connected with ``naughty''. A lot of word-play in Shakespeare based on this. It amuses me that the concept of zero was thought to be ``dangerous Saracen magic'' in medieval times (William of Malmesbury). According to John Donne, ``The less anything is, the less we know it: how invisible, unintelligible a thing is nothing''. % I think I remember Harold % Simmons suggesting that the symbol for zero was chosen to be a % circle because it is through a circle that we emerged into the % world. %If you prefer, We may think of its symbol as the first letter of `Origin'.} itself (but retain |(^), (*), 1 = (<>)^(<>)|) we get the linear lambda calculus. \iffalse On the aesthetic side, the resulting programs resemble a four-letter genetic code. (With lots of irritating single parentheses.) If on the other hand one uses Haskell's section notation, programs in combinatory form resemble illusions caused by a serious eye disease, the ultimate in obfuscation. If I get round to it I will make a postcript picture of a large one, in figure \ref{fig:eye}. \begin{figure} \begin{center} \includegraphics[scale=0.3]{Picture.pdf}. \end{center} \caption{An advanced form of eye disease.} \label{fig:eye} \end{figure} \fi If one uses the notation ``AMEN'' for the combinators addition, multiplication, exponentiation and naught (nil,no-operation), surely one has the last word in combinators~\footnote{Thanks to Jim Laird for the title.}. In this file I implement a rewriting calculus for arithmetical expressions built up with constructors for addition, multiplication, exponentiation and naught. I've found it useful for experimentation (really, playing around) with `arithmetical' versions of standard combinators. The end of the file consists mostly of debris from such experiments. \section{Definitions of : $+$, $\times$, $\wedge$, $0$.} It is one of the very nice features of Haskell that one can take over and redefine symbols such as for the arithmetical operations |(+)|, |(*)|, and |(^)|. Three (out of four) cheers for the `hiding' keyword! However, it doesn't seem that we can take over `|0|'. This is a pity, as it is the only other symbol I need. (PS: I'm told that by using ghc with the '-fno-implicit-prelude' flag one can actually take over `|0|'. I haven't yet had the indefatiguability to try it.) \begin{code} module Main where import Prelude hiding ((*),(^),(+)) infixr 8 ^ infixr 7 * infixr 6 + infixr 9 <> \end{code} Here are some simple definitions of binary operations corresponding to the arithmetical combinators: \begin{code} a ^ b = b a a * b = \c -> (c ^ a) ^ b a + b = \c -> (c ^ a) * (c ^ b) a `naught` b = b \end{code} Instead of |naught|, I shall use the infix operator |(<>)|, that looks a little like a `|0|'. \begin{code} (<>) = naught \end{code} The type-schemes\footnote{ I suspect that these have been given as a Hilbert-style axiomatisation of propositional logic. } inferred for the definitions are as follows: \begin{code} (^) :: a -> (a -> b) -> b (*) :: (a -> b) -> (b -> c) -> a -> c (+) :: (a -> b -> c) -> (a -> c -> d) -> a -> b -> d (<>) :: a -> b -> b \end{code} % The definitions above generate an equivalence relation between: the least one % extending them, congruent to all operators. Equations can be proved by substituting equals for equals. One can also allow instances of the following "$\zeta$" Rule in proving equations. \begin{center} \begin{tabular}{c} |x ^ a = x ^ b| $\mbox{}\ruleimplies\mbox{}$ |a = b| \end{tabular} \end{center} with the side condition that |x| is fresh to both |a| and |b|. This is an expression of extensionality, or perhaps `exponentiality': two values that behave the same as exponents are the very same value. I shall call this relation $\zeta$-equality. All equations asserted below should be interpreted as $\zeta$-equations. \section{Combinatorial completeness, and other amusements} \label{sec:cc} An amusing phenomenon is that |(+),(*),(^)| and |(<>)| are combinatorially complete: they can replace $\lambda$-abstraction. For a technical definition and full discussion, see \cite{Barendregt84} or \cite{Hindley86}. The gist of it is that you can translate, or compile an expression in the $\lambda$-calculus or a functional program into a $\zeta$-equivalent expression in which the only definitions are those of |(+),(*),(^)| and |(<>)|. I doubt this would be a sensible approach for implementing a functional language, though the arithmetical combinators are among several sets of combinators, complete or not, which it may be worth treating specially when compiling or evaluating $\lambda$-calculus expressions. To establish completeness it is enough to define the following Curry combinators in terms of them. This particular set was perhaps designed to be combinatorially complete. They are all but one well known to Haskell programmers, under the names in the left hand column of the following table. The second column gives a possible definition as a $\lambda$-term. The third column has the upper case capital letters given as names by Curry. The last column contains an aide memoire. \begin{center} \begin{tabular}{lllcl} |flip |&| (\f a b |&| -> f b a) |&| C |&| -- swap the arguments of a binary function | \\ |(.) |&| (\f a b |&| -> f (a b)) |&| B |&| -- compose two functions | \\ |id |&| (\f |&| -> f) |&| I |&| -- identity | \\ |const |&| (\f a |&| -> f) |&| K |&| -- return a function with a single value | \\ &| (\f a |&| -> f a a) |&| W |&| -- this might be called diag, or dupl | \end{tabular} \end{center} These are well known (and were perhaps even designed) to be combinatorially complete. (They were introduced in Curry's thesis \cite{Curry30}. They were used -- with important extensions for the sake of efficiency -- in David Turner's implementation \cite{DBLP:journals/spe/Turner79} of the seminal functional language SASL. They can be viewed as an optimisation of the standard `SKI' combinators, providing important special \emph{linear} cases of |S| using |B| and |C|. The definition of |S| in terms of the arithmetic combinators is not difficult, but isn't blindingly enlightening, and is given in the appendix.) The definitions of the Curry combinators in terms of the arithmetic combinators are quite simple, though it may not be immediately clear where they come from. \begin{code} combC = (*) * (^) ^ (*) -- called "flip" by fp'ers combB = (^) * (*) ^ (*) -- |(*) ^ combC| i.e. composition (.) combI = evil ^ (<>) -- or |(^) * (^) ^ (*)|, inter alia combK = (^) * (<>) ^ (*) -- |(<>) ^ combC| combW = (^) * ((^) + (^)) ^ (*) -- |((^) + (^)) ^ combC| evil = error "Unthinkable" \end{code} We finish this section by deriving these definitions from the definition of each Curry combinator. \def\commentbegin{\quad\{\ } \def\commentend{\}} The key thing is to start with the |C| combinator. \begin{description} \item[C] takes a binary function, and transposes or `flips' its arguments. \begin{spec} C a b c = {- def -} a c b = {- re-express using exponentiation -} b ^ (c ^ a) = {- def of |(^)| -} (c ^ a) ^ b ^ (^) = {- def of |(*)| -} c ^ (a * (b ^ (^))) \end{spec} So, \begin{spec} C a b = {- by the above, and $\zeta$ -} a * (b ^ (^)) = {- def of |(*)| -} (b ^ (^)) ^ a ^ (*) = {- def of |(*)| -} b ^ ((^) * a ^ (*)) \end{spec} So, \begin{spec} C a = {- by the above, and $\zeta$ -} (^) * a ^ (*) = {- def of |(*)| -} (a ^ (*)) ^ (^) ^ (*) = {- def of |(*)| -} a ^ ((*) * (^) ^ (*)) \end{spec} So | C = (*) * (^) ^ (*) |. \item[B] % As for |B|, it is clear that it is the transpose of |(*)|, or in other words | (*) ^ C |. From the middle step in the derivation of |C|'s arithmetic form, we therefore have as a by-product \begin{spec} B = (^) * (*) ^ (*) \end{spec} \item[K] % As for |K|, it is clear that it is the transpose of |(<>)|, or in other words |(<>) ^ C|. Therefore, just as for |B|, \begin{spec} K = (^) * (<>) ^ (*) \end{spec} \item[I] % As for |I|, it is the transpose of |(^)|, modulo extensionality. So we could take the following. \begin{spec} I = (^) * (^) ^ (*) {- ie. | I = (^) ^ C | -} \end{spec} But we can also take any of the following: \begin{spec} I = C * C I = anything^(<>) \end{spec} \item[W] %As for |W|, first l Let's first express its transpose |CW|, which is quite easy. \begin{spec} CW a b = {- def -} b a a = {- re-express using exponentiation -} a ^ a ^ b = {- def of |(^)|, twice -} (b ^ a ^ (^)) ^ a ^ (^) = {- def of |(*)| -} b ^ (a ^ (^) * a ^ (^)) = {- def of |(+)| -} b ^ a ^ ((^) + (^)) \end{spec} So by extensionality |CW = (^) + (^)|, that is |W = ((^) + (^)) ^ C|. Note how this fits with the definitions of K and I. \begin{spec} K = (<>)^C I = (^)^C W = ((^)+(^))^C ; ... \end{spec} \end{description} This completes the derivation of the |BWICK| combinators. Amusingly, \begin{spec} (^) = 1^C {- |(^)| and |1| mutually converse -} W^C = 1^C + 1^C {- ie. |W| is a dual of 2 -} C^2 = 1 {- |C| is a square root of 1 -} 1^W = (^)^W {- self application -} W = C*W {- |W| is symmetric in first arg -} K = (<>)^C {- |K| and |(<>)| mutually converse. -} 1 = (<>)^(<>) = ((^)*) ^ ((^)*) 1^W ((^)*) = 1^W (<>) \end{spec} There are many other amusements in the AMEN arcade, that can be worked out in the edge of a newspaper, or on a computer. Appendix \ref{sec:arcade} contains a selection. \section{Algebra} \label{sec:algebra} When equality is interpreted as extensional equality, . |(+,(<>))| forms a monoid. . |(*,1)| forms a monoid, where |1 = combI| . . |a * (b + c) = a * b + a * c| . . |a * (<>) = (<>)| . Addition and multiplication are not in general commutative. The laws of |(+),(<>),(*),1| above (ie. the ones which do not mention exponentiation) coincide roughly with the basic laws of the the arithmetic of (not necessarily linear or well-founded) orderings. (However the coincidence is not exact. In the combinatory world, we don't have, among other things that hold in the world of orderings, |(<>) * a = (<>)|. This is because we don't have |1 ^ a = 1|. It seems that an algebraic structure satisfying the axioms might be called a `weak near-rig'. A rig is like a ring, except one doesn't ask for additive inverses. Neither addition nor multiplication are commutative. `Nearness' refers to just one half of the distributivity laws. Personally, I call the structure `an arithmetic'. It is probably just a curiosity, but the unit laws for the monoids can be put in the form of closed equations~\footnote{Many interesting observations seem to have the form |... = 1|. Two other examples are |(^)*((^)*) = 1|, |C ^ 2 = 1|. }. \begin{spec} (+) * ((<>)^) = (+)^C * ((<>)^) = 1 (*) * (1^) = (*)^C * (1^) = 1 \end{spec} % In some respects |C| seems to behave like |-1|. This would make a square root of |C| % something like the complex number $i$. This in turn would make a solution for $x$ of |(^)^ (i * x) = 1| a % candidate for $\pi$. I know of no square root for |C|, but I can express it in the form |R ^ R ^ R|. The associativity rules can be put in the form of commutativity laws. \begin{spec} (((*)^C) gamma)*((*) alpha) = ((*) alpha)*(((*)^C) gamma) (((+)^C gamma))*((+) alpha) = ((+) alpha)*(((+)^C) gamma) \end{spec} These can be reduced further to equations between constants. \section{Logarithms} \label{sec:log} One can introduce `logarithms', as a sort of lambda-abstraction, with |x ^ (log_x e) = e|. Linear logarithms (with only one occurrence of the `base' |x| in |e|) obey many delightful arithmetico-combinatorial laws, that can be figured out on the average paper napkin. The following are easily verified, where $a, b, b_1, \ldots b_k$ are expressions that do not contain any occurrences of the variable $x$. \begin{spec} log_x (a x b) = log_x (b ^ x ^ a) = log_x ((x ^ a) ^ (b^)) = a * (b^) log_x (a x b1 .. bk) = a * (b1 ^) * .. * (bk ^) log_x (a x x) = ((^)+(^))*(a ^) log_x a = 0 * (a ^) \end{spec} In fact, any linear abstraction (in which the bound variable occurs exactly once) is a product (ie. a composite) of factors that each look like \begin{spec} a * (b1^) * ... * (bk^) \end{spec} Logarithms need not be linear. For example, when the base occurs in both factors of a product, the product is turned into a sum. If $a$, $b$ and $c$ are expressions such that $c$ contains no occurrences of $x$, then \begin{spec} log_x (a * b) = (log_x a) + (log_x b) log_x 1 = (<>) log_x (a ^ c) = (log_x a) * c \end{spec} These equations were at one time familiar to schoolchildren. From these we can derive the logarithm of a monomial \begin{spec} log_x (b1 ^ k1 * ... * bn ^ kn) = (log_x b1) * k1 + ... + (log_x bn) * kn \end{spec} B{\"o}hm studied the arithmetical combinators and was well aware of the similarity between $\lambda$-abstraction and logarithms, as shown in the publication \cite{bohm:1979}\footnote{I am very grateful to Roger Hindley for a copy of this almost unobtainable paper}. At this point, one should have a picture. There is one in figure \ref{fig:logbook}. \begin{figure} \begin{center} \includegraphics[scale=0.5]{Napier10.pdf}. \end{center} \caption{Front page of Laird Napier of Merchiston's book on logarithms.} \label{fig:logbook} \end{figure} \section{Arithmetical calculus} The arithmetical combinators are rather fascinating, but it is easy to make mistakes when performing calculations. We now write some code to explore on the computer the evaluation of arithmetical expressions, built out of our four combinators. The first piece of code is an evaluator, that computes the normal form of an expression (with respect to some rewriting rules) if one exists. This lets us see the value of an expression, but not how it was arrived at. The second piece of code is for watching the reduction rules in action. There are various systems and reduction strategies of interest. They arise from the algebraic structure: the additive and multiplicative monoids, weak distributivity, etc. Here is a datatype |E| for arithmetical expressions. The symbols for the constructors are chosen to suggest their interpretation as combinators. \begin{code} infixr 8 :^: infixr 7 :*: infixr 6 :+: \end{code} \begin{code} data E = V String | E :^: E | E :*: E | E :+: E deriving (Eq) -- (Show,Eq) \end{code} We can think of these expressions as fancy Lisp S-expressions, with three `cons' operations, each with an arithmetical flavour. Like Neapolitan ice cream. It is convenient to have atomic constants identified by arbitrary strings. The constants |"+"|, |"*"|, |"^"| and "|0|" are treated specially. For each arithmetical operator, we define a function that takes two arguments, and (sometimes) returns a `normal' form of the expression formed with that operator. (This doesn't allow us to trace reduction sequences -- we turn to that later.) The definitions correspond to the transitions of an arithmetical machine. \begin{code} infixr 8 <^> infixr 7 <*> infixr 6 <+> \end{code} \begin{code} (<+>),(<*>),(<^>) :: E -> E -> E a <+> b = case b of V "0" -> a b1 :+: b2 -> (a <+> b1) <+> b2 _ -> a :+: b a <*> b = case b of V "0" -> b b1 :+: b2 -> (a <*> b1) <+> (a <*> b2) b1 :*: b2 -> (a <*> b1) <*> b2 _ :^: V "0" -> a _ -> a :*: b a <^> b = case b of V "0" -> b :^: b b1 :+: b2 -> (a <^> b1) <*> (a <^> b2) b1 :*: b2 -> (a <^> b1) <^> b2 _ :^: V "0" -> a b1 :^: V "^" -> b1 <^> a -- note: destroys termination b1 :^: V "*" -> b1 <*> a b1 :^: V "+" -> b1 <+> a b1 :^: b2 -> a :^: (b1 <^> b2) _ -> a :^: b \end{code} The following (partial!) function then evaluates an arithmetic expression. \begin{code} eval a = case a of b1 :+: b2 -> eval b1 <+> eval b2 b1 :*: b2 -> eval b1 <*> eval b2 b1 :^: b2 -> eval b1 <^> eval b2 _ -> a \end{code} \section{Reduction sequences} We now define for each expression the list of expressions to which it can be reduced in one toplevel step. One can tinker here. (Be careful of overlap between patterns). This following function returns the list of expressions that can be reached from a given expression in a single top-level reduction step. Although the lists returned here are singletons, there can be overlap between rewriting rules: more than one reduction rule may apply. \begin{code} tlr :: E -> [E] tlr e = case e of (a :+: (b :+: c)) -> [ (a :+: b) :+: c ] (a :+: V "0") -> [ a ] (V "0" :+: a) -> [ a ] (a :*: (b :+: c)) -> [ (a :*: b) :+: (a :*: c) ] (a :*: V "0") -> [ v0 ] (a :*: (b :*: c)) -> [ (a :*: b) :*: c ] (a :*: V "1") -> [ a ] (V "1" :*: a) -> [ a ] (a :^: (b :+: c)) -> [ (a :^: b) :*: (a :^: c) ] (a :^: V "0") -> [ v1 ] (a :^: (b :*: c)) -> [ (a :^: b) :^: c ] (a :^: V "1") -> [ a ] (a :^: b :^: V "+") -> [ b :+: a ] (a :^: b :^: V "*") -> [ b :*: a ] (a :^: b :^: V "^") -> [ b :^: a ] (a :^: b :^: V "0") -> [ a ] _ -> [ ] v0 = V "0 " v1 = V "1" -- |v0 :^: v0| \end{code} To represent subexpressions, I use % an idea I saw in a program by Mark % Jones. (It is essentially the "zipper" attributed to Gerard Huet, a `zipper', in a form in which the context of a subexpression is represented by a linear function.) We represent each part |e| of an expression |e'| as a pair |(f,e)| consisting of the subexpression |e| there, and a linear function |f| such that |f e = e'|. (By construction, the function is linear in the sense that it uses its argument exactly once.) Intuitively you `plug' the subexpression |e| into the `context' |f| to get back |e'|. The function |parts| returns all the subexpressions of a given expression, in the contexts in which they occur. This includes the improper case of the expression itself in the empty context. The function |pparts| returns the proper parts. \begin{code} parts, pparts :: E -> [(E->E,E)] parts e = (id,e) : pparts e pparts e = case e of (a :+: b) -> g (:+:) a b (a :*: b) -> g (:*:) a b (a :^: b) -> g (:^:) a b _ -> [] where g op a b = [ ((a `op`) . f,p) | (f,p) <- parts b ] ++ [ ((`op` b) . f,p) | (f,p) <- parts a ] \end{code} Now we define for any expression a list of the expressions to which it reduces in a single, possibly internal step. \begin{code} reducts :: E -> [ E ] reducts a = [ f a'' | (f,a') <- parts a, a'' <- tlr a' ] \end{code} We need a structure to hold the reduction sequences from an expression. So-called `rose' trees seem to be ideal. \begin{code} data Tree a = Node a [ Tree a ] \end{code} We define a function which maps an expression to its tree of reduction sequences. \begin{code} redTree :: E -> Tree E redTree e = Node e [ redTree e' | e' <- reducts e ] \end{code} To list the reduction sequences in a tree, is quite easy. I call a tree with no subtrees a tip. \begin{code} tip :: a -> Tree a tip a = Node a [] \end{code} The branches function maps a tree to a list (which may be infinite) of the sequences of node labels encountered on some path to a tip. \begin{code} branches :: Tree a -> [[a]] branches (Node a []) = [ [a] ] branches (Node a ts) = [ a : b | t <- ts, b <- branches t] \end{code} \section{Calculators} In the dawn of functional programming, there were a few working implementations of combinator machines, using a complete set of combinators such as $SK$, $BWCK$, or a variant thereof\footnote{For example: \cite{DBLP:journals/spe/Turner79} \cite{UCAM-CL-TR-81} \cite{UCAM-CL-TR-40}. For implementing functional languages, attention quickly switched to supercombinators extracted from a particular program, but research on complete sets of combinators continues today. (Simmons.)}. If we count paper and vapour implementations, there were about a dozen. It is amusing to speculate about a combinator machine incorporating the combinators $AMEN$. This would indeed be a arithmetical calculator. For the sake of optimising common cases, in such an arithmetical machine one might use `polyadic' forms of |sum| and |prod|, taking finite lists as arguments. \begin{spec} sum [a1,..,ak] = a1 + ... + ak prod [a1,..,ak] = a1 * ... * ak \end{spec} It seems important to recognise the associativity of addition and multiplication. No doubt a lot of other such gadgetry could be put to use. Because the fragment $MEI$ captures linear abstraction (and $MEN$ affine abstraction), the machine meshes well with a concern with linearity. It is well-known that in graph reduction, the garbage collector can perform certain forms of reduction. For example, it can perform projections from tuples. See `Fixing some space leaks with a garbage collector' by Philip Wadler \cite{wadler87fixing} (Software Practice and Experience, 17(9):595-608, September 1987). More generally, linear reductions can be regarded as performed by the garbage collector. In some sense, an arithmetical machine (a combinator machine for the arithmetical combinators would spend most of its time in multiplicative (affine) mode, performing garbage collection. Every now and then, it might perform an addition. \section{Origins, and variants } Definitions of slight variants of the arithmetical combinators are abundant. Some examples are in Rosenbloom (\cite[sec. 3.4]{rosenbloom50} %: `The elements of mathematical logic', Dover 1950 ), Stenlund (\cite[sec. 2.4]{Ste:comltp} %: Combinators, lambda-terms and proof theory, Almqvist and Wiksell 1972, sec 2.4), and Burge (\cite[sec. 1.8]{burge75:_recur_progr_techn} %: `Recursive Programming Techniques', Addison-Wesley 1975), They were surely defined by Church, and -- to stretch a point -- Wittgenstein. But in some sense we all know the definitions, if we understand the concept of iteration at all. They go back to Archimedes. Of the authors mentioned above, as far as I know, only Stenlund notes the combinatorial completeness of the arithmetical combinators. Stenlund remembers corresponding with students of Fitch, who were aware of it. Apparently independently, B{\"o}hm was by 1977 aware of the combinatorial completeness (\cite{bohm:1979},\cite{bohm:1981} -- written in 1977). The publication \cite{bohm:1981} (and presumably \cite{bohm:1979}) notes the analogy between $\lambda$-abstraction and logarithms referred to in section \ref{sec:log}, and in fact wrote the logarithm function as $\lambda$ogarithm. He also noted in \cite{bohm:1981} some of amusing arithmetical properties of the combinators, such as that |C| is a square root of unity. A later paper by B{\"o}hm (\cite{bohm:1982}) is somewhat in this area, but with a particular focus on the algebraic structure described in section \ref{sec:algebra}. In particular he describes a notion that is clearly inspired by the notion of an ideal in a ring, A subset is called by B{\"o}hm a ``notion of zero'' if it contains |(<>)|, is closed under addition, and for any |a| is closed under both |(a *)| and |(* a)|. Example: $Z =$ the set of terms of the form $a^K$. %(One can alternatively describe these |(<>)*(a^)|.) \begin{itemize} \setlength{\itemsep}{0pt} \setlength{\topsep}{0pt} \setlength{\parskip}{0pt} \item (Closure under addition: |a^K + b^K = (a * b)^K|. Also |(<>) = 1^K|, so |(<>)| is also in $Z$, reassuringly.) \item (Closure under arbitrary products: |b * (a^K) = a^K|, |(a^K) * b = (a^b)^K|.) \end{itemize} A subset is called by B{\"o}hm a ``notion of infinity'' if it is closed under |(a+)| and |(+a)| for any |a|. Let $I =$ the set of terms |a * K|. Then $I$ is a notion of infinity. In B{\"o}hm's paper he also looks at notions of tupling, and the monoid of lists under concatenation. % The algebraic structure of the arithmetical combinators seems too % weak to be interesting. \subsection{Repulsive notation for multiplication} Many definitions of arithmetical combinators I've seen get the argument order slightly wrong, in my humble opinion. What goes wrong is the multiplication combinator is made the same as the |B| combinator. This affects in turn the argument order for addition, which is a pointwise-lifted composition. To establish the scriptural correctness of my version, allow me to assert that my definitions (at least for $\times$) can be read into Wittgenstein's Tractatus (around 6.02 and 6.241). They also have also the authority of Cantor according to whom the alternative is `repulsive' -- absto{\ss}ende. In fact Cantor started off using the repulsive argument order, but soon thought better of it. (This is according to Michael Potter, \cite[p. 120]{potter90:_sets_introd}.) %In my opinion, the other way of writing |*| is repulsive. \bibliographystyle{alpha} \bibliography{arithmetic} \appendix \section{Some infrastructure used above, and experimental apparatus} If one wants to investigate reduction sequences of arithmetical expressions by running this code, one needs to display them. To display expressions, we use the following code, which is slightly less noisy than the built in show instance. \begin{code} showE :: E -> Int -> String -> String showE (V "^") = \p->("(^)"++) showE (V "*") = \p->("(*)"++) showE (V "+") = \p->("(+)"++) showE (V str) = \p->(str++) showE (a :+: b) = \p->opp p 0 (showE a 1 . (" + "++) . showE b 0) showE (a :*: b) = \p->opp p 2 (showE a 3 . (" * "++) . showE b 2) showE (a :^: b) = \p->opp p 4 (showE a 5 . (" ^ "++) . showE b 4) opp p op f = if p > op then showString"(" . f . showString")" else f \end{code} \begin{code} instance Show E where showsPrec p e = showE e 0 \end{code} Some other code may be helpful for displaying reduction trees and sequences. The following uses indentation in an attempt to make the branching structure of a tree visible. \begin{code} newtype NTree a = NTree (Tree a) instance Show a => Show (NTree a) where showsPrec p (NTree t) = f id (1,t) where -- | f :: Show a => ShowS -> (Int,Tree a) -> ShowS | f pr (n,Node a ts) = (pr -- emit indentation . showString "[" . shows n . showString "] " -- child number . shows a -- node label . showString "\n" . ( composelist . map (f (pr . showString "! ")) . number ) ts) \end{code} A function for displaying a list with numbers, throwing a line between entries. \begin{code} newtype NList a = NList [a] instance Show a => Show (NList a) where showsPrec _ (NList es) = (composelist . seplist ('\n':) . map showline . number ) es where showline (n,e) = shows n . showString ". " . shows e \end{code} \begin{code} number :: [a] -> [(Int,a)] number = zip [1..] \end{code} \begin{code} composelist :: [ a -> a ] -> a -> a composelist = foldr (.) id \end{code} \begin{code} seplist :: a -> [a] -> [a] seplist s (x:(xs'@(_:_))) = x:s:seplist s xs' seplist s xs = xs \end{code} Show the first/last reduction sequence \begin{code} test, test' :: E -> NList E test = NList . hd . branches . redTree test' = NList . hd . reverse . branches . redTree hd (x:_) = x \end{code} The n'th reduction sequence. \begin{code} nth_rs :: Int -> E -> [E] nth_rs n = (!! n) . branches . redTree \end{code} The number of reduction sequences \begin{code} number_rss :: E -> Int number_rss = length . branches . redTree \end{code} First difference \begin{code} fdiff :: Eq a => [a] -> [a] -> (a,a) fdiff (a:as) (b:bs) | a /= b = (a,b) fdiff (a:as) (b:bs) | True = fdiff as bs fdiff _ _ = error"fdiff" \end{code} To save typing \begin{code} va, vb, vc, vd, ve, vf :: E va = V "a" vb = V "b" vc = V "c" vd = V "d" ve = V "e" vf = V "f" \end{code} Bureaucracy \begin{code} main :: IO() main = error"Meant for interpreter" \end{code} \section{The AMEN arcade} \label{sec:arcade} In this section, we give the arithmetical form of some naturally occurring combinators. \subsection{CBKIW0} The combinators |C|, |B|, |K|, |I| and |W| can be encoded as follows in our calculus. \begin{code} cC, cB, cK, cI, cI', cW, c0 :: E cC = (V "*") :*: (V "^") :^: (V "*") cB = (V "^") :*: (V "*") :^: (V "*") cK = (V "^") :*: (V "0") :^: (V "*") cI = jnk :^: V "0" cI' = (V "^") :*: (V "^") :^: (V "*") cW = (V "^") :*: (V "^" :+: V "^") :^: (V "*") c0 = V "0" jnk = V "Garbage" \end{code} %\susection{Expression of some other combinators} \subsection{$S$ and its ilk} If one is compiling $\lambda$-expressions into combinators, for many reasons ways it is not always sensible to treat occurrences of the same variable by pretending the variables are distinct, and then tying them together with something derived from the |W| combinator. What one actually wants is actually something like the |S| combinator, for binding a variable that occurs in both parts of an application or exponentiation. After a little playing around, another combinator emerges. This is |S'|, where |S a b| (the normal S combinator) is |W (S' a b)|. \begin{spec} S' a b c1 c2 = {- def -} a c1 (b c2) \end{spec} So, \begin{spec} S' a b c1 = {- def of composition -} a c1 . b = {- |.| is the transpose of |*| -} b * a c1 \end{spec} So, \begin{spec} S' a b = {- def of composition -} (b *) . a = {- |.| is the transpose of |*| -} a * (b *) \end{spec} So, \begin{spec} S' a = {- def of composition -} (a *) . (*) = {- |.| is the transpose of |*| -} (*) * (a *) \end{spec} So, \begin{spec} S' = {- def of composition -} ((*) *) . (*) = {- |.| is the transpose of |*| -} (*) * ((*) *) = (*) ^ (1 + (*)) \end{spec} In particular, we have the following remarkable equations: \begin{spec} S = S' * (*) * (W ^ (^)) S' = S' (*) C = S' (^) B = S' (^) (*) = (*) ^ C I = S' (^) (^) = (^) ^ C K = S' (^) (<>) = (<>) ^ C W = S' (^) ((^) + (^)) = ((^) + (^)) ^ C S' 1 = (*) \end{spec} One can define the |S'| and |S| combinators as follows: \begin{code} combS' = let x = (*) in x * (x ^ x) combS = combS' * (*) * (combW ^) \end{code} The following arithmetical code implements variants of the |S| and |S'| combinators. \begin{code} cS, cS' :: E cS' = let x = V"*" in x :*: (x :^: x ) cS = cS' :*: cW :^: cB \end{code} \subsection{Self application and Fixed points} There are two interesting definitions of the fixed point combinator: Curry's (\cite[p. 178]{CurryFeys}) and Turing's. \footnote{There are endless variations on Turing's} \cite{DBLP:journals/jsyml/Turing37a}. Both the fixed point operators use self application. \begin{spec} sap x = x x = W (^) x = W 1 x So sap = (^)^W = 1^W \end{spec} Note that the expressions |(^)^combW| and |id^combW| do not typecheck. However we can write the code. Which is the better definition: with |(^)| or |1| ? \begin{code} cSap, cSap' :: E cSap = let e = V "^" in e :^: (e :+: e) :^: cC cSap' = let e = V "^" in V "1" :^: (e :+: e) :^: cC \end{code} \subsubsection{Curry's} We call Curry's combinator simply $Y$. \begin{spec} f^Y = sap (sap * f) Y = (sap *) * sap = sap ^ ((*) + 1) \end{spec} To encode |Y|: \begin{code} cY :: E cY = let x = cSap :^: V"*" in x :^: x :^: cS \end{code} \subsubsection{Turing's} Turing's combinator is |T ^ T|, \ie{} |T ^ sap| where $T x y = y (x x y)$. \begin{spec} T x y = y (x x y) = y (sap x y) = y ((sap^C) y x) (T^C) y x = y ((sap^C) y x) = (y . (sap^C) y) x (T^C) y = sap^C y * y (T^C) = sap^C + 1 T = (sap^C + 1)^C = sap ^ ( (^C) * (+1) * (^C) ) \end{spec} $T$ can thus be seen as applying a kind of dual (with respect to the involution |(^C)|) of the successor operator to the value |sap|. Syntax for |T|: \begin{code} cTuring, cTuringY :: E cTuring = (cSap :^: cC :+: cI) :^: cC cTuringY = cTuring :^: cSap \end{code} \subsection{Sestoft's examples} There is a systematic way of encoding data structures (pairs, tuples, in the $\lambda$-calculus, sometimes called Church-encoding. Here are some examples in the list of predefined constants in Sestoft's Lambda calculus reduction workbench at http://www.dina.kvl.dk/~sestoft/lamreduce/index.html. The first line shows the definition, the remaining lines show the reduction to arithmetic form. \begin{spec} pair x y z = z x y = y ^ x ^ z = (x ^ z) ^ (y^) = (z ^ (x ^)) ^ (y ^) pair x y = (x^) * (y^) = (y^) ^ ((x^)*) pair x = (^) * ((x^)*) = ((x^)*) ^ ((^)*) = ((x ^ (^))^(*)) ^ ((^)*) pair = (^)*(*)*((^)*) \end{spec} \begin{spec} tru x y = x = x^y^(<>) = (y^(<>))^(x^) tru x = (<>)*(x^) = (x^)^((<>)*) tru = (^)*((<>)*) = (<>)^C \end{spec} \begin{spec} fal x y = y = y ^ x ^ (<>) fal = (<>) \end{spec} \begin{spec} fst p = p tru = tru ^ p = p^(tru^) fst = (tru^) snd = (fal^) \end{spec} \begin{spec} iszero n = n (K fal) tru = n ((<>)*(fal^)) tru = tru ^ ((<>)*(fal^)) ^ n = (n^(((<>)*(fal^))^))^(tru^) iszero = (((<>)*(fal^))^)*(tru^) \end{spec} \subsection{Tupling, projections} We use the usual notation $(a,b)$ for pairs. In general \begin{spec} (a1,...,ak) = (a1^) * ... * (ak^) \end{spec} and the projection operators $\pi^k_i$ have the form \begin{spec} (K^i (K^j))^ where i + j + 1 = k \end{spec} In fact the binary projections are defined using the booleans, and other projections using selector terms such as |\ x1 .. xn -> xi|. This is done by applying | (^) | to the selector. \begin{spec} \ p -> p sel = (sel^) \end{spec} The booleans are |K = (K^0) (K^1)| and |0 = (K^1) (K^0)|. The i'th element of a set with |i+j+1| elements is |(K^i) (K^j)|. It may be interesting to remark that \begin{spec} (a,a) = W pr a = (a^) * (a^) = a ^((^) + (^)) \end{spec} So that |W pr = (^) + (^) = W ^ C| \subsection{Rotation combinators} The following combinator |combR| `rotates' 3 arguments. \begin{code} combR :: a -> (b -> a -> c) -> b -> c combR = (^) * (((*) * ((^)*))*) combR' = (^) * (^) * ((*)*) \end{code} Some such operation is often provided by the instruction set of a `stack machine', to rotate the top three enties on the stack. It can be encoded as follows: \begin{code} cR, cR' :: E cR = cC :^: cC cR' = (V "^") :*: (V "^") :*: (V "*") :^: (V "*") \end{code} It so happens that the |cC| combinator and the |cR| are each definable from the other. \begin{spec} cR :^: cR :^: cR = cC cC :^: cC = cR \end{spec} To be a little frivolous, we have a way of churning out endless versions of the combinator |combR|, aka |flip|. \begin{code} flip', flip'' :: (a -> b -> c) -> b -> a -> c flip' = flip flip (flip flip) (flip flip) flip'' = flip' flip' (flip' flip') (flip' flip') \end{code} \subsection{Continuation transform} The following function |^| which takes |a| to |a ^| occurs everywhere when one works with arithmetical combinators, as it the basic means of switching the positions of variables: | a^b = b^(a^) = b^a^(^) |. On the topic of the continuation transform, for a fixed answer type |Prog|, the type-transformer |CT| \begin{spec} CT a = (a -> Prog) -> Prog \end{spec} is a well known monad, with unit \begin{spec} return a = (a^) -- ie. |return = (^)| \end{spec} and bind operator |>>=|, \begin{spec} m >>= f = m . (f^C) = (f^C) * m = (^) * (f*) * m \end{spec} You may interested to see what |callCC| looks like. That's the function whose type is the Kleislified version of Peirce's law: |((a -> CT b) -> CT a) -> CT a|. Unless I'm missing something, it is (surprisingly) not very fascinating: \begin{spec} (((*) * ((^) * 0 ^ (*)) ^ (^)) ^ (*) * (^)) * ((^) + (^)) ^ (*) \end{spec} Well, that's classical logic for you. The monadic apparatus can be encoded as follows \begin{code} ct :: E -> E ct a = a :^: V "^" -- unit cb m f = V "^" :*: (f :^: V "*") :*: m -- bind \end{code} \subsection{Church Numerals} If we think of `genuine' natural numbers, these also satisfy the following equations. Perhaps they actually characterise the `genuinely numerical' part of the model. \begin{spec} a = (<>) ^ (+ 1) ^ a a + b = a ^ (+ 1) ^ b a * b = (<>) ^ (+ a) ^ b a ^ b = 1 ^ (* a) ^ b \end{spec} We code a few useful numbers: \begin{code} naughtE, oneE, twoE, threeE, fourE :: E fiveE, sixE, sevenE, eightE, nineE, tenE :: E naughtE = c0 oneE = cI twoE = oneE :+: oneE threeE = twoE :+: oneE fourE = twoE :^: twoE fiveE = twoE :+: threeE sixE = twoE :*: threeE sevenE = threeE :+: fourE eightE = twoE :^: threeE nineE = threeE :^: twoE tenE = twoE :*: fiveE \end{code} \subsection{Peano numerals} Oleg Kiselyov \cite{oleg} was once and may still be interested in what I think he calls or once called `p-numerals'.These are (so to speak) related to primitive recursion as the Church numerals are related to iteration. So the successor of n is not \begin{spec} \ f,z->f(n f z) \end{spec} as it is with Church numerals, but rather \begin{spec} \ f,z->f n (n f z) \end{spec} I have heard other people express an interest in this encoding, which is quite natural. So, letting the variable |n| vary over p-numerals, one has \begin{spec} n b a = b (n-1) (b (n-2) ... (b 1 (b (<>) a)) ...) \end{spec} Using the combinators of this paper, one can derive \begin{spec} n b = b (<>) * b 1 * ... * b (n-2) * b (n-1) = b^((<>)^) * b^(1^) * ... * b^((n-2)^) * b^((n-1)^) = b^(((<>)^) + (1^) + ... + ((n-2)^) + ((n-1)^) \end{spec} By exponentiality ($\zeta$), \begin{spec} n = ((<>)^) + (1^) + ... + ((n-2)^) + ((n-1)^) \end{spec} %(Remember that all the numbers here are to be understood as p-numerals!) In fact, if |Osucc| is Oleg's successor, we have | Osucc n = n + (n^) |. \begin{spec} (<>)_p = (<>) 1_p = ((<>)^) 2_p = ((<>)^) + (((<>)^)^) 3_p = ((<>)^) + (((<>)^)^) + ((((<>)^) + (((<>)^)^))^) ... \end{spec} One may be reminded here of von-Neumann's representation for ordinals, with successor operation is $n \mapsto n \cup \{n\}$. and origin the empty set $\{\}$. \begin{spec} 0 = {} 1 = {{}} 2 = {{},{{}}} 3 = {{},{{}},{{},{{}}}} ... \end{spec} Clearly the operation of raising to the power of exponentiation (that takes |n| to |(n^)|) plays the role of the singleton operation $n \mapsto \{n\}$. \subsection{sgbar} |sgbar|, or exponentiation to base zero, is the function which is 1 at 0, and 0 everywhere else. In other words, it is the characteristic function of the zero numbers. \begin{code} sgbar = ((<>) ^) \end{code} Using |sgbar|, we can define |sg|, which is 0 at 0, and 1 elsewhere (the sign function, or the characteristic function of the non-zero numbers). \begin{code} sg = sgbar * sgbar \end{code} It may be clearer to write it |sg a = (<>) ^ (<>) ^ a|. Think of double negation. Using |sg| and |sgbar|, we can implement a form of boolean conditionals. | IF b=0 THEN a ELSE c | can be defined as | a*sg(b)+c*sgbar(b) |. In fact we have forms of definition by finite cases. \end{document}