簡約
与えられた式に対して計算を一歩進めて別の式を与える
$ e\longrightarrow e'
(ex.
$ S(S(Z))*S(S(S(Z)))+Z*S(S(S(S(Z))))\longrightarrow S(S(Z))*S(S(S(Z)))+Z
)
$ e\longrightarrow^* e'
(複数回の簡約)
非決定性簡約
(
non-deterministic reduction
)
一つの式に対して異なる式が得られることがある簡約
決定性簡約
(
deterministic
)
簡約結果が一意になるように簡約を制限
$ e\longrightarrow_d e'