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 對於直覺邏輯的蘊涵片段是完整的。為了使組合邏輯能模型化為直覺邏輯:


參見

引用

註釋

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

外部連結