test2.mdwn

   1
   2 Some authors reserve the term "term" for just variables and abstracts. We'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
   3
   4 Examples of expressions:
   5
   6         x
   7         (y x)
   8         (x x)
   9         (\x y)
  10         (\x x)
  11         (\x (\y x))
  12         (x (\x x))
  13         ((\x (x x)) (\x (x x)))
  14
  15 The lambda calculus has an associated proof theory. For now, we can regard the
  16 proof theory as having just one rule, called the rule of **beta-reduction** or
  17 "beta-contraction". Suppose you have some expression of the form: