Definition.
一步规约
Definition. 一步规约
以 词项的集合 的词项作为执行状态， nv 只取 值与数值 中的数值． 一步规约关系 ，即此模型的小步转移关系， 是对下面十条推导规则封闭的最小二元关系． 成立，当且仅当存在以这个判断为结论的有限推导．
每条横线之上的判断是前提，横线之下的是结论；前提全部成立，结论才成立． 没有前提的规则称为公理，可以直接使用． 同一条规则中相同的元变量必须代换成同一个项，见 元变量 ．
E-IfTrue：前提 无；结论 if true then t_(2) else t_(3) ⟶ t_(2) E-IfFalse：前提 无；结论 if false then t_(2) else t_(3) ⟶ t_(3)
E-If：前提 t_(1) ⟶ t'_(1)；结论 if t_(1) then t_(2) else t_(3) ⟶ if t'_(1) then t_(2) else t_(3)
E-Succ：前提 t_(1) ⟶ t'_(1)；结论 succ t_(1) ⟶ succ t'_(1) E-PredZero：前提 无；结论 pred 0 ⟶ 0 E-PredSucc：前提 无；结论 pred (succ nv) ⟶ nv E-Pred：前提 t_(1) ⟶ t'_(1)；结论 pred t_(1) ⟶ pred t'_(1)
E-IsZeroZero：前提 无；结论 iszero 0 ⟶ true E-IsZeroSucc：前提 无；结论 iszero (succ nv) ⟶ false E-IsZero：前提 t_(1) ⟶ t'_(1)；结论 iszero t_(1) ⟶ iszero t'_(1)