B,C,K,W系统

1930年哈斯凯尔·加里在他的博士论文《Grundlagen der kombinatorischen Logik》中提议了一个组合子逻辑系统。它带有基本组合子BCKW(采用了现在的命名)。

定义

  • B x y z = x(y z)
  • C x y z = x z y
  • K x y = x
  • W x y = x y y

直觉上,

  • B x y是函数复合x o y
  • C x y z交换参数y和z
  • K x y忽略第二个参数y
  • W x y复制参数y

在当代,只有两个基本组合子KSSKI组合子演算成为了组合子逻辑的规范方式。B, CW可以使用SK表达为如下:

  • B = S (K S) K
  • C = S (S (K (S (K S) K)) S)(K K)
  • K = K
  • W = S SK (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: (BC) → ((AB) → (AC)),
AC: (A → (BC)) → (B → (AC)),
AK: A → (BA),
AW: (A → (AB)) → (AB).

而函数应用对应于肯定前件

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. 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.   )
  • Raymond Smullyan(1994)Diagonalization and Self-Reference. Oxford Univ. Press.

注释

  1. ^ Raymond Smullyan(1994)Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d).

外部链接