programming contest

Implement a lambda calculus evaluator in whatever language you choose.

I will pick the winner in one week based on undisclosed criteria.


data Binding = NameBind
type Context = [(String, Binding)]

data Term = TmVariable Int Int
          | TmAbstraction String Term
          | TmApplication Term Term
    deriving (Show, Eq)

termShift :: Int -> Term -> Term
termShift d t = walk 0 t
    where walk c t = case t of
            (TmVariable x n)      -> if x >= c then (TmVariable (x+d) (n+d))
                                     else (TmVariable x (n+d))
            (TmAbstraction x t)   -> (TmAbstraction x (walk (c+1) t))
            (TmApplication t1 t2) -> (TmApplication (walk c t1) (walk c t2))

termSubst :: Int -> Term -> Term -> Term
termSubst j s t = walk 0 t
    where walk c t = case t of
            (TmVariable x n)      -> if x == (j+c) then termShift c s
                                     else (TmVariable x n)
            (TmAbstraction x t)   -> (TmAbstraction x (walk (c+1) t))
            (TmApplication t1 t2) -> (TmApplication (walk c t1) (walk c t2))

termSubstTop :: Term -> Term -> Term
termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)

isVal :: Context -> Term -> Bool
isVal _ (TmAbstraction _ _) = True
isVal _ _                   = False

eval1 :: Context -> Term -> Maybe Term
eval1 ctx (TmApplication (TmAbstraction x t) v) | (isVal ctx v)  = Just (termSubstTop v t)
eval1 ctx (TmApplication t1 t2)                 | (isVal ctx t1) = (eval1 ctx t2) >>= (\t2' -> Just (TmApplication t1 t2'))
                                                | otherwise      = (eval1 ctx t1) >>= (\t1' -> Just (TmApplication t1' t2))
eval1 ctx _                                     = Nothing

eval :: Term -> Term
eval t = case (eval1 t) of
            (Just t') -> eval t'
            Nothing   -> t