Preface
对与ITP感觉其实我不是很懂，最近的话买了T.F Melham的书来看着玩， 简单的记一下顺便也准备下期末作业。。。。。
在这里讨论的Higher Order Logic 的定义主要来自Mike Gordon(R.I.P)的描述， 他的HOL 主要是基于Simple typed lambda calculus (STLC),准确的说是Hindley-Milner type 外加几个新的常量和额外的逻辑,.
Type
高阶逻辑是一种类型逻辑。从语法的角度上来说， 类型必须要能够消除‘悖论’，也就是说我们要使用一种类型系统使得我们在表达我们的逻辑表达式时所有的‘悖论’比如罗素悖论能够称为一个'ill-formed', 同时也要保持类型系统具有对于硬件描述比较好的表达能力。
e.g.
c是const, v 是var。 c和v被称为原子类型(atomic type) , op 构造的被称为复合类型(compound type ). 其中v可以用来代表‘任意类型’，通常用希腊字母来表示。 带有v的类型表达式叫做多态(polymophic).
HOL中的原始常量类型有两种，一种bool, 代表T,F构成的集合， 另外一种叫ind, 是individual的缩写，代表一个可以表示无穷多个明确元素集合的HOL 公式。
复合类型表示了一个由n阶的类型操作符op作用在N个类型上所构造的集合。原始类型操作符只有一种就是fun,代表一个用来构造函数的二元操作符。简单的说比如
就表示
.其他的类型可以通过显式定义的方式来引入类型和相关的公理。比较常用的比如自然数和乘积类型
，在HOL中都可以通过定义的方式形式化的引入 。其中prod代表卡式积， 就是一个tuple或者叫pair。
HOL系统中已经预先定义的一些类型
为了方便讨论， 通常我们会引入一些简单的记号(Melham的书真的是对新人非常友好hhhh,可惜没法做他学生)
| Type | Abbreviation |
|---|---|
Term
HOL中的term表示支持高阶变量和高阶函数的一个谓词演算系统。
无类型的可以有如下的语法
没啥好说的典型的Lambda Calculus的形式 。和STLC一样所有的term必须是类型良好(well typed)的。
HOL中支持三种原始常量term
表示相等关系，
表示客观推出，
表示选择，一个类型谓词到一个具体值的映射函数。当然HOL的库里还有一些通过定义的常量，
. 同时也有一些缩写记号比如
表示
就是函数组合， 都是为了方便书写的。
Sequents , Theroem and Inference Rule
Gorden在HOL中使用的证明风格主要是基于Milner PP的一种自然演绎(nutual deduction)。 其中使用相继式(sequent )来跟踪假设的变化。 相继式可以写为
。其中
和P是两组布尔表达式，
被称为假定(assumption)， 而P被称为结论(conclusion).在HOL中这两者没有什么句法上的区别， 都是布尔类型。 相继式在元语言学断言中也可以读作：存在一个从
中的假定到结论P的自然演绎证明。
当相继式中的是空集的时候也可以写为
这时候， 此时这个P被称为一个在此逻辑下的形式化定理(Theorem)。这个同样也使用于公理(Axiom)。
高阶逻辑的推理规则(inference rule)可以有如下的记号表达：
MP：
这条是肯定前件(Modus Pones), 是HOL中最原始的推理规则。表示横线上的部分可以演绎得到横线下的部分，这种记号表示了一个相继演算，其中相继式是一个在宾语中的断言。 虽说是一个相继演算，但是HOL中的证明系统还是主要基于自然演绎的， 相继式值是仅仅被用来记录一下assumption而以。 所以也应该被读作一个关于自然演绎证明能力的元定理。最初Gorden完成的HOL系统只有五跳公理和8条推理规则。实际在HOL使用过程中有如下的一些常用的规则
HOL的推理规则
...还没完。。。
Ref:
T. F. Melham. 2009. Higher Order Logic and Hardware Verification (1st ed.). Cambridge University Press, New York, NY, USA.
HOL手册
网友评论