> module Lambda(Cexp(Cvar,CombS,CombK,(:$)),Lexp(Lvar,Lapp,Labs),Bexp(Bvar,Bapp,Babs),tob,toc,tol,cons,app,listtol,eval,bittol,uniL,lkupL) where
> import Char
> import List

Variable Identifier

> type Id = String

A Combinatory Logic expression is either a variable, combinator S,
combinator K, or an application.

> data Cexp = Cvar Id | CombS | CombK | Cexp :$ Cexp deriving Eq

A Lambda expression is either a variable, an abstraction,
or an application.

> data Lexp = Lvar Id | Labs Id Lexp | Lapp Lexp Lexp

A Bruijn expression is either an integer, an abstraction,
or an application.

> data Bexp = Bvar Int | Babs Bexp | Bapp Bexp Bexp deriving Eq

Lambda terms are considered identical up to renaming of bound variables.
Renaming of a bound variable is called alpha conversion, and its transitive
closure is alpha equivalence. We implement this test for identity by
translation to de Bruijn form.

> instance Eq Lexp where
>   l1 == l2 = (tob l1) == (tob l2)

The class of Applicative expressions collects all the methods that
make sense on all of the above 3 types.

> class Aexp a where
>   app :: a -> a -> a

Does a variable occur freely in an expression?

>   freeIn :: Id -> a -> Bool

Substitute a term for all free occurances of a variable,
ignoring possible variable capture.

>   subst :: Id -> a -> a -> a

Reduce an expression to normal form.

>   eval :: a -> a

Translate an expression to Combinatory Logic.

>   toc :: a -> Cexp

Convert an expression to Lambda Calculus.

>   tol :: a -> Lexp

Convert an expression to de Bruijn form.

>   tob :: a -> Bexp

Size in bits of an expression, assuming no free variables

>   size :: a -> Int
>   size = length . encode

Encode an expression as a binary string.

>   encode :: a -> String
>   encode x = prebin x ""

Prefix a string with a binary-encoded expression.

>   prebin :: a -> String -> String

Interpret an expression as a list of binary strings.

>   bshow :: a -> String

Read an expression according to BNF Grammar
Exp = Abstraction
    | Atoms
Atoms = Atom
      | Atom Atoms
Atom = '(' Exp ')'
     | Identifier

>   readsExp, readsAbs, readsVar :: ReadS a
>   readsExp = readsAbs `unionP` (readsAtom `bindP` readsApps) where
>     readsAtom = readsVar `unionP` (readParen True readsExp)
>     readsApps x = (readsAtom `bindP` (\y -> readsApps (app x y))) `unionP`
>                       (unitP x) -- greedy parses first

>     unitP :: a -> ReadS a
>     unitP x = \r -> [(x,r)]

>     bindP :: ReadS a -> (a -> ReadS a) -> ReadS a
>     m `bindP` k = (\r -> [(y,t)| (x,s) <- m r, (y,t) <- k x s])

>     unionP :: ReadS a -> ReadS a -> ReadS a
>     p `unionP` q = (\r -> (p r) ++ (q r))

Infinite list of identifiers.

> tmpids = map (('x':) . show) [0..] -- needed both in ctol and btol

> instance Aexp Cexp where
>   app = (:$)

>   toc = id

>   freeIn var (CombS :$ CombK :$ _) = False
>   freeIn var (x :$ y) = freeIn var x || freeIn var y
>   freeIn var (Cvar v) = var==v
>   freeIn var _ = False

Variable free combinators have a simple and natural encoding.

>   prebin CombS s = '0':'0':s
>   prebin CombK s = '0':'1':s
>   prebin (x :$ y) s = '1': (prebin x (prebin y s))

Converting combinatory expressions to lambda form seems easy enough.
Just replace S by \x\y\z.xz(yz) and K by \x\y.x, right? But that's not
quite what we want, since we want to map normal forms to normal forms.
So S K K should map to \x.x. This requires doing a sort of inverse
bracket abstraction. Apply a term T to a temporary variable v and reduce it
to say, T'. Then T is equivalent to [v]T' and we continue until we're left
with K, K M, or S, all of which convert directly to normal form.

>   tol = ctol tmpids  where
>     ctol :: [Id] -> Cexp -> Lexp
>     ctol ids (Cvar id) = Lvar id
>     ctol ids CombK = lkupL "K"
>     ctol (id:ids) (CombK :$ x) = Labs id (ctol ids x)
>     ctol ids CombS = lkupL "S"
>     ctol (id:id2:ids) a@(CombS :$ x)
>       = etaabs id (etaabs id2 (ctol ids (eval (a :$ (Cvar id) :$ (Cvar id2)))))
>     ctol (id:ids) a@((CombS :$ x) :$ y)
>       = etaabs id (ctol ids (eval (a :$ (Cvar id))))
>     ctol ids (x :$ y) = (ctol ids x) `Lapp` (ctol ids y)

>     etaabs :: Id -> Lexp -> Lexp -- eta-smart lambda abstraction
>     etaabs id (x `Lapp` (Lvar v)) | v==id && not (id `freeIn` x) = x
>     etaabs id e = Labs id e

>   tob = tob . tol

>   subst var t x@(Cvar v) | var==v = t
>                          | otherwise = x
>   subst var t (x :$ y) = (subst var t x) :$ (subst var t y)
>   subst var t x = x

>   eval (x :$ y) = eval2 (eval x) (eval y) where
>     eval2 :: Cexp -> Cexp -> Cexp
>     eval2 (CombK :$ x) y = x
>     eval2 ((CombS :$ x) :$ y) z = eval2 (eval2 x z) (eval2 y z)
>     eval2 x y = x :$ y
>   eval x = x

>   bshow = bshow . tob

>   readsAbs r = []
                                                                                
>   readsVar r = [ (varKS id, s) | (id@(a:_), s) <- lex r, isAlphaNum a] where
>     varKS "S" = CombS
>     varKS "K" = CombK
>     varKS id = Cvar id

> instance Read Cexp where
>   readsPrec _ = readsExp

> instance Show Cexp where
>   showsPrec _ (Cvar id) = showString id
>   showsPrec _ CombS = showChar 'S'
>   showsPrec _ CombK = showChar 'K'
>   showsPrec p (t1 :$ t2) = showParen (p>0) (showsPrec 0 t1 .
>                                               showChar ' ' .
>                                               showsPrec 5 t2)

> instance Aexp Lexp where
>   app = Lapp

>   tol = id

>   freeIn var (x `Lapp` y) = freeIn var x || freeIn var y
>   freeIn var (Labs x e) = x /= var && freeIn var e
>   freeIn var (Lvar v) = var==v

>   prebin = prebin . tob

>   toc (Lvar id) = Cvar id
>   toc (Lapp x y) = (toc x) :$ (toc y)
>   toc (Labs x e) = abstract x (toc e) where
>     abstract :: Id -> Cexp -> Cexp
>     abstract v (CombS :$ CombK :$ _) = lkupC "SK"
>     abstract v e = if freeIn v e
>                    then occabstract v e
>                    else CombK :$ e where

>     occabstract :: Id -> Cexp -> Cexp
>     occabstract var (Cvar v) = lkupC "I"
>     occabstract var (e1 :$ (Cvar v)) | not (freeIn var e1) = e1
>     occabstract var (e1 :$ (e2 :$ e3)) | isconst e1 && isconst e2
>         = occabstract var (CombS :$ (abstract var e1) :$ e2 :$ e3)
>     occabstract var ((e1 :$ e2) :$ e3) | isconst e1 && isconst e3
>         = occabstract var (CombS :$ e1 :$ (abstract var e3) :$ e2)
>     occabstract var (e1 :$ e2)
>       = CombS :$ (abstract var e1) :$ (abstract var e2)

>     isconst :: Cexp -> Bool
>     isconst (CombS :$ CombK :$ _) = True
>     isconst (x :$ y) = isconst x && isconst y
>     isconst (Cvar v) = False
>     isconst _ = True

>   tob = ltob [] where
>     ltob ids (Lvar id) = Bvar n where Just n = (elemIndex id ids)
>     ltob ids (Lapp e1 e2) = Bapp (ltob ids e1) (ltob ids e2)
>     ltob ids (Labs x e) = Babs (ltob (x:ids) e)

>   subst var t x@(Lvar v) | var==v = t
>                          | otherwise = x
>   subst var t (Lapp x y) = Lapp (subst var t x) (subst var t y)
>   subst var t x@(Labs v e) | var==v = x
>                            | otherwise = Labs v (subst var t e)

>   eval = tol . eval . toc

>   bshow = bshow . tob

>   readsVar r = [ (Lvar id, s) | (id@(a:_), s) <- lex r, isAlphaNum a]
                                                                                
>   readsAbs r = [ (Labs x e, u) | ("^", s) <- lex r,
>                              (x@(a:_), t) <- lex s, a=='_' || isAlphaNum a,
>                                    (e, u) <- readsExp t]
                                                                                
> instance Read Lexp where
>   readsPrec _ = readsExp

> instance Show Lexp where
>   showsPrec _ (Lvar id) = showString id
>   showsPrec p (Labs x e) = showParen (p>0) (showChar '^' .
>                                             showString x .
>                                             showChar ' ' .
>                                             showsPrec 0 e)
>   showsPrec p (Lapp t1 t2) = showParen (p>1) (showsPrec 1 t1 .
>                                               showChar ' ' .
>                                               showsPrec 5 t2)

> instance Aexp Bexp where
>   app = Bapp

>   tob = id

>   freeIn var exp = False

>   subst var t x = x

>   eval = tob . eval . tol

>   prebin (Bvar 0) s = '1':'0':s
>   prebin (Bvar (i+1)) s = '1':(prebin (Bvar i) s)
>   prebin (Babs e) s = '0':'0':(prebin e s)
>   prebin (x `Bapp` y) s = '0':'1':(prebin x (prebin y s))

>   tol = btol [] tmpids where
>     btol ids pool (Bvar i) = Lvar (ids !! i)
>     btol ids pool (Bapp e1 e2) = Lapp (btol ids pool e1) (btol ids pool e2)
>     btol ids (id:pool) (Babs e) = Labs id (btol (id:ids) pool e)

>   toc = toc . tol

>   bshow (Babs (Babs (Bvar 0))) = "" -- empty
>   bshow (Babs ((Bvar 0) `Bapp` (Babs (Babs (Bvar 1))) `Bapp` y)) = '0':(bshow y)
>   bshow (Babs ((Bvar 0) `Bapp` (Babs (Babs (Bvar 0))) `Bapp` y)) = '1':(bshow y)
>   bshow (Babs ((Bvar 0) `Bapp` x `Bapp` y)) = "<"++(bshow x)++","++(bshow y)++">"
>   bshow x = '(': (shows x ")")

>   readsVar r = [ (Bvar (read id::Int), s)|(id@(a:_), s)<-lex r,isDigit a ]
>   readsAbs r = [ (Babs e, t) | ("^", s) <- lex r,
>                                  (e, t) <- readsExp s]


> instance Read Bexp where
>   readsPrec _ = readsExp

> instance Show Bexp where
>   showsPrec _ (Bvar i) = shows i
>   showsPrec p (Babs e) = showParen (p>0) (showChar '^' .
>                                           showsPrec 0 e)
>   showsPrec p (Bapp t1 t2) = showParen (p>1) (showsPrec 1 t1 .
>                                               showChar ' ' .
>                                               showsPrec 5 t2)

apply a lambda abstraction and beta-reduce assuming no variable capture

> appred :: Lexp -> Lexp -> Lexp
> appred (Labs id e) t = subst id t e

> infixl 9 `appred`

> type Environment a = [(Id,a)]
> type ChangeEnv a = Environment a -> Environment a
> type Parse a = String -> ChangeEnv a

> addC :: Parse Cexp
> addC s env = (name,cexp):env where
>   [(name, s2)] = lex s
>   [("=", s3)] = lex s2
>   cexp = foldr (\(name,exp) -> (subst name exp .)) id env (read s3 :: Cexp)

> ycurry = read "^f(^x x x)(^x f(x x))" :: Lexp

> addL :: Parse Lexp
> addL s env = (name,lexp''):env where
>   [(name, s2)] = lex s
>   [("=", s3)] = lex s2
>   lexp = read s3 :: Lexp
>   lexp' = if name `freeIn` lexp
>           then ycurry `appred` (Labs name lexp)
>           else lexp
>   lexp'' = foldr (\(name,exp) -> (subst name exp .)) id env lexp'
 
Bitstring functions -----------------------------------------------------

> cons :: Lexp -> Lexp -> Lexp
> cons x y = lkupL "cons" `appred` x `appred` y

> listtol :: [Lexp] -> Lexp
> listtol = foldr cons (lkupL "nil")

> bittol :: Char -> Lexp
> bittol '0' = lkupL "true"
> bittol '1' = lkupL "false"

> bitstol :: String -> Lexp
> bitstol = listtol . map bittol

AIT Prelude ----------------------------------------------------

> envC = foldl (flip addC) [] [
>   "SK = S K",
>   "I = S K K",
>   "Y = S S K(S(K(S S(S(S S K))))K)" -- Tromp's minimal fixpoint combinator
>   ]
> lkupC :: String -> Cexp
> lkupC s = exp where Just exp = lookup s envC

> envL = foldl (flip addL) [] [
>   "I = ^x x",
>   "K = ^x^y x",
>   "S = ^x^y^z x z(y z)",
>   "Ycurry = ^f(^x x x)(^x f(x x))", --standard fixpoint operator
>   "Yturing = (^z z z)(^z^f f(z z f))",--Turing's alternative
>   "Ytromp = (^x^y x y x)(^x(^k^y(k y)((^x^y x y x)y(k y)))(^y x))",--translates to Tromp's minimal fixpoint combinator
>   "true = ^x^y x",
>   "false = ^x^y y",
>   "cons = ^x^y^z z x y",
>   "nil = false",--allows for list processing as: list(^head^tail^x non-nil-code)(nil-code)
>   "null = ^z z(^x^x^x false)true",--tests if list is nil
>   "double = ^x x x",
>   "omega = double double",
>   "intC = ^cont^list list(^ifsk ifsk\
>   \  (^sklist sklist(^skbit cont(skbit S K)))\
>   \  (intC(^comb1 intC(^comb2 cont(comb1 comb2)))))",--binary CL interpreter
>   "uniC = intC I",--binary CL universal machine
>   "intL = ^cont^list list(^bit0^list1 list1(^bit1 bit0\
>   \  (intL(^exp bit1(cont(^args^arg exp(^z z arg args)))\
>   \                 (intL(^exp2 cont(^args exp args(exp2 args))))))\
>   \  (bit1(cont(^args args bit1))\
>   \       (^list2 intL(^var cont(^args var(args bit1)))list1))))",--binary LC interpreter
>   "uniL = intL double",--binary LC universal machine
>   "intC' = Ytromp(^intC^cont^list list(^ifsk ifsk\
>   \  (^sklist sklist(^skbit cont(skbit S K)))\
>   \  (intC(^comb1 intC(^comb2 cont(comb1 comb2))))))",
>   "uniC' = intC' I",--similar but optimized for bracket abstraction
>   "intL' = Ytromp(^intL^cont^list list(^bit0 bit0\
>   \  (^list1 list1(^bit1 intL(^exp bit1\
>   \          (cont(^args^arg exp(^b^r b arg(r args))))\
>   \          (intL(^exp2 cont(^args exp args(exp2 args)))))))\
>   \  (^list1(cont list1(Ytromp(^r^l l(^b b I r))list1)))))",
>   "uniL' = intL'(^x^y x y y)",--again optimized for bracket abstraction
>   "inc = ^list^z list(^lsb^list1^dummy z(^x^y lsb y x)(lsb I inc list1))(z true list)",--increment a binary number
>   "dec = ^list list(^lsb^list1 lsb(list1(^x^x^f^z z f(dec list1))false)(^z z true list1))",--decrement a binary number
>
>   "reducible' = ^app^list list(^a^list1 a(list1(^b b(app(^list2 app)(reducible' app))(reducible' a)))a)",
>   "reducible = reducible' false",
>   "update = ^cont^n^k^list list(^a^list1 list1(^b^list2 a(b(b)(b))(b(b)(b))))",
>   "skip = ^list list(^a^list1 list1(^b^list2 a(b(skip list2)(skip(skip list2)))(b list2(skip list1))))",
>   "substvar = ^cont^k^k'^exp^list list(^a^list1 a(a)(a))",
>   "subst = ^cont^k^exp^list list(^a a(^list1 list1(^b^list2 b(^z z b(^z z b(subst cont (dec k) exp list2)))(^z z a(^z z b(subst(subst cont k exp)k exp list2)))))(substvar cont k k exp))",
>   "appheadreduce = ^list(^a^list1 list1(^b^list2 b(subst I nil(update I nil nil(skip list2))list2)(^z z a(^z z b(appheadreduce list2)))))",
>   "headreduce = ^list(^a^list1 list1(^b b(^list2^z z b(^z z b(headreduce list2)))appheadreduce))",
>   "freeheadvar' = ^k^list list(^a^list1 a(list1(^b b(app(^list2 app)(reducible' app))(reducible' a)))a)",
>   "freeheadvar = freeheadvar' nil",
>
>   "readbits = ^list^len^z len(^a^b^c list(^bit^list1 readbits list1(dec len)(^x^y z(^z z bit x)y)))(z len list)",--read n bits from bitstream
>   "delimit = ^list^z list(^bit^list1 bit(z false list1)(delimit list1(^len^y readbits y len(^n^y z(inc n)y))))",--read delimited string from bitstream
>   "cat = ^x^y x(^b^r^y^z z b(cat r y))y",
>   "halfquine = ^x cat x x",
>   "church0 = ^f^x x",
>   "church1 = ^f^x f x",
>   "church2 = ^f^x f(f x)",
>   "church3 = ^f^x f(f(f x))",
>   "church8 = church3 church2",
>   "church9 = church2 church3",
>   "church16 = church2 church2 church2",
>   "prefix0 = ^x^z z true x",
>   "prefix8zeros = church8 prefix0",
>   "prefix16zeros = church16 prefix0",
>   "prefix42 = ^r^z z(^z z false(^z z false(^z z true(^z z false(^z z true false)))))r",
>   "reverse' = ^a^l l(^h^t^a reverse'(^z z h a)t)a",
>   "reverse = reverse' nil",
>   "stutter = ^l l(^h^t^n^z z h (^z z h (stutter t)))nil"
>   ]
> lkupL :: String -> Lexp
> lkupL s = exp where Just exp = lookup s envL

> ----------------------------------------------------------------------------

> uniL = bshow . eval . (lkupL "uniL" `app`) . bitstol
> uniC = bshow . eval . toc . (lkupL "uniC'" `app`) . bitstol
> bltol = encode (lkupL "uniL")
> bltoc = encode (lkupL "uniC")
> bctoc = encode (toc (lkupL "uniC'"))
> bctol = encode (toc (lkupL "uniL'"))

> type BitString = [Bool]
> data BitIO a = BitIO (BitString -> (a, BitString))
> instance Monad BitIO where
>    (BitIO m) >>= f = BitIO (\s -> case m s of
>                      (x, t) -> case f x of
>                          BitIO n -> n t)
>    return x   = BitIO (\s -> (x,s))

Lambda interpreter is designed according to
 interpret continuation lambda-expr-code-with-suffix
 = continuation (\args.lambda-expr) suffix
where the free variables in lambda-expr are bound with entries from
the args list.

(plain) kolmogorov complexity C(x) of a binary string x is
length of shortest program p such that luni p = x

prefix kolmogorov complexity K(x) of a binary string x is
length of shortest program p such that luni (p++z) = cons x z

example executions of lambda universal machine:

uniL (x++x) where x = encode (lkupL "halfquine")
-> "0001010100011010000100000001011100000000001011011110010111111110111011010011010101000010101000110100001000000010111000000000010110111100101111111101110110100110101010"

uniL (bltoc++bctol++bltoc++"11000101")
-> ""

uniL ((encode (lkupL "delimit"))++"1111001001010")
-> "<11010,>"

shows that KP(42) = KP("11010") <= 450 + 14
of course, KP(42) <= 91 by the shorter program (lkupL "prefix42")

Command line use--------------------------------------------------------------

import Lambda
import System

chartol :: Char -> Lexp
chartol = inttol . fromEnum

inttol :: Int -> Lexp
inttol n | 0 == n = lkupL "nil"
         | odd  n = cons (lkupL "true") (inttol ((n-1) `div` 2))
         | even n = cons (lkupL "false") (inttol ((n-2) `div` 2))

ltochars :: Lexp -> String
ltochars = btochars . tob

btochars :: Bexp -> String
btochars (Babs (Babs (Bvar 0))) = "" -- empty
btochars (Babs ((Bvar 0) `Bapp` x `Bapp` y)) = (btochar x):(btochars y)

btochar :: Bexp -> Char
btochar = toEnum . btoint

btoint :: Bexp -> Int
btoint (Babs (Babs (Bvar 0))) = 0
btoint (Babs ((Bvar 0) `Bapp` x `Bapp` y)) = 2*(btoint y) + 1 + (btobit x)

btobit :: Bexp -> Int
btobit (Babs (Babs (Bvar n))) = 1-n

main :: IO ()
main = do [program] <- getArgs
          interact (\input ->
            ltochars (eval (lkupL "uniL" `app` (listtol
              ((map bittol program) ++ (map chartol input))))))

this appends standard input, converted to a list of integers in the
range [0..255], to the list of bits provided as single commandline argument
and runs the universal lambda computer on that, parsing the result as
another list of integers which goes to standard output.

example using "reverse":

a.out 0101000110100001000000010110000000010111111100001011011110110110110011010000010
hello, world!
 
!dlrow ,olleh

example using "stutter":

a.out 010001101000010000010110000000000101101111000010110111110011111111011110000010011010
hello, world!
-> hheelllloo,,  wwoorrlldd!!