类型系统和逻辑
计算机科学领域中一个重要成就是:类型理论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的值,要么是一个摧毁世界的机制?至少我不能,许多经典逻辑规则在你只思考“真理”这个抽象概念时是很明显正确的,但是当我们从“可证明”角度考虑时很显然没有意义了。
....