On Jan 10, 2008 8:39 PM, apfelmus
Victor Nazarov wrote:
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)
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)
Thanks. Zippers seemed very cool when I first encountered them in some text about xmonad. But I've never used them in my own code.
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
My version just return when the state in State monad is not Nothing, so we can print result and start over again.
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
Is this function lazy? Can I run this code on term without nf and print n-first steps:
printTraceN :: Int -> Writer (Trace v) (Term v) -> IO () printTraceN n w = let (t, ts) = runWriter t ts in putStrLn . unlines . map show $ take n ts
Will this work:
printTraceN 5 (read "(\x. x x x) (\x. x x x)")
?
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
Thank you. -- vir http://vir.comtv.ru/