- 💬 写在前面：本章我们将讲解推导树证明，推导树实际上就是推理规则的应用。只要学会如何选择并应用适当的推理规则，证明就不是难事了。
目录
0x00 推导树证明 𝝓 ⊢ 𝒆 ∶ 𝒕
0x01 继续定义关系：𝚪 ⊢ 𝒆 ∶ 𝒕
0x00 推导树证明 𝝓 ⊢ 𝒆 ∶ 𝒕
对于程序 ，如果我们能画出一个推导树来证明：
那么我们的类型系统接受 ，这意味着该程序没有类型错误。
推导树就是推理规则的应用，整个程序的形式为 let x = e1 in e2，因此我们应用以下推理规则：
实例化 为
，
：
左子树必须证明：
右子树必须证明：
完整的推导树如下所示，注意观察每个子树部分应用了哪些推理规则：
0x01 继续定义关系：𝚪 ⊢ 𝒆 ∶ 𝒕
下面我们继续定义关系：
考虑 let f x = e1 in e2（函数定义），假设当参数 的类型为
时，
的类型为
。
那么函数 的类型是
：
思考 的和函数应用：
如果 的类型为
，且参数
的类型为
，则函数调用的结果为
证明对于以下程序 ，写出其推导树：
使用以下推理规则，实例化 为
，
。
同时，我们知道 必须是 int，而
是 bool：
完整的推导树如下：
0x02 注意多种类型地情况
意对于某些程序 (𝒆)，可能存在多种类型 (𝒕)，使得 𝝓 ⊢ 𝒆 ∶ 𝒕 成立。
换句话说，类型可能不唯一确定！
以 let f x = x in f 为例：以下几种情况下的 𝝓 ⊢ 𝒆 ∶ 𝒕 都是可以证明，可以画出推导树的：
📌 [ 笔者 ] 王亦优
📃 [ 更新 ] 2024.6.15
❌ [ 勘误 ] /* 暂无 */
📜 [ 声明 ] 由于作者水平有限，本文有错误和不准确之处在所难免，本人也很想知道这些错误，恳望读者批评指正！| 📜 参考资料 - R. Neapolitan, Foundations of Algorithms (5th ed.), Jones & Bartlett, 2015. - T. Cormen《算法导论》（第三版），麻省理工学院出版社，2009年。 - T. Roughgarden, Algorithms Illuminated, Part 1~3, Soundlikeyourself Publishing, 2018. - J. Kleinberg&E. Tardos, Algorithm Design, Addison Wesley, 2005. - R. Sedgewick&K. Wayne，《算法》（第四版），Addison-Wesley，2011 - S. Dasgupta，《算法》，McGraw-Hill教育出版社，2006。 - S. Baase&A. Van Gelder, Computer Algorithms: 设计与分析简介》，Addison Wesley，2000。 - E. Horowitz，《C语言中的数据结构基础》，计算机科学出版社，1993 - S. Skiena, The Algorithm Design Manual (2nd ed.), Springer, 2008. - A. Aho, J. Hopcroft, and J. Ullman, Design and Analysis of Algorithms, Addison-Wesley, 1974. - M. Weiss, Data Structure and Algorithm Analysis in C (2nd ed.), Pearson, 1997. - A. Levitin, Introduction to the Design and Analysis of Algorithms, Addison Wesley, 2003. - A. Aho, J. Hopcroft, and J. Ullman, Data Structures and Algorithms, Addison-Wesley, 1983. - E. Horowitz, S. Sahni and S. Rajasekaran, Computer Algorithms/C++, Computer Science Press, 1997. - R. Sedgewick, Algorithms in C: 第1-4部分（第三版），Addison-Wesley，1998 - R. Sedgewick，《C语言中的算法》。第5部分（第3版），Addison-Wesley，2002 |
