B,C,K,Wシステム

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

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

コンビネータは次のように定義される：

  • 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 y の関数合成;
  • C x y z は引数 y z を交換する;
  • K x y は引数 y を破棄する;
  • W x y は引数 y を複製する。

近年では、2つの基本的な定数記号 S, K（及び SKK と外延的に同値な閉項 I）からなる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 (S K)

逆に、S, K, I は B, C, K, W からなる項によって次のように表現できる：

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

目次

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

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

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: \dfrac{A\to B\ A}{B}

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

関連項目 [編集]

脚注 [編集]

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

参考文献 [編集]

外部リンク [編集]

「http://ja.wikipedia.org/w/index.php?title=B,C,K,Wシステム&oldid=47262997」から取得