Arithmetical combinators

    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

• (+,naught) forms a monoid.
• (*,one) forms a monoid, where one = tI
• a * (b + c) = a * b + a * c
• a * naught = naught

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

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.