Signed-off-by: Jim Pryor <profjim@jimpryor.net>
<strong>Application</strong>: <code>(M N)</code>
</blockquote>
<strong>Application</strong>: <code>(M N)</code>
</blockquote>
-Some *authors* reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
+Some authors reserve the term "term" for just variables and abstracts. We won't participate in that convention; we'll probably just say "term" and "expression" indiscriminately for expressions of any of these three forms.
(\x x)
(\x (\y x))
(x (\x x))
(\x x)
(\x (\y x))
(x (\x x))
- ((\x (x x)) (\x (x x)))
+ ((\x (x x)) (\x (x x)))
The lambda calculus has an associated proof theory. For now, we can regard the
proof theory as having just one rule, called the rule of **beta-reduction** or
The lambda calculus has an associated proof theory. For now, we can regard the
proof theory as having just one rule, called the rule of **beta-reduction** or