2009年5月4日星期一

A Lambda Calculus Interpreter in Haskell

I will present a Lambda Calculus interpreter in this post. It is an (almost) exact translation from the ML code in chapter 9 of ML for the Working Programmer by Lawrence C. Paulson. This program incorporates a parser to convert string to an internal represenation of lambda expression, a pretty printer to reconvert the internal represenation to a formatted string in a human-readable form, and two evaluation functions (lazy and strict respectively) to reduce a given lambda expression to its normal form.

Enjoy.

Code below:
------------

module Lci (
            Lambda
           ,reader           -- String -> Lambda
           ,pr               -- Lambda -> String
           ,byValue          -- Lambda -> Lambda
           ,byName           -- Lambda -> Lambda
           ,evalV            -- String -> Lambda
           ,evalN            -- String -> Lambda
           ,tryV             -- String -> IO ()
           ,tryN             -- String -> IO ()
           ) where

-- Parser
import Text.ParserCombinators.Parsec
import qualified Text.ParserCombinators.Parsec.Token as T
import Text.ParserCombinators.Parsec.Language (emptyDef)

-- Pretty Printing
import qualified Text.PrettyPrint as PP
import Text.PrettyPrint (Doc, (<>), (<+>))

-- Environment
import qualified Data.Map as Map
import Data.Maybe


-------------------
-- Data
-------------------

data Lambda = Free String
            | Bound Int
            | Abs String Lambda
            | App Lambda Lambda
              deriving (Eq, Show, Read)

type Env = Map.Map String Lambda
 

-------------------
-- Parser
-------------------

abstract :: Int -> String -> Lambda -> Lambda
abstract i s (Free s') | s == s'   = Bound i
                       | otherwise = Free s'
abstract _ _ (Bound i) = Bound i
abstract i s (Abs s' t) = Abs s' (abstract (i+1) s t)
abstract i s (App t1 t2) = App (abstract i s t1) (abstract i s t2)

-- Abstraction over several free variables
absList :: [String] -> Lambda -> Lambda
absList xs t = foldr (\x acc -> Abs x (abstract 0 x acc)) t xs

-- Application of t to several terms               
appList :: Lambda -> [Lambda] -> Lambda
appList = foldl (\acc x -> App acc x)

-- Shift a term's non-local indices by i
shift :: Int -> Int -> Lambda -> Lambda
shift 0 _ u = u
shift i d u@(Free s) = u
shift i d u@(Bound j) = if j >= d then Bound (j+i) else Bound j
shift i d (Abs s t) = Abs s (shift i (d+1) t)
shift i d (App t1 t2) = App (shift i d t1) (shift i d t2)

-- Substitution for bound variable

subst :: Int -> Lambda -> Lambda -> Lambda
subst _ _ t@(Free _) = t
subst i u t@(Bound i') | i' <>
                       | i' == i   = shift i 0 u
                       | otherwise = Bound (i' - 1) -- non-local to t
subst i u (Abs s t') = Abs s (subst (i+1) u t')
subst i u (App t1 t2) = App (subst i u t1) (subst i u t2)

-- Lexer & Parser
lexer :: T.TokenParser ()
lexer = T.makeTokenParser emptyDef

whiteSpace= T.whiteSpace lexer
lexeme    = T.lexeme lexer
symbol    = T.symbol lexer
parens    = T.parens lexer
identifier= T.identifier lexer

p_term :: Parser Lambda
p_term = do{ symbol "^"
           ; ids <- many1 identifier
           ; symbol "."
           ; t <- p_term
           ; return $ absList ids t
           }
     <|> do{ t <- p_atom
           ; ts <- many p_atom
           ; return $ appList t ts
           }

p_atom :: Parser Lambda
p_atom = do{ s <- identifier
           ; return $ Free s
           }
     <|> parens p_term

p_top :: Parser Lambda
p_top = do{ whiteSpace
          ; t <- p_term
          ; eof
          ; return t
          }

reader :: String -> Lambda
reader input = case (parse p_top "" input) of
                  Left err -> error $ show err
                  Right x  -> x


-------------------
-- Pretty Printing
-------------------

-- Free variables in a term
vars :: Lambda -> [String]
vars (Free s) = [s]
vars (Bound _) = []
vars (Abs s t) = vars t
vars (App t u) = vars t ++ vars u

-- Rename variable "a" to avoid clashes
rename bs a = if a `elem` bs then rename bs (a ++ "'") else a

-- Remove leading lambdas, return bound variable names
stripAbs t = strip [] t
    where strip bs (Abs s t) =
              let b = rename (vars t) s
              in strip (b:bs) (subst 0 (Free b) t)
          strip bs u = (reverse bs, u)

pr_term :: Lambda -> Doc
pr_term (Free s) = PP.text s
pr_term (Bound i) = PP.text "??UNMATCHED INDEX??"
pr_term t@(Abs _ _) = 
    let (b:bs, u)     = stripAbs t
        spaceJoin b z = " " ++ b ++ z
        binder        = "^" ++ b ++ (foldr spaceJoin ". " bs)
    in PP.sep [PP.text binder, pr_term u]
pr_term t = PP.sep (pr_app t)
            
pr_app (App t u) = pr_app t ++ [PP.nest 1 (pr_atom u)]
pr_app t         = [pr_atom t]
pr_atom (Free s) = PP.text s
pr_atom t        = PP.nest 1 $ PP.parens $ pr_term t

pr :: Lambda -> String
pr = PP.render . pr_term


-------------------
-- Reduction
-------------------

eval (App t1 t2) =
    case eval t1 of
      (Abs a u) -> eval (subst 0 (eval t2) u)
      t         -> App t (eval t2)
eval t = t

byValue :: Lambda -> Lambda
byValue t = bodies (eval t)
    where bodies (Abs a t) = Abs a (byValue t)
          bodies (App t u) = App (bodies t) (bodies u)
          bodies t         = t

headNF (Abs a t) = Abs a (headNF t)
headNF (App t u) = 
    case headNF t of
      (Abs a t') -> headNF (subst 0 u t')
      u'         -> App u' u
headNF t = t

byName :: Lambda -> Lambda
byName = args . headNF
    where args (Abs a t) = Abs a (args t)
          args (App t u) = App (args t) (byName u)
          args t         = t


-----------------------------------------
-- Standard Environment (Lambda Prelude)
-----------------------------------------

-- Substitution for free variables from environment
inst :: Env -> Lambda -> Lambda
inst env t@(Free s)  = fromMaybe t (Map.lookup s env)
inst env t@(Bound i) = t
inst env (Abs s t')  = Abs s (inst env t')
inst env (App t1 t2) = App (inst env t1) (inst env t2)

insertEnv :: Env -> (String, String) -> Env
insertEnv env (a, s) = Map.insert a (reader s) env

stdEnv = foldl insertEnv Map.empty [
          -- booleans
          ("true",  "^x y. x"), ("false", "^x y. y")
         ,("if",    "^p x y. p x y")
          -- pairs
         ,("pair",  "^x y f. f x y")
         ,("fst",   "^p. p true"), ("snd", "^p. p false")
         ]


-------------------
-- Evaluators
-------------------

evalWith :: (Lambda -> Lambda) -> Env -> String -> Lambda
evalWith fn env = fn . inst env . reader
              
evalV = evalWith byValue stdEnv
evalN = evalWith byName  stdEnv

tryV = putStrLn . pr . evalV
tryN = putStrLn . pr . evalN

1 条评论:

tphyahoo 说...

This line appears to be a syntax error:

subst i u t@(Bound i') | i' <>