Re: [Haskell-cafe] Programming an Evaluation Context
in structural operational semantics, an evaluation context is often used to
decompose an expression into a redex and its context. In a formal semantics on
paper, an expression can just be pattern matched over the grammar of an
evaluation context. If one wants to implement such a semantics in the form of an
interpreter, I could not come up with a similarly nice solution. I have declared
two separate data types (one for expressions, and one for evaluation contexts)
and explicit functions to convert an expression into a (evaluation context,
redex) pair.
do you really need an explicit representation of evaluation contexts?
yes, explicit representation of contexts through zippers makes for more
efficient
evaluation, but for small prototypes, that may not be necessary, and for larger
prototypes, you may want to represent the optimizations implicit in zipper
traversal
explicitly by moving from interpreter to compiler+stack-based abstract machine.
Are there any tricks to mimick more closely what is going on in the formal
semantics?
I tend to find MonadPlus and pattern-match failure as mzero very helpful, for
almost direct translation of operational semantics represented in terms of
evaluation contexts and reduction rules. See below for a sketch.
Hth,
Claus
--
import Control.Monad
data Expr = Val Int | Plus Expr Expr deriving Show
-- evaluation: stepwise reduction until done
eval e = done e `mplus` (step e = eval)
-- normal form
done e = do { (Val i) - return e; return (Val i) }
-- reduction rule
reduce e = do { (Plus (Val i) (Val j)) - return e; return (Val (i+j)) }
-- one-step reduction: apply reduction rule in evaluation context
step e = ctxt reduce e
-- evaluation contexts, parameterized by rule to apply
ctxt rule e = rule e `mplus` left (ctxt rule) e `mplus` right (ctxt rule) e
left act e = do { (Plus l r) - return e; lv - act l; return (Plus
lv r) }
right act e = do { (Plus lv@(Val _) r) - return e; rv - act r; return (Plus
lv rv) }
-- example
main = do
let e = (Val 1 `Plus` Val 2) `Plus` (Val 3 `Plus` Val 4)
print e
print (eval e :: Maybe Expr)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Programming an Evaluation Context
-- evaluation contexts, parameterized by rule to apply
ctxt rule e = rule e `mplus` left (ctxt rule) e `mplus` right (ctxt rule) e
left act e = do { (Plus l r) - return e; lv - act l; return (Plus
lv r) }
right act e = do { (Plus lv@(Val _) r) - return e; rv - act r; return (Plus
lv rv) }
actually, for the common case of reduction in context (contexts being preserved
unchanged), we can build contexts from context constructors corresponding to the
data constructors. moving the common plumbing into the context constructors
makes the context specification itself a lot clearer (a transliteration of the formal
specification:-):
-- context constructors
val fie = do { Val i- return e; return (Val (fi i)) }
plus cl cr e = do { Plus l r - return e; l' - cl l; r' - cr r; return
(Plus l' r') }
expr e = return e
(a .|. b) e = a e `mplus` b e
-- evaluation contexts, parameterized by rule to apply, abstract style
ctxt' hole = hole .|. plus (ctxt' hole) expr .|. plus (val id) (ctxt' hole)
Claus
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Programming an Evaluation Context
Hi there, in structural operational semantics, an evaluation context is often used to decompose an expression into a redex and its context. In a formal semantics on paper, an expression can just be pattern matched over the grammar of an evaluation context. If one wants to implement such a semantics in the form of an interpreter, I could not come up with a similarly nice solution. I have declared two separate data types (one for expressions, and one for evaluation contexts) and explicit functions to convert an expression into a (evaluation context, redex) pair. For example, I could have data Expr = Val Int | Plus Expr Expr and data Ctx = Hole | CPlusl Ctx Expr | CPlusr Int Expr Are there any tricks to mimick more closely what is going on in the formal semantics? Klaus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Programming an Evaluation Context
On 2/14/07, Klaus Ostermann [EMAIL PROTECTED] wrote: in structural operational semantics, an evaluation context is often used to decompose an expression into a redex and its context. Have you seen http://citeseer.ist.psu.edu/mcbride01derivative.html The Derivative of a Regular Type is its Type of One-Hole Contexts Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
