|
| 1 | +--- Evolution of a Haskell/Frege programmer |
| 2 | +--- Doing everything with SKI combinators |
| 3 | +module examples.CombinatorEvolution |
| 4 | + inline (decode) |
| 5 | + where |
| 6 | + |
| 7 | +import frege.Prelude hiding (*>, pred, succ, zero, one) |
| 8 | + |
| 9 | +infixl 15 `*>` |
| 10 | +infixl 15 `:>` |
| 11 | + |
| 12 | +data Combinator = Fun { !f :: Combinator -> Combinator } | T | F |
| 13 | +instance Show Combinator where |
| 14 | + show (Fun{}) = "Fun" |
| 15 | + show T = "T" |
| 16 | + show F = "F" |
| 17 | + |
| 18 | +--- > Kab = a |
| 19 | +k = Fun (\a -> Fun (\b -> a)) |
| 20 | + |
| 21 | +--- > Ia = a |
| 22 | +i = Fun (\a -> a) |
| 23 | + |
| 24 | +--- > Sfgx = fx(gx) |
| 25 | +s = Fun (\f -> Fun (\g -> Fun (\x -> f *> x *> (g *> x)))) |
| 26 | + |
| 27 | +--- > a *> b |
| 28 | +--- is the 'Combinator' that results from applying _a_ to _b_ |
| 29 | +left *> right = case left of |
| 30 | + Fun f -> f right |
| 31 | + _ -> error ((show left) ++ " applied to " ++ show right) |
| 32 | + |
| 33 | +{-- |
| 34 | +
|
| 35 | + Because we don't want to write crazy expressions like |
| 36 | + |
| 37 | + > s *> (s *> (k *> s) *> (s *> (k *> k) *> (s *> (k *> s) *> (s *> (k *> (s *> i)) *> k)))) *> (k *> k) |
| 38 | + |
| 39 | + we devise a data type from which we can create any combinator we want. |
| 40 | + |
| 41 | + We also allow variables, yet those must all get eliminated before we generate actual code |
| 42 | + (as the calculus is finally variable free). |
| 43 | + |
| 44 | +-} |
| 45 | + |
| 46 | +data Expr = S | K | I | Var Char | App Expr Expr |
| 47 | +instance Show Expr where |
| 48 | + show S = "S" |
| 49 | + show K = "K" |
| 50 | + show I = "I" |
| 51 | + show (Var c) = display c |
| 52 | + show (App a b) = show a ++ showsub b |
| 53 | + showsub (x@App{}) = "(" ++ show x ++ ")" |
| 54 | + showsub x = show x |
| 55 | + |
| 56 | + |
| 57 | +(:>) = App |
| 58 | + |
| 59 | +gen S = s |
| 60 | +gen K = k |
| 61 | +gen I = i |
| 62 | +gen (App a b) = gen a *> gen b |
| 63 | +gen (Var c) = error ("Can't generate variable " ++ display c) |
| 64 | + |
| 65 | +{-- |
| 66 | + Elimination |
| 67 | + |
| 68 | + If we have a formula like |
| 69 | + |
| 70 | + > Bfgx = f(gx) |
| 71 | + |
| 72 | + we need to eliminate all variables from both sides to get a 'Combinator' |
| 73 | + that consists only of S, K and I |
| 74 | + |
| 75 | + For this we define alpha elimination as follows: |
| 76 | + |
| 77 | + The elimination of variable v from expression x is an expression y such |
| 78 | + that yv is equivalent to x. |
| 79 | + |
| 80 | + This can be done by applying the following rules: |
| 81 | + |
| 82 | + 1. If x does not contain v, the v-elimination of x is Kx (because Kxv = x) |
| 83 | + 2. If x is just v, the v-elimination is I (because Iv = v = x) |
| 84 | + 3. If x is of the form ev and e does not contain v, the v-elimination |
| 85 | + is just e (because ev = x) |
| 86 | + 4. Otherwise, x is of the form ab, and the v-elimination is Scd, where |
| 87 | + c is the v-elimination of a and d is the v-elimination of b (because |
| 88 | + Scdv = cv(dv) and cv = a and dv = b and a(b) = ab = x |
| 89 | + |
| 90 | + The variables are eliminated starting with the rightmost variable of |
| 91 | + the left hand side, until none are left. Note that this way, we can always |
| 92 | + apply rule 3 to the left hand side, and when the right hand side did not |
| 93 | + contain any free variables, we will get a variable-free expression. |
| 94 | + |
| 95 | + Here is the elimination of the B combinator in detail: |
| 96 | + |
| 97 | + > Bfgx = f(gx) -- for x apply rule 4, then 1 on f and 3 on gx |
| 98 | + > Bfg = S(Kf)g -- for g apply rule 3 |
| 99 | + > Bf = S(Kf) -- for f apply rule 4, then 1 on S and 3 on Kf |
| 100 | + > B = S(KS)K |
| 101 | +-} |
| 102 | +v `elim` x |
| 103 | + | not (x `contains` v) = K :> x -- rule 1 |
| 104 | + | Var c <- x, c == v = I -- rule 2 |
| 105 | + | App e (Var c) <- x, |
| 106 | + c == v, |
| 107 | + not (e `contains` v) = e -- rule 3 |
| 108 | + | App a b <- x = S :> (v `elim` a) :> (v `elim` b) -- rule 4 |
| 109 | + | otherwise = undefined -- cannot happen, rules 1&2 |
| 110 | + -- already eliminate S, K, I and Var |
| 111 | + where |
| 112 | + Var c `contains` a = c == a |
| 113 | + App x y `contains` a = x `contains` a || y `contains` a |
| 114 | + _ `contains` a = false |
| 115 | + |
| 116 | +--- eliminate all given variables from an expression |
| 117 | +--- Use like |
| 118 | +--- > make (Var 'f' :> Var 'b' :> Var 'a') "fab" |
| 119 | +make ∷ Expr → String → Expr |
| 120 | +make x = foldr elim x . _.toList |
| 121 | + |
| 122 | + |
| 123 | +--- > Vabf = f a b |
| 124 | +--- > V = S(S(KS)(S(KK)(S(KS)(S(K(SI))K))))(KK) |
| 125 | +{-- |
| 126 | + This 'Combinator' is used to construct numbers. |
| 127 | + |
| 128 | + A number is a 'Combinator' with the following properties: |
| 129 | + - Let _n_ be a number. Then _n_ '*>' 'k' is 'k' if and only if _n_ |
| 130 | + represents 0. Otherwise, the result is 'k' '*>' 'i'. |
| 131 | + - Let _n_ be a number that is not 0. Then _n_ '*>' ('k' *> 'i') is the |
| 132 | + predecessor of _n_. |
| 133 | + |
| 134 | + The encoding for 0 is |
| 135 | + > v *> k *> k |
| 136 | + The successor function is |
| 137 | + > v *> (k *> i) |
| 138 | + and all numbers that have a predecessor _p_ are encoded as |
| 139 | + > v *> (k *> i) *> p |
| 140 | +-} |
| 141 | +xV = make (Var 'f' :> Var 'a' :> Var 'b') "abf" |
| 142 | +v = gen xV |
| 143 | + |
| 144 | +--- The number 0. See also 'xV' |
| 145 | +x0 = xV :> K :> K |
| 146 | +zero = gen x0 |
| 147 | + |
| 148 | +--- The successor of some number, see also 'xV' and 'x0' |
| 149 | +xN = xV :> (K :> I) |
| 150 | +succ = gen xN |
| 151 | + |
| 152 | +---- Null test. |
| 153 | +--- > Z n f g = n K f g |
| 154 | +--- > Z = SI(KK) |
| 155 | +--- will be _f_ if and only if _n_ is 0, otherwise _g_ |
| 156 | +xZ = S :> I :> (K :> K) |
| 157 | +ifnull = gen xZ |
| 158 | + |
| 159 | +--- Predecessor of a number, or 'zero' if it has none |
| 160 | +--- > pred n = ifnull *> n *> zero *> (n *> ki) |
| 161 | +--- > pred = S(S(SI(KK))(K(VKK)))(SI(K(KI))) |
| 162 | +xP = make (xZ :> Var 'n' :> x0 :> (Var 'n' :> (K :> I))) "n" |
| 163 | +pred = gen xP |
| 164 | + |
| 165 | +--- The @U@ combinator, aka Turing bird |
| 166 | +--- > Uuf = f(uuf) |
| 167 | +--- > U = S(K(SI))(SII) |
| 168 | +xU = S :> (K :> (S :> I)) :> (S :> I :> I) |
| 169 | + |
| 170 | +--- The @Y@ combinator, provides recursion |
| 171 | +--- > Yf = f(Yf) |
| 172 | +--- > Y = UU |
| 173 | +xY = xU :> xU |
| 174 | + |
| 175 | +x1 = xN :> x0 |
| 176 | +x6 = xN :> (xN :> (xN :> (xN :> (xN :> (xN :> x0))))) |
| 177 | + |
| 178 | +{--- |
| 179 | + Addition is a primitive recursive function, like this: |
| 180 | + |
| 181 | + > add a b = if a==0 then b else add (pred a) (succ b) |
| 182 | + |
| 183 | + Since there is no direct recursion, we need an extra argument for the recursion: |
| 184 | + |
| 185 | + > add' r a b = if a==0 then b else r (pred a) (succ b) |
| 186 | + > add = Y add' |
| 187 | +-} |
| 188 | +xA = xY :> make (xZ :> Var 'a' :> Var 'b' :> (Var 'r' :> (xP :> Var 'a') :> (xN :> Var 'b'))) "rab" |
| 189 | + |
| 190 | +{-- |
| 191 | + Even scarier is multiplication. We use the formula |
| 192 | + |
| 193 | + mul r a b = if a == 0 then 0 else if pred a == 0 then b else b + mul (pred a) b |
| 194 | +-} |
| 195 | +xT = xY :> make (xZ :> Var 'a' |
| 196 | + :> x0 |
| 197 | + :> (xZ :> (xP :> Var 'a') |
| 198 | + :> Var 'b' |
| 199 | + :> (xA :> Var 'b' :> (Var 'r' :> (xP :> Var 'a') :> Var 'b')))) |
| 200 | + "rab" |
| 201 | + |
| 202 | +{-- |
| 203 | + Now the fac! |
| 204 | + |
| 205 | + F r n = if n == 0 then 1 else n * r (pred n) |
| 206 | +--} |
| 207 | +xF = xY :> make (xZ :> Var 'n' |
| 208 | + :> x1 |
| 209 | + :> (xT :> Var 'n' :> (Var 'r' :> (xP :> Var 'n')))) "rn" |
| 210 | + |
| 211 | +{-- |
| 212 | + Tries to apply first 'T' and then 'F' to a 'Combinator'. |
| 213 | + If the result is 'Just' 'T', the 'Combinator' was 'k', |
| 214 | + if it is 'Just' 'F', the 'Combinator' was 'k' '*>' 'i' |
| 215 | + and if it is 'Nothing' or 'Just' 'Fun', the 'Combinator' was something else. |
| 216 | + If the answer is 'Just' 'Fun', we had a 'Combinator' that took more than 2 arguments, |
| 217 | + such as 's' or 'v'. |
| 218 | + |
| 219 | + This is a meta function to look inside the calculus. |
| 220 | +-} |
| 221 | +tell (x@Fun{}) = case x *> T of |
| 222 | + y@Fun{} -> Just (y *> F) |
| 223 | + _ -> Nothing |
| 224 | +tell _ = Nothing |
| 225 | + |
| 226 | +--- fold a numeric combinator |
| 227 | +--- This should return 'Nothing' if the combinator is not numeric |
| 228 | +--- Otherwise, it replaces 'zero' with the accumulator and applies the given function for every 'succ' |
| 229 | +--- > foldv (1+) 0 c -- decodes a numeric combinator |
| 230 | +--- > foldv (true:) [] (succ *> (succ *> zero)) == Just [true, true] |
| 231 | +foldv :: (a -> a) -> a -> Combinator -> Maybe a |
| 232 | +foldv f !a comb = case tell (ifnull *> comb) of |
| 233 | + Just T -> Just a |
| 234 | + Just F -> foldv f (f a) (pred *> comb) |
| 235 | + _ -> Nothing |
| 236 | + |
| 237 | +--- decode a numeric 'Combinator' |
| 238 | +--- This is a meta function to look inside the calculus. |
| 239 | +decode :: Combinator -> Maybe Integer |
| 240 | +decode = foldv (1+) 0 |
| 241 | + |
| 242 | +--- Encode an 'Integral' number as a 'Combinator' expression |
| 243 | +encode :: Integer -> Combinator |
| 244 | +encode 0 = zero |
| 245 | +encode n = succ *> encode (n-1) |
| 246 | + |
| 247 | + |
| 248 | +main [arg] = case arg.integer of |
| 249 | + Left _ -> stderr.println "usage: java -Xss100m examples.CombinatorEvolution number # give plenty of stack space!" |
| 250 | + Right n -> println . decode . (gen xF *>) . encode $ n |
| 251 | +main _ = do |
| 252 | + println ("The combinator: " ++ show xF) |
| 253 | + print "6! is " |
| 254 | + println . decode . gen $ (xF :> x6) |
0 commit comments