Questions tagged [normal-form]

A normal form is expression that can no longer be reduced, typically in the lambda calculus. See also [weak-head-normal-form] and [normalization].

Filter by
Sorted by
Tagged with
6 votes
1 answer

What is a neutral term?

A neutral/normal term in the lambda calculus is typically defined data nf = Lam of nf | Neu of ne data ne = Var of int | App of ne * nf Now the question is what to ...
user avatar
  • 1,662