B,C,K,Wシステム

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

B, C, K, Wシステムは、基本的な4つの定数記号 B, C, K, W からなるコンビネータ論理の変種である。この体系はハスケル・カリーの博士論文Grundlagen der kombinatorischen Logikによるもので、その結論部分はCurry 1930において示された。

概要[編集]

定数記号 B, C, K, W の簡約基の簡約規則は次のように定義される:

  • B x y zx (y z)
  • C x y zx z y
  • K x yx
  • W x yx y y

これらのコンビネータは、直感的に次のような働きをするものと考えられる:

  • B x y は関数合成。
  • C x y z は引数交換。
  • K x y は破棄;
  • W x y は複製。

2つの基本的な定数記号 S, K(及び SKK と外延的に同値な閉項 I)からなるSKIコンビネータ計算があり、ここでは B, C, WS, K からなる項によって次のように表現できる:

  • B = S (K S) K
  • C = S (S (K (S (K S) K)) S) (K K)
  • K = K
  • W = S S (S K)

一方で、S, K, IB, C, K, W からなる項によって次のように表現できる:

  • I = W K
  • K = K
  • S = B (B (B W) C) (B B) = B (B W) (B B C).[1]

すなわち、SKIコンビネータ計算とB,C,K,Wシステムは等価な計算体系である。

直観主義論理との関係[編集]

定数記号 B, C, K, W はそれぞれよく知られた4つの命題論理の公理と対応する[2]

AB: (BC) → ((AB) → (AC)),
AC: (A → (BC)) → (B → (AC)),
AK: A → (BA),
AW: (A → (AB)) → (AB).

関数適用はモーダスポネンスに対応する:

MP: A\to B,A\vdash B

公理 AB, AC, AK, AW 及び推論規則 MP は、直観主義命題論理含意断片英語版に対して完全である。この体系に爆発原理 FA排中律に類する規則(例:パースの法則英語版)を加えたものは古典命題論理と対応する。コンビネータ W とそれに関する公理図式を取り除いたものはBCK論理と対応する。これはBCK-λ計算と対応するものである。

関連項目[編集]

脚注[編集]

  1. ^ Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.
  2. ^ より正確には、定数記号の型と公理図式とが対応する。

参考文献[編集]

外部リンク[編集]