beta reduction

English

Pronunciation

• IPA^(key): /ˈbeɪ.tə.ɹɪˌdʌk.ʃən/
  • (weak vowel merger) IPA^(key): /ˈbeɪ.tə.ɹəˌdʌk.ʃən/

  • Audio (US):

    (file)

• IPA^(key): /ˈbiː.tə.ɹɪˌdʌk.ʃən/
  • (weak vowel merger) IPA^(key): /ˈbiː.tə.ɹəˌdʌk.ʃən/

Noun

beta reduction (countable and uncountable, plural beta reductions)

1. The act of beta reducing, an instance of replacing a function call by the result of calling a function.
2. (computing theory) One of the three rewrite rules of the lambda calculus, which states that the application of a lambda abstraction $(\lambda x.t)$ to a term $s$ yields an expression $t[s/x]$, "t with s instead of x", where all free instances of x in t have been replaced by s.
   • 1996, Roberto DiCosmo with Vincent Danos, The Linear Logic Primer‎^[1], Université de Paris VII, archived from the original on 10 June 2023, 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.

Coordinate terms

• alpha conversion
• eta conversion