|
|
|
|
|
|
|
|
• |
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) | ...
|