Untyped Lambda Calculas

またまたHaskellで実装してみました。
変数名の衝突を避けるためにde Bruijn indiciesという方法を使ってます。
だいたい内側のラムダ抽象の引数から順に0,1,2...と番号をふる感じの方法です。
詳しいことは本で確認してもらえれば・・・。

{- Untyped Lambda Calculus -}

data Term = LVar Int
          | LAbs Term
          | LApp Term Term
          deriving (Eq)
                   
newtype Context = Context [String]
type Binding = String

showTerm (LVar x) = show x
showTerm (LAbs t) = "(lambda. " ++ (showTerm t) ++ ")"
showTerm (LApp t1 t2) = "(" ++ (showTerm t1) ++ " " ++ (showTerm t2) ++ ")"

instance Show Term where
  show t = showTerm t

termShift :: Int -> Term -> Term
termShift d t = walk 0 t
  where walk c td =
          case td of
            LVar x
              | x >= c -> LVar (x+d)
              | otherwise -> LVar x
            LAbs t1 -> LAbs (walk (c+1) t1)
            LApp t1 t2 -> LApp (walk c t1) (walk c t2)
            
termSubst :: Int -> Term -> Term -> Term
termSubst j s t =
  case t of
    LVar k
      | k == j -> s
      | otherwise -> LVar k
    LAbs t1 -> LAbs (termSubst (j+1) (termShift 1 s) t1)
    LApp t1 t2 -> LApp (termSubst j s t1) (termSubst j s t2)

termSubstTop :: Term -> Term -> Term
termSubstTop s t =
  termShift (-1) (termSubst 0 (termShift 1 s) t)
  
isval :: Context -> Term -> Bool  
isval ctx t = case t of  
  LAbs _ -> True
  _ -> False

type ErrorMessage = String
eval1 :: Context -> Term -> Either ErrorMessage Term       
eval1 ctx t =
  case t of
    LApp (LAbs t12) v2
      | isval ctx v2 -> Right (termSubstTop v2 t12)
    LApp v1 t2
      | (isval ctx v1) -> Right (LApp v1 t22)
        where Right t22 = eval1 ctx t2
    LApp t1 t2 -> Right (LApp t11 t2)
      where Right t11 = eval1 ctx t1
    _ -> Left "No Rule Applies"
    
eval :: Context -> Term -> Term
eval ctx t =
  case res of
    Left err -> t
    Right u -> eval ctx u
    where res = eval1 ctx t

使い方は

> let true = (LAbs (LAbs (LVar 1)))
> let false = (LAbs (LAbs (LVar 0)))
> let ifl = (LAbs (LAbs (LAbs (LApp (LApp (LVar 2) (LVar 1)) (LVar 0)))))
> true
(lambda. (lambda. 1))
> false
(lambda. (lambda. 0))
> ifl
(lambda. (lambda. (lambda. ((2 1) 0))))
> eval (Context []) (LApp (LApp (LApp ifl true) true) false)
(lambda. (lambda. 1))

って感じです。
関数適用が左結合なのを実装に組み込めてないので、一つ一つ自分で書かないといけないのがちょっとうざいですね。
いよいよ次の章から型が登場するらしいです。わくわく


以下、本に乗ってた関数たち

-- Bools
tru  = (LAbs (LAbs (LVar 1)))          
fls  = (LAbs (LAbs (LVar 0)))
test = (LAbs (LAbs (LAbs (LApp (LApp (LVar 2) (LVar 1)) (LVar 0)))))
andl = (LAbs (LAbs (LApp (LApp (LVar 1) (LVar 0)) fls)))
orl  = (LAbs (LAbs (LApp (LApp (LVar 1) tru) (LVar 0))))
notl = (LAbs (LApp (LApp (LVar 0) fls) tru))

-- Pair
pairl = (LAbs (LAbs (LAbs (LApp (LApp (LVar 0) (LVar 2)) (LVar 1)))))
fstl  = (LAbs (LApp (LVar 0) tru))
sndl  = (LAbs (LApp (LVar 0) fls))

-- Church Numerals
c0   = (LAbs (LAbs (LVar 0)))
scc  = (LAbs (LAbs (LAbs (LApp (LVar 1) (LApp (LApp (LVar 2) (LVar 1)) (LVar 0))))))
plus = (LAbs (LAbs (LAbs (LAbs
         (LApp
          (LApp (LVar 3) (LVar 1))
          (LApp
           (LApp (LVar 2) (LVar 1))
           (LVar 0)))))))
       
times = (LAbs (LAbs (LAbs (LApp (LApp (LVar 1) (LApp plus (LVar 0))) c0))))
iszro = (LAbs (LApp (LApp (LVar 0) (LAbs fls)) tru))