Normalization property (abstract rewriting)

In mathematical logic and theoretical computer science, a rewrite system has the (strong) normalization property or is terminating if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates with an irreducible term, also called a 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, i.e., an irreducible term.

Lambda calculus

Untyped lambda calculus

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

(\mathbf {\lambda } x.xxx)t\rightarrow ttt

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

{\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \ldots \,\end{aligned}}

Therefore the term $(\lambda x.xxx)(\lambda x.xxx)$ is neither strongly nor weakly normalizing.

Typed lambda calculus

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.[1] 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 a self-interpreter in any of the calculi cited above [2].[3][4]

gollark: ++magic py await bot.user.set_nickname("LyricLy®")

gollark: NO EVIDENCE of actual implementation (except maybe the parser)NO COHERENT SPEC describing how any if it actually worksLANGUAGES WERE NOT MEANT TO HAVE TYPES BE TRAITS OR WHATEVERWanted to use macros anyway for a laugh? We had a tool for that. It was called Lisp."Hello I would like impl<u8(a)> T(a) apples please" - statements made by the utterly Deranged.And after all the computers and compiler tooling we gave them!

gollark: And yet.

gollark: Well, the lesson is more that LyricLy's language ideas are bad and impossible.

gollark: *You* thought of then made Macron?

Notes

University of Rochester,
(in the sense that it forces the language to be untyped or not to be a total language); assume "eval" is the function that interprets language TLC (typed lambda calculus) and it takes the "code" as its argument , it is impossible semantically to type "eval" correctly (that is to define its type) either cause you can't type all possible TLC code fragments (since there are uncountably infinite number of them (Diagonal Argument), or if you made it take type like "string" type, the parse it you covered the problem in terms of implementation but not in terms of semantical correctness (assume another function "evil" which does the following (evil = 1 + eval([evil's code goes here]) and that escapes Normalization property ("evil" will never normalize, and that is because it breaks some of the Strong Normalization Proof assumptions (cause it implies dependent data types) ) ) ).
Conor McBride (May 2003), "on termination" (posted to the Haskell-Cafe mailing list).
Andrej Bauer (June 2014), Answer to: A total language that only a Turing complete language can interpret (posted to the Theoretical Computer Science StackExchange site)

References

Baader, Franz; Nipkow, Tobias (1999). Term rewriting and all that. Cambridge University Press. ISBN 0-521-77920-0. 316 pages.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] University of Rochester,

[2] (in the sense that it forces the language to be untyped or not to be a total language); assume "eval" is the function that interprets language TLC (typed lambda calculus) and it takes the "code" as its argument , it is impossible semantically to type "eval" correctly (that is to define its type) either cause you can't type all possible TLC code fragments (since there are uncountably infinite number of them (Diagonal Argument), or if you made it take type like "string" type, the parse it you covered the problem in terms of implementation but not in terms of semantical correctness (assume another function "evil" which does the following (evil = 1 + eval([evil's code goes here]) and that escapes Normalization property ("evil" will never normalize, and that is because it breaks some of the Strong Normalization Proof assumptions (cause it implies dependent data types) ) ) ).

[3] Conor McBride (May 2003), "on termination" (posted to the Haskell-Cafe mailing list).

[4] Andrej Bauer (June 2014), Answer to: A total language that only a Turing complete language can interpret (posted to the Theoretical Computer Science StackExchange site)