----------------------------------------------------------------------------- -- -- This file contains the original source code for my entry, which was -- written in the lambda calculus using a slightly extended syntax -- compared to that accepted by my entry (in particular, it has -- multi-character identifiers and uses ` instead of \ because that's -- easier to enter inside a Haskell string). It also contains the Haskell -- code I used to translate the lambda calculus into combinators using -- the fully optimising algorithm described in the .hint file. -- -- Tony Finch -- ----------------------------------------------------------------------------- -- -- Source code for my entry -- unit = `val`k(k val) = CI bind = `op`fop`k(op `res(fop res k)) = (CC B B C) revacc = Y `f(`acc`list(list `nil(acc) `head`tail(f tail (pair head acc)))) rev = revacc I fold = `atomf`pairf(Y `rec(`list(list atomf (pairf rec)))) = (B (B Y) (BB B C CI)) pair = `x`y`f`g( f x y ) atom = `a`f`g( g a ) ore = `a`b`c(a c K (b c)) = (SS (CI K)) gns = Y `f(bind G `c(ore sp (ore nl ht) c f (C I c))) pr = Y `f`e(e `x`y(bind (P ob) `i(bind (f x) `i(bind (f y) `i(P cb)))) `a(P a)) trans = Y `f(bind gns `c( lm c (lambda f) ob c (brac f) cb c (unit (atom sp)) ef c (unit (atom sp)) (unit (atom c)) )) brac = `f(bind f (Y `l`ea(bind f `eb(eb `x`y(l (pair ea eb)) `a(a sp (unit ea) (l (pair ea eb))))))) lam = `f(bind gns `v(bind f `e(unit (abstract v e)))) abs = Y `r`v`e(e `x`y(optimise (r v x) (r v y)) `a(a v (atom i) (pair (atom k) (atom a)) )) make = `x`y(pair (pair (atom s) x) y) unopt = `a`b(pair (pair (atom s) a) b) opt = `x(x `xx`xy(xx `xxx`xxy(make x) `xxa(xxa k `y(y `yx`yy(yx `yxx`yxy(make x y) `yxa(yxa k (pair (atom k) (pair xy yy)) (make x y))) `ya(ya i xy (make x y))) (make x))) `xa(make x)) (Y `f(bind (bind trans pr) `i(f i)) I) ----------------------------------------------------------------------------- -- -- Haskell lambda and combinator utilities -- infixl 9 :@: data Expr = Expr :@: Expr | Lambda String Expr | Var String | Y | I | J | K | S | C | B | SS | CC | BB | P | G | E Int deriving (Eq, Read, Show) data EType = EFun | EArg | ELam deriving Eq isGraph c = c >= '!' && c <= '~' isToken c = isAlphanum c || '_' == c disp e = display ELam e "" exec e = do e' <- execute (compile (fst (parse e))) putStr (disp e') comp = disp . compile . fst . parse simp = disp . simplify . fst . parse -- turn String into Expr parse (a : as) | isSpace a = parse as | a == '`' = let (var, bs) = span isToken (dropWhile isSpace as) (expr, cs) = parse bs in (Lambda var expr, cs) | a == '(' = let (left, bs) = parse as fun left (c : cs) | isSpace c = fun left cs | c == ')' = (left, cs) | otherwise = let (right, ds) = parse (c:cs) in fun (left :@: right) ds in fun left bs | a == '\'' = case as of c:cs -> (E (ord c), cs) [] -> (E (-1), []) | isDigit a = let (bs, cs) = span isDigit as n = read (a:bs) in (E n, cs) | a == '-' = let (bs, cs) = span isDigit as n = read (if bs == "" then "1" else bs) in (E (-n), cs) | isToken a = let (bs, cs) = span isToken as in (case a:bs of "Y" -> Y; "I" -> I; "J" -> J; "K" -> K; "S" -> S; "C" -> C; "B" -> B "SS" -> SS; "CC" -> CC; "BB" -> BB; "P" -> P; "G" -> G; x -> Var x , cs) -- pretty printer display t (Lambda v e) = showChar '`' . showString v . display ELam e display t (a :@: b) = showParen (t /= EFun) (display EFun a . showChar ' ' . display EArg b) display t (Var v) = showParen (t == ELam) (showString v) display t (E n) = let c = chr n in if isGraph c then showChar '\'' . showChar c else shows n display t e = showParen (t == ELam) (shows e) -- translate into optimised combinators compile (a :@: b) = compile a :@: compile b compile (Lambda var e) = abstract var (compile e) compile e = e abstract v (a :@: b) = optimise (abstract v a) (abstract v b) abstract v e | e == Var v = I | otherwise = K :@: e optimise (K :@: p) I = p optimise (K :@: p) (K :@: r) = K :@: ( p :@: r ) optimise (K :@: p) (B :@: r :@: s) = BB :@: p :@: r :@: s optimise (K :@: p) r = B :@: p :@: r optimise (B :@: p :@: q) (K :@: r) = CC :@: p :@: q :@: r optimise p (K :@: r) = C :@: p :@: r optimise (B :@: p :@: q) r = SS :@: p :@: q :@: r optimise p r = S :@: p :@: r -- do combinator reduction execute ( Y :@: f) = let g = f :@: g in execute g execute ( I :@: f ) = execute f execute ( J :@: f :@: g) = execute g execute ( K :@: f :@: g ) = execute f execute ( S :@: f :@: g :@: x) = execute ((f :@: x) :@: (g :@: x)) execute ( C :@: f :@: g :@: x ) = execute ((f :@: x) :@: g) execute ( B :@: f :@: g :@: x ) = execute (f :@: (g :@: x)) execute (SS :@: c :@: f :@: g :@: x) = execute (c :@: (f :@: x) :@: (g :@: x)) execute (CC :@: c :@: f :@: g :@: x ) = execute (c :@: (f :@: x) :@: g) execute (BB :@: c :@: f :@: g :@: x ) = execute (c :@: (f :@: (g :@: x))) execute (G :@: f) = do c <- getChar execute (f :@: E (ord c)) execute (P :@: f :@: g) = do f' <- execute f case f' of E n -> do putChar (chr n) execute (I :@: g) _ -> return (f' :@: g) execute (E n :@: f) = do f' <- execute f case f' of E m -> if n == m then return K else return J _ -> return (E n :@: f') execute (f :@: g) = do f' <- execute f if f' == f then return (f' :@: g) else execute (f' :@: g) execute e = return e -- translate into lambda calculus and do beta reduction simplify I = fst (parse " `f f ") simplify J = fst (parse " `f`g g ") simplify K = fst (parse " `f`g f ") simplify S = fst (parse " `f`g`x ((f x) (g x)) ") simplify C = fst (parse " `f`g`x ((f x) g) ") simplify B = fst (parse " `f`g`x (f (g x)) ") simplify CC = fst (parse " `c`f`g`x (c (f x) g) ") simplify SS = fst (parse " `c`f`g`x (c (f x) (g x)) ") simplify BB = fst (parse " `c`f`g`x (c (f (g x))) ") simplify (Lambda v b) = Lambda v (simplify b) simplify (Lambda v b :@: a) = simplify (substitute v a b) simplify (a :@: b) = let a' = simplify a b' = simplify b in if a' == a then (a' :@: b') else simplify (a' :@: b') simplify x = x -- replace instances of variable v in body b with argument a, avoiding variable capture substitute v a b = let wf b = newvar (merge (vars a) (vars b)) subst (Var v') | v == v' = a | otherwise = Var v' subst (Lambda v' b) | v == v' = Lambda v' b | otherwise = let w = wf b in Lambda w (subst (substitute v' (Var w) b)) subst (b :@: c) = (subst b) :@: (subst c) subst x = x in subst b -- return a variable not in vs (which is sorted) newvar vs = let x `isin` [] = False x `isin` (y:ys) | x < y = False | x == y = True | otherwise = x `isin` ys try v = if v `isin` vs then try (next v) else v next (v:vs) = if v < 'z' then (succ v):vs else 'a':(next vs) next [] = "a" in try "a" -- get (sorted, unrepetitive) list of variables in an Expr vars (Lambda v b) = merge [v] (vars b) vars (a :@: b) = merge (vars a) (vars b) vars (Var v) = [v] vars _ = [] -- combine two sorted lists, omitting duplicates merge [] ys = ys merge xs [] = xs merge (x:xs) (y:ys) | x < y = x : merge (xs) (y:ys) | x == y = x : merge (xs) (ys) | otherwise = y : merge (x:xs) (ys)