正規化 (項書き換え)のソースを表示

[[項書き換え]]などにおいて'''正規化'''（せいきか、{{Lang-en-short|normalization}}）とは、[[項]]をそれ以上書き換えられなくなるまで書き換えることや、あるいはこのような操作が可能だという性質のことである。ある項がそのような性質を持つこと指して「項が正規化する」({{lang|en|normalizing}}) あるいは「項が正規化可能である」({{lang|en|normalizable}}) ともいう。また、そのような操作の末に辿り着いたそれ以上書き換えできない項のことを'''正規形''' ({{lang|en|normal form}}) とよぶ。

== 概要 ==
正規化と呼ばれる性質には、一般に'''弱正規化''' ({{lang|en|weak normalization, WN}}) と'''強正規化''' ({{lang|en|strong normalization, SN}}) と呼ばれる2つがあり、単に正規化と言った場合にどちらを意味するかは分野の慣習によって異なる。弱正規化とは、ある項が与えられたときに、うまく書き換えの手順を選べば何度かの書き換えの末にある正規形に辿り着くことができるような性質を表し、一方、強正規化は、どのように書き換えたとしてもいつかは正規形に到達するという性質を表す。明らかに、項が強正規化するなら弱正規化するが、逆は必ずしも成り立たない。

項書き換え系を[[計算]]として見たときには、強正規化は計算の[[停止性]]に対応し、ある種の「よい」性質とみなされることがある。例えば、[[型無しラムダ計算]]は強正規化しないが、[[単純型付きラムダ計算]]は強正規化する。

== 定義 ==
項の集合 <math>T</math> と簡約関係 <math>{\rightarrow} \subseteq T \times T</math> からなる[[抽象項書き換え系]] <math>\left\langle T, {\rightarrow}\right\rangle</math> を考えるとき、以下のように定義される。

# <math>t \in T</math> について、<math>u \in T</math> で <math>t \rightarrow u</math> であるような項が存在しないとき、<math>t</math> は'''正規形'''であるという。
# <math>t \in T</math> について、ある正規形 <math>u \in T</math> があって <math>t \rightarrow^{*} u</math> となるとき、<math>t</math> は'''弱正規化する''' (WN) という。ここに <math>{\rightarrow}^{*}</math> は <math>{\rightarrow}</math> の[[反射推移閉包]]である。任意の <math>t \in T</math> が弱正規化するとき、<math>{\rightarrow}</math> は弱正規化するという。
# <math>t \in T</math> について、<math>t</math> から始まる無限長の簡約列が存在しないとき、<math>t</math> は'''強正規化する''' (SN)、あるいは'''停止する'''という。任意の <math>t \in T</math> が強正規化するとき、<math>{\rightarrow}</math> は強正規化するという。

<!-- == 脚注 ==
{{脚注ヘルプ}}
{{Reflist}} -->
== 参考文献 ==
* {{cite book|title=Term Rewriting Systems|author=Terese|publisher=Cambridge University Press|isbn=9780521391153|date=2003-03|series=Cambridge Tracts in Theoretical Computer Science|volume=55}}
== 関連項目 ==
* [[合流性]]

{{Math-stub}}
{{DEFAULTSORT:せいきか}}
[[Category:数学に関する記事]]