正規化 (項書き換え)
項の集合 T {\displaystyle T} と簡約関係 → ⊆ T × T {\displaystyle {\rightarrow }\subseteq T\times T} からなる抽象項書き換え系 ⟨ T , → ⟩ {\displaystyle \left\langle T,{\rightarrow }\right\rangle } を考えるとき、以下のように定義される。
t ∈ T {\displaystyle t\in T} について、 u ∈ T {\displaystyle u\in T} で t → u {\displaystyle t\rightarrow u} であるような項が存在しないとき、 t {\displaystyle t} は正規形であるという。
t ∈ T {\displaystyle t\in T} について、ある正規形 u ∈ T {\displaystyle u\in T} があって t → ∗ u {\displaystyle t\rightarrow ^{*}u} となるとき、 t {\displaystyle t} は弱正規化する (WN) という。
正規化と呼ばれる性質には、一般に弱正規化 (weak normalization, WN) と強正規化 (strong normalization, SN) と呼ばれる2つがあり、単に正規化と言った場合にどちらを意味するかは分野の慣習によって異なる。弱正規化とは、ある項が与えられたときに、うまく書き換えの手順を選べば何度かの書き換えの末にある正規形に辿り着くことができるような性質を表し、一方、強正規化は、どのように書き換えたとしてもいつかは正規形に到達するという性質を表す。明らかに、項が強正規化するなら弱正規化するが、逆は必ずしも成り立たない。
項書き換え系を計算として見たときには、強正規化は計算の停止性に対応し、ある種の「よい」性質とみなされることがある。例えば、型無しラムダ計算は強正規化しないが、単純型付きラムダ計算は強正規化する。