Normalization property (lambda-calculus)

﻿
Normalization property (lambda-calculus)

In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property (in short: the normalization property) if every term is "strongly normalizing"; that is, if every sequence of rewrites eventually terminates to a term in normal form. A rewrite system may also have the weak normalization property, meaning that for every term, there exists at least one particular sequence of rewrites that eventually yields a normal form.

The "pure" untyped lambda calculus does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term $lambda x . x x x$. It has the following rewrite rule: For any term $t$,

: $\left(mathbf\left\{lambda\right\} x . x x x\right) t ightarrow t t t$

But consider what happens when we apply $lambda x . x x x$ to itself:

Therefore the term $\left(lambda x . x x x\right) \left(lambda x . x x x\right)$ is not strongly normalizing.

Various systems of typed lambda calculus including the
simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are strongly normalizing.

A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete. That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be computed in the calculus of constructions or system F). As an example, it is impossible to define the normalization algorithms of any of the calculi cited above within the same calculus.

ee also

* lambda calculus
* typed lambda calculus
* rewriting
* calculus of constructions
* total functional programming

Wikimedia Foundation. 2010.

Look at other dictionaries:

• Normalization property (abstract rewriting) — In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property (in short: the normalization property) if every term is strongly normalizing; that is, if every sequence of rewrites eventually… …   Wikipedia

• Simply typed lambda calculus — The simply typed lambda calculus (lambda^ o) is a typed interpretation of the lambda calculus with only one type combinator: o (function type). It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus… …   Wikipedia

• Calculus of variations — is a field of mathematics that deals with extremizing functionals, as opposed to ordinary calculus which deals with functions. A functional is usually a mapping from a set of functions to the real numbers. Functionals are often formed as definite …   Wikipedia

• List of mathematics articles (N) — NOTOC N N body problem N category N category number N connected space N dimensional sequential move puzzles N dimensional space N huge cardinal N jet N Mahlo cardinal N monoid N player game N set N skeleton N sphere N! conjecture Nabla symbol… …   Wikipedia

• List of philosophy topics (I-Q) — II and thou I Ching I Ching I proposition I Thou I Thou relationshipIaIamblichus (philosopher)IbYahya Ibn Adi Yahya Ibn Adi Ibn al Arabi Muhyi al Din Ibn al Arabi Abu Bakr Ibn Bajja Abu Bakr Ibn Bājja Abu Bakr Muhammad Ibn Yahya Ibn as Say igh… …   Wikipedia

• Cut-elimination theorem — The cut elimination theorem (or Gentzen s Hauptsatz) is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper Investigations in Logical Deduction for the… …   Wikipedia

• Normal form — may refer to: Normal form (abstract rewriting) Normal form (databases) Normal form (game theory) Normal form (mathematics) In formal language theory: Beta normal form Chomsky normal form Greibach normal form Kuroda normal form Normal form… …   Wikipedia

• Category:Logic in computer science — Logic in computer science is that branch of mathematical logic which is approximately the intersection between mathematical logic and computer science. It contains: Those investigations into logic that are guided by applications in computer… …   Wikipedia

• Hilbert space — For the Hilbert space filling curve, see Hilbert curve. Hilbert spaces can be used to study the harmonics of vibrating strings. The mathematical concept of a Hilbert space, named after David Hilbert, generalizes the notion of Euclidean space. It… …   Wikipedia

• Legendre polynomials — Note: People sometimes refer to the more general associated Legendre polynomials as simply Legendre polynomials . In mathematics, Legendre functions are solutions to Legendre s differential equation::{d over dx} left [ (1 x^2) {d over dx} P n(x)… …   Wikipedia