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
3 votes
1 answer
134 views

untyped lambda expressions may not have normal forms; are they used (or OK to use) in proof assistants?

I heard that untyped lambda expressions can have no normal forms. As an example, the expression $(\lambda x. x\space x) (\lambda x. x\space x)$ , when put to a $\beta$ conversion, gives back the same ...
tinlyx's user avatar
  • 1,906
2 votes
1 answer
140 views

Canonical forms of combinators

Binders are painful when dealing with metatheory. Combinators are one potential approach to avoid the pain of binders. But it'd be nice if I could normalize combinators to canonical forms. Is there ...
Molly Stewart-Gallus's user avatar
1 vote
1 answer
98 views

Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

In this question, I am talking about the language Pie described in the book The Little Typer. Consider the definition ...
CrabMan's user avatar
  • 317
7 votes
1 answer
304 views

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 ...
Couchy's user avatar
  • 2,181