--- The AMEN combinators and their reduction If one represents natural numbers by Church numerals, there are natural definitions of the arithmetic operators |(+)|, |(*)|, and |(^)| which make sense as definitions of general combinators. It turns out that these combinators are combinatorially complete. This was pointed out in print by B{\"o}hm, but may have been previously noticed by Fitch. In the arithmetical notation arising from this combinatory completeness, the symbol |(^)| for exponentiation becomes the transpose of the normal application operator (usually represented by juxtaposition). It becomes backwards application', which is sometimes used in algebra. The symbol |(*)| becomes the transpose of the normal composition |(.)| - ie. forwards composition' sometimes written with a semi-colon. The addition operator ia a pointwise lifted' version of |(*)|, and is sometimes useful. Interestingly, the fragment without the addition combinator characterises the linear lambda calculus. 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 (ie. playing around) with arithmetical' versions of standard combinators. The end of the file consists mostly of debris from such experiments. -- combinatorial completeness 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 |(^)|. Two 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. Instead, for zero, nought, or naught, I use the infix symbol |<>|', in the form |(<>)|. (It looks a little bit like an |0|'.) > module Main where > import Prelude hiding ((*),(^),(+)) > infixr 8 ^ > infixr 7 * > infixr 6 + The calculus of iterative exponents can be summarised in the following Haskell definitions. The second and third definitions arise very naturally in connection with exponential notation for the iterates of a function, while the fourth is only a little more recondite. The first can be regarded as introducing the exponential as an alternative notation for application, with the arguments flipped. > a ^ b = b a > a * b = \c -> (c ^ a) ^ b > a + b = \c -> (c ^ a) * (c ^ b) > a <> b = b An amusing phenomenon is that |(+),(*),(^),(<>)| are combinatorially complete. To convince oneself of this it is enough to define the BWICK' combinators. > combC = (*) * (^) ^ (*) -- called "flip" by fp'ers > combB = (^) * (*) ^ (*) -- (*) ^ combC, i.e. composition (.) > combI = evil ^ (<>) > combK = (^) * (<>) ^ (*) -- (<>) ^ combC > combW = (^) * ((^) + (^)) ^ (*) -- ((^) + (^)) ^ combC > evil = error"The unthinkable has occurred." You may like to see derivations of some of these. The key thing is to start with the |C| (argument swapping, or) transpose combinator. | 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 ^ (^))) So, | C a b | = { by the above, & extensionality } | a * (b ^ (^)) | = { def of (*) } | (b ^ (^)) ^ a ^ (*) | = { def of (*) } | b ^ ((^) * a ^ (*)) So, | C a | = { by the above, & extensionality } | (^) * a ^ (*) | = { def of (*) } | (a ^ (*)) ^ (^) ^ (*) | = { def of (*) } | a ^ ((*) * (^) ^ (*)) So | C = (*) * (^) ^ (*) |. 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 | B = (^) * (*) ^ (*) As for |K|, it is clear that it is the transpose of |(<>)|, that is |C (<>)| and therefore, just as for |B|, | K = (^) * (<>) ^ (*) As for |I|, it is the transpose of |(^)|, modulo extensionality. So we could take the following. | I = (^) * (^) ^ (*) But we can also take the following. | I = (<>) ^ (<>) As for |W|, first let's express its transpose |CW| | 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 ^ ((^) + (^)) So by extensionality |CW = (^) + (^)|. From this, as in the cases of |B| and |K|, we have | W = (^) * ((^) + (^)) ^ (*) This completes the derivation of the |BWICK| combinators. After a little familiarisation with these combinators, it becomes clear that another combinator plays a central role. This is |S'|, where |S a b| (the normal S combinator) | = |W (S' a b)|. | S' a b c1 c2 | = { def } | a c1 (b c2) So, | S' a b c1 | = {} | a c1 . b | = {} | b * a c1 So, | S' a b | = {} | (b *) . a | = {} | a * (b *) So, | S' a | = {} | (a *) . (*) | = {} | (*) * (a *) So, | S' | = {} | ((*) *) . (*) | = {} | (*) * ((*) *) In particular, we have: | S' = S' (*) | C = S' (^) | B = S' (^) (*) | I = S' (^) (^) | K = S' (^) 0 | W = S' (^) ((^) + (^)) This is at any rate pretty. If one uses the notation AMEN'' for addition, multiplication, exponentiation and naught, then not only does one have the last word in combinators, 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 an advanced form of eye disease, the ultimate in obfuscation. If I get round to it I will make a postcript picture of a large one. -- Origins The arithmetical combinators above are similar to, but not exactly the same as those defined by Burge (Recursive Programming Techniques, Addison-Wesley 1975, section 1.8), Stenlund (Combinators, lambda-terms and proof theory, Almqvist and Wiksell 1972, sec 2.4), or Rosenbloom (the elements of mathematical logic, Dover 1950 sec 3.4), among other places. Of these people, as far as I know, only Stenlund noticed the combinatorial completeness; others have of course defined them in connection with so-called Church numerals. These gentry have the wrong argument order. With their definitions, the multiplication combinator is the same as the |B| combinator. My definitions (at least for |*|) can be read into Wittgenstein's Tractatus (around 6.02 and 6.241). They also have also the authority of Cantor, who called the alternative repulsive' -- absto{\ss}ende -- having started off using it. (Potter, "Sets" Clarendon Press 1990, p 120.) In combinatory logic, the observation that they are complete is (according to Stendlund's book, p22) due to F. B. Fitch. (Maybe Fitch never published this observation -- Stenlund doesn't give an exact reference.) Or maybe the observation is in | [Fitch 1952] | Fredric Brenton Fitch, Symbolic Logic, the Ronald Press Company, New | York, 1952. But I haven't looked at it yet. PS: I was recently (summer 2001) told by Felice Cardone that B{\"o}hm (he of the trees) used arithmetical combinators as a basis for combinatory logic, with lambda interpreted as logarithm (better, $\lambda$ogarithm, as B{\"o}hm writes sometimes), for example in his papers: | @INCOLLECTION{bohm:1979, | author = "C. B{\"o}hm", | title = "Un mod{\e}le arithm{\'e}tique des termes de la logique | combinatoire", | BOOKTITLE="Lambda Calcul et S{\'e}mantique Formelle des Langages | de Programmation. | Actes de la Sixi{\e}me Ecole de Printemps d'Informatique | Theorique, La Ch{\^a}tre, 1978", | EDITOR="B. Robinet", | PUBLISHER="LITP et ENSTA", | ADDRESS="Paris", | YEAR = 1979, | PAGES = "97--108", | } | @INCOLLECTION{bohm:1980, | AUTHOR="C. B{\"o}hm", | TITLE="Logic and computers", | BOOKTITLE="Modern Logic --- A Survey", | EDITOR="E. Agazzi", | PUBLISHER={Reidel}, | ADDRESS="Dordrecht", | PAGES={297--309}, | YEAR={1980} | } I don't have access to a library at the moment, but look forward to finding these! -- algebra When equality is interpreted as extensional equality, . |(+,0)| forms a monoid. . |(*,1)| forms a monoid, where |1 = combI| . . |a * (b + c) = a * b + a * c| . . |a * 0 = 0| . . Addition and multiplication are not in general commutative. Intriguingly enough, The laws of |(+),0,(*),1| above (which do not mention exponentiation) coincide with the basic laws of the transfinite arithmetic or addition and multiplication, or indeed of the theory of general (not necessarily linear) orderings, well-founded or not. (However the coincidence is not exact. In the combinatory world, we don't have, among other things, |0 * a = 0|. This is because we don't have |1 ^ a = 1|.) If we think of "real" natural numbers, these also satisfy the following equations. These seem to characterise the "genuinely numerical" part of the model. | a + b = a ^ (+ 1) ^ b | a * b = 0 ^ (+ a) ^ b | a ^ b = 1 ^ (* a) ^ b -- logarithms 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. What (for example) is |log_x a x b c|, where |a|, |b|, |c| have no free occurrences of |x|? | log_x a x b c = log_x c ^ b ^ x ^ a | = log_x ((x ^ a) ^ (b^)) ^ (c^) | = a * (b^) * (c^) Any linear abstraction is a product (ie. a composite) of "factors" that each look like | a * (b1^) * ... * (bk^) A general abstraction (in which the "base" variable may have more than one occurrence) has the normal form | ((^) + ... + (^)) * (pie^) | where pie = Pi_i (ai * (bi1^) * .. * (bij^)) where there is a summand for each occurrence of the variable. There are many optimisations, such as | log_x (a * b) = (log_x a) + (log_x b) | log_x 1 = 0 These equations were once familiar to schoolchildren. -- subtraction, division, logarithm Dull would he be of soul who didn't wonder whether he couldn't define subtraction, division and logarithms such that | a + x .leq. b <=> x .leq. b - a | a * x .leq. b <=> x .leq. b / a | a ^ x .leq. b <=> x .leq. log_a b . Perhaps floor' and ceiling' are worth thinking about too. My wonderings (mainly about what .leq. might mean) have not been productive. Should one have gadgets like subtraction, division and logarithms, then one will surely have something like Cantor Normal form. This might be interesting. What might it mean to represent subtraction, division, and logarithms as syntactical operations? "Oleg" someone (I don't know his full name) has an interesting collection of web pages at | http://www.pobox.com/~oleg/ftp/ about these and other matters. One idea of Oleg's is to use fixed points. For example, | -a, 1/a, log_a b is a fixed point of | \x -> a + x*2, \x -> x * (a+1) - 1, \x->a ^ x + x - b respectively. He talks about least fixed points, but I think (integer, ie. cutoff) division and logarithms should (somehow) be greatest fixed points. But "oleg" has other ideas too. An interesting guy! -- Arithmetical calculus Here is a datatype for arithmetical expressions. The symbols for the constructors are chosen to suggest their interpretation as combinators. > infixr 8 :^: > infixr 7 :*: > infixr 6 :+: > data E = V String | E :^: E | E :*: E | E :+: E > deriving (Show,Eq) We can think of them as like Lisp S-expressions, but with three kinds of cons' operation. It is convenient to allow constants identified by arbitrary strings, so we can have constants besides zero. 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. > infixr 8 <^> > infixr 7 <*> > infixr 6 <+> > (<+>),(<*>),(<^>) :: 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 ^ (up2 (<+>) (<*> b1) (<*> b2)) > b1 :*: b2 -> a ^ ( (<*> b1) * (<*> b2) ) > _ :^: V "0" -> a > _ -> a :*: b > a <^> b = case b of > V "0" -> b :^: b > b1 :+: b2 -> a ^ (up2 (<*>) (<^> b1) (<^> 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 The following (partial!) function then evaluates an arithmetic expression. > eval a = case a of b1 :+: b2 -> eval b1 <+> eval b2 > b1 :*: b2 -> eval b1 <*> eval b2 > b1 :^: b2 -> eval b1 <^> eval b2 > _ -> a A variant. Does it give the same answers? > eval' a = case a of b1 :+: b2 -> b1 <+> eval' b2 > b1 :*: b2 -> b1 <*> eval' b2 > b1 :^: b2 -> b1 <^> eval' b2 > _ -> a A convenient abbreviation, used above for applying a binary function pointwise. For example |(+) = up2 (*)|. > up2 f a b c = (c ^ a) f (c ^ b) -- show function for expressions The parameter "p" below is precedence. I forget how to use it. > 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 Disable it. The default one is just as good. | > instance Show E where showsPrec p e = showE e 0 -- 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. Although the lists returned here are singletons, there can be overlap between rewriting rules. > redex :: E -> [E] > redex e = case e of > (a :+: (b :+: c)) -> [ (a :+: b) :+: c ] > (a :+: V "0") -> [ a ] > (a :*: (b :+: c)) -> [ (a :*: b) :+: (a :*: c) ] > (a :*: V "0") -> [ v0 ] > (a :*: (b :*: c)) -> [ (a :*: b) :*: c ] > (a :*: V "1") -> [ 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 To represent subexpressions, we use a clever idea of Mark Jones, Hugo Herberlin, or whoever. We represent each part |e| of an expression |e'| as a pair |(f,e)| consisting of the subexpression |e'| there, and a 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 socket' |f| to get back |e'|. > 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 ] Now we define for any expression the list of expressions to which it reduces in a single, possibly internal step. > reducts :: E -> [ E ] > reducts a = [ f a'' | (f,a') <- parts a, a'' <- redex a' ] We need a structure to hold the reduction sequences from an expression. So-called rose' trees seem to be ideal. > data Tree a = Node a [ Tree a ] We define a function which maps an expression to its tree of reduction sequences. > exec :: E -> Tree E > exec e = Node e [ exec e' | e' <- reducts e ] We use the branches in a tree to represent reduction sequences. > branches :: Tree a -> [[a]] > branches (Node a []) = [ [a] ] > branches (Node a ts) = [ a : b | t <- ts, b <- branches t] A function for displaying a tree, branch by branch. > 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) A function for displaying a list with numbers. > newtype NList a = NList [a] > instance Show a => Show (NList a) where > showsPrec p (NList es) = > (composelist . seplist ('\n':) . map showline . number ) es > where showline (n,e) = shows n . showString ". " . shows e -- Some expressions for playing with > 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 "Junk" -- evil"The unthinkable has happened" -- Rotation combinators The following combinator |cR| rotates' 3 arguments. | vc :^: vb :^: va :^: cR = va :^: vc :^: vb Such an operation is often provided by an instruction of a `stack machine', to rotate the top three enties on the stack. It so happens that the |C| combinator and the |cR| are definable from each other. | cR :^: cR :^: cR = cC | cC :^: cC = cR One upshot of this observation is that we have a way of churning out endless versions of the C combinator, aka |flip|. > flip', flip'' :: (a -> b -> c) -> b -> a -> c > flip' = flip flip (flip flip) (flip flip) > flip'' = flip' flip' (flip' flip') (flip' flip') We can write the rotation combinator as follows. > cR = cC :^: cC Some other versions > combR = (^) * (((*) * ((^)*))*) > combR' = (^) * (^) * ((*)*) > cR' = (V "^") :*: (V "^") :*: (V "*") :^: (V "*") -- Numbers. > naught = c0 > one = cI > two = one :+: one > three = two :+: one > four = two :^: two > five = two :+: three > six = two :*: three > seven = three :+: four > eight = two :^: three > nine = three :^: two > ten = two :*: five -- S combinator. The following combinator is useful for defining the S combinator, since |S a b = W (S' a b)| It has quite interesting properties: | S' (*) = S' |, | S' (^) = C |, and so on. > cS' = let x = V"*" in x :*: (x :^: x ) > cS = cS' :*: cW :^: cB > combS' = let x = (*) in x * (x ^ x) > combS = combS' * (*) * (combW ^) -- Y combinator. > cSap = V"^" :^: cW > cY = let x = cSap :^: V"*" in x :^: x :^: cS Although |(cI :^: cY)| runs in constant space (Hugs doesn't run out of stack or heap), matters are different with |(cI' :^: cY)|. -- Alternative W combinator I retain this for sentimental reasons, as it was the first definition I thought of, though clearly a very terrible one. > cW' = t1 :*: V "*" :*: t2 > where t1 = cK :^: V"+" > t2 = jnk :^: (V"^" :*: V"^") -- Some mildly interesting functions. > ct a = a :^: V "^" -- unit of continuation transform Question: what do the continuation transforms look like in arithmetic combinators? > line gradient x0 x = x0 :+: gradient :*: x The idea is to look at some schoolroom things like the equations of lines, polynomials, derivates, etc. > sgbar n = V "0" :^: n sgbar is the function which is 1 at 0, and 0 everywhere else. It can be used to define sg, which is 0 at 0, and 1 elsewhere by sg = sgbar . sgbar It is interesting because it is non-monotone on numerals, and somehow the source of all non-monotonicity. -- Some convenient things > va = V "a" > vb = V "b" > vc = V "c" > vd = V "d" > ve = V "e" > vf = V "f" > number :: [a] -> [(Int,a)] > number = zip [1..] > composelist :: [ a -> a ] -> a -> a > composelist = foldr (.) id > seplist :: a -> [a] -> [a] > seplist s (x:(xs'@(_:_))) = x:s:seplist s xs' > seplist s xs = xs First difference > 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" -- Testing and experimenting > help = "The tests are: test, number_rss, nth_rs" The first reduction sequence > test :: E -> NList E > test = NList . (nth_rs 0) The n'th reduction sequence. > nth_rs :: Int -> E -> [E] > nth_rs n = (!! n) . branches . exec The number of reduction sequences > number_rss :: E -> Int > number_rss = length . branches . exec -- Projections > p22 = cK > p21 = c0 > p33 = (cK :*: cK) :^: cK > p32 = cK :^: cK > p31 = c0 :^: cK > p44 = cK :*: cK :*: cK > p43 = (cK :*: cK) :^: cK > p42 = cK :^: (cK :*: cK) > p41 = c0 :^: (cK :*: cK) > p55 = cK :*: cK :*: cK :*: cK > p54 = (cK :*: cK :*: cK) :^: cK > p53 = (cK :*: cK) :^: (cK :*: cK) > p52 = cK :^: (cK :*: cK :*: cK) > p51 = c0 :^: (cK :*: cK :*: cK) Tests of projections > test5 p = test( ((V"a" :^: V"^") :*: > (V"b" :^: V"^") :*: > (V"c" :^: V"^") :*: > (V"d" :^: V"^") :*: > (V"e" :^: V"^")) > :^: (p :^: V"^") > ) > test4 p = test( ((V"a" :^: V"^") :*: > (V"b" :^: V"^") :*: > (V"c" :^: V"^") :*: > (V"d" :^: V"^")) > :^: (p :^: V"^") > ) > test3 p = test( ((V"a" :^: V"^") :*: > (V"b" :^: V"^") :*: > (V"c" :^: V"^")) > :^: (p :^: V"^") > ) > test2 p = test( ((V"a" :^: V"^") :*: > (V"b" :^: V"^")) > :^: (p :^: V"^") > ) -- Bureaucracy > main :: IO() > main = error"Meant for interpreter"