Deductive

最近有好多人问我，你到底在做什么。。。。
其实说实话以我现在的水平我也不能说的很清楚。 简单，雪城的计算机从本科开始的教育方针就基本上是偏向于fromal method 的， 对Program Language Theroy 有所了解的人可能会比较熟悉，特别是它在程序静态分析中的应用。嘛。。从定理自动证明器（Theorem Prover）的角度来说， 其实这东西本身就需要用到大量的PLT相关的知识，但是我感觉我目前所学还是有些区别。

0x00

什么是定理（Theorem ）?

定理是一种永远为真的表达式

举个例子？

ground truth is true

有点抽象，能更加具体一点吗

def  ture_is_true():
    return true

Ok明白了， 一个python函数如果返回true那它就是一个theorem

表达式的形式可以有很多， 他可以是形式化的（Formal），也可以是非形式化（unformal）的。是的编程语言是一种Formal的语言。

有了Throem我们就可以做你说的形式验证了吗？

形式验证的话题有点复杂，我们还是先聊聊Deductive System吧

什么是Deductive?

一组由公理（Axiom) 和推论（(Inference Rule）组成的形式系统

cool,虽然还不太明白

0x01

公理和定理有什么区别呢？

定理Theorem 是 公理 Axiom的一个推论Inference

定理可以是一个函数，可是有的函数的返回值并不能像true is true 那么平凡（trival）

是的，所以我们在给出一个定理的本体之后需要给出证明（Proof）

什么是Proof?

Proof是将定理根据inference rule 进行操作和变换最终得到true的过程

所以我们需要逻辑

是的，比如零阶逻辑（zero-order logic）

什么是零阶逻辑？

or and 之类的逻辑运算

听起来不难证明
我上过数学课，数学证明很讲技巧！

是的一种常见的技巧叫做数学归纳（Mathematic Induction）

0x02

数学归纳我知道，给出一个base case和一个归纳假设IH, 就能证明啦。

是的，归纳是一种常见的通过有限的步骤来证明无限结论的方式

无限！ 逻辑运算符怎么会有无限？

因为有时候我们会使用一阶逻辑（First-Order Logic）, 他包含了全称量词（Universal Qantifier）forall(∀), exists(∃).

举个例子

所有的自然数加0都等于自己本身 for all arbitrary nature number a, a + 0 = a

所以我们只需要证明
0+0 = 0
在n+0 = 0时候有n+1+0=n+1

是的，不过有的时候可能还不够，我们需要超限归纳法，或者完全归纳法（complete induction）

什么叫完全归纳？

归纳假设更加强， 我们可以不但实用上一步作为假设，之前的所有步骤都可以作为假设进行归纳

听起来挺复杂的。。。。，这有什么限制么

步骤n 真的能够推回到第0步

我们需要证明它吗？

是的，你需要证明它的测度（measure）每一步都在减小

比如？

list的一种测度是它的长度，递归的时候我们每次都会缩短，所以有限次缩短一定能到0

听起来我们没有用 Formal language!!!

嘛。。形式化无非是用符号或者代码去描述罢了，下次再说吧