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 calculationThe following laws are satisfied by the additive and multiplicative combinators, when equality is interpreted as beta-eta equality:
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) = bIn 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.