类型系统和逻辑

15-01-04 banq
              

计算机科学领域中一个重要成就是:类型理论type theory对应于一个特别的逻辑系统。Type systems and logic一文以Haskell语言为例详细介绍了其中细节:

那么这种对应到底是怎样的?其基本思想来自于Curry-Howard Correspondence. 一个类型被解释为一个命题proposition, 而一个值被解释为一个命题的证明proof, 大部分标准逻辑连接词都来自于这个思想。

举例来说:(A, B)的一对类型的值是类型A和B值的一对, 这意思是:它们是A和B的证明的一对,那就意味着(A, B)代表了逻辑连接词“A && B”.

同样类似,逻辑分离词disjunction (“A | | B”)代表一个所谓“标签联合tagged union”类型: A B两者中任何一个的值(证明) 是A的值(证明)或者是B的值(证明)。

类似 Int 和 String类型都是命题 – 你能认为像这些简单类型只是代表某种陈述:也就是“一个 Int存在” 或 “一个String存在”. 1是Int的证明, 而 "hands"是 String的证明. (Int, String) 是一个简单类型组, 陈述的是 “有存在一个Int和有存在一个String”,(1, "hands")是 (Int, String)的证明。

如果你不熟悉Haskell,Either类型会更加神秘一些, 类型Either a b 代表包含一个类型值出现在Either的左边,而类型b的值出现在Either的右边. 所以,Either Int String 意味着“可能存在一个Int或存在一个String”, 它被可能左边的1 或右边的"hands"证明了. 这种左右标签确保你在出现两个同样类型时,不会丢失任何信息。

如果两个类型相同,如:Either Int Int能被左边的1 或者右边的1证明, 这可以从它们彼此标签位置来进行区分。

当你思考蕴涵逻辑implication时会更加有趣. 函数的类型是转换类型A的值 (证明) 到类型B的值 (证明) ,也就是A -> B. 这意味着一个函数是也一个证明,这个证明代表:无论什么时候有一个A的证明,你都能得到B的证明,“如果A是真,那么B是真”(“if A is true, then B is true.”) ,这样函数是一种代表关系的蕴涵逻辑的证明。

有一件事比较奇怪,代表“not A”的命题是使用类型 A -> ⊥, 这里字符“ ⊥ ”被称为一个空类型,所谓空类型也就是没有值的类型,(类型的符号来自于数学,它通常代表明确的 “bottom.”含义), A -> Void可以被读作:“如果我们有一个A, 我们能用它做些不存在的事情” –相对“我们并没有一个A”,这有一个很大的延伸,这好像是一种否定句,但是有一个问题: 在经典逻辑中,否定是可逆的reversible. 你能说“not (not A),” 经典逻辑认为那等同于说“A.”

看来经典逻辑是正确的 – 如果A不是假, 它一定是真, 对吗? 但是如果我们使用 A -> Void 作为否定的定义, 我们通常的直觉和经典逻辑规则就Hold不住了,一个类型(A -> Void) -> Void的值并不会让你得到一个 类型A的值,双否定不等同于正肯定了,这意味着什么?

这里其实代表了范式切换,.类型系统并不对应经典逻辑, 而是对应一种称为“constructive logic(构造逻辑)”. 这个范式切换是这样:我们从思考一个事物是否是真, 切换到我们是否能够证明它们,更重要的是,我们不再考虑是否存在等量化词(existential quantifications ),除非它被一个案例证明。

我们不能通过矛盾contradiction来证明, (比如:“至少肯定存在一个蓝色的事物,因为如果没有,那么我们就有矛盾了”). 相反,如果我们展示某个事物一些属性的存在,我们就能够发现这个事物,(“至少肯定存在一个事物,这个细节已经表明”). 只要我们记住我们的逻辑模型是可证明的,而不是单纯的真理(banq注:单纯的真理代表灌输:我就是比你强,我说的话就是真理,没有我就没有你们,这些都是单纯的真理,你只要记住就可以,无需知道如何证明它们,它们是怎么得出的)。

让我们重新考虑“not (not A)”这个案例,在构造逻辑constructive logic中 , 一个 A -> Void的证明, 或者 “not A,”的证明,是一个机制,其将获取一个 A,不能做任何事,返回了命题"false"的证明,如果你有一个实际的假false的证明 (比如如果你既有一个 A 和一个 A -> Void 同时满足), 那就很坏: 在大多数逻辑中,你能用这个不可能逐个证明其他任何事,所有陈述都是等同,它们都是true且false。如果你将逻辑自身作为一个小宇宙,那么在那里逻辑规则就是物理规律,那么你可以说一个假false的证明会摧毁这个小宇宙,将黑洞会吸入整个宇宙到一个单点。

那么,回到not A. 大部分我们感兴趣的逻辑是“一致性consistent”, 其基本意思是那是不可能摧毁整个宇宙的。那么, A -> Void 意味着 “如果你给我一个 A, 我会摧毁整个世界” – 也就是说,如果我们用一致性逻辑,我们证明了 A -> Void, 我们知道就不可能证明A. 这样 A -> Void 似乎只能是我们预期的not A 的意思.

最后,回到双否定,如果 not A 是 a -> Void, 那么not (not A)就是 (A -> Void) -> Void, 或者 “如果你给我一个机器,获得输入A,并摧毁整个世界,那么我也将摧毁整个世界.” 但是这其实不会给你一个A,如果你关心一些不可触及的真理概念,你会肯定将这个概念应用到A,但是以我们构成主义的逻辑来说,我们现在不感兴趣真相,我们只感兴趣为什么(As)。

双否定的离奇怪异来自于排中律(the Law of the Excluded Middle) – 对于任何命题“A”, 或者 “A”是真或者“not A”是真 – 但这并不符合构造逻辑(constructive logic).

当你谈论抽象的真理时,很显然,任何命题要么是真要么是假,但是涉及证明时 – 你能建立吗?你能建立一个没有任何信息的盒子,当你输入一个类型A的值时,它要么是类型A的值,要么是一个摧毁世界的机制?至少我不能,许多经典逻辑规则在你只思考“真理”这个抽象概念时是很明显正确的,但是当我们从“可证明”角度考虑时很显然没有意义了。

....

              

3
banq
2015-01-04 13:59

基于类型的逻辑让我们使用构造逻辑而不是经典逻辑,而且以这样一种奇怪扭曲的方式否定排中律,为什么我们要这么做?

有一些理由,首先,构造逻辑其实不奇怪,只要你以它的方式思考,在经典逻辑中,排中律是“对于任何语句P,要么P是真,要么是假”,听起来很显然,但是在构造逻辑中,最好将这个法则叙述为:“对于任何语句P,要么我具备P的证明,要么我具备P的反证”,现在哪个是明显错误的呢?

我并不是无所不知,即使我是,我们也知道应该有一个语句,既不能可被证明,也不能被反证。

但是我们是要谈论的是可证明而不是真理,有很多理由,其中一个主要是:真理对于计算是无用的,而证明则不是,构成主义思想比经典逻辑更加严密,一个构成的证明比非构成的经典逻辑会包含很多可用来分析的信息,在计算科学中,我们都是构成逻辑的特别粉丝,因为一些规定实现对于构成证明来说是这样:存在一段程序满足那条规定约束。

通常,你也会通过构造证明来很多解决头脑中哪些是"可用的可实现的"想法,但是如果你有一个证明是经典逻辑范围内有效,而不是构造逻辑,那么它不能告诉你任何是否可用可实现的判断。所以,构造性证明是更靠近实践。(banq注:实践是检验真理唯一标准 这句话已经不重要,重要的是我们的真理要更靠近实践,否则无用,也无需等待实践检验,也肯定等不到检验,只能蒙混下去)。

构造逻辑对于我们知识如何工作是很好的模型,一个命题可以是真或假,但是我们不会知道它是真,除非我们有一个证明,排中律则是从一个旁观者角度观察和俯瞰数学的柏拉图王国(从数学外部观看),而从里面我们不能看到任何纯洁如水晶的真理,一个语句“要么是真,要么是假”对于我们很少有用。(banq注:敌人反对的我们赞成等语句属于经典逻辑)