# beta reduction

Jump to navigation
Jump to search

## English[edit]

### Noun[edit]

**beta reduction** (*plural* **beta reductions**)

- The act of beta reducing, an instance of replacing a function call by the result of calling a function.
- (computing theory) One of the three rewrite rules of the lambda calculus, which states that the application of a lambda abstraction to a term yields an expression , "
*t*with*s*instead of*x*", where all free instances of*x*in*t*have been replaced by*s*.**1996**, Roberto DiCosmo; Vincent Danos, The Linear Logic Primer^{[1]}, Université de Paris VII, retrieved 2016-04-18, page 43:- A natural deduction tree can be put in exact correspondence with typed λ-calculus (that can be considered as just a notation for such deductions), and the cut-elimination in Natural Deduction corresponds exactly to
**β-reduction**in λ-calculus.

- A natural deduction tree can be put in exact correspondence with typed λ-calculus (that can be considered as just a notation for such deductions), and the cut-elimination in Natural Deduction corresponds exactly to