正規化 (項書き換え)

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

概要[編集]

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

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

定義[編集]

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

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