•E —
expression, u — expression variable
•box E
— term, x — term variable
•let
box u = M in N — substitute expression denoted by
M for u in N
•embed(x)
= let box u = x in box (...u...)
•eval(x)
= let box u = x in u
•simplify(x)
= case x of box (0*u) Þ
box (0) | ...