Victor Nazarov wrote:
The goal of the code is to implement the evaluator for untyped lambda-calculus. The main problem is how to display each step of reduction? More detailed questions follows in the end of the code.
Terms of lambda-calculus is the following data-type:
data (Binder bndr) => Term bndr = Var bndr | Lam bndr (Term bndr) | App (Term bndr) (Term bndr)
Next we'll define the evaluator. Evaluator returns the WHNF for each well-formed term, or _|_ if there is no WHNF
Straight forward version:
whnf :: Term bndr -> Term bndr whnf = reduce [] where reduce (a:as) (Lam b i) = reduce as $ subst b a i reduce as (App f a) = reduce (a:as) f reduce as term = foldl term App as
But our goal is to perform only one step of reduction. And to display term after each reduction
Is there a more effective way to perform this? In printReductions I have to rescan the syntax tree over and over again to find the redex. Is there a way to save the position in the tree, to print the tree and then to resume from saved position?
Yes, there is: you can use a zipper http://en.wikibooks.org/wiki/Haskell/Zippers Here's how: data Branch v = AppL (Term v) | AppR (Term v) | Lamb v type Context v = [Branch v] type Zipper v = (Context v, Term v) whnf :: Term v -> Term v whnf t = whnf' ([],t) where whnf' (AppL e':cxt, Lam x e) = whnf' (cxt , subst x e' e) whnf' (cxt , App f e) = whnf' (AppL e:cxt, f) whnf' z = unwind z unwind :: Zipper v -> Term v unwind ([] , t) = t unwind (AppL e:cxt, f) = unwind (cxt, App f e) unwind (AppR f:cxt, e) = unwind (cxt, App f e) unwind (Lamb x:cxt, e) = unwind (cxt, Lam x e) Note how this whnf and your whnf are pretty much exactly the same. In fact, your stack of pending applications (the as in reduce' as ) is already a zipper. The only difference here is that we are no longer limited to only walk down the left spine and can now implement other reduction strategies like nf or wnf too. Concerning the problem of printing intermediate steps, I don't quite understand your approach. I'd simply use a Writer monad to keep track of intermediate terms import Control.Monad.Writer -- use a difference list or something for better performance type Trace v = [Zipper v] whnf :: Term v -> Writer (Trace v) (Term v) whnf t = whnf' ([],t) where whnf' (AppL e':cxt, Lam x e) = tell (cxt, App (Lam x e) e') >> whnf' (cxt , subst x e' e) whnf' (cxt , App f e) = whnf' (AppL e:cxt, f) whnf' z = return $ unwind z The definition of whnf is basically left unchanged, except that a redex is recorded via tell whenever a beta-reduction is about to be performed. The recorded terms can be printed afterwards printTrace :: Writer (Trace v) (Term v) -> IO () printTrace w = let (t, ts) = runWriter t ts putStrLn . unlines . map show $ ts Note that "zipped" terms are recorded, i.e. the redex enclosed in its context and you can even highlight the redex while printing. Last but not least, there is a nice introductory paper about the many possible reduction strategies for lambda calculus http://www.itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf Regards, apfelmus