《通往逻辑、数学和编程的Haskell之路》—— 一阶逻辑的形式和意义(3)

我们上篇笔记的目的是熟悉五大逻辑连接符如何用Haskell定义和表示，下面再简单总结一下（假定你已经进入GHCi的repl环境，并成功:load TAMO.hs）：
否定（非）：
not : : Bool -> Bool
not True = False
not False = True
合取（与）：
(&&) : : Bool -> Bool -> Bool
False && x = False
True && x = x
注意：若一个连接符由多个字符组成，那么定义时必须用括号
析取（或）：
(||) : : Bool -> Bool -> Bool
False || x = x
True || x = True
蕴含（若...则）：
infix 1 ==>
(==>) : : Bool -> Bool -> Bool
x ==> y = (not x) || y
或者
True ==> x = x
False ==> x = True
其中，
infix 1 ==>
表示“==>”这个运算符是由用户定义，它的句法规则是中缀式，运算优先顺序是9-0中的1，数字越大优先度越高。
双蕴含（等价）（当且当）：
infix 1 <=>
(<=>) : : Bool -> Bool -> Bool
x <=> = x == y
注意这里的符号用法：“=”在这里的意思是“定义为”，而“==”是一阶谓词，返回True或False
排他析取（排他或）
infix 2 <+>
(<+>) : : Bool -> Bool -> Bool
x <+> y = x /= y
其中，“/=”是一阶谓词，是“==”的否定，亦即：not ==
本篇笔记的内容是关于真值表、逻辑公式和永真式的问题。
首先假定你已经在Haskell的repl环境GHCi中、并加载了TAMO.hs，并且用文本编辑器打开了TAMO.hs（以下简称源文件）。
这时你的repl提示符应当是：
*TAMO>
这时如果你键入小写字母p
*TAMO> p
False
键入小写字母q
*TAMO> q
True
键入大写字母P
*TAMO> P
<interactive>:28:1: Not in scope: data constructor ‘P’
出错了！如果你浏览一下TAMO.hs源文件会发现在第21行和22行，对命题字母p和q都定义了相应的真值，但是却没有对P的定义。
下面我们看一下第24行：这是一个命题逻辑的句子，之所以是句子是因为这个表达式有确定的真值。如果键入这个句子的名称formula1
*TAMO> formula1
False
源文件中是这个句子的Haskell表示法
formula1 = (not p) && (p ==> q) <=> not (q && (not p))
如果是用常规的命题逻辑语言表示
formula1 = ~p ∧(p → q) ↔︎ ~(q ∧ ~p)
如果做真值表
                
                
根据源文件，我们知道p=False，q=True
所以按照上述真值表，formula1=False
如果我们更改p和q的值，
*TAMO> let p = False
*TAMO> let q = False
这时，根据上述真值表，formula1的真值应当是True
*TAMO> formula1
False
咦！为什么？先不说为什么了，现在我们不用formula1这个名字，而直接把这个句子键入：
*TAMO> (not p) && (p ==> q) <=> not (q && (not p))
True
为什么会出现这样的不一致？这是因为当我们改变p和q的值时，并没有改变源文件中的p和q的值，而只是重新定义了一个新值。所以formula1使用的值，仍然是源文件定义的值。如果想要formula1反映新的真值，就必须修改源文件，将q改成False，再次保存文件，然后，重新加载TAMO.hs文件
*TAMO> :load TAMO.hs
如果嫌打字麻烦，可以
*TAMO> :l tamo
在调入文件时，repl环境是不区分大小写的，而且，只要文件扩展名是.hs，就可以省略。
这时重新调用formula1
*TAMO> formula1
True
有了这些基本的概念和技巧，我们可以通过repl环境建立真值表了
首先，定义p和q的真值为True
*TAMO> let p = True
*TAMO> let q = True
现在我们定义自己的句子，命名为F1
*TAMO> let F1 = (not p) && (p ==> q) <=> not (q && (not p))
现在，调用F1
*TAMO> F1
False
然后我们依次赋予p、q不同的值
p=True q=False
测试F1
*TAMO> F1
False
p=False q=True
*TAMO> F1
False
p=False q=False
*TAMO> F1
True
这样，只要我们给出句子中原子命题字母的真值，Haskell就会自动计算、给出整个句子的真值。
 如果我们检查F1的类型
*TAMO> :type F1
F1 : : Bool
这时我们知道F1是一个常项函数，所谓常项函数就是只有输出没有输入的函数，所以从广义来说，任何一个常项，例如True、False、10、2.178等，都可以看做是常项函数。例如：
*TAMO> :type False
False : : Bool
和我们定义的F1属于同一类型。但是为什么不叫常项、或常量，而叫常项函数？我们知道Haskell是基于函数的语言，而函数语言的基础是λ-演算，λ-演算对常项的定义λx . e，其中e是除x以外的任何λ-项。而在我们现在的例子中，e就是布尔值False。
下面我们回到主题，看一下另一个例子，源文件中的formula2。如果已经知道公式名，想知道这个公式的定义，可以在repl中键入
*TAMO> :info <公式名>
例如
*TAMO> :info formula2
formula2 :: Bool -> Bool -> Bool -- Defined at tamo.hs:26:1
这里不但给出了类型定义，还给出了这个公式在源文件中的位置：文件名和行号。所以我们可以查看文件中的第26行
formula2 p q = ((not p) && (p ==> q) <=> not (q && (not p)))
从上面的:info可知，formula2的类型和formula1完全不同，是典型的函数，因为它需要两个类型为Bool的参数。所以，在调用formula2时，后面必须要跟两个已定义的命题字母
*TAMO> formula2 p q
False
为了尽快熟悉Haskell表达逻辑公式的格式，这里就不再翻译成一阶语言。利用上面的方法我们也可以为formula2建立真值表。
从逻辑的角度，formula2和formula1的区别是：前者公式中的p和q是变项，后者是常项。正如上面所说，formula2是标准的函数，称作命题函数，或真值函数，或者，布尔值函数。在函数的类型定义中，我们需要正确解读定义的含义
formula2 : : Bool -> Bool -> Bool
函数名后面的双冒号可以理解为函数名作用于一个布尔值类型，箭头右侧表示函数值，因此，这个定义的解读是
((formula2 : : Bool) -> Bool) -> Bool
函数名作用于第一个Bool项，得到新函数(formula2 : : Bool) ，再作用于第二个Bool项的((formula2 : : Bool) -> Bool)，得到第三个Bool项。
这有点像我们做加法或乘法计算，从左到右，先计算前两项，然后计算的结果和后一个项再进行计算直到最后一项。
下面介绍永真式的概念和Haskell的表达。
永真式，又称重言式，是指句子的真值不受句子内部分表达式真值的影响，永远为真。例如排中律表达式：p∨~p，用Haskell语言表示：
let excluded_middle p = p || not p
这个定义可以在源文件第32行找到，或者用
*TAMO> :info excluded_middle
命题函数的类型是：
excluded_middle : : Bool -> Bool
为了实验其永真性，我们这里不用源文件，而是自己定义：
1. let p = True
2. let excluded_middle p = p || (not p)
3. excluded_middle p
3. let p = False
4. excluded_middle p
不管p的值是True还是False，excluded_middle的返回值都是True。
在源文件中，我们可以找到两个函数，分别是valid1和valid2，用来检查给定的公式、函数是否是永真式。其中，valid1用来检查单参数的命题函数，例如像excluded_middle，valid2用来检查双参数命题函数，例如像formula2。
*TAMO> valid1 excluded_middle
True
*TAMO> valid1 formula2
False
说明命题函数excluded_middle是永真式，而formula2不是。
这里最有意思的是，作为函数valid1和valid2的参数也是函数，所以它们的定义也反映了这个特点：
valid1 :: (Bool -> Bool) -> Bool
valid1 bf = (bf True) && (bf False)
这种定义法，正如上篇笔记所指出的，反映了函数的二象性：外延性和内涵性。在外延性定义中，我们知道函数valid1是一个单参数函数，而这个参数也是一个从Bool到Bool的函数，而valid1的返回值是Bool。而内涵性定义中，bf是作为参数的函数，这个函数要调用两次，第一次给出参数True，第二次False，如果这两次的结果都为True，则valid的函数值为True，否则为False。这等于是自动遍历了作为参数的函数的真值表，如果在给定所有原子项的真值组合后所有的真值都为True的情况下（永真式）则返回True。
类似的，我们可以看到valid2的定义：
valid2 :: (Bool -> Bool -> Bool) -> Bool
valid2 bf = (bf True True)
           && (bf True False)
           && (bf False True)
           && (bf False False)
valid2的外延定义是以一个双参函数为参数，返回Bool值；
valid2的内涵定义是遍历双值参数的所有True和False的组合，如果均为True，则返回True，作为参数的命题函数是永真式。
Haskell可以自动化我们建立真值表的过程，这一点特别当句子的结构非常复杂时非常有用，可以看做是我们的命题逻辑公式计算器吧。
如果你有兴趣了，可以建立一个德摩根恒等式，然后利用valid2检查其永真性。