Today I Learned

Some of the things I've learned every day since Oct 10, 2016

50: Normalization Property (Lambda Calculus)

In a rewrite system, such as \beta-reduction in the lambda calculus, a term may or may not satisfy either the  weak normalization or the strong normalization property.

A term T satisfies the weak normalization property if there exists a sequence of rewrites on T that eventually results in a normal form of T: a term which is irreducible.

A term T satisfies the strong normalization property if every sequence of rewrites on T eventually results in a normal form of T.

If every term in a rewrite system satisfies the [weak | strong] normalization property, then the system itself is said to satisfy the same property.


Examples:

An example of a system which satisfies neither of the normalization properties is the pure untyped lambda calculus. An example of a non-normal term within this system is

(\lambda y . y y) (\lambda y . y y).

Under \beta-reduction, this term reduces to itself, and so it never terminates in an irreducible form.

Conversely, a term within this system which is weakly normal is

(\lambda x . x) x.

Under \beta-reduction, this term reduces to just the variable x, an irreducible term.


There are other forms of the lambda calculus, as well as other similar systems, which are normal. These can be viewed as programming languages in which every program eventually will (or can) terminate. A significant drawback to such a system, however, is that if a system is normal it cannot be Turing complete.

Additionally, in the lambda calculus every normalizing term has a unique normal form.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: