In mathematical logic and theoretical computer science, a rewrite system has the strong 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.

PropertyValue
dbpprop:abstract
  • In mathematical logic and theoretical computer science, a rewrite system has the strong 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 <math>\lambda x . x x x</math>. It has the following rewrite rule: For any term <math>t</math>, <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math> But consider what happens when we apply <math>\lambda x . x x x</math> to itself: Therefore the term <math>(\lambda x . x x x) (\lambda x . x x x)</math> 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.
  • 在数理逻辑和理论计算机科学中，一个重写系统有规范化性质，如果所有项都是强规范化的；就是说所有重写序列都最终终止于规范形式的项。 纯粹无类型 lambda 演算不是强规范化的。考虑项 <math>\lambda x . x x x</math>。它有如下重写规则: 对于任何项 t， <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math> 但是考虑在应用 <math>\lambda x . x x x</math> 于自身时所发生的: 所以项 <math>(\lambda x . x x x) (\lambda x . x x x)</math> 不是规范化的。 各种有类型 lambda 演算系统包括简单类型 lambda 演算，Jean-Yves Girard 的系统F，和 Thierry Coquand 的构造演算都有规范化性质。 带有规范化性质的 lambda 演算系统可以被看作带有所有程序都终止性质的编程语言。尽管这是一个非常有用的性质，它也有缺点: 带有规范化性质的编程语言不可能是图灵完全的。这意味着有可计算函数不能在简单类型的 lambda 演算中定义(类似的有可计算函数不能在构造演算或系统 F 中计算)。
dbpprop:hasPhotoCollection
rdfs:comment
  • In mathematical logic and theoretical computer science, a rewrite system has the strong 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.
  • 在数理逻辑和理论计算机科学中，一个重写系统有规范化性质，如果所有项都是强规范化的；就是说所有重写序列都最终终止于规范形式的项。 纯粹无类型 lambda 演算不是强规范化的。考虑项 <math>\lambda x . x x x</math>。它有如下重写规则: 对于任何项 t， <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math> 但是考虑在应用 <math>\lambda x .
rdfs:label
  • Normalization property (lambda-calculus)
  • 规范化性质
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of