最近有好多人问我,你到底在做什么。。。。
其实说实话以我现在的水平我也不能说的很清楚。 简单,雪城的计算机从本科开始的教育方针就基本上是偏向于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!!!
嘛。。形式化无非是用符号或者代码去描述罢了,下次再说吧
网友评论