处理「定义」最简单的方式我想应该是先区分「後设语言」(meta-language) 和 「对象语言」(object language), 然後说「定义」是後设语言里的机制， 目的是为了方便写出对象语言里常用或重要的样式。 我自己的经验是传统数学里很少谈「型式」「语法」(syntax) 这类数学物件， 到了後设数学必须谈这些了，传统数学写作风格却又容易让後设语言和 对象语言混杂在一起。相较之下，程式的本质是符号操作 (symbol/syntax manipulation), 程式员的工作是撰写（後设）符号以操作（对象）符号， 因此若有程式基础，要区分後设语言和对象语言应该是很容易的。 以下我尝试简单介绍一下程式观点，用的语言基本上是 Haskell: http://www.haskell.org 但符号上略作变动以利数学背景读者理解，也不使用 Haskell 的完整语意。 前半段是 Haskell 简介，後半段我用 Haskell 写一点点命题逻辑，藉以说明 後设语言和对象语言之分别，以阐明上述「定义为後设语言里的机制」之意思。 Haskell 程式是由「函式定义」构成，例如 double : Int -> Int double x = x + x square : Int -> Int square x = x * x 这里定义两个函式 double 和 square, 它们都接收一个整数并算出另一个整数。 （注意 Haskell 语法上套用函式时不写 double(x) 而只写 double x, 但必要时 还是要加括号。欸，细节就不详述了... 这篇的例子应该都可以看懂才是。） Haskell 程式执行就只是把一个给定式子尽量化简，遇到函式时参考其定义， 将等号左边的样式换成右边的式子。例如 square (double 4) 的计算过程是 square (double 4) = square (4 + 4) = square 8 = 8 * 8 = 64 （假设 '+' 和 '*' 的行为是我们熟悉的那样）计算结果即为 64. 简单地说：直接理解成数学上的代换就行了。 在 Haskell 里面我们可以处理比 Int 更复杂的资料型态 (datatypes), 例如下面这行 data IntList = Nil | Cons (Int × IntList) 定义了一个新的型态 IntList（想像成集合），里面的元素是用 Nil : IntList 和 Cons : Int × IntList -> IntList 自由生成的。（Nil 本身就是个 IntList；Cons 接收一个 Int 和一个 IntList, 产出一个 IntList.）例如以下 Nil Cons (0, Nil) Cons (0, Cons (1, Nil)) Cons (0, Cons (1, Cons (2, Nil))) 都是 IntList 的元素（如同 0, 1, 2 都是 Int 的元素一般）。 如此定义的资料型态我们称为「代数型态」(algebraic datatypes). Haskell 提供一种机制「样式匹配」(pattern matching) 让我们在代数型态上定义函式。 例如，我们可以写一个函式把某个 IntList 里面所有的整数加起来： sum : IntList -> Int sum Nil = 0 sum (Cons (x, xs)) = x + sum xs 如此我们便指定当 sum 遇到 Nil 和 Cons 时应如何化简。 因为 IntList 的元素只可能用 Nil 和 Cons 构造出来，有了以上两条化简规则， sum 便对任何 IntList 都定义妥当（亦即对任何 IntList 都能确切算出一个 Int）。 例： sum (Cons (0, Cons (1, Nil))) = 0 + sum (Cons (1, Nil)) = 0 + 1 + sum Nil = 0 + 1 + 0 = 1 至此 Haskell 简介结束。 接下来我们考虑命题逻辑语言最简单、仅有「蕴含」的版本。 这语言在 Haskell 里定义成 data Prop = Var Int | Imp (Prop × Prop) 我们用 Prop 的元素表示「命题式」 (propositional formulae), 而且变数 直接以整数命名（而非常见的 P, Q, R, ... 之类的）。 例如 Imp (Imp (Imp (Var 0, Var 1), Var 0), Var 0) 代表的是 Peirce's law, 对应的一般写法是 ((P => Q) => P) => P （假设 P 对应於 0, Q 对应於 1.） 命题逻辑上可定义二值语意：令真假值之型态为 data Bool = False | True 则命题式之真假值可如此定义： truth : (Int -> Bool) × Prop -> Bool truth (s, Var x) = s x truth (s, Imp (p, q)) | truth (s, p) == False = True | otherwise = truth (s, q) 即：固定变数上的真假值（表示为一个 Int 到 Bool 的函式），给定一命题式， 此命题式只可能是变数或蕴含型式。第一个情况时，直接回传赋予该变数之真假值； 第二个情况时，令前件为 p, 後件为 q, 若 p 的真假值为 False, 整个命题式之真假值即算为 True, 反之则算为 q 之真假值。 循此脉络，可继续以 Haskell 写下命题逻辑其余定义（然後证明定理）。 但至此我们已经可以试着理解後设语言和对象语言的分别：我们探讨的「对象」 是命题逻辑的语言，而探讨所用的（後设）语言是 Haskell. 命题逻辑语言 在 Haskell 里面定义成一个资料型态（命题式之集合），其元素是以 Var 和 Imp 自由生成的树状结构，本质只是纯粹的符号，而我们写 Haskell 程式 来操作这些符号。传统数理逻辑的後设语言和对象语言直觉上太过类似，从而 容易混淆两种语言，改用 Haskell 的好处是後设语言和对象语言变得很容易区分 （前者是整个 Haskell, 後者只是用 Haskell 写下的一个资料型态）。 最後我们回到一开始的问题：何谓定义？例如，定义 bi-implication P <=> Q 为 (P => Q) /\ (Q => P) 是什麽意思？假设我们扩充 Prop 的定义，多加一条 Conj (Prop × Prop) 代表 conjunction. 双向蕴含在 Haskell 便写为 biImp : Prop × Prop -> Prop biImp (p, q) = Conj (Imp (p, q), Imp (q, p)) 即：biImp (p, q) 是在後设语言里对 Conj (Imp (p, q), Imp (q, p)) 的缩写， 而不是对象语言内的构件。更进一步的定义可引用既有定义，但最终会全部 化简（展开）为对象语言。一般说数学基础是公理化集合论也是这个意思： 数学用的符号繁多，但这些（原则上）最终都可化简（展开）为集合论的单纯语言。 ※ 引述《yueayase (scrya)》之铭言： : 看了以上的讨论, 我不知道type theory和逻辑符号语言之间的差别 Martin-Lof's type theory 可理解为表达能力极其丰富的程式语言或 具完整计算意义的数学基础理论（包括高阶逻辑）—「直构数学」 (intuitionistic mathematics) 的定理与证明可在 MLTT 内型式化， 并等价於真正能跑的程式。 这领域仍在火热发展，如近年来由 Fields Medal 得主 Vladimir Voevodsky 领军的 univalent foundations of mathematics http://uf-ias-2012.wikispaces.com 企图将 homotopy theory 带入 type theory, 打造数学的全新基础。（不过我不熟...） : 因为我也曾经看过像logic set and recursion(http://ppt.cc/PatL)之类的书 : 里面主要就是在说逻辑符号系统的language structure是怎样 : 怎样去interpret这些language意思 : 像之前提到的 A Mathematical Introduction to Logic也是在说这些东西 : 就不是很清楚type theory和这类书籍所说的有什麽差别 : 附带一提, : 这些东西又好像和computer science 的 formal language(eg: context-free grammar) : 或是 computation theory(eg: Turing machine <=> λ-calculus, decidability...) : 有一些关联 : 的确, 听说作Artificial Intelligence的人, 早期好像也在研究logic... 是的，关联密切。整个来龙去脉详细要说清楚得花不少篇幅，所以直接打个广告： 这些在「逻辑、语言、与计算」暑期研习营（的偶数年）会提到！课程教材都会上网， 例如去年的在这里： http://flolac.iis.sinica.edu.tw/flolac12 -- 感谢 xcycl 邀我下水以及审稿。 --

※ 发信站: 批踢踢实业坊(ptt.cc) ◆ From: 86.2.123.53 ※ 编辑: joshs 来自: 86.2.123.53 (04/19 09:00)