Theorem. 算法完备性

Glomzzz
2026-10-10
About

取 Rust 类型检查算法 type_of type_of ，类型关系采用类型与类型判断．实现论证采用算术语言形式化的未展开前提的资源与基础操作假设； Rust 的 Bool Bool 、 Nat Nat 分别对应 $Bool$ 、 $Nat$ ．对任意项 $𝑡$ 和类型 $𝑇$ ：若 $𝑡 : 𝑇$ ，则 type_of(t) = Some(T) type_of(t) = Some(T) ．

Proof.

对

𝑡 : 𝑇

作规则归纳，按最后一步的规则分情形．对公理 T-True、T-False、T-Zero，直接计算 type_of type_of 即得．对 T-Succ，前提

𝑡_{1} : Nat

由归纳假设给出 type_of(t1) = Some(Nat) type_of(t1) = Some(Nat) ，于是 Succ Succ 分支返回 Some(Nat) Some(Nat) ；T-Pred、T-IsZero 同理．对 T-If，三个前提由归纳假设给出 type_of type_of 在三个子项上分别返回 Bool Bool 、 T T 、 T T ；代入 If If 分支后 ta = T ta = T ，两个比较都成立，返回 Some(T) Some(T) ．

∎

Theorem. 算法完备性

References

Backlinks