> import Prelude hiding ((+),(*),(^))
> infixr 9 ^
> infixr 8 *
> infixr 7 +
calculus of exponents, alias laws of logarithms
> a ^ b = b a
> f * g = \ x -> (x ^ f) ^ g
> f + g = \ x -> (x ^ f) * (x ^ g)
> naught = \ x -> id
the last word in combinators
> cA = (+)
> cM = (*)
> cE = (^)
> cN = naught
their combinatorial completeness
> cC = (*) * (^) ^ (*)
> cB = (*) ^ cC -- = (^) * (*) ^ (*)
> cK = naught ^ cC -- = (^) * naught ^ (*)
> cI = evil ^ naught -- or (^) * (^) ^ (*)
> cW = ((^) + (^)) ^ cC -- = (^) * ((^) + (^)) ^ (*)
> evil = error"The unthinkable has occurred!" -- used for "anything"
note 1: ^, *, naught are complete for affine \-calculus.
2: ^, * are complete for linear \-calculus.
3: Assuming extensionality (or "exponentiality"?),
3.1 (+,0) and (*,1) are both monoids.
3.2 * distributes over (0,+) from left.
But we don't have eg. 0*a = 0 in general.
--------------------------------------------------------------
sequence versions (power series)
> infixr 9 $^
> infixr 8 $*
> infixr 7 $+
> ($^) :: [a] -> [a -> b] -> [b]
> ($*) :: [a -> b] -> [b -> c] -> [a -> c]
> ($+) :: [a -> b -> c] -> [a -> c -> d] -> [a -> b -> d]
> bang :: a -> [a]
> ($^) (a:as) (f:fs) = a ^ f : (as $^ fs)
> ($*) (a:as) (f:fs) = a * f : (as $* fs)
> ($+) (a:as) (f:fs) = a + f : (as $+ fs)
> bang a = a : bang a
cumulative product/composition, and cumulative sum
> cprod :: [a -> a] -> [a -> a]
> csum :: [a -> b -> b] -> [a -> b -> b]
> cprod (a:as) = id : bang a $* cprod as
> csum (a:as) = naught : bang a $+ csum as
--------------------------------------------------------------
detritus
cY = let sap = id ^ cW in (sap ^ (*)) * sap isn't typable.
For testing.
> ss = \ str -> str ++ "'"
> zz = "0"
> one = two ^ naught
> two = one + one
> three = two ^ one + one
> four = two ^ two
> sixteen = two ^ four
--------------------------------------------------------------
Origins.
Some similar arithmetical combinators (in reverse date order) are
defined by
. Burge,
Recursive Programming Techniques,
Addison Wesley 1975, sec 1.8,
. Stenlund,
Combinators, lambda-terms and proof theory,
D. Reidel 1972, sec 2.4,
. Rosenbloom,
Elements of mathematical logic,
Dover 1950, sec 3.4,
among other places. According to Stenlund, Fitch and his students
knew of the combinatorial completeness.)
Mine are not quite the same.
The argument order for `my' multiplication combinator (and hence
also the addition combinator) is the reverse of the others. With
the other, the multiplication combinator comes out the same as the
B combinator, the ordinary ("reverse"!) composition operator. This
has something `repulsive' (absto\3ende) about it, according to
Cantor (who had actually started off using it). One has,
repulsively enough:
> f . g = \ x -> (x ^ g) ^ f
`My' multiplication (which is based on "^" as reversed application)
corresponds to *forwards* composition, sometimes written with a
semicolon.
As for priority, `my' definitions for the arithmetical combinators
can be found in, extracted from, or read into Wittgenstein's
Tractatus (6.02, 6.241 and environs). Certainly the key idea that a
number is the exponent of an operation, surely more or less
Church's idea, is Wittgenstein's. But perhaps `my' definitions
should really be attributed to Cantor. Or anyone who has used in
practice exponential notation for iteration of functions.