Example. 一棵推导

Glomzzz
2026-10-10
About

使用一步规约的规则，推导树的每条横线都是一条规则的实例：横线上方的子推导满足前提，下方给出结论．这棵三层的推导树合起来证明整项的一步规约（整棵树只对应一步转移，要与三步运行区分开）．

E-Pred：前提 [E-If：前提 [E-IsZeroZero：前提 [无]；结论 iszero 0 ⟶ true]；结论 if (iszero 0) then succ 0 else 0 ⟶ if true then succ 0 else 0]；结论 pred (if (iszero 0) then succ 0 else 0) ⟶ pred (if true then succ 0 else 0)

从下往上读：要说明最下面那一步成立，用 E-Pred，它要求里面的 $if$ 能一步规约；这又用 E-If，它要求条件 $iszero 0$ 能一步规约；最后 E-IsZeroZero 是公理，无条件成立．

Example. 一棵推导

References

Backlinks