diff --git a/Graph.hs b/Graph.hs
--- a/Graph.hs
+++ b/Graph.hs
@@ -20,7 +20,7 @@
 	| Multiplexer {out ∷ Port, ins ∷ [Port]} -- only intermediate compilation result
 	| Case        {inp ∷ Port, out ∷ Port, alts ∷ [Port], names ∷ [String]}
 	| Operator    {inp ∷ Port, ops ∷ [Port], arity ∷ Int, lmop ∷ Int,
-	               function ∷ [String] → String, name ∷ String}
+	               function ∷ [String] → Maybe String, name ∷ String}
 
 -- | equality as defined in the paper with only the relevant cases included
 instance Eq NodeLS where
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -2,6 +2,8 @@
 module Main where
 
 import Prelude.Unicode
+import Data.Foldable (toList)
+import Data.Traversable (mapAccumL)
 import Data.List (delete)
 import GraphRewriting.Graph
 import GraphRewriting.GL.Render
@@ -34,29 +36,45 @@
 	(prog,args) ← UI.initialise
 	let lmo = "--lmo" ∈ args
 	args ← return $ "--lmo" `delete` args
+	let bench = "--bench" ∈ args
+	args ← return $ "--bench" `delete` args
 	file ← case args of
 		[f] → return f
-		___ → error "usage: lambdascope [GLUT-options] [--lmo] <file>"
+		___ → error "usage: lambdascope [GLUT-options] [--lmo] [--bench] <file>"
 	term ← parseFile file
 	let hypergraph = execGraph (apply $ exhaustive compileShare) (resolve term)
-	let layoutGraph = Layout.wrapGraph hypergraph
 
-	if lmo
-		then UI.run 50 id layoutStep (Control.wrapGraph layoutGraph) (lmoTree ruleTree)
-		else UI.run 50 id layoutStep layoutGraph ruleTree
+	if bench
+		then do
+			let tree = lmoTree ruleTree
+			let indexes = evalGraph (benchmark $ toList tree) (Control.wrapGraph hypergraph)
+			print indexes
+			let indexTable = foldl (flip incIndex) [] indexes
+			print indexTable
+			let (_, numTree) = mapAccumL (\(i:is) _ → (is,i)) (indexTable ⧺ repeat 0) tree
+			putStrLn $ showLabelledTree 2 0 (+) numTree
+		else let layoutGraph = Layout.wrapGraph hypergraph in if lmo 
+			then UI.run 50 id layoutStep (Control.wrapGraph layoutGraph) (lmoTree ruleTree)
+			else UI.run 50 id layoutStep layoutGraph ruleTree
 
+incIndex ∷ Int → [Int] → [Int]
+incIndex 0 (i:is) = i+1 : is
+incIndex 0 [    ] = [1]
+incIndex n (i:is) = i : incIndex (n-1) is
+incIndex n [    ] = 0 : incIndex (n-1) []
+
 -- | Modifies the rules of the rule tree with a given function.
 -- This can be used to for example wrap a strategy rule around the existing rules.
-mapRules :: (n -> m) -> LabeledTree n -> LabeledTree m
+mapRules ∷ (n → m) → LabelledTree n → LabelledTree m
 mapRules f (Leaf n r)    = Leaf n (f r)
 mapRules f (Branch n rs) = Branch n (map (mapRules f) rs)
 
 -- Appends a rule to the top branch of a rule tree
-appendRule :: n -> LabeledTree n -> LabeledTree n
-appendRule r l@(Leaf n rr) = Branch n [l, Leaf "moveControl" r]
-appendRule r (Branch n rs) = Branch n (rs ++ [Leaf "moveControl" r])
+appendRule ∷ n → LabelledTree n → LabelledTree n
+appendRule r l@(Leaf n rr) = Branch n [l, Leaf "Move Control" r]
+appendRule r (Branch n rs) = Branch n (rs ++ [Leaf "Move Control" r])
 
--- layoutStep :: (View Rotation n, View [Port] n, View Position n) => n -> IO ()
+layoutStep ∷ (PortSpec n, View Position n, View Rotation n, View [Port] n) ⇒ Node → Rewrite n ()
 layoutStep n = do
 	(cgf, cf, sf, rot) ← readOnly $ do
 		cgf ← centralGravitation n
@@ -67,10 +85,10 @@
 	Unsafe.adjustNode n $ Position . sf (\x → min 10 (x*0.9)) . cgf (\x → min 10 (x*0.01)) . cf (\x → min 10 (100/(x^2+0.1))) . position
 	Unsafe.adjustNode n $ rot (*0.9)
 
-lmoTree ∷ (LeftmostOutermost n, View [Port] n, View Control n) ⇒ LabeledTree (Rule n) -> LabeledTree (Rule n)
+lmoTree ∷ (LeftmostOutermost n, View [Port] n, View Control n) ⇒ LabelledTree (Rule n) → LabelledTree (Rule n)
 lmoTree = appendRule moveControl . mapRules leftmostOutermost
 
-ruleTree :: (View NodeLS n, View [Port] n) => LabeledTree (Rule n)
+ruleTree ∷ (View NodeLS n, View [Port] n) ⇒ LabelledTree (Rule n)
 ruleTree = Branch "All"
 	[Leaf "Beta Reduction" beta,
 	 Branch "All but Beta"
@@ -84,4 +102,4 @@
 			[Leaf "Constant" applyConstant,
 			 Leaf "Apply Operator" applyOperator,
 			 Leaf "Exec Operator" execOperator,
-			 Leaf "Reduce Operator Args" reduceOperatorArgs]]]
+			 Leaf "Reduce Operand" reduceOperand]]]
diff --git a/Resolver.hs b/Resolver.hs
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -59,11 +59,20 @@
 		compile env o exp -- compile the scrutiny
 
 operator ∷ String → Edge → Maybe NodeLS
-operator name p = case name of
-	"+" → op 2 $ show . sum . map (read :: String → Int)
+operator n p = case n of
+	"+" → op 2 $ liftM (show . sum) . mapM read
+	"-" → op 2 $ liftM (show . minus) . mapM read where minus [x,y] = x - y
+	"==" → op 2 $ \[x,y] → Just $ if x ≡ y then "T" else "F"
 	_ → Nothing
-	where op a f = Just Operator
-		{inp = p, ops = [], arity = a, lmop = 0, function = f, name = "+"}
+	where
+
+	read ∷ Read a ⇒ String → Maybe a
+	read str = case [ x | (x, "") ← reads str ] of
+		[] → Nothing
+		x:_ → Just x
+
+	op a f = Just Operator
+		{inp = p, ops = [], arity = a, lmop = 0, function = f, name = n}
 
 bindName ∷ Bool → String → Compiler (Edge, Name)
 bindName lambda sym = do
diff --git a/Rules.hs b/Rules.hs
--- a/Rules.hs
+++ b/Rules.hs
@@ -85,13 +85,13 @@
 -- This rule doesn't trigger for constants with arguments
 eliminateDelimiterConstant ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 eliminateDelimiterConstant = do
-	c@Constant {args = as, name = n} :-: Delimiter {inp = iD} <- activePair
+	c@Constant {args = as, name = n} :-: Delimiter {inp = iD} ← activePair
 	require (inp c ≢ iD && as == [])
 	replace $ byNode $ Constant {inp = iD, args = [], name = n}
 
 eliminateDelimiterEraser ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 eliminateDelimiterEraser = do
-	c@Eraser {} :-: Delimiter {inp = iD} <- activePair
+	c@Eraser {} :-: Delimiter {inp = iD} ← activePair
 	require (inp c ≢ iD)
 	replace $ byNode $ Eraser {inp = iD}
 
@@ -142,39 +142,40 @@
 
 -- TODO: Require that the lmoPort is not on one of the unreduced ports yet
 -- Do we only reduce operator args, if the operator has all args already?
-reduceOperatorArgs ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
-reduceOperatorArgs = do
-	o@(Operator {ops = os, lmop = lmo}) <- node
-	opid <- previous
-	let ports = inspect o :: [Port]
+reduceOperand ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
+reduceOperand = do
+	o@(Operator {ops = os, lmop = lmo}) ← node
+	opid ← previous
+	let ports = inspect o ∷ [Port]
 	let lmoport = ports !! lmo
 	-- only change the lmo port if it is on top or if it is attached to a Constant
-	require (lmo == 0) <|> do {Constant {} <- nodeWith lmoport; return ()}
-	port <- branch os -- get a pattern that matches each port in os
+	require (lmo == 0) <|> do {Constant {} ← nodeWith lmoport; return ()}
+	port ← branch os -- get a pattern that matches each port in os
 	-- we require that at least one node attached to the operator is not a constant
 	requireFailure $ do
-		Constant {} <- nodeWith port
+		Constant {} ← nodeWith port
 		return ()
 	-- we need to add one, since the input port is not part of os, but is part of the port numbering
 	let unreducedport = 1 + fromJust (elemIndex port os)
-	return $ do
-		updateNode opid (o {lmop = unreducedport})
+	return $ updateNode opid (o {lmop = unreducedport})
 
 execOperator ∷ forall n. (View [Port] n, View NodeLS n) ⇒ Rule n
 execOperator = do
-	Operator {inp = i, ops = os, arity = ar, function = fn, name = n} <- node
-	opid <- previous
+	Operator {inp = i, ops = os, arity = ar, function = fn, name = n} ← node
+	opid ← previous
 	require (length os == ar)
 	-- check that all args are constants
-	argss ← forM os $ \o -> do
-			c@Constant {} <- adverse o opid
+	argss ← forM os $ \o → do
+			c@Constant {} ← adverse o opid
 			return c
-	replace $ byNode $ Constant {inp = i, args = [], name = fn (map name argss)}
+	case fn (map name argss) of
+		Nothing → mempty
+		Just n' → replace $ byNode $ Constant {inp = i, args = [], name = n'}
 
-caseNode :: (View [Port] n, View NodeLS n) ⇒ Rule n
+caseNode ∷ (View [Port] n, View NodeLS n) ⇒ Rule n
 caseNode = do
 	-- the order of constant and case here is important, otherwise strategies don't work
-	Case {inp = i, alts = alts, names = names} :-: Constant {name = n, args = as} <- activePair
+	Case {inp = i, alts = alts, names = names} :-: Constant {name = n, args = as} ← activePair
 	let matchingport = alts !! (fromJust $ elemIndex n names)
 	let nn = length alts
 	let m = length as
@@ -184,12 +185,12 @@
 			es ← replicateM (m+1) byEdge
 			byWire matchingport (es !! 0) -- We merge the first new edge with the matching port from the Case node
 			byWire i (es !! m) -- We merge the last new edge with the input edge of the Case node
-			mconcat [byNode $ Applicator {inp = es !! (i+1), func = es !! i, arg = as !! i} | i <- [0..m-1]]
-			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]
+			mconcat [byNode $ Applicator {inp = es !! (i+1), func = es !! i, arg = as !! i} | i ← [0..m-1]]
+			mconcat [byNode $ Eraser {inp = alts !! i} | i ← filter (/= fromJust (elemIndex n names)) [0..nn-1]]
 			 else do
 		replace $ do
 			byWire i matchingport -- Attach the alternative directly to the input of the case node
-			mconcat [byNode $ Eraser {inp = alts !! i} | i <- filter (/= fromJust (elemIndex n names)) [0..nn-1]]
+			mconcat [byNode $ Eraser {inp = alts !! i} | i ← filter (/= fromJust (elemIndex n names)) [0..nn-1]]
 
 -- | Not the readback semantics as defined in the paper. Just a non semantics preserving erasure of all
 -- delimiters to make the graph more readable
@@ -197,41 +198,3 @@
 readback = do
 	Delimiter {inp = i, out = o} ← node
 	rewire [[i,o]]
-
--- getLmoPort ∷ (View [Port] n, LeftmostOutermost n) ⇒ Node → Pattern n Port
--- getLmoPort n = do
--- 	node ← liftReader $ readNode n
--- 	let ports = inspect node
--- 	case lmoPort node of
--- 		Nothing → fail "Term is in WHNF"
--- 		Just ix → return $ ports !! ix
---
--- moveControl :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n
--- moveControl = do
--- 	Control {stack = s} ← node
--- 	control ← previous
--- 	lmo1 ← getLmoPort control
--- 	n ← branchNodes =<< liftReader . adverseNodes control =<< getLmoPort control
--- 	return $ do
--- 		updateNode control NoControl
--- 		updateNode n (Control {stack = control : s})
---
--- leftmostOutermost :: (View [Port] n, View Control n, LeftmostOutermost n, View NodeLS n) => Rule n -> Rule n
--- leftmostOutermost r = do
--- 	rewrite <- r
--- 	ns <- history -- we want the first node of the matching pattern
--- 	let topnode = last ns
--- 	Control {stack = s} ← liftReader $ inspectNode topnode
--- 	return $ do
--- 		updateNode topnode NoControl -- First we set the topnode to not be the control node any more
--- 		oldNodes ← readNodeList
--- 		rewrite -- then we perform the rewrite
--- 		newNodes ← readNodeList
--- 		let s' = intersect s newNodes -- only consider nodes for the control marker that exist
--- 		if null s' -- even the topmost node has been replaced
--- 			then do -- we assign the control marker to one of the newly created nodes
--- 				let addedNodes = newNodes \\ oldNodes
--- 				updateNode (head addedNodes) (Control {stack = []}) -- finally we set the previous node on the stack as the control node
--- 			else do -- set the previous node on the stack as the control node
--- 				updateNode (head s') (Control {stack = tail s'})
---
diff --git a/Term.hs b/Term.hs
--- a/Term.hs
+++ b/Term.hs
@@ -30,13 +30,13 @@
 	deriving (Show,Eq,Ord)
 
 -- | The LHS of a case expression. Numbers are parsed as strings.
-data Pattern = Pat {constr :: String, vars :: [String]} deriving (Show, Eq, Ord)
+data Pattern = Pat {constr ∷ String, vars ∷ [String]} deriving (Show, Eq, Ord)
 
-testParser :: [tok] -> IndentParser tok () c -> c
-testParser str parser = either (error ∘ show) id (Indent.parse parser "(null)" str)
+testParser ∷ IndentParser tok () c → [tok] → c
+testParser parser str = either (error ∘ show) id (Indent.parse parser "(null)" str)
 
-parse :: [Char] -> Λ
-parse str = testParser str expression
+parse ∷ [Char] → Λ
+parse = testParser expression
 
 parseFile ∷ FilePath → IO Λ
 parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile expression
@@ -48,7 +48,7 @@
 application = foldl1 A <$> many1 (parenthetic <|> abstraction <|> variable <|> numeral)
 
 variable ∷ IndentCharParser st Λ
-variable = C <$> ident <*> pure []
+variable = C <$> (ident <|> operator haskell) <*> pure []
 
 numeral ∷ IndentCharParser st Λ
 numeral = C <$> numeric <*> pure []
@@ -59,20 +59,20 @@
 parenthetic ∷ IndentCharParser st Λ
 parenthetic = parens haskell expression
 
-tokP :: T.TokenParser st
+tokP ∷ T.TokenParser st
 tokP = T.makeTokenParser haskellDef
 
 caseExpr ∷ IndentCharParser st Λ
 caseExpr = flip label "case expression" $
 	Case <$> (keyword "case" *> expression <* keyword "of") <*> bracesOrBlock tokP patterns
 
-patterns :: IndentCharParser st [(Pattern, Λ)]
+patterns ∷ IndentCharParser st [(Pattern, Λ)]
 patterns = semiOrNewLineSep tokP pattern
 
 arrow ∷ IndentCharParser st String
-arrow = sym "->" <|> sym "→"
+arrow = sym "→" <|> sym "->"
 
-pattern :: IndentCharParser st (Pattern, Λ)
+pattern ∷ IndentCharParser st (Pattern, Λ)
 pattern = (,) <$> lhs <*> (arrow *> expression) where
 	lhs = Pat <$> (ident <|> numeric) <*> many (ident <|> numeric)
 
@@ -110,11 +110,11 @@
 	rhs ← flip (foldr Λ) <$> many ident <*> (sym "=" *> expression)
 	return (funct, rhs)
 
-keyword :: String -> IndentCharParser st ()
+keyword ∷ String → IndentCharParser st ()
 keyword = reserved haskell
 
-ident :: IndentCharParser st String
+ident ∷ IndentCharParser st String
 ident = identifier haskell
 
-sym :: String -> IndentCharParser st String
+sym ∷ String → IndentCharParser st String
 sym = symbol haskell
diff --git a/examples/sum.l b/examples/sum.l
--- a/examples/sum.l
+++ b/examples/sum.l
@@ -2,4 +2,4 @@
 	sum list = case list of
 		Nil -> 0
 		Cons z zs -> (\x.λy -> + x y) z (sum zs)
-in sum (Cons 1 Nil)
+in sum (Cons 1 (Cons 2 Nil))
diff --git a/examples/sum1234.l b/examples/sum1234.l
--- a/examples/sum1234.l
+++ b/examples/sum1234.l
@@ -1,5 +1,5 @@
 let
 	Cons x xs = λcons nil. cons x xs
 	Nil = λcons nil. nil
-	sum list = list (λx xs . (λx y . Plus x y) x (sum xs)) 0
+	sum list = list (λx xs . (λx y . + x y) x (sum xs)) 0
 in sum (Cons 1 (Cons 2 (Cons 3 Nil)))
diff --git a/graph-rewriting-lambdascope.cabal b/graph-rewriting-lambdascope.cabal
--- a/graph-rewriting-lambdascope.cabal
+++ b/graph-rewriting-lambdascope.cabal
@@ -1,5 +1,5 @@
 Name:           graph-rewriting-lambdascope
-Version:        0.5
+Version:        0.5.2
 Copyright:      (c) 2010, Jan Rochel
 License:        BSD3
 License-File:   LICENSE
@@ -9,7 +9,7 @@
 Stability:      alpha
 Build-Type:     Simple
 Synopsis:       Implementation of Lambdascope as an interactive graph-rewriting system
-Description:    Lambdascope is an optimal implementation of the λβ-calculus described in the paper "Lambdascope - Another optimal implementation of the lambda-calculus" by Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI". Use the "--lmo" flag for leftmost outermost evalution
+Description:    Lambdascope is an optimal implementation of the λβ-calculus described in the paper "Lambdascope - Another optimal implementation of the lambda-calculus" by Vincent van Oostrom, Kees-Jan van de Looij, and Marijn Zwitserlood. Call "lambdascope" with one of the files from the "examples" directory as an argument. For usage of the GUI see "GraphRewriting.GL.UI". Use the "--lmo" flag for leftmost outermost evalution and "--bench" for non-graphical evaluation to weak head normal form.
 Category:       Graphs, Application
 Cabal-Version:  >= 1.6
 Data-Files:     examples/*.l
@@ -19,9 +19,9 @@
   Build-Depends:
     base >= 4 && < 4.5,
     base-unicode-symbols >= 0.2 && < 0.3,
-    graph-rewriting >= 0.7 && < 0.8,
-    graph-rewriting-layout >= 0.5.0 && < 0.6,
-    graph-rewriting-gl >= 0.6.9 && < 0.7,
+    graph-rewriting >= 0.7.1 && < 0.8,
+    graph-rewriting-layout >= 0.5.1 && < 0.6,
+    graph-rewriting-gl >= 0.7.1 && < 0.8,
     graph-rewriting-strategies >= 0.2 && < 0.3,
     parsec >= 2.1 && < 2.2,
     GLUT >= 2.2 && < 2.3,