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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
