B,C,K,W系统
1930年哈斯凯尔·加里在他的博士论文《Grundlagen der kombinatorischen Logik》中提议了一个组合子逻辑系统。它带有基本组合子B、C、K和W(采用了现在的命名)。
定义
- B x y z = x(y z)
- C x y z = x z y
- K x y = x
- W x y = x y y
直觉上,
在当代,只有两个基本组合子K和S的SKI组合子演算成为了组合子逻辑的规范方式。B, C和W可以使用S和K表达为如下:
- B = S (K S) K
- C = S (S (K (S (K S) K)) S)(K K)
- K = K
- W = S S(K (S K K))
在另一个方向上,SKI可以依据B,C,K,W定义为:
- I = W K
- K = K
- S = B (B (B W) C) (B B)[1] = B (B B B W B) C
与直觉主义逻辑的连结
组合子 , , 和 对应于众所周知的命题逻辑四公理:
- AB: (B → C) → ((A → B) → (A → C)),
- AC: (A → (B → C)) → (B → (A → C)),
- AK: A → (B → A),
- AW: (A → (A → B)) → (A → B).
而函数应用对应于肯定前件
- MP: 如果 A 且 A → B,则 B。
公理 AB, AC, AK 和 AW 以及函数应用规则 MP 对于直觉逻辑的蕴涵片段是完整的。为了使组合逻辑能模型化为直觉逻辑:
参见
引用
- Hendrik Pieter Barendregt(1984)The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies in Logic and the Foundations of Mathematics. North-Holland. ISBN 978-0-444-87508-2
- Haskell Curry(1930)"Grundlagen der kombinatorischen Logik," Amer. J. Math. 52: 509-536; 789-834.
- Curry, Haskell B.; J. Roger Hindley, and Jonathan P. Seldin. Combinatory Logic Vol. II 2. Amsterdam: North Holland. 1972. ISBN 978-0-7204-2208-5.
- Raymond Smullyan(1994)Diagonalization and Self-Reference. Oxford Univ. Press.
注释
- ^ Raymond Smullyan(1994)Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d).
外部链接
- Keenan, David C. (2001) "To Dissect a Mockingbird."
- Rathman, Chris, "Combinator Birds.(页面存档备份,存于互联网档案馆)"
- ""Drag 'n' Drop Combinators (Java Applet)."