Proof checking
Reduction
Computing a term according to the core language's evaluation rules.
Definition
Reduction
Reduction replaces a term with a computationally simpler term allowed by the calculus.
Function application can substitute an argument into a body, and pattern matching can select a constructor case. Kernels use reduction when deciding definitional equality.
01
Example
Applying the function fun x => x + 1 to 2 reduces to 2 + 1 and then to 3.
02
Important distinction
Reduction follows built-in computation rules. It does not apply every proved mathematical equality automatically.
After reading this article, you should be able to
- Define Reduction in the sense used on this site.
- Perform one beta-reduction and explain why it preserves the term's meaning.