等式公理

Posted on

公式: $$P{Q}R\ ({P}Q{R})$$

P 和 R 都是一阶公式, 如果前提条件 P 在执行 Q 前成立, 则执行后得到满足条件 R 的状态
部分正确性断言: 如果 P 在 Q 执行前为真, 那么, 如果 Q 的执行终止,则终止在使 R 为真的某个状态
终止性断言:如果 P 在 Q 执行前为真, 那么 Q 将终止在使 R 为真的某个状态
赋值公理: $$\vdash P_0 {x:=f} P$$

推理规则的表示

$$\frac{premise -> f_0, f_1, …, f_n}{conclusion -> f_0}$$

推理规则

  • Rules of Consequence:
    $$\frac{P{Q}R,\ R\rightarrow S}{P{Q}S}\ \ \ \ \ \frac{P{Q}R,\ S\rightarrow P}{S{Q}R}$$
  • Rule of Composition:
    $$\frac{P{Q_1}R_1,\ R_1{Q_2}R}{P{Q_1, Q_2}R}$$
  • Rules of Iteration:
    $$\frac{P\ &\ B{S}P}{P\ {while\ B\ do\ S}\ \neg B \ &\ P}$$

等式公理

  • 代换: $[N/x]M$ 表示表示 M 中的自由变元 x 用 N 代换的结果, N 中的自由变元代换后不能成为约束变元
  • 约束变元改名: $\lambda x:\sigma .M = \lambda y:\sigma.[y/x]M$ 例如:$\lambda x:\sigma.x + y = \lambda z:\sigma .z+y$
  • 等价公理: 计算函数实际就是在函数中使用实在变元替换形式变元, $(\lambda x:\sigma.M)N = [N/x]M$
  • 同余性规则: 相等的函数作用于相等的变元产生相等的结果, $\frac{M_1=M_2,\ N_1=N_2}{M_1N_1=M_2N_2}$