Dictionary
Words, grammatical forms and meanings linked to the ontology.
beta reduction en · NOUN
Pronunciation
- /ˈbiː.tə.ɹɪˌdʌk.ʃən/
- /ˈbeɪ.tə.ɹɪˌdʌk.ʃən/
- /ˈbiː.tə.ɹəˌdʌk.ʃən/ weak vowel merger
- (US) audio
- /ˈbeɪ.tə.ɹəˌdʌk.ʃən/ weak vowel merger
Meanings
-
(countable, uncountable) The act of beta reducing, an instance of replacing a function call by the result of calling a function.
-
(countable, uncountable) One of the three rewrite rules of the lambda calculus, which states that the application of a lambda abstraction (λ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.
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.
1996, Roberto DiCosmo with Vincent Danos, The Linear Logic Primer, Université de Paris VII, retrieved 18 Apr 2016, page 43:
Forms
Coordinates
eta conversion · alpha conversion