B, C, K, W system

The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This system was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik, whose results are set out in Curry (1930).

Definition

The combinators are defined as follows:

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

Intuitively,

  • B x y z is the composition of the arguments x and y applied to the argument z;
  • C x y z swaps the arguments y and z;
  • K x y discards the argument y;
  • W x y duplicates the argument y.

Connection to other combinators

In recent decades, the SKI combinator calculus, with only two primitive combinators, K and S, has become the canonical approach to combinatory logic. B, C, and W can be expressed in terms of S and K as follows:

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

Going the other direction, SKI can be defined in terms of B,C,K,W as:

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

Connection to intuitionistic logic

The combinators B, C, K and W correspond to four well-known axioms of sentential logic:

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

Function application corresponds to the rule modus ponens:

MP: from A and A → B infer B.

The axioms AB, AC, AK and AW, and the rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model:

See also

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

References
  • Hendrik Pieter Barendregt (1984) The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies in Logic and the Foundations of Mathematics. North-Holland. ISBN 0-444-87508-5
  • Haskell Curry (1930) "Grundlagen der kombinatorischen Logik," Amer. J. Math. 52: 509–536; 789–834.
  • Curry, Haskell B.; Hindley, J. Roger; Seldin, Jonathan P. (1972). Combinatory Logic. Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
  • Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.