diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,104 @@
+GULCII
+======
+
+GULCII is an untyped lambda calculus interpreter supporting interactive
+modification of a running program with graphical display of graph reduction.
+
+
+Syntax
+------
+
+Lambda calculus terms with some sugar coating:
+  
+    term ::= variable                    -- free or bound
+         | '\' var+ strategy term        -- lambda abstraction
+         | term+                         -- application
+         | '(' term ')'
+         | integer
+         | list
+    variable ::= [a-z][A-Za-z0-9]*
+    strategy = '.' | '!' | '?'           -- lazy | strict | copy
+    integer ::= [0-9]+                   -- uses Scott-encoding
+    list ::= '[' (term (, T)*)? ']'      -- uses Scott-encoding
+
+There are three variants of lambda abstraction: lazy, strict, and copy:
+
+    \x . f x x    -- x is evaluated lazily with sharing
+    \x ! f x x    -- x is evaluated strictly and shared
+    \x ? f x x    -- x is copied before any evaluation
+
+There is additional syntax sugar for natural numbers and lists, using
+<http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding#Scott_encoding>:
+
+    [0,1,2,3]
+
+There is a small standard library based loosely around the Haskell Prelude:
+
+    :load prelude
+    :browse
+
+If you define a term using free variables, they can be modified while
+the program is running, but sharing is lost.  If you define a term as
+a fixed point (perhaps with Y-combinator) then sharing works (to some
+extent), but you can't modify the code while it is running any more.
+
+
+Meta Commands
+-------------
+
+To exit type:
+
+    :quit
+
+Entering a term evaluates it.
+
+Terms can be bound to names, stored in a global dictionary:
+
+    foo = bar
+
+The global dictionary can be listed or wiped clean:
+
+    :browse
+    :clear
+
+Installed files can be loaded:
+
+    :load church
+
+Machine-readable node statistics are output to stdout, as well as when
+free variables are instantiated by looking up their definitions.  These
+are intended to be used for sonification, for example with Pure-data:
+
+    pd extra/gulcii.pd &
+    sleep 5
+    gulcii | pdsend 8765
+
+The sonification is controlled by two commands:
+
+    :start
+    :stop
+
+
+Settings
+--------
+
+There are some runtime adjustable settings:
+
+    :get NewsOnTop
+    :set NewsOnTop
+    :unset NewsOnTop
+    :toggle NewsOnTop
+
+Where NewsOnTop is a setting.  Settings include:
+
+    TraceEvaluation
+    CollectGarbage
+    RealTimeDelay
+    RealTimeAcceleration
+    RetryIrreducible
+    EmitStatistics
+    EmitRebindings
+    EchoToStdOut
+    EchoToGUI
+    SaveImages
+    NewsOnTop
diff --git a/doc/Makefile b/doc/Makefile
new file mode 100644
--- /dev/null
+++ b/doc/Makefile
@@ -0,0 +1,12 @@
+all: encoding.pdf
+
+clean:
+	-rm -f encoding.aux encoding.log encoding.md.tex encoding.nav encoding.out encoding.pdf encoding.snm encoding.toc encoding.vrb
+
+encoding.pdf: encoding.tex encoding.md.tex
+	pdflatex encoding.tex
+	pdflatex encoding.tex
+	pdflatex encoding.tex
+
+encoding.md.tex: encoding.md
+	pandoc -t beamer --slide-level 2 encoding.md -o encoding.md.tex
diff --git a/doc/encoding.md b/doc/encoding.md
new file mode 100644
--- /dev/null
+++ b/doc/encoding.md
@@ -0,0 +1,518 @@
+# Lambda calculus encodings
+
+## Notation
+
+Backslash is used for lambda:
+
+* easier to type
+* familiar from Haskell
+
+Neighbouring lambdas can be combined with one backslash:
+
+    \a b s z . a s (b s z)
+
+Corresponds to:
+
+    λa. λb. λs. λz. a s (b s z)
+
+
+## Church and Scott encodings
+
+* encode data as lambda terms
+* continuation passing style
+* Church folds vs Scott case analysis
+
+
+## Continuation passing style
+
+* the datum is a black box that knows itself
+* the datum is passed functions that it calls with its deconstruction
+* the datum has one argument per constructor
+* each continuation has one argument per constructor argument
+
+
+## Simple types
+
+Church and Scott encoding coincide for simple types.
+
+
+## Bool
+
+Haskell:
+
+    data Bool
+      = False
+      | True
+
+Church, Scott:
+
+    true  = \t f . t
+    false = \t f . f
+
+    and = \a b . a b a
+    or  = \a b . a a b
+    not = \a . a false true
+
+The datum "true" takes two arguments, and returns the first, which (by
+convention) denotes the value True.
+
+
+## Pair
+
+Haskell:
+
+    data Pair a b
+      = Pair a b
+
+Church, Scott:
+
+    pair = \a b p . p a b
+
+    fst  = \p . p (\a b . a)
+    snd  = \p . p (\a b . b)
+
+The datum "pair x y" takes one argument, which is a function of two arguments,
+and passes it the stored values of "x" and "y".
+
+
+## Maybe
+
+Haskell:
+
+    data Maybe a
+      = Nothing
+      | Just a
+
+Church, Scott:
+
+    nothing = \n j . n
+    just    = \a n j . j a
+
+    maybe   = \n j m . m n j
+
+
+## Either
+
+Haskell:
+
+    data Either a b
+      = Left a
+      | Right b
+
+Church, Scott:
+
+    left   = \a l r . l a
+    right  = \b l r . r b
+
+    either = \l r e . e l r
+
+
+## Recursive types
+
+* Church and Scott encoding differ for recursive types.
+
+* Church encoding uses folds.
+
+    The deconstruction continuation threads throughout
+    the structure.
+
+* Scott encoding is similar to case analysis.
+
+    The deconstruction continuation
+    unwraps one layer of constructors only.
+
+
+## Natural numbers
+
+Haskell:
+
+    data Nat
+      = Zero
+      | Succ Nat
+  
+Church:
+
+    zero = \s z . z
+    succ = \n s z . s (n s z)
+  
+Scott:
+
+    zero = \s z . z
+    succ = \n s z . s n
+
+
+## Nat examples
+
+Haskell:
+
+    Zero, Succ Zero, Succ(Succ Zero), Succ(Succ(Succ Zero))
+
+Church, applying the same "s" "n" times at once:
+
+    \s z . z
+    \s z . s z
+    \s z . s (s z)
+    \s z . s (s (s z))
+
+Scott, applying different "s" "n" times separately:
+
+    \s z . z
+    \s z . s (\s z . z)
+    \s z . s (\s z . s (\s z . z))
+    \s z . s (\s z . s (\s z . s (\s z . z)))
+
+
+## Church Nat succ
+
+    zero = \s z . z
+    succ = \n s z . s (n s z)
+
+      succ zero
+    = {- definition of succ -}
+      (\n s z . s (n s z)) zero
+    = {- beta -}
+      \s z . s (zero s z)
+    = {- definition of zero -}
+      \s z . s ((\s z . z) s z)
+    = {- beta -}
+      \s z . s ((\z . z) z)
+    = {- beta -}
+      \s z . s z
+    = {- definition of one -}
+      one
+
+
+## Scott Nat succ
+
+    zero = \s z . z
+    succ = \n s z . s n
+
+      succ zero
+    = {- definition of succ -}
+      (\n s z . s n) zero
+    = {- beta -}
+      \s z . s zero
+    = {- definition of zero -}
+      \s z . s (\s z . z)
+    = {- definition of one -}
+      one
+
+
+## Nat arithmetic
+
+Church:
+
+    add = \m n . m succ n
+    mul = \m n . m (add n) zero
+    exp = \m n . n m
+
+Scott, open terms with `letrec`:
+
+    add = \m n . m (\p . succ  (add p n)) n
+    mul = \m n . m (\p . add n (mul p n)) zero
+    exp = \m n . n (\p . mul m (exp m p)) one
+
+Scott, closed terms with `fix`:
+
+    add = fix (\add . \m n . m (\p . succ  (add p n)) n)
+    mul = fix (\mul . \m n . m (\p . add n (mul p n)) zero)
+    exp = fix (\exp . \m n . n (\p . mul m (exp m p)) one)
+
+
+## Fixed point combinator
+
+Semantics:
+
+    fix f = f (fix f)
+
+Implementation:
+
+    \f . (\x . f (x x)) (\x . f (x x))
+
+What it computes:
+
+* The unique least fixed point under the definedness order.
+
+* Allows recursive functions to be defined as closed terms.
+
+
+## Nat predecessor
+
+Church (courtesy Wikipedia):
+
+    pred = \n f x . n (\g h . h (g f)) (\u . x) (\v . v)
+
+Scott:
+
+    pred = \n . n (\p . p) zero
+
+
+## Nat conversion
+
+Church arithmetic is more concise (and doesn't need `fix`).
+
+Scott predecessor is comprehensible.
+
+Mix and match?
+
+    churchToScott = \n . n scottSucc scottZero
+
+    scottToChurch = \n . n
+        (\p . churchSucc (scottToChurch p))
+        churchZero
+
+    scottToChurch = fix (\scottToChurch . \n . n
+        (\p . churchSucc (scottToChurch p))
+        churchZero)
+
+
+## Nat subtract and equality
+
+Church:
+
+    sub = \m n . n pred m
+
+Scott:
+
+    sub = \m n . m
+      (\p . n (\q . sub p q) m)
+      zero
+    equal = \m n . m
+      (\p . n (\q . equal p q) false)
+      (n (\q . false) true)
+
+Unwrap a layer of constructor from each number and recurse.
+
+There is a different `equal` for booleans:
+
+    equalBool = \a b . a b (not b)
+
+
+## List
+
+Haskell:
+
+    data List a
+      = Nil
+      | Cons a (List a)
+
+Church:
+
+    nil  = \c n . n
+    cons = \x xs c n . c x (xs c n)
+
+Scott:
+
+    nil  = \c n . n
+    cons = \x xs c n . c x xs
+
+
+## List operations
+
+Church, Scott:
+
+    isnil  = \l . l (\x xs . false) true
+    head   = \l . l (\x xs . x) error
+
+Church (`tail` courtesy Wikipedia):
+
+    length = \l . l (\x xs . succ xs) zero
+    tail   = \l c n . l
+        (\x xs g . g x (xs c)) (\xs . n) (\x xs . xs)
+
+Scott:
+
+    length = \l . l (\x xs . succ (length xs)) zero
+    tail   = \l . l (\x xs . xs) nil
+
+
+## More Scott functions
+
+    compose = \f g x . f (g x)
+
+    fold = \f e l . l (\x xs . f x (fold f e xs)) e
+
+    sum  = fold add zero
+    ands = fold and true
+    ors  = fold or false
+
+    map = \f . fold (compose cons f) nil
+    all = \f . compose ands (map f)
+    any = \f . compose ors (map f)
+
+    take = \n l. n(\p. l (\x xs. cons x (take p xs))nil)nil
+    drop = \n l. n(\p. l (\x xs. drop p xs) nil) l
+
+    iterate = \f x . cons x (iterate f (f x))
+
+
+# How to perform lambda calculus
+
+
+## How to perform lambda calculus
+
+* single step graph reduction
+
+* visualisation of current state
+
+* sonification of changes in state
+
+* open terms vs closed terms
+
+
+## Graph reduction
+
+    data Term
+      = Free String
+      | Reference Integer
+      | Bound          -- de Bruijn index 0
+      | Scope Term     -- see Lambdascope paper
+      | Lambda Strategy Term
+      | Apply Term Term
+
+    reduce
+      :: Definitions   -- Map String  Term
+      -> References    -- Map Integer Term
+      -> Term
+      -> Maybe (References, Term)
+
+
+## Three kinds of Lambda
+
+* strict (syntax inspired by Haskell's -XBangPatterns):
+
+        (\v ! s) t
+
+    t is fully reduced before substitution into s.
+
+* copy:
+
+        (\v ? s) t
+
+    t is substituted for each occurrence of v in s.
+
+* lazy:
+
+        (\v . s) t
+
+    a new `Reference` is created for t, and substituted into s.
+
+    `reduce` reduces *inside* the `References` until it is irreducible, at which
+    point the `Reference` is replaced with the `Term` it refers to.
+
+
+## Visualisation
+
+![](visualisation.png){width=100%}\ 
+
+## Sonification
+
+* count number of nodes of each type
+
+* statistics are forwarded to a Pure-data patch
+
+* changes in each count control a harmonic (one for each type of node) in a
+  simple phase modulation synth
+
+
+## Open terms
+
+* free variables looked up on demand from environment
+
+* allows definitions to be changed at runtime
+
+* easier to write
+
+
+## Drawbacks of open terms
+
+* no sharing
+
+    subterms can be evaluated many times due to duplication
+
+* exponential work (worst case)
+
+* exponential space (worst case)
+
+
+## Fixed points
+
+* closed terms with fixed point combinators
+
+* allows evaluation to be shared
+
+* sharing can be vital for efficiency
+
+
+# Future work
+
+
+## Better Evaluator
+
+* current evaluator is still somewhat ad-hoc and doesn't preserve sharing
+
+* previous evaluator even had correctness bugs
+
+* switch to using Lambdascope (or similar) as a library?
+
+
+## Auto Fix
+
+Automatically translating open terms to use fixed point combinators:
+
+* recursive functions can use `fix`
+* mutually recursive functions can use `fix` combined with tuples
+
+        many = some `orElse` none
+        some = one `andThen` many
+
+    becomes:
+
+        manysome = fix (\p -> pair
+            (snd p `orElse` none)
+            (one `andThen` fst p) )
+        many = fst manysome
+        some = snd manysome
+
+
+## Magic It
+
+* refer to previously evaluated terms
+* including the currently evaluating term
+* without restarting evaluation
+
+Haskell example (`ghci-8.0.1`):
+
+    > 3
+    3
+    > it + 5
+    8
+    > it * 2
+    16
+
+
+## Further Performances / Project Ideas
+
+* "An infinite deal of nothing", a variety of non-terminating loops each with
+  their own intrinsic computational rhythm.
+
+* Implement in untyped lambda calculus an interpreter for a known
+  Turing-complete tape mutation based language and run some simple programs
+  in it.
+
+    Illustrates Turing-completeness of untyped lambda calculus, albeit slowly.
+
+
+# EOF
+
+## EOF
+
+Thanks!
+
+Questions?
+
+    https://mathr.co.uk
+    mailto:claude@mathr.co.uk
+
+    https://hackage.haskell.org/package/gulcii
+    https://code.mathr.co.uk/gulcii
diff --git a/doc/encoding.tex b/doc/encoding.tex
new file mode 100644
--- /dev/null
+++ b/doc/encoding.tex
@@ -0,0 +1,31 @@
+\documentclass[aspectratio=43]{beamer}
+\usepackage{lmodern}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\DeclareUnicodeCharacter{03BB}{\(\lambda\)}
+\AtBeginSection[]{\begin{frame}\frametitle{Outline}\tableofcontents[currentsection]\end{frame}}
+\def\tightlist{}
+
+\definecolor{mathr}{RGB}{128,64,64}
+\setbeamercolor{structure}{fg=mathr}
+\setbeamercolor{title}{fg=mathr}
+\setbeamercolor{titlelike}{fg=mathr}
+\beamertemplatenavigationsymbolsempty
+
+\renewcommand{\familydefault}{\sfdefault}
+
+\title[GULCII]{Graphical\\ Untyped Lambda Calculus\\ Interactive Interpreter}
+\subtitle{(GULCII)}
+\author{Claude Heiland-Allen}
+\institute{\url{https://mathr.co.uk} \\ \url{mailto:claude@mathr.co.uk}}
+\date[Ed 2017]{Edinburgh, 2017}
+\subject{Computer Science}
+
+\begin{document}
+
+\begin{frame} \titlepage \end{frame}
+\begin{frame} \frametitle{Outline} \tableofcontents \end{frame}
+
+\input{encoding.md.tex}
+
+\end{document}
diff --git a/doc/visualisation.png b/doc/visualisation.png
new file mode 100644
Binary files /dev/null and b/doc/visualisation.png differ
diff --git a/extra/fudi2midi.pd b/extra/fudi2midi.pd
deleted file mode 100644
--- a/extra/fudi2midi.pd
+++ /dev/null
@@ -1,59 +0,0 @@
-#N canvas 0 0 547 342 10;
-#X obj 28 2 netreceive 8765;
-#X obj 29 172 noteout;
-#X msg 29 127 \$2 \$3 \$1;
-#X msg 35 148 \$2 0 \$1;
-#X obj 109 173 pgmout;
-#X msg 109 150 \$2 \$1;
-#X obj 176 173 ctlout;
-#X msg 177 150 \$3 \$2 \$1;
-#X msg 242 150 \$2 \$1;
-#X obj 242 171 touchout;
-#X msg 315 148 \$3 \$2 \$1;
-#X obj 315 169 polytouchout;
-#X msg 398 148 \$2 \$1;
-#X obj 398 169 bendout;
-#X obj 371 84 spigot;
-#X obj 404 18 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 1
-1;
-#X obj 158 1 print connection;
-#X obj 371 105 print unhandled;
-#X obj 416 44 spigot;
-#X obj 447 16 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 0
-1;
-#X obj 418 65 print debug;
-#X obj 29 48 route noteon noteoff program control pressure touch bend
-rebound;
-#X floatatom 116 29 5 0 0 0 - - -;
-#X obj 300 12 route rebound;
-#X obj 296 36 print midi;
-#X obj 297 -7 spigot;
-#X obj 342 -5 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 1
-1;
-#X connect 0 0 18 0;
-#X connect 0 0 21 0;
-#X connect 0 0 25 0;
-#X connect 0 1 16 0;
-#X connect 0 1 22 0;
-#X connect 2 0 1 0;
-#X connect 3 0 1 0;
-#X connect 5 0 4 0;
-#X connect 7 0 6 0;
-#X connect 8 0 9 0;
-#X connect 10 0 11 0;
-#X connect 12 0 13 0;
-#X connect 14 0 17 0;
-#X connect 15 0 14 1;
-#X connect 18 0 20 0;
-#X connect 19 0 18 1;
-#X connect 21 0 2 0;
-#X connect 21 1 3 0;
-#X connect 21 2 5 0;
-#X connect 21 3 7 0;
-#X connect 21 4 8 0;
-#X connect 21 5 10 0;
-#X connect 21 6 12 0;
-#X connect 21 8 14 0;
-#X connect 23 1 24 0;
-#X connect 25 0 23 0;
-#X connect 26 0 25 1;
diff --git a/extra/gulcii.pd b/extra/gulcii.pd
new file mode 100644
--- /dev/null
+++ b/extra/gulcii.pd
@@ -0,0 +1,29 @@
+#N canvas 3 58 335 369 10;
+#X obj 18 10 netreceive 8765;
+#X obj 21 101 loadbang;
+#X obj 21 122 delay 1000;
+#X msg 22 148 \; pd dsp 1;
+#X obj 121 40 print;
+#X obj 141 252 catch~ \$0-r;
+#X obj 70 209 gulcii_v \$0 0;
+#X obj 27 251 catch~ \$0-l;
+#X obj 19 40 s \$0-control;
+#X obj 168 126 list prepend set;
+#X obj 168 148 list trim;
+#X msg 168 170 rebound succ;
+#X obj 59 65 route statistics;
+#X obj 90 310 dac~;
+#X obj 27 273 expr~ tanh($v1);
+#X obj 142 275 expr~ tanh($v1);
+#X connect 0 0 8 0;
+#X connect 0 0 12 0;
+#X connect 0 1 4 0;
+#X connect 1 0 2 0;
+#X connect 2 0 3 0;
+#X connect 5 0 15 0;
+#X connect 7 0 14 0;
+#X connect 9 0 10 0;
+#X connect 10 0 11 0;
+#X connect 12 1 9 0;
+#X connect 14 0 13 0;
+#X connect 15 0 13 1;
diff --git a/extra/gulcii_m.pd b/extra/gulcii_m.pd
new file mode 100644
--- /dev/null
+++ b/extra/gulcii_m.pd
@@ -0,0 +1,29 @@
+#N canvas 3 58 450 300 10;
+#X obj 21 22 receive~ \$1-p;
+#X obj 20 218 throw~ \$1-l;
+#X obj 97 218 throw~ \$1-r;
+#X obj 21 134 expr~ sin($v1*6.283185307179586);
+#X obj 97 157 expr~ sin($v1*6.283185307179586);
+#X obj 147 19 inlet;
+#X obj 147 40 float;
+#X obj 147 61 vline~;
+#X obj 21 43 *~ \$2;
+#X obj 97 189 *~;
+#X obj 20 192 *~;
+#X obj 96 106 +~ 0.25;
+#X obj 147 82 hip~ 1;
+#X obj 147 103 lop~ 15;
+#X connect 0 0 8 0;
+#X connect 3 0 10 0;
+#X connect 4 0 9 0;
+#X connect 5 0 6 0;
+#X connect 6 0 7 0;
+#X connect 7 0 12 0;
+#X connect 8 0 3 0;
+#X connect 8 0 11 0;
+#X connect 9 0 2 0;
+#X connect 10 0 1 0;
+#X connect 11 0 4 0;
+#X connect 12 0 13 0;
+#X connect 13 0 9 1;
+#X connect 13 0 10 1;
diff --git a/extra/gulcii_v.pd b/extra/gulcii_v.pd
new file mode 100644
--- /dev/null
+++ b/extra/gulcii_v.pd
@@ -0,0 +1,78 @@
+#N canvas 3 63 472 453 10;
+#X obj 46 214 vline~;
+#X obj 37 392 *~;
+#X obj 125 392 *~;
+#X obj 182 246 send~ \$0-p;
+#X obj 127 312 +~;
+#X obj 143 267 catch~ \$0-l;
+#X obj 223 267 catch~ \$0-r;
+#X obj 209 312 +~;
+#X obj 127 345 expr~ sin($v1*6.283185307179586);
+#X obj 207 365 expr~ sin($v1*6.283185307179586);
+#X obj 18 43 route start stop statistics;
+#X obj 37 413 throw~ \$1-l;
+#X obj 125 413 throw~ \$1-r;
+#X obj 18 18 r \$1-control;
+#X obj 358 107 gulcii_m \$0 6;
+#X obj 358 128 gulcii_m \$0 5;
+#X obj 358 149 gulcii_m \$0 4;
+#X obj 358 170 gulcii_m \$0 3;
+#X obj 358 191 gulcii_m \$0 2;
+#X obj 358 212 gulcii_m \$0 1;
+#X obj 143 288 *~ 0.125;
+#X obj 224 288 *~ 0.125;
+#X obj 133 109 +;
+#X obj 163 109 +;
+#X obj 193 109 +;
+#X obj 223 109 +;
+#X obj 253 109 +;
+#X obj 132 136 vline~;
+#X obj 132 179 lop~ 15;
+#X obj 130 228 phasor~;
+#X obj 132 158 hip~ 1;
+#X obj 131 203 +~ 50;
+#X msg 18 166 1 1000;
+#X msg 80 168 0 1000;
+#X obj 143 68 unpack f f f f f f;
+#X connect 0 0 1 0;
+#X connect 0 0 2 0;
+#X connect 1 0 11 0;
+#X connect 2 0 12 0;
+#X connect 4 0 8 0;
+#X connect 5 0 20 0;
+#X connect 6 0 21 0;
+#X connect 7 0 9 0;
+#X connect 8 0 1 1;
+#X connect 9 0 2 1;
+#X connect 10 0 32 0;
+#X connect 10 1 33 0;
+#X connect 10 2 34 0;
+#X connect 13 0 10 0;
+#X connect 20 0 4 1;
+#X connect 21 0 7 1;
+#X connect 22 0 27 0;
+#X connect 23 0 22 1;
+#X connect 24 0 23 1;
+#X connect 25 0 24 1;
+#X connect 26 0 25 1;
+#X connect 27 0 30 0;
+#X connect 28 0 31 0;
+#X connect 29 0 3 0;
+#X connect 29 0 4 0;
+#X connect 29 0 7 0;
+#X connect 30 0 28 0;
+#X connect 31 0 29 0;
+#X connect 32 0 0 0;
+#X connect 33 0 0 0;
+#X connect 34 0 19 0;
+#X connect 34 0 22 0;
+#X connect 34 1 18 0;
+#X connect 34 1 23 0;
+#X connect 34 2 17 0;
+#X connect 34 2 24 0;
+#X connect 34 3 16 0;
+#X connect 34 3 25 0;
+#X connect 34 4 15 0;
+#X connect 34 4 26 0;
+#X connect 34 5 14 0;
+#X connect 34 5 26 1;
diff --git a/gulcii.cabal b/gulcii.cabal
--- a/gulcii.cabal
+++ b/gulcii.cabal
@@ -1,84 +1,73 @@
 Name:               gulcii
-Version:            0.2.0.3
+Version:            0.3
 Synopsis:           graphical untyped lambda calculus interactive interpreter
 Description:
   GULCII is an untyped lambda calculus interpreter supporting interactive
   modification of a running program with graphical display of graph reduction.
   .
-  There are three variants of lambda abstraction: lazy, strict, and copy:
-  .
-  @> \x . f x x    -- x is evaluated lazily with sharing@
-  @> \x ! f x x    -- x is evaluated strictly and shared@
-  @> \x ? f x x    -- x is copied before any evaluation@
-  .
-  There is additional syntax sugar for natural numbers and lists, using
-  <http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding#Scott_encoding>:
-  .
-  @> [0,1,2,3]@
-  .
-  There is a small standard library based loosely around the Haskell Prelude,
-  with additions geared towards MIDI generation for live-coding music, implemented
-  using a mechanism similar to 'Debug.Trace.trace':
-  .
-  @> \x y . &#123; print : x &#125; y@
-  .
-  Quick start:
-  .
-  > gulcii
-  > :load mars
-  > main
-  > :quit
-  .
-  If you have Pure-data and Timidity, try:
-  .
-  > timidity -iA -Oj &
-  > pd -alsamidi ~/.cabal/share/gulcii-0.2.0.3/extra/fudi2midi.pd &
-  > gulcii | pdsend 8765
-  .
-  See also: live-sequencer which has many more features (but no sharing during
-  evaluation).
+  See README.md for the user manual.
 
-Homepage:           http://code.mathr.co.uk/gulcii
+Homepage:           https://code.mathr.co.uk/gulcii
 License:            GPL-2
 License-file:       LICENSE
 Author:             Claude Heiland-Allen
 Maintainer:         claude@mathr.co.uk
-Category:           Sound, Music, GUI
+Category:           Compilers/Interpreters
 Build-type:         Simple
 Cabal-version:      >=1.6
-Tested-With:        GHC==7.6.3, GHC==7.8.2
+Tested-With:        GHC==8.2.1
 
-Data-files:         extra/fudi2midi.pd,
-                    lib/bits.gu,
+extra-source-files: doc/Makefile
+                    doc/encoding.md
+                    doc/encoding.tex
+                    doc/visualisation.png
+                    README.md
+
+Data-files:         lib/bits.gu,
                     lib/bool.gu,
+                    lib/church.gu,
                     lib/either.gu,
-                    lib/event.gu,
                     lib/function.gu,
                     lib/list.gu,
                     lib/maybe.gu,
-                    lib/midi.gu,
                     lib/natural.gu,
                     lib/pair.gu,
                     lib/prelude.gu,
-                    lib/mars.gu
+                    lib/edinburgh.gu,
+                    extra/gulcii.pd,
+                    extra/gulcii_m.pd,
+                    extra/gulcii_v.pd
 
 Executable gulcii
   HS-source-dirs:   src
   Main-is:          Main.hs
   Build-depends:    base >= 3 && < 6,
                     containers >= 0.3 && < 0.6,
-                    filepath >= 1.1 && < 1.4,
-                    gtk >= 0.11 && < 0.14,
+                    filepath >= 1.1 && < 1.5,
+                    gtk >= 0.11 && < 0.15,
                     cairo >= 0.11 && < 0.14
-  Other-modules:    Bruijn Command Draw Evaluation Graph Lambda Layout Meta Parse Sugar
+  Other-modules:    Bruijn
+                    Command
+                    Draw
+                    Evaluation
+                    GC
+                    Graph
+                    Lambda
+                    Layout
+                    Meta
+                    Parse
+                    Paths_gulcii
+                    Reduce
+                    Setting
+                    Sugar
   ghc-options:      -Wall -threaded -rtsopts
 --  ghc-prof-options: -prof -auto-all -caf-all
 
 Source-Repository head
   Type: git
-  Location: http://code.mathr.co.uk/gulcii.git
+  Location: https://code.mathr.co.uk/gulcii.git
 
 Source-Repository this
   Type: git
-  Tag: v0.2.0.3
-  Location: http://code.mathr.co.uk/gulcii.git
+  Tag: v0.3
+  Location: https://code.mathr.co.uk/gulcii.git
diff --git a/lib/church.gu b/lib/church.gu
new file mode 100644
--- /dev/null
+++ b/lib/church.gu
@@ -0,0 +1,33 @@
+id = \x . x
+const = \x y . x
+true = \t f . t
+false = \t f . f
+and = \a b . a b a
+or = \a b . a a b
+not = \a . a false true
+zero = \s z . z
+succ = \n s z . s (n s z)
+iszero = \n . n (const false) true
+add = \m n . m succ n
+mul = \m n . m (add n) zero
+exp = \m n . n m
+pred = \n s z . n (\g h . h (g s)) (\u . z) (\u . u)
+sub = \m n . n pred m
+equal = \m n . and (iszero (sub m n)) (iszero (sub n m))
+nil = \c n . n
+cons = \x xs c n . c x (xs c n)
+isnil = \l . l (\x xs . false) true
+head = \l . l (\x xs . x) id
+tail = \l c n . l (\x xs g . g x (xs c)) (\xs . n) (\x xs . xs)
+map = \f l . l (\x xs . cons (f x) xs) nil
+sum = \l . l (\x xs . add x xs) zero
+length = \l . l (\x xs . succ xs) zero
+pair = \a b p . p a b
+fst = \p . p (\a b . a)
+snd = \p . p (\a b . b)
+nothing = \n j . n
+just = \a n j . j a
+maybe = \n j m . m n j
+left = \a l r . l a
+right = \b l r . r b
+either = \l r e . e l r
diff --git a/lib/edinburgh.gu b/lib/edinburgh.gu
new file mode 100644
--- /dev/null
+++ b/lib/edinburgh.gu
@@ -0,0 +1,55 @@
+# boolean
+false = \ t f . f
+true = \ t f . t
+and = \ a b . a b a
+or = \ a b . a a b
+not = \ a . a false true
+# function
+id = \ a . a
+const = \ a b . a
+compose = \ bc ab a . bc (ab a)
+flip = \ abc b a . abc a b
+fix = \ f . (\x . f (x x)) (\x . f (x x))
+error = \e . error e
+seq = \ a ! \b . b
+# list
+nil = \ c n . n
+cons = \ x xs c n . c x xs
+null = \ l . l (\x xs . false) true
+head = \ l . l (\x xs . x) (error head)
+tail = \ l . l (\x xs . xs) (error tail)
+map = \ f l . l (\x xs . cons (f x) (map f xs)) nil
+append = \ us vs . us (\x xs . cons x (append xs vs)) vs
+filter = \ p l . l (\x xs . p x (cons x) id (filter p xs)) nil
+index = \ l n . n (\p . l (\x xs . index xs p) (error index)) (l (\x xs . x) (error index))
+reverse = \ l . l (\x xs . append (reverse xs) (cons x nil)) nil
+foldr = \ f e l . l (\x xs . f x (foldr f e xs)) e
+length = foldr (const succ) zero
+ands = foldr and true
+ors = foldr or false
+concat = foldr append nil
+all = \f . compose ands (map f)
+any = \f . compose ors (map f)
+concatMap = \f . compose concat (map f)
+composes = foldr compose id
+sum = foldr add zero
+product = foldr mul (succ zero)
+repeat = \x . cons x (repeat x)
+cycle = compose concat repeat
+take = \n l . n (\p . l (\x xs . cons x (take p xs)) nil) nil
+drop = \n l . n (\p . l (\x xs . drop p xs) nil) l
+transpose = \l . l (\xs xss . xs (\y ys . cons (cons y (concatMap (take 1) xss)) (transpose (cons ys (map (drop 1) xss)))) (transpose xss)) nil
+iterate = \f x . cons x (iterate f (f x))
+last = \l . l (\x xs . xs (\y ys . last xs) x) (error last)
+replicate = \n x . take n (repeat x)
+# natural
+zero = \ s z . z
+succ = \ n s z . s n
+infinity = succ infinity
+even = \n . n odd true
+odd = \n . n even false
+add = \ m n . m (\p . succ (add n p)) n
+mul = \ m n . m (\p . add n (mul n p)) zero
+exp = \ m n . n (\p . mul m (exp m p)) one
+sub = \ m n . m (\p . n (sub p) m) zero
+equal = \ m n . m (\mm . n (\nn . equal mm nn) false) (n (\nn . false) true)
diff --git a/lib/event.gu b/lib/event.gu
deleted file mode 100644
--- a/lib/event.gu
+++ /dev/null
@@ -1,6 +0,0 @@
-# event
-wait = \n w e . w n
-event = \x w e . e x
-merge = \al bl . al (\a as . bl (\b bs . a (\aw . b (\bw . lessthan aw bw (cons a (merge as (cons (wait (sub bw aw)) bs))) (cons b (merge (cons (wait (sub aw bw)) as) bs))) (\e . cons b (merge al bs))) (\e . cons a (merge as bl))) al) bl
-merges = foldr merge nil
-play = \l . l (\x xs . x (\w . { wait : w } (play xs)) (\e . e (play xs))) (error play)
diff --git a/lib/mars.gu b/lib/mars.gu
deleted file mode 100644
--- a/lib/mars.gu
+++ /dev/null
@@ -1,5 +0,0 @@
-:load prelude
-main = play (cons (event (program 0 48)) timpanis)
-timpanis = append timpani timpanis
-timpani = concatMap makeNote [20,20,20,60,60,30,30,60]
-makeNote = \d ! note d 0 43 96
diff --git a/lib/midi.gu b/lib/midi.gu
deleted file mode 100644
--- a/lib/midi.gu
+++ /dev/null
@@ -1,7 +0,0 @@
-# midi
-noteOn = \c n v ! \x . { noteon : [c, n, v] } x
-noteOff = \c n v ! \x . { noteoff : [c, n, v] } x
-program = \c p ! \x . { program : [c, p] } x
-control = \c p v ! \x . { control : [c, p, v] } x
-note = \d ! \c n v . [ event (noteOn c n v), wait d, event (noteOff c n v) ]
-rest = \d ! [ wait d ]
diff --git a/lib/prelude.gu b/lib/prelude.gu
--- a/lib/prelude.gu
+++ b/lib/prelude.gu
@@ -1,10 +1,8 @@
 :load bits
 :load bool
 :load either
-:load event
 :load function
 :load list
 :load maybe
-:load midi
 :load natural
 :load pair
diff --git a/src/Bruijn.hs b/src/Bruijn.hs
--- a/src/Bruijn.hs
+++ b/src/Bruijn.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -17,7 +17,7 @@
     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 -}
 
-module Bruijn (Term(..), bruijn, freeVariablesIn, bind) where
+module Bruijn (Term(..), bruijn, freeVariablesIn) where
 
 import Data.Maybe (listToMaybe)
 import Data.Set (Set, empty, singleton, union)
@@ -27,10 +27,10 @@
 
 data Term
   = Free String
-  | Bound Integer
+  | Bound0
+  | Scope Term
   | Lambda Strategy Term
   | Apply Term Term
-  | Trace String Term Term
   deriving (Read, Show, Eq, Ord)
 
 bruijn :: U.Term -> Term
@@ -42,25 +42,19 @@
 bruijn' m (U.Variable v) =
   case genericElemIndex v m of
     Nothing -> Free v
-    Just i -> Bound i
-bruijn' m (U.Trace k s t) = Trace k (bruijn' m s) (bruijn' m t)
-
-bind :: Strategy -> String -> Term -> Term
-bind k v t = Lambda k (bind' 0 v t)
+    Just i -> applyN i Scope Bound0
 
-bind' :: Integer -> String -> Term -> Term
-bind' i v f@(Free u) = if u == v then Bound i else f
-bind' _ _ b@(Bound _) = b
-bind' i v (Apply s t) = Apply (bind' i v s) (bind' i v t)
-bind' i v (Lambda _ t) = bind' (i + 1) v t
-bind' i v (Trace k s t) = Trace k (bind' i v s) (bind' i v t)
+applyN :: Integer -> (a -> a) -> a -> a
+applyN n f
+  | n == 0 = id
+  | otherwise = f . applyN (n - 1) f
 
 freeVariablesIn :: Term -> Set String
 freeVariablesIn (Free v) = singleton v
-freeVariablesIn (Bound _) = empty
+freeVariablesIn Bound0 = empty
+freeVariablesIn (Scope t) = freeVariablesIn t
 freeVariablesIn (Lambda _ t) = freeVariablesIn t
 freeVariablesIn (Apply s t) = freeVariablesIn s `union` freeVariablesIn t
-freeVariablesIn (Trace _ s t) = freeVariablesIn s `union` freeVariablesIn t
 
 {-
 Generic list functions.
diff --git a/src/Command.hs b/src/Command.hs
--- a/src/Command.hs
+++ b/src/Command.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -25,11 +25,10 @@
 import qualified Meta as M
 import Parse
 
-data Command = Define String S.Term | Evaluate S.Term | Execute S.Term | Meta M.Meta
+data Command = Define String S.Term | Evaluate S.Term | Meta M.Meta
   deriving (Read, Show, Eq, Ord)
 
 parse :: Parser String Command
 parse =  (Define   <$> name <* sym "=" <*> S.parse)
      <|> (Evaluate <$> S.parse)
-     <|> (Execute  <$  sym "~" <*> S.parse)
      <|> (Meta     <$  sym ":" <*> M.parse)
diff --git a/src/Draw.hs b/src/Draw.hs
--- a/src/Draw.hs
+++ b/src/Draw.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -19,11 +19,10 @@
 
 module Draw (draw) where
 
-import Data.List (genericDrop)
 import qualified Data.Map.Strict as M
 import Data.Map.Strict (Map)
 
-import Graphics.Rendering.Cairo
+import Graphics.Rendering.Cairo hiding (x, y)
 
 import qualified Layout as L
 import Evaluation (Strategy(..))
@@ -32,14 +31,14 @@
 
 colour :: L.Term -> RGB
 colour (L.Free      _ _) = (0, 0.5, 1)
-colour (L.Bound     _ _) = (0.5, 0, 1)
+colour (L.Bound0      _) = (0.5, 0, 1)
+colour (L.Scope     _ _) = (1, 1, 0)
 colour (L.Lambda Strict _ _) = (1, 0, 0)
 colour (L.Lambda Lazy   _ _) = (1, 0, 0.5)
 colour (L.Lambda Copy   _ _) = (1, 0, 1)
 colour (L.Apply   _ _ _) = (1, 0.5, 0)
 colour (L.RefInst _ _ _) = (0.5, 1, 0)
 colour (L.Reference _ _) = (0, 1, 0.5)
-colour (L.Trace _ _ _ _) = (1, 1, 0)
 
 circle :: L.Coords -> RGB -> Render ()
 circle (x, y) (r, g, b) = do
@@ -94,54 +93,53 @@
   e <- textExtents s
   moveTo (fromIntegral x - textExtentsWidth e / 2) (fromIntegral y)
   textPath s
-drawNames (L.Bound _ _) = return ()
+drawNames (L.Bound0 _) = return ()
+drawNames (L.Scope t _) = drawNames t
 drawNames (L.Lambda _ t _) = drawNames t
 drawNames (L.Apply a b _) = drawNames a >> drawNames b
 drawNames (L.RefInst _ t _) = drawNames t
 drawNames (L.Reference _ _) = return ()
-drawNames (L.Trace s a b (x,y)) = do
-  e <- textExtents s
-  moveTo (fromIntegral x - textExtentsWidth e / 2) (fromIntegral y)
-  textPath s
-  drawNames a
-  drawNames b
 
 drawLinks :: Map Integer L.Coords -> L.Term -> Render ()
-drawLinks _  (L.Free _ _) = return ()
-drawLinks _  (L.Bound _ _) = return ()
-drawLinks ps (L.Lambda _ t xy) = let x'y' = L.coordinates t
-                                 in line xy x'y' >> drawLinks ps t
-drawLinks ps (L.Apply a b xy) = let axay = L.coordinates a
-                                    bxby = L.coordinates b
-                                in line xy axay >> line xy bxby >> drawLinks ps a >> drawLinks ps b
-drawLinks ps (L.RefInst _ t xy) = let x'y' = L.coordinates t
-                                  in line xy x'y' >> drawLinks ps t
-drawLinks ps (L.Reference p xy) = let Just x'y' = M.lookup p ps
-                                  in line xy x'y'
-drawLinks ps (L.Trace _ a b xy) =
+drawLinks _  (L.Free _ _) =
+  return ()
+drawLinks _  (L.Bound0 _) =
+  return ()
+drawLinks ps (L.Scope t xy) =
+  let x'y' = L.coordinates t
+  in  line xy x'y' >> drawLinks ps t
+drawLinks ps (L.Lambda _ t xy) =
+  let x'y' = L.coordinates t
+  in  line xy x'y' >> drawLinks ps t
+drawLinks ps (L.Apply a b xy) =
   let axay = L.coordinates a
       bxby = L.coordinates b
   in  line xy axay >> line xy bxby >> drawLinks ps a >> drawLinks ps b
+drawLinks ps (L.RefInst _ t xy) =
+  let x'y' = L.coordinates t
+  in  line xy x'y' >> drawLinks ps t
+drawLinks ps (L.Reference p xy) =
+  let Just x'y' = M.lookup p ps
+  in  line xy x'y'
 
 drawVLinks :: [L.Coords] -> L.Term -> Render ()
-drawVLinks ls (L.Bound n xy) =
-  case genericDrop n ls of
-    [] -> return ()
-    x'y':_ -> line xy x'y'
+drawVLinks ls (L.Bound0 xy) = case ls of
+  [] -> return () -- should be error?
+  x'y':_ -> line xy x'y'
+drawVLinks ls (L.Scope t _) = drawVLinks (drop 1 ls) t
 drawVLinks ls (L.Lambda _ t xy) = drawVLinks (xy : ls) t
 drawVLinks ls (L.Apply  s t _) = drawVLinks ls s >> drawVLinks ls t
 drawVLinks ls (L.RefInst _ t _) = drawVLinks ls t
-drawVLinks ls (L.Trace _ s t _) = drawVLinks ls s >> drawVLinks ls t
 drawVLinks _ _ = return ()
 
 drawNodes :: L.Term -> Render ()
 drawNodes n@(L.Free      _ _) = drawNode n
-drawNodes n@(L.Bound     _ _) = drawNode n
+drawNodes n@(L.Bound0      _) = drawNode n
+drawNodes n@(L.Scope     t _) = drawNode n >> drawNodes t
 drawNodes n@(L.Lambda  _ t _) = drawNode n >> drawNodes t
 drawNodes n@(L.Apply   a b _) = drawNode n >> drawNodes a >> drawNodes b
 drawNodes n@(L.RefInst _ t _) = drawNode n >> drawNodes t
 drawNodes n@(L.Reference _ _) = drawNode n
-drawNodes n@(L.Trace _ a b _) = drawNode n >> drawNodes a >> drawNodes b
 
 drawNode :: L.Term -> Render ()
 drawNode n = circle (L.coordinates n) (colour n)
diff --git a/src/GC.hs b/src/GC.hs
new file mode 100644
--- /dev/null
+++ b/src/GC.hs
@@ -0,0 +1,85 @@
+{-
+    gulcii -- graphical untyped lambda calculus interpreter
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+-}
+
+module GC (gc) where
+
+import Graph
+
+import Data.Map as Map
+
+gc
+  :: References -> Term
+  -> (References, Term)
+
+gc refs term
+  = let counts = refCount refs term Map.empty
+    in ( Map.fromList
+           [ (r, compact counts refs (refs Map.! r))
+           | (r, n) <- Map.toList counts
+           , n > 1 ]
+        , compact counts refs term )
+
+
+type Count = Integer
+
+refCount
+  :: References -> Term
+  -> Map Integer Count -> Map Integer Count
+
+compact
+  :: Map Integer Count -> References
+  -> Term -> Term
+
+
+refCount refs (Scope a) counts
+  = refCount refs a counts
+
+refCount refs (Lambda _ a) counts
+  = refCount refs a counts
+
+refCount refs (Apply a b) counts
+  = refCount refs a (refCount refs b counts)
+
+refCount refs (Reference r) counts
+  = case r `Map.lookup` counts of
+      Just n ->
+        Map.insert r (n + 1) counts
+      Nothing ->
+        refCount refs (refs Map.! r)
+               (Map.insert r 1 counts)
+
+refCount _ _ counts = counts
+
+
+compact counts refs (Scope term)
+  = Scope (compact counts refs term)
+
+compact counts refs (Lambda strat term)
+  = Lambda strat (compact counts refs term)
+
+compact counts refs (Apply a b)
+  = Apply (compact counts refs a)
+          (compact counts refs b)
+
+compact counts refs term@(Reference r)
+  = case r `Map.lookup` counts of
+      Just 1 -> compact counts refs (refs Map.! r)
+      _ -> term
+
+compact _ _ term = term
diff --git a/src/Graph.hs b/src/Graph.hs
--- a/src/Graph.hs
+++ b/src/Graph.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -17,9 +17,8 @@
     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 -}
 
-module Graph (Term(..), Definitions, References, Reduction(..), graph, reduce, pretty) where
+module Graph (Term(..), Definitions, References, graph, pretty) where
 
-import qualified Data.Map.Strict as M
 import Data.Map.Strict (Map)
 
 import qualified Bruijn as B
@@ -27,23 +26,23 @@
 
 data Term
   = Free !String
-  | Bound !Integer
+  | Bound0
+  | Scope !Term
   | Lambda !Strategy !Term
   | Apply !Term !Term
   | Reference !Integer
-  | Trace !String !Term !Term
   deriving (Read, Show, Eq, Ord)
 
 pretty :: Term -> String
-pretty = unwords . pretty'
+pretty = concat . pretty'
 
 pretty' :: Term -> [String]
 pretty' (Free s) = [s]
-pretty' (Bound i) = [show i]
+pretty' (Bound0) = ["0"]
+pretty' (Scope t) = ["S"] ++ pretty' t
 pretty' (Reference i) = ['#':show i]
 pretty' (Lambda k t) = ["(", "\\", pretty'' k] ++ pretty' t ++ [")"]
-pretty' (Apply s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]
-pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]
+pretty' (Apply s t) = ["("] ++ pretty' s ++ [" "] ++ pretty' t ++ [")"]
 
 pretty'' :: Strategy -> String
 pretty'' Strict = "!"
@@ -53,96 +52,9 @@
 type Definitions = Map String Term
 type References = Map Integer Term
 
-next :: Map Integer a -> Integer
-next refs = case M.maxViewWithKey refs of
-  Nothing        -> 0
-  Just ((k,_),_) -> k + 1
-
 graph :: B.Term -> Term
 graph (B.Free v) = Free v
-graph (B.Bound i) = Bound i
+graph (B.Bound0) = Bound0
+graph (B.Scope t) = Scope (graph t)
 graph (B.Lambda k t) = Lambda k (graph t)
 graph (B.Apply s t) = Apply (graph s) (graph t)
-graph (B.Trace k s t) = Trace k (graph s) (graph t)
-
-{-
-bind :: String -> Term -> Term -> Term
-bind v s t@(Free u) = if u == v then s else t
-bind _ _ t@(Bound _) = t
-bind v s (Lambda k t) = Lambda k (bind v s t)
-bind v s (Apply a b) = Apply (bind v s a) (bind v s b)
-bind _ _ t@(Reference _) = t
--}
-
-{-
-Reduce a graph one step, returning Nothing if it is irreducible.
--}
-
-data Reduction = Reduced Term References | Rebound String Term References | Traced String Term Term References
-  deriving (Read, Show, Eq, Ord)
-
-mapR :: (Term -> Term) -> Reduction -> Reduction
-mapR f (Reduced t refs) = Reduced (f t) refs
-mapR f (Rebound s t refs) = Rebound s (f t) refs
-mapR f (Traced k s t refs) = Traced k s (f t) refs
-
-reduce, reduce' :: Definitions -> References -> Term -> Maybe Reduction
-reduce _ refs (Trace k s t) = Just (Traced k s t refs)
-reduce defs refs term = reduce' defs refs term
-
--- free variables are replaced with their definition
-reduce' defs refs (Free v) = case M.lookup v defs of
-  Nothing -> Nothing
-  Just t -> let r = next refs in Just (Rebound v (Reference r) (M.insert r t refs))
-
--- bound variables are irreducible
-reduce' _ _ (Bound _) = Nothing
-
--- non top-level traces are irreducible?
---reduce' _ _ (Trace _ _ _) = Nothing
-reduce' _ refs (Trace k s t) = Just (Traced k s t refs)
-
--- maybe reduce inside lambda
-reduce' defs refs (Lambda k t) = mapR (Lambda k) `fmap` reduce' defs refs t
-
-reduce' defs refs (Apply a b) = case a of
-  -- beta reduction
-  Lambda Strict a' -> case reduce defs refs b of
-    Just r -> Just (mapR (a `Apply`) r)
-    Nothing -> Just (uncurry Reduced (beta refs a' b))
-  Lambda Copy a' -> Just (Reduced (beta' 0 a' b) refs)
-  Lambda Lazy a' -> Just (uncurry Reduced (beta refs a' b))
-  Reference r -> case M.lookup r refs of
-    Just a' -> Just (Reduced (Apply a' b) refs)
-    _ -> Nothing
-  Free s -> case M.lookup s defs of
-    Just a' -> Just (Rebound s (Apply a' b) refs)
-    _ -> Nothing
-  t@(Apply _ _) -> case reduce defs refs t of
-    Just r -> Just (mapR (`Apply` b) r)
-    _ -> Nothing
-  _ -> Nothing -- Bound, Trace
-
--- reduce references
-reduce' defs refs s@(Reference r) = case M.lookup r refs of
-  Nothing -> Nothing
-  Just t -> case reduce' defs refs t of
-    Just (Reduced t' refs') -> Just (Reduced s (M.insert r t' refs'))
-    Just (Rebound v t' refs') -> Just (Rebound v s (M.insert r t' refs'))
-    _ -> Just (Reduced t refs)
-
--- beta reduction
-beta :: References -> Term -> Term -> (Term, References)
-beta refs a b = (beta' 0 a t, refs')
-  where
-    r = next refs
-    refs' = M.insert r b refs
-    t = Reference r
-
-beta' :: Integer -> Term -> Term -> Term
-beta' i s@(Bound j) t = if i == j then t else s
-beta' i (Lambda k s) t = Lambda k (beta' (i + 1) s t)
-beta' i (Apply a b) t = Apply (beta' i a t) (beta' i b t)
-beta' _ s@(Free _) _ = s
-beta' _ s@(Reference _) _ = s
-beta' i (Trace k a b) t = Trace k (beta' i a t) (beta' i b t)
diff --git a/src/Lambda.hs b/src/Lambda.hs
--- a/src/Lambda.hs
+++ b/src/Lambda.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -31,7 +31,6 @@
   = Variable String
   | Lambda Strategy String Term
   | Apply Term Term
-  | Trace String Term Term
   deriving (Read, Show, Eq, Ord)
 
 {-
@@ -45,7 +44,6 @@
 pretty' (Variable v) = [v]
 pretty' (Lambda k v t) = ["(", "\\", v, pretty'' k] ++ pretty' t ++ [")"]
 pretty' (Apply  s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]
-pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]
 
 pretty'' :: Strategy -> String
 pretty'' Strict = "!"
@@ -60,7 +58,6 @@
 isFreeIn n (Variable v)  = n == v
 isFreeIn n (Lambda _ v t)  = if n == v then False else n `isFreeIn` t
 isFreeIn n (Apply t t')  = n `isFreeIn` t || n `isFreeIn` t'
-isFreeIn n (Trace _ t t')  = n `isFreeIn` t || n `isFreeIn` t'
 
 {-
 Get all variable names defined or referenced by a term.
@@ -70,7 +67,6 @@
 variablesIn (Variable v)  = [v]
 variablesIn (Lambda _ v t)  = nub $ v : variablesIn t
 variablesIn (Apply t t')  = nub $ variablesIn t ++ variablesIn t'
-variablesIn (Trace _ t t')  = nub $ variablesIn t ++ variablesIn t'
 
 {-
 Get all free variables referenced by a term.
diff --git a/src/Layout.hs b/src/Layout.hs
--- a/src/Layout.hs
+++ b/src/Layout.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -17,7 +17,7 @@
     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 -}
 
-module Layout (Term(..), Coords, Layout(..), layout, coordinates) where
+module Layout (Term(..), Coords, Layout(..), layout, coordinates, Counts(..), counts) where
 
 import qualified Data.Map.Strict as M
 import Data.Map.Strict (Map)
@@ -29,12 +29,12 @@
 
 data Term
   = Free String Coords
-  | Bound Integer Coords
+  | Bound0 Coords
+  | Scope Term Coords
   | Lambda Strategy Term Coords
   | Apply Term Term Coords
   | RefInst Integer Term Coords
   | Reference Integer Coords
-  | Trace String Term Term Coords
   deriving (Read, Show, Eq, Ord)
 
 data Layout = Layout Term Integer Integer (Map Integer Coords)
@@ -42,33 +42,63 @@
 
 coordinates :: Term -> Coords
 coordinates (Free      _ xy) = xy
-coordinates (Bound     _ xy) = xy
+coordinates (Bound0      xy) = xy
+coordinates (Scope     _ xy) = xy
 coordinates (Lambda  _ _ xy) = xy
 coordinates (Apply   _ _ xy) = xy
 coordinates (RefInst _ _ xy) = xy
 coordinates (Reference _ xy) = xy
-coordinates (Trace _ _ _ xy) = xy
 
 layout :: G.Term -> G.References -> Layout
 layout = layout' (0, 0) M.empty
 
 layout' :: Coords -> Map Integer Coords -> G.Term -> G.References -> Layout
-layout' xy ps (G.Free v) _ = Layout (Free v xy) 1 1 ps
-layout' xy ps (G.Bound v) _ = Layout (Bound v xy) 1 1 ps
-layout' (x,y) ps (G.Lambda k t) g = let Layout lt w h ps' = layout' (x, y + 1) ps t g
-                                        (px, _) = coordinates lt
-                                    in  Layout (Lambda k lt (px, y)) w (h + 1) ps'
-layout' (x,y) ps (G.Apply a b) g = let Layout la aw ah psa = layout' (x, y + 1) ps a g
-                                       Layout lb bw bh psb = layout' (x + aw + 1, y + 1) psa b g
-                                   in  Layout (Apply la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb
-layout' xy@(x,y) ps (G.Reference p) g = if p `M.member` ps
-                                 then Layout (Reference p xy) 1 1 ps
-                                 else case M.lookup p g of
-                                        Nothing -> error $ "layout': bad pointer: " ++ show p
-                                        Just t  -> let Layout lt w h pst = layout' (x, y + 1) ps t g
-                                                       (px, py) = coordinates lt
-                                                   in Layout (RefInst p lt (px, y)) w (1 + h) (M.insert p (px, py) pst)
-layout' (x,y) ps (G.Trace s a b) g =
+layout' xy ps (G.Free v) _ =
+  Layout (Free v xy) 1 1 ps
+layout' xy ps (G.Bound0) _ =
+  Layout (Bound0 xy) 1 1 ps
+layout' (x, y) ps (G.Scope t) g =
+  let Layout lt w h ps' = layout' (x, y + 1) ps t g
+      (px, _) = coordinates lt
+  in  Layout (Scope lt (px, y)) w (h + 1) ps'
+layout' (x,y) ps (G.Lambda k t) g =
+  let Layout lt w h ps' = layout' (x, y + 1) ps t g
+      (px, _) = coordinates lt
+  in  Layout (Lambda k lt (px, y)) w (h + 1) ps'
+layout' (x,y) ps (G.Apply a b) g =
   let Layout la aw ah psa = layout' (x, y + 1) ps a g
       Layout lb bw bh psb = layout' (x + aw + 1, y + 1) psa b g
-  in  Layout (Trace s la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb
+  in  Layout (Apply la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb
+layout' xy@(x,y) ps (G.Reference p) g =
+  if p `M.member` ps
+    then Layout (Reference p xy) 1 1 ps
+    else case M.lookup p g of
+      Nothing -> error $ "layout': bad pointer: " ++ show p
+      Just t  ->
+        let Layout lt w h pst = layout' (x, y + 1) ps t g
+            (px, py) = coordinates lt
+        in  Layout (RefInst p lt (px, y)) w (1 + h) (M.insert p (px, py) pst)
+
+data Counts = Counts
+  { nFree, nBound0, nScope, nLambda, nApply, nRefInst, nReference :: !Int }
+
+instance Monoid Counts where
+  mempty = Counts 0 0 0 0 0 0 0
+  mappend c d = Counts
+                  { nFree = nFree c + nFree d
+                  , nBound0 = nBound0 c + nBound0 d
+                  , nScope = nScope c + nScope d
+                  , nLambda = nLambda c + nLambda d
+                  , nApply = nApply c + nApply d
+                  , nRefInst = nRefInst c + nRefInst d
+                  , nReference = nReference c + nReference d
+                  }
+
+counts :: Term -> Counts
+counts (Free _ _) = mempty{ nFree = 1 }
+counts (Bound0 _) = mempty{ nBound0 = 1 }
+counts (Scope t _) =  let c = counts t in c{ nScope = nScope c + 1 }
+counts (Lambda _ t _) = let c = counts t in c{ nLambda = nLambda c + 1 }
+counts (Apply a b _) = let c = counts a ; d = counts b in mappend c d
+counts (RefInst _ t _) = let c = counts t in c{ nRefInst = nRefInst c + 1 }
+counts (Reference _ _) = mempty{ nReference = 1 }
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -19,30 +19,34 @@
 
 module Main (main) where
 
-import Control.Applicative ((<$>), (<*>))
-import Control.Concurrent (forkIO, killThread, threadDelay, Chan, newChan, readChan, writeChan)
-import Control.Monad (forever, when)
+import Control.Applicative ((<$>))
+import Control.Concurrent (forkIO, killThread, threadDelay, newChan, readChan, writeChan)
+import Control.Monad (forever, when, unless, forM_)
 import qualified Data.Map.Strict as M
-import Data.Map.Strict (Map)
+import Data.Maybe (isJust)
 import Data.IORef (IORef, newIORef, readIORef, writeIORef, atomicModifyIORef)
 import System.IO (hSetBuffering, BufferMode(LineBuffering), stdout)
 import System.IO.Error (catchIOError)
 import System.FilePath ((</>), (<.>))
-import Graphics.UI.Gtk hiding (Meta)
-import Graphics.Rendering.Cairo
+import Graphics.UI.Gtk hiding (Meta, Settings)
+import Graphics.Rendering.Cairo hiding (width, height)
 
 import Paths_gulcii (getDataFileName)
 
 import qualified Command as C
 import qualified Meta as M
+import Setting (Settings)
+import qualified Setting
 import qualified Sugar as S
 import qualified Bruijn as B
 import qualified Graph as G
+import qualified GC as GC
+import qualified Reduce as R
 import qualified Layout as L
 import qualified Draw as D
 import qualified Parse as P
 
-data Interpret = Fail | Skip | Define String G.Term | Pure G.Term | Run G.Term | Meta M.Meta
+data Interpret = Fail | Skip | Define String G.Term | Pure G.Term | Meta M.Meta
   deriving (Read, Show, Eq, Ord)
 
 interpret :: String -> Interpret
@@ -56,26 +60,32 @@
       case S.desugar sterm of
         Just term -> Pure . G.graph . B.bruijn $ term
         _ -> Fail
-    Just ((C.Execute sterm, []):_) ->
-      case S.desugar sterm of
-        Just term -> Run . G.graph . B.bruijn $ term
-        _ -> Fail
     Just ((C.Meta m, []):_) -> Meta m
     Just [] -> Skip
     _ -> Fail
 
 main :: IO ()
 main = do
-  _args <- initGUI
+  args <- initGUI
+  let (width, height, fullscreen) = case args of
+        [w,h,"fullscreen"] -> (read w, read h, True)
+        [w,h] -> (read w, read h, False)
+        _ -> (1280, 720, False)
   envR <- newIORef M.empty
   lRef <- newIORef Nothing
   evalR <- newIORef Nothing
+  settingsR <- newIORef Setting.defaults
   outC <- newChan
-  _ <- forkIO $ outputter outC
   let out = writeChan outC
   win <- windowNew
   _ <- onDestroy win mainQuit
-  windowSetDefaultSize win 1024 720
+  windowSetDefaultSize win width height
+  when fullscreen $ do
+    windowSetGeometryHints win (Nothing `asTypeOf` Just win)
+      (Just (width, height)) (Just (width, height)) Nothing Nothing Nothing
+    set win [ windowDecorated := False ]
+    windowSetKeepAbove win True
+    windowMove win 0 0
   vb <- vBoxNew False 0
   hb <- hPanedNew
   tt <- textTagTableNew
@@ -115,7 +125,7 @@
   _ <- da `on` exposeEvent $ do
     dw <- eventWindow
     liftIO $ do
-      ml <- atomicModifyIORef lRef (\m -> (m, m))
+      ml <- atomicModifyIORef lRef (\m -> (Nothing, m))
       case ml of
         Nothing -> return ()
         Just l -> do
@@ -124,7 +134,7 @@
             D.draw (fromIntegral ww) (fromIntegral hh) l
     return True
   en <- entryNew
-  entrySetWidthChars en 24
+  entrySetWidthChars en 25
   font <- fontDescriptionFromString "Monospaced 18"
   widgetModifyFont tv (Just font)
   widgetModifyFont en (Just font)
@@ -133,8 +143,13 @@
   containerAdd sw tv
   al <- alignmentNew 1 0 1 1
   set al [ containerChild := da ]
-  boxPackStart vb en PackNatural 0
-  boxPackStart vb sw PackGrow 0
+  if Setting.newsOnTop Setting.defaults
+    then do
+      boxPackStart vb en PackNatural 0
+      boxPackStart vb sw PackGrow 0
+    else do
+      boxPackStart vb sw PackGrow 0
+      boxPackStart vb en PackNatural 0
   panedPack1 hb vb False True
   panedPack2 hb al True True
   set win [ containerChild := hb ]
@@ -142,6 +157,7 @@
   let scrollDown = do
         textViewScrollToMark tv mk 0 Nothing
       addText tag txt = do
+        newsOnTop <- Setting.newsOnTop <$> readIORef settingsR
         start' <- textBufferGetIterAtOffset tb 0
         end' <- textBufferGetIterAtOffset tb (-1)
         textBufferDelete tb start' end'
@@ -149,9 +165,10 @@
         start <- textBufferGetIterAtOffset tb 0
         end <- textBufferGetIterAtOffset tb (-1)
         textBufferApplyTag tb tag start end
-        pos <- textBufferGetIterAtOffset tf (-1)
+        pos <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)
         textBufferInsertRange tf pos start end
-        textBufferMoveMark tf mk pos
+        pos' <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)
+        textBufferMoveMark tf mk pos'
   _ <- en `onEntryActivate` do
     let exec echo txt =
           case interpret txt of
@@ -172,21 +189,25 @@
               case mtid of
                 Nothing -> return ()
                 Just tid -> killThread tid
-              tid <- forkIO $ evaluator 10000 lRef out envR M.empty term goPure
+              tid <- forkIO $ evaluator "gulcii-" 0 settingsR 500000 lRef out envR M.empty term goPure
               writeIORef evalR (Just tid)
-            Run term -> do
+            Meta M.Start -> do
               when echo $ do
-                addText tagInputRun txt
+                addText tagInputMeta txt
                 entrySetText en ""
-              mtid <- readIORef evalR
-              case mtid of
-                Nothing -> return ()
-                Just tid -> killThread tid
-              tid <- forkIO $ evaluator 10000 lRef out envR M.empty term (goRun (postGUIAsync . addText tagOutput))
-              writeIORef evalR (Just tid)
+              _ <- forkIO $ do
+                out "start;"
+              return ()
+            Meta M.Stop -> do
+              when echo $ do
+                addText tagInputMeta txt
+                entrySetText en ""
+              _ <- forkIO $ do
+                out "stop;"
+              return ()
             Meta M.Quit -> do
               _ <- forkIO $ do
-                out "quit ;"
+                out "quit;"
                 postGUISync mainQuit
               return ()
             Meta M.Clear -> do
@@ -212,10 +233,45 @@
                   mapM_ (exec False) (lines t)
                 Left e ->
                   addText tagError e
+            Meta (M.Get s) -> do
+              when echo $ do
+                addText tagInputMeta txt
+                entrySetText en ""
+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
+            Meta (M.Set s) -> do
+              when echo $ do
+                addText tagInputMeta txt
+                entrySetText en ""
+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s True ss, ()))
+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
+            Meta (M.UnSet s) -> do
+              when echo $ do
+                addText tagInputMeta txt
+                entrySetText en ""
+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s False ss, ()))
+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
+            Meta (M.Toggle s) -> do
+              when echo $ do
+                addText tagInputMeta txt
+                entrySetText en ""
+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s (not (Setting.get s ss)) ss, ()))
+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR
     txt <- entryGetText en
     exec True txt
     scrollDown
-  _ <- flip timeoutAdd 100 $ widgetQueueDraw da >> return True
+
+  _ <- forkIO $ do
+        hSetBuffering stdout LineBuffering
+        forever $ do
+          settings <- readIORef settingsR
+          s <- readChan outC
+          when (Setting.echoToStdOut settings) $ putStrLn s
+          when (Setting.echoToGUI    settings) $ postGUIAsync (addText tagOutput s >> scrollDown)
+
+  _ <- flip timeoutAdd 10 $ do
+    ml <- atomicModifyIORef lRef (\m -> (m, m))
+    when (isJust ml) $ widgetQueueDraw da
+    return True
   widgetShowAll win
   mainGUI
 
@@ -224,82 +280,59 @@
 goPure :: Go
 goPure refs term = return (term, refs)
 
-goRun :: (String -> IO ()) -> Go
-goRun out refs term = do
-  out (G.pretty term)
-  return (term, refs)
-
-gc :: G.References -> G.Term -> (G.Term, G.References)
-gc refs term =
-  let keep = reachable refs term M.empty
-      (collapse, later) = M.partition (1 ==) keep
-  in  (compact refs term, M.fromList [ (k, compact refs (refs M.! k)) | k <- M.keys collapse ] `M.union` M.fromList [ (k, refs M.! k) | k <- M.keys later ])
-
-reachable :: G.References -> G.Term -> Map Integer Integer -> Map Integer Integer
-reachable r (G.Lambda _ t) m = reachable r t m
-reachable r (G.Apply s t) m = reachable r s (reachable r t m)
-reachable r (G.Reference p) m = (if p `M.member` m then id else reachable r (r M.! p)) (M.insertWith (+) p 1 m)
-reachable r (G.Trace _ s t) m = reachable r s (reachable r t m)
-reachable _ _ m = m
-
-compact :: G.References -> G.Term -> G.Term
-compact r (G.Reference p) = r M.! p
-compact _ t = t
-
-evaluator :: Int -> IORef (Maybe L.Layout) -> (String -> IO ()) -> IORef G.Definitions -> G.References -> G.Term -> Go -> IO ()
-evaluator tick layout out defsR refs term go = do
+evaluator :: String -> Int -> IORef Settings -> Int -> IORef (Maybe L.Layout) -> (String -> IO ()) -> IORef G.Definitions -> G.References -> G.Term -> Go -> IO ()
+evaluator pngPrefix frame settingsR tick layout out defsR refs term go = do
   defs <- readIORef defsR
-  let (term1, refs1) = gc refs term
+  settings <- readIORef settingsR
+  when (Setting.traceEvaluation settings) $ do
+    out $ "  " ++ G.pretty term
+    unless (M.null refs) $ do
+      out "   where"
+      forM_ (M.toList refs) $ \(r, t) -> do
+        out $ "    #" ++ show r ++ " = " ++ G.pretty t
+  let (refs1, term1)
+        | Setting.collectGarbage settings = GC.gc refs term
+        | otherwise = (refs, term)
+      collectedGarbage = term1 /= term || refs1 /= refs
+  when (Setting.traceEvaluation settings && collectedGarbage) $ do
+    out "$\\to$      {- collect garbage -}"
+    out $ "  " ++ G.pretty term1
+    unless (M.null refs1) $ do
+      out "   where"
+      forM_ (M.toList refs1) $ \(r, t) -> do
+        out $ "    #" ++ show r ++ " = " ++ G.pretty t
   (term0, refs0) <- go refs1 term1
-  case G.reduce defs refs0 term0 of
-    Nothing -> threadDelay tick >>        evaluator tick layout out defsR refs0 term0 go
-    Just (G.Reduced term' refs') ->       evaluator tick layout out defsR refs' term' go
-    Just (G.Rebound _var' term' refs') -> evaluator tick layout out defsR refs' term' go
-    Just (G.Traced k s term' refs') -> do
-      atomicModifyIORef layout $ \_ -> (Just $ L.layout term0 refs0, ())
-      case k of
-        "wait" -> case evalNatural (dereference refs0 s) of
-          Just n -> threadDelay (tick * fromInteger n)
-          _ -> return ()
-        "noteon" -> case evalList evalNatural (dereference refs0 s) of
-          Just msg@[_channel, _note, _velocity] ->
-            out $ "noteon " ++ unwords (map show msg) ++ " ;"
-          _ -> return ()
-        "noteoff" -> case evalList evalNatural (dereference refs0 s) of
-          Just msg@[_channel, _note, _velocity] ->
-            out $ "noteoff " ++ unwords (map show msg) ++ " ;"
-          _ -> return ()
-        "program" -> case evalList evalNatural (dereference refs0 s) of
-          Just msg@[_channel, _program] ->
-            out $ "program " ++ unwords (map show msg) ++ " ;"
-          _ -> return ()
-        "control" -> case evalList evalNatural (dereference refs0 s) of
-          Just msg@[_channel, _control, _value] ->
-            out $ "control " ++ unwords (map show msg) ++ " ;"
-          _ -> return ()
-        _ -> print (k, G.pretty (dereference refs0 s))
-      evaluator tick layout out defsR refs' term' go
-
-dereference :: G.References -> G.Term -> G.Term
-dereference r (G.Reference p) = dereference r (r M.! p)
-dereference r (G.Lambda k t) = G.Lambda k (dereference r t)
-dereference r (G.Apply a b) = G.Apply (dereference r a) (dereference r b)
-dereference r (G.Trace k a b) = G.Trace k (dereference r a) (dereference r b)
-dereference _ t = t
-
-evalNatural :: G.Term -> Maybe Integer
-evalNatural (G.Lambda _ (G.Lambda _ (G.Bound 0))) = Just 0
-evalNatural (G.Lambda _ (G.Lambda _ (G.Apply (G.Bound 1) t))) = (1 +) `fmap` evalNatural t
-evalNatural _ = Nothing
-
-evalList :: (G.Term -> Maybe a) -> G.Term -> Maybe [a]
-evalList _ (G.Lambda _ (G.Lambda _ (G.Bound 0))) = Just []
-evalList f (G.Lambda _ (G.Lambda _ (G.Apply (G.Apply (G.Bound 1) s) t))) = (:) <$> f s <*> evalList f t
-evalList _ _ = Nothing
-
-outputter :: Chan String -> IO ()
-outputter out = do
-  hSetBuffering stdout LineBuffering
-  forever $ do
-    s <- readChan out
-    putStrLn s
+  (l, L.Counts c1 c2 c3 c4 c5 c6 c7) <- atomicModifyIORef layout $ \_ ->
+    let l@(L.Layout lt _ _ _) = L.layout term0 refs0
+    in  (Just l, (l, L.counts lt))
+  when (Setting.saveImages settings) $ do
+    withImageSurface FormatRGB24 1920 1080 $ \surface -> do
+      renderWith surface $ do
+        let g = 23 / 255
+        setSourceRGB g g g
+        paint
+        D.draw 1920 1080 l
+      surfaceWriteToPNG surface (pngPrefix ++ show frame ++ ".png")
+  when (Setting.emitStatistics settings) $ do
+    out $ "statistics " ++ unwords (map show [c1,c2,c3,c4,c5,c6,c7]) ++ ";"
+  when (Setting.realTimeDelay settings) $ do
+    threadDelay tick
+  let tick'
+        | Setting.realTimeAcceleration settings = ceiling (fromIntegral tick * 0.97 + 0.03 * 42000 :: Double)
+        | otherwise = tick
+  case R.reduce defs refs0 term0 of
+    Nothing -> do
+      when (Setting.traceEvaluation settings) $ do
+        out "$\\to$      {- in normal form -}"
+        out "  $\\qedsymbol$"
+      when (Setting.retryIrreducible settings) $ do
+        evaluator pngPrefix (frame + 1) settingsR tick layout out defsR refs0 term0 go
+    Just (reason, (refs', term')) -> do
+      when (Setting.traceEvaluation settings) $ do
+        out $ "$\\to$      {- " ++ (case reason of
+            R.Beta -> "beta reduce"
+            R.RefInst -> "instantiate reference"
+            R.Rebound var -> "definition of \"" ++ var ++ "\""
+            R.Extrude -> "scope extrude"
+          ) ++ " -}"
+      evaluator pngPrefix (frame + 1) settingsR tick' layout out defsR refs' term' go
diff --git a/src/Meta.hs b/src/Meta.hs
--- a/src/Meta.hs
+++ b/src/Meta.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -21,13 +21,21 @@
 
 import Control.Applicative((<|>), (<$), (<*>))
 
+import Setting (Setting)
+import qualified Setting
 import Parse
 
-data Meta = Quit | Clear | Browse | Load String
+data Meta = Start | Stop | Quit | Clear | Browse | Load String | Get Setting | Set Setting | UnSet Setting | Toggle Setting
   deriving (Read, Show, Eq, Ord)
 
 parse :: Parser String Meta
-parse =  (Quit   <$ sym "quit")
+parse =  (Start  <$ sym "start")
+     <|> (Stop   <$ sym "stop")
+     <|> (Quit   <$ sym "quit")
      <|> (Clear  <$ sym "clear")
      <|> (Browse <$ sym "browse")
      <|> (Load   <$ sym "load" <*> name)
+     <|> (Get    <$ sym "get" <*> Setting.parse)
+     <|> (Set    <$ sym "set" <*> Setting.parse)
+     <|> (UnSet  <$ sym "unset" <*> Setting.parse)
+     <|> (Toggle <$ sym "toggle" <*> Setting.parse)
diff --git a/src/Parse.hs b/src/Parse.hs
--- a/src/Parse.hs
+++ b/src/Parse.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -52,7 +52,7 @@
 alphanum = alpha ++ digits
 
 symbols :: String
-symbols = "\\.!?()[],=~:{}"
+symbols = "\\.!?()[],=:"
 
 spaces :: String
 spaces = " "
@@ -68,7 +68,8 @@
 tokenize (c:cs)
   | c `elem` digits  = let (t,ts) = span (`elem` digits) cs
                        in ((c:t):) <$> tokenize ts
-  | c `elem` lowers  = let (t,ts) = span (`elem` alphanum) cs
+  | c `elem` uppers
+  ||c `elem` lowers  = let (t,ts) = span (`elem` alphanum) cs
                        in ((c:t):) <$> tokenize ts
   | c `elem` symbols = ([c]:) <$> tokenize cs
   | c `elem` spaces  = tokenize cs
diff --git a/src/Reduce.hs b/src/Reduce.hs
new file mode 100644
--- /dev/null
+++ b/src/Reduce.hs
@@ -0,0 +1,142 @@
+{-
+    gulcii -- graphical untyped lambda calculus interpreter
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+-}
+
+module Reduce (Reduce(..), Reduction, reduce) where
+
+import Prelude hiding (replicate)
+
+import qualified Data.Map.Strict as Map
+
+import Evaluation (Strategy(..))
+import Graph
+
+{-
+Reduce a graph one step, returning Nothing if it is irreducible.
+-}
+
+data Reduce = Beta | RefInst | Rebound String | Extrude
+  deriving (Read, Show, Eq, Ord)
+
+type Reduction = (Reduce, (References, Term))
+
+mapTerm :: (Term -> Term) -> Reduction -> Reduction
+mapTerm f = fmap (fmap f)
+
+
+reduce :: Definitions -> References -> Term -> Maybe Reduction
+reduce defs refs term =
+  case reduce' False defs refs term of
+    Nothing -> reduce' True defs refs term
+    r -> r
+
+
+reduce' :: Bool -> Definitions -> References -> Term -> Maybe Reduction
+
+reduce' _ defs refs (Free var)
+  = (,) (Rebound var) `fmap` (,) refs `fmap` Map.lookup var defs
+
+reduce' _ _    _    (Bound0)
+  = Nothing
+
+reduce' _ _    refs (Scope (Lambda strat term))
+  = Just (Extrude, (refs, Lambda strat (lifting refs 1 term)))
+
+reduce' f defs refs (Scope t@(Reference _))
+  = case dereference refs t of
+      l@(Lambda _ _) ->
+        Just (RefInst, (refs, Scope l))
+      _ -> mapTerm Scope `fmap` reduce' f defs refs t
+
+reduce' _ _    refs (Scope (Apply a b))
+  = Just (Extrude, (refs, Apply (Scope a) (Scope b)))
+
+reduce' f defs refs (Scope term)
+  = mapTerm Scope `fmap` reduce' f defs refs term
+
+reduce' f defs refs (Lambda strat term)
+  = mapTerm (Lambda strat) `fmap` reduce' f defs refs term
+
+reduce' f defs refs term@(Reference ref)
+  = case Map.lookup ref refs of
+      Just refTerm ->
+        case reduce' f defs refs refTerm of
+          Just (reason, (refs', term')) ->
+            Just (reason, (Map.insert ref term' refs', term))
+          Nothing ->
+            Just (RefInst, (refs, refTerm))
+      Nothing -> Nothing -- error "reference not found"
+
+reduce' _ _    refs (Apply (Lambda Copy a) b)
+  = Just (Beta, (refs, beta refs a b))
+
+reduce' f defs refs (Apply l@(Lambda Strict a) b)
+  = case reduce' f defs refs b of
+      Just (reason, (refs', b')) -> Just (reason, (refs', Apply l b'))
+      Nothing -> Just (Beta, (refs, beta refs a b))
+
+reduce' _ _    refs (Apply (Lambda Lazy a) b)
+  = let r = next refs
+        refs' = Map.insert r b refs
+    in  Just (Beta, ( refs'
+                    , beta refs' a (Reference r) ))
+
+reduce' f defs refs (Apply a b)
+  = case (a, dereference refs a) of
+      (Reference _, l@(Lambda _ _)) -> Just (RefInst, (refs, Apply l b))
+      _ ->
+       case reduce' f defs refs a of
+          Just (reason, (refs', a')) ->
+            Just (reason, (refs', Apply a' b))
+          Nothing
+            | f -> mapTerm (Apply a) `fmap` reduce' f defs refs b
+            | otherwise -> Nothing
+
+
+beta :: References -> Term -> Term -> Term
+beta refs l v = substitute refs l v 0
+
+substitute :: References -> Term -> Term -> Integer -> Term
+substitute _    Bound0 s 0 = s
+substitute _    Bound0 _ _ = Bound0
+substitute _    (Scope t) _ 0 = t
+substitute refs (Scope t) s i = Scope (substitute refs t s (i - 1))
+substitute refs (Lambda k t) s i = Lambda k (substitute refs t s (i + 1))
+substitute refs (Apply a b) s i = Apply (substitute refs a s i) (substitute refs b s i)
+substitute _    t@(Free _) _ _ = t
+substitute refs (Reference r) s i = substitute refs (refs Map.! r) s i
+
+lifting :: References -> Integer -> Term -> Term
+lifting _    0 t = Scope t
+lifting _    _ s@(Free _) = s
+lifting _    _ Bound0 = Bound0
+lifting refs i (Scope t) = Scope (lifting refs (i - 1) t)
+lifting refs i (Lambda k t) = Lambda k (lifting refs (i + 1) t)
+lifting refs i (Apply a b) = Apply (lifting refs i a) (lifting refs i b)
+lifting refs i (Reference r) = lifting refs i (refs Map.! r)
+
+
+dereference :: References -> Term -> Term
+dereference refs (Reference r) = dereference refs (refs Map.! r)
+dereference _ t = t
+
+
+next :: References -> Integer
+next refs = case Map.maxViewWithKey refs of
+  Nothing        -> 0
+  Just ((k,_),_) -> k + 1
diff --git a/src/Setting.hs b/src/Setting.hs
new file mode 100644
--- /dev/null
+++ b/src/Setting.hs
@@ -0,0 +1,97 @@
+{-
+    gulcii -- graphical untyped lambda calculus interpreter
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+-}
+
+module Setting (Setting(..), parse, Settings(..), get, set, defaults) where
+
+import Control.Applicative ((<$))
+import Data.Foldable (asum)
+
+import Parse
+
+data Setting
+  = TraceEvaluation
+  | CollectGarbage
+  | RealTimeDelay
+  | RealTimeAcceleration
+  | RetryIrreducible
+  | EmitStatistics
+  | EmitRebindings
+  | EchoToStdOut
+  | EchoToGUI
+  | SaveImages
+  | NewsOnTop
+  deriving (Eq, Ord, Enum, Bounded, Read, Show)
+
+parse :: Parser String Setting
+parse = asum [ s <$ sym (show s) | s <- [minBound .. maxBound :: Setting] ]
+
+data Settings = Settings
+  { traceEvaluation :: Bool
+  , collectGarbage :: Bool
+  , realTimeDelay :: Bool
+  , realTimeAcceleration :: Bool
+  , retryIrreducible :: Bool
+  , emitStatistics :: Bool
+  , emitRebindings :: Bool
+  , echoToStdOut :: Bool
+  , echoToGUI :: Bool
+  , saveImages :: Bool
+  , newsOnTop :: Bool
+  }
+
+get :: Setting -> Settings -> Bool
+get TraceEvaluation = traceEvaluation
+get CollectGarbage = collectGarbage
+get RealTimeDelay = realTimeDelay
+get RealTimeAcceleration = realTimeAcceleration
+get RetryIrreducible = retryIrreducible
+get EmitStatistics = emitStatistics
+get EmitRebindings = emitRebindings
+get EchoToStdOut = echoToStdOut
+get EchoToGUI = echoToGUI
+get SaveImages = saveImages
+get NewsOnTop = newsOnTop
+
+set :: Setting -> Bool -> Settings -> Settings
+set TraceEvaluation b s = s{ traceEvaluation = b }
+set CollectGarbage b s = s{ collectGarbage = b }
+set RealTimeDelay b s = s{ realTimeDelay = b }
+set RealTimeAcceleration b s = s{ realTimeAcceleration = b }
+set RetryIrreducible b s = s{ retryIrreducible = b }
+set EmitStatistics b s = s{ emitStatistics = b }
+set EmitRebindings b s = s{ emitRebindings = b }
+set EchoToStdOut b s = s{ echoToStdOut = b }
+set EchoToGUI b s = s{ echoToGUI = b }
+set SaveImages b s = s{ saveImages = b }
+set NewsOnTop b s = s{ newsOnTop = b }
+
+defaults :: Settings
+defaults = Settings
+  { traceEvaluation = False
+  , collectGarbage = True
+  , realTimeDelay = True
+  , realTimeAcceleration = True
+  , retryIrreducible = True
+  , emitStatistics = True
+  , emitRebindings = True
+  , echoToStdOut = True
+  , echoToGUI = False
+  , saveImages = False
+  , newsOnTop = True
+  }
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -1,6 +1,6 @@
 {-
     gulcii -- graphical untyped lambda calculus interpreter
-    Copyright (C) 2011, 2013  Claude Heiland-Allen
+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen
 
     This program is free software; you can redistribute it and/or modify
     it under the terms of the GNU General Public License as published by
@@ -31,7 +31,7 @@
 
 module Sugar(Term(..), parse, desugar) where
 
-import Control.Applicative(Applicative, Alternative, (<|>), (<$>), (<$), (<*>), (<*), some, liftA2)
+import Control.Applicative((<|>), (<$>), (<$), (<*>), (<*), some, liftA2)
 import Data.List ((\\))
 
 import Parse
@@ -45,7 +45,6 @@
   | Group Term
   | Natural Integer
   | List [Term]
-  | Trace String Term Term
   deriving (Read, Show, Eq, Ord)
 
 parse :: Parser String Term
@@ -57,7 +56,6 @@
       <|> (Variable <$> name)
       <|> (Natural <$> integer)
       <|> (List <$ sym "[" <*> manySep (sym ",") parse <* sym "]")
-      <|> (Trace <$ sym "{" <*> name <* sym ":" <*> parse <* sym "}" <*> parse)
 
 strategy :: Parser String Strategy
 strategy =  (Strict <$ sym "!") <|> (Lazy <$ sym ".") <|> (Copy <$ sym "?")
@@ -118,7 +116,6 @@
       let (c:n:_) = (variables \\ U.freeVariablesIn t') \\ U.freeVariablesIn ts'
       in Just $ lam c (lam n (U.Apply (U.Apply (U.Variable c) t') ts'))
     _ -> Nothing
-desugar (Trace k s t) = U.Trace k <$> desugar s <*> desugar t
 
 lam :: String -> U.Term -> U.Term
 lam = U.Lambda Lazy