Beta normal form

In the lambda calculus, a term is in beta normal form if no beta reduction is possible.[1] A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible. A term is in head normal form if there is no beta-redex in head position. The normal form of a term, if one exists, is unique (as a corollary of the Church–Rosser theorem).[2] However, a term may have more than one head normal form.

  1. ^ "Beta normal form". Encyclopedia. TheFreeDictionary.com. Retrieved 18 November 2013.
  2. ^ Thompson, Simon (1991). Type theory and functional programming. Wokingham, England: Addison-Wesley. p. 38. ISBN 0-201-41667-0. OCLC 23287456.