跳至內容

B,C,K,W系統

出自Taiwan Tongues 台語維基
這是此頁批准，以及是最近的修訂。

一九三空年哈斯凱爾 ・ 加里佇伊的博士論文《Grundlagen der kombinatorischen Logik》中提議了一个組合子邏輯系統。伊帶有基本組合子B、C、K和W（採用這馬的號名）。

定義

  • Bx y z=x ( y z )
  • Cx y z=x z y
  • Kx y=x
  • Wx y=x y y

直覺上，

  • Bx y 是函數複合 x o y
  • Cx y z 交換參數 y 和 z
  • Kx y 忽略第二个參數 y
  • Wx 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)=B(B B B W B)C


佮直覺主義邏輯的連結

組合子 $ B $ , $ C $ , $ K $ 和 $ W $ 對應眾所周知的命題邏輯四公理：


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

  • 古典邏輯的蘊涵命題演算，需要佮排中律相結合，比如講，皮爾士定律；
  • 完整的古典邏輯，需要用組合子模擬著命題公式 F → A。


參見

  • 組合子邏輯
  • SKI 組合子演算

引用

  • Hendrik Pieter Barendregt（一千九百八十四）_ The Lambda Calculus , Its Syntax and Semantics _ , Vol . 一百空三 in _ Studies in Logic and the Foundations of Mathematics _ . North-Holland . ISBN 九百七十八追空九四百四十四抹八七千五百空八孵二
  • Haskell Curry（一千九百三十）" Grundlagen der kombinatorischen Logik , " _ Amer . J . Math . 五十二 _ : 五百空九五百三十六 ; 七百八十九石八百三十四 .
  • Curry , Haskell B . ; J . Roger Hindley , and Jonathan P . Seldin . Combinatory Logic Vol . II二. Amsterdam : North Holland . 一千九百七十二 . ISBN 九百七十八追空抹七千二百空四四淋二千二百空八孵五 .
  • Raymond Smullyan（一千九百九十四）_ Diagonalization and Self-Reference _ . Oxford Univ . Press .

注釋

外部連結

  • Keenan , David C . ( 兩千空一 ) " To Dissect a Mockingbird . "
  • Rathman , Chris , " Combinator Birds . "
  • " " Drag'n'Drop Combinators ( Java Applet ) . "
取自「https://wiki.taigi.ima.org.tw/w/index.php?title=B,C,K,W系統&oldid=485536」