# Arithmetical combinators

The following is code for the functional programming language Haskell that redefines the combinators (+) (*) (^) and naught so as to satisfy the familiar laws of arithmetic exponents. (There is an actually runnable Haskell program here exploring some implementation related aspects which I have yet to merge with this file.)
```
infixr 8 ^                          -- the usual relative precedences
infixr 7 *
infixr 6 +

(^) :: a -> (a -> b) -> b           -- the types
(*) :: (a -> b) -> (b -> c) -> a -> c
(+) :: (a -> b -> c) -> (a -> c -> d) -> a -> b -> d
naught :: a -> b -> b

(a ^ b) = b a                       -- "backwards" application
(a * b) = \c -> (c ^ a) ^ b         -- cf Tractatus 6.241
(a + b) = \c -> (c ^ a) * (c ^ b)   -- only combinator to duplicate an arg
naught   = \s z -> z                -- cf Tractatus 6.02
```

Amusingly enough, these combinators turn out to be functionally complete, in the sense that one can define a bracket-abstraction algorithm which works both for untyped terms, and for Hindley-Milner terms. As the combinators represent addition, multiplication, exponentiation and naught, they cry out to be called the AMEN combinators -- surely the last word in combinators.

These arithmetical combinators are not quite the same as the ones defined by Burge (Recursive Programming Techniques, sec 1.8), Stenlund (Combinators, lambda-terms and proof theory, sec 2.4), or Rosenbloom (the elements of mathematical logic, Dover 1950 sec 3.4), among other places. The argument order for `my' addition and multiplication combinators is reversed from these other definitions. With the other definitions, the multiplication combinator comes out the same as the B combinator, and has something `repulsive' (absto\3ende) about it, in Cantor's opinion. The definitions above can be extracted from or read into Wittgenstein's Tractatus (6.02,6.241 and environs) if one is a little charitable.

We can prove combinatorial completeness by reducing the `BWICK' combinators to these.

```
evil      = error "can't happen"        -- used for "any term"

tC = (*) * (^) ^ (*)                    -- called "flip" by fp'ers
tB = (^) * (*) ^ (*)                    -- (*) ^ tC, i.e. composition (.)
tI = evil ^ naught
tK = (^) * naught ^ (*)                 -- naught ^ tC
tW = t1 * (*) * t2
where t1 = tK ^ (+)                -- :: (a -> a -> b) -> a -> c -> b
t2 = evil ^ ((^) * (^))      -- :: (((a -> b) -> b) -> c) -> c
-- W f a = f a a = (K + f) a evil = evil ^ (K + f) a
-- so, W f = (evil ^) . (K + f)
-- so, W   = ((evil ^) .) . (K +)
-- from which tW above was obtained by putting tB for (.), and calculation
```
The following laws are satisfied by the additive and multiplicative combinators, when equality is interpreted as beta-eta equality:
• (+,naught) forms a monoid.
• (*,one) forms a monoid, where one = tI
• a * (b + c) = a * b + a * c
• a * naught = naught
However, addition and multiplication are not commutative. The laws satisfied by all 4 combinators are uncannily (though not exactly) like those valid in transfinite arithmetic.

Logarithm is a kind of lambda abstraction, in the sense that it satisfies the following "beta law" (among a host of other equations familiar from elementary school).

```
x ^ (log_x b) = b
```
In view of this, various questions arises naturally of whether one can make any `sense' of division, subtraction, roots, power series, .. ?

Here is a rather old and disorganised ps file on the same subject of this note that may also be of interest. More distantly related is a note about variable binding.

Peter Hancock