import Char(isSpace,isAlpha)

--Def: Lambda Term

data Variable = Var Char deriving(Eq)

data LambdaTerm = VT Variable
                | FuncAbs Variable LambdaTerm
                | FuncApp LambdaTerm LambdaTerm
                  deriving(Eq)

--show and read

instance Show Variable where
    showsPrec _ (Var c) = (c:)

instance Show LambdaTerm where
    showsPrec _ (VT var) = showsPrec 0 var
    showsPrec _ (FuncAbs var term) = ("(/"++) . showsPrec 0 var . ('.':) . showsPrec 0 term . (')':)
    showsPrec _ (FuncApp t0 t1) = ('(':) . showsPrec 0 t0 . showsPrec 0 t1 . (')':)

instance Read Variable where
    readsPrec _ [] = []
    readsPrec _ s = if isAlpha c then [(Var c,l)] else []
        where (c:l) = dropWhile isSpace s

instance Read LambdaTerm where
    readsPrec _ s = [(VT var,q) | (var,q) <- reads s]
                    ++
                    [(FuncAbs var term,q) |
                     ("(",l00) <- lex s,
                     ("/",l01) <- lex l00,
                     (var,l1) <- reads l01,
                     (".",l2) <- lex l1,
                     (term,l3) <- reads l2,
                     (")",q) <- lex l3]
                    ++
                    [(FuncApp t0 t1,q) |
                     ("(",l0) <- lex s,
                     (t0,l1) <- reads l0,
                     (t1,l2) <- reads l1,
                     (")",q) <- lex l2]


--for only reading omit format of lambda-term

data LambdaTermOmit = VTOmit Variable
                    | FuncAbsOmit [Variable] [LambdaTermOmit]
                    | FuncAppOmit [LambdaTermOmit]

instance Read LambdaTermOmit where
    readsPrec _ s = [(VTOmit x,q) | (x,q) <- reads s]
                    ++
                    [(FuncAbsOmit (x:xs) (t:ts),q) |
                     ("(",l0)  <- lex s,
                     ("/",l1)  <- lex l0,
                     (x,l2)    <- reads l1,  --needs at least one parameter
                     (xs,l3)   <- readlv l2,  --terminated by "."
                     (t,l4)    <- reads l3,
                     (ts,q)    <- readlt l4]  --terminated by ")"
                    ++
                    [(FuncAppOmit (x:y:xs),q) |
                     ("(",l0) <- lex s,
                     (x,l1)   <- reads l0,
                     (y,l2)   <- reads l1,
                     (xs,q)   <- readlt l2] --terminated by ")"
                    ++
                    [(lto,q) | 
                     ("(",l0)   <- lex s,
                     (lto,l1)   <- reads l0,
                     (")",q)    <- lex l1]
        where readlv s = [([],q)   | (".",q)<- lex s] ++
                         [(x:xs,q) | (x,l)  <- reads s,
                                     (xs,q) <- readlv l]
              readlt :: String -> [([LambdaTermOmit],String)]
              readlt s = [([],q)   | (")",q)<- lex s] ++
                         [(x:xs,q) | (x,l)  <- reads s,
                                     (xs,q) <- readlt l]

validLTomit :: LambdaTermOmit -> Bool
validLTomit (VTOmit var) = True
validLTomit (FuncAbsOmit vs l) = (and (map validLTomit l)) && unique vs
    where unique (x:xs) = (not(x `elem` xs)) && (unique xs)
          unique [] = True
validLTomit (FuncAppOmit p) = (and (map validLTomit p))


canonicalize :: LambdaTermOmit -> LambdaTerm
canonicalize (VTOmit var) = (VT var)
canonicalize (FuncAbsOmit (x:xs) ts) = (FuncAbs (x) (canonicalize(FuncAbsOmit xs ts))) 
canonicalize (FuncAbsOmit [] ts) = (canonicalize (FuncAppOmit ts))
--left associate
canonicalize (FuncAppOmit [x,y]) = FuncApp (canonicalize x) (canonicalize y)
canonicalize (FuncAppOmit []) = error "never come"
canonicalize (FuncAppOmit l) = canonicalize(la l)
    where la (x:y:xs) = la ((FuncAppOmit [x,y]):xs)
          la [x] = x


readLambdaTerm :: String -> LambdaTerm
readLambdaTerm s = if validLTomit o then canonicalize o else error "invalid FunctionalAbstruction"
    where o :: LambdaTermOmit
          o = read ("("++s++")")

--Def: FV (free variable), closed term

fv :: LambdaTerm -> [Variable]
fv (VT var) = [var]
fv (FuncApp t0 t1) = (fv t0)++(fv t1)
fv (FuncAbs x t) = filter (x/=) (fv t)

isClosedTerm t = (fv t)==[]

--Def: Leftmost Reduction

isBetaNormalForm :: LambdaTerm -> Bool
isBetaNormalForm (VT var) = True
isBetaNormalForm (FuncAbs x t) = False
isBetaNormalForm (FuncApp p q) = (isBetaNormalForm p) && (isBetaNormalForm q)


--betaRedexReduction :: FuncApp (FuncAbs Variable LambdaTerm) LambdaTerm -> LambdaTerm
betaRedexReduction :: LambdaTerm -> LambdaTerm
betaRedexReduction (FuncApp (FuncAbs x t) s) = replaceLT t x s
betaRedexReduction o = error "bad argument"

replaceLT :: LambdaTerm -> Variable -> LambdaTerm -> LambdaTerm
replaceLT s@(VT var) from to = if var==from then to else s
replaceLT (FuncAbs x t) from to = (FuncAbs x (if x==from then t else (replaceLT t from to))) --guards
replaceLT (FuncApp p q) from to = (FuncApp (replaceLT p from to) (replaceLT q from to))

leftmostReduction :: LambdaTerm -> LambdaTerm
leftmostReduction (VT var) = (VT var)
leftmostReduction (FuncAbs x t) = error "dont have beta-nf"
leftmostReduction b@(FuncApp (FuncAbs x t) s) = betaRedexReduction b
leftmostReduction a@(FuncApp p q) | haslambda p = FuncApp (leftmostReduction p) q
                                  | haslambda q = FuncApp p (leftmostReduction q)
                                  | otherwise = a
    where haslambda (VT var)=False
          haslambda (FuncAbs x t)=False
          haslambda (FuncApp (FuncAbs x t) q)=True
          haslambda (FuncApp p q) = (haslambda p) || (haslambda q)


associateFreeVariable :: LambdaTerm -> [(Variable,LambdaTerm)] -> LambdaTerm
associateFreeVariable t [] = t
associateFreeVariable t (y:ys)= associateFreeVariable (FuncApp (FuncAbs v t) l) ys
    where (v,l) = y


--main

readLT = readLambdaTerm
lmr = leftmostReduction
afv = associateFreeVariable

lmrloop l = if isBetaNormalForm l then l else lmrloop (lmr l)

lmrloopprint l = do
                 putStrLn(show(l))
                 if isBetaNormalForm l 
                    then return()
                    else lmrloopprint (lmr l)

main :: IO()
main = do
       lmrloopprint skkx
--       lmrloopprint ym
    where k = readLT "(/xy.x)"
          s = readLT "(/xyz.xz(yz))"
          skk = readLT "skk"
          skkx = FuncApp (afv skk [(Var 's',s),(Var 'k',k)]) (VT (Var 'x'))
          ym = readLT "(/y.(/x.y(xx))(/x.y(xx)))m"

らぶHaskell。これC++で書く気になれないなぁ。

lexのあやしい構文を使う時、haskell-modeが邪魔だ。

一応本に忠実。\lambdaのかわりに"/"、省略記法対応。 mainではSKKxを最左変換(leftmost reduction)してxがでてくる。

*Main> main
(((/k.((/s.((sk)k))(/x.(/y.(/z.((xz)(yz)))))))(/x.(/y.x)))x)
(((/s.((s(/x.(/y.x)))(/x.(/y.x))))(/x.(/y.(/z.((xz)(yz))))))x)
((((/x.(/y.(/z.((xz)(yz)))))(/x.(/y.x)))(/x.(/y.x)))x)
(((/y.(/z.(((/x.(/y.x))z)(yz))))(/x.(/y.x)))x)
((/z.(((/x.(/y.x))z)((/x.(/y.x))z)))x)
(((/x.(/y.x))x)((/x.(/y.x))x))
((/y.x)((/x.(/y.x))x))
x

haskellの本それなりにまとまってるんだけど、標準ライブラリについてはあまり書いてない。 Prelude他のソースはかなり参考になる。

最近やっとboost本を買った。どうせリファレンスならもっとでかくてもよかったと思ったが、リファレンスではないのか。

Python入門(O'Reilly)つうのも入手した。でも1/3ほど読んでpythonへの熱はさめた。

学校を出よう(6)が熱い。ハルヒのほうが売れてるみたいだけど。