El sistema B, C, K, W es una variante de lógica combinatoria que toma como primitivas a los combinadores B, C, K, y W. Este sistema fue propuesto originalmente por el matemático estadounidense Haskell Curry en su tesis doctoral Grundlagen der kombinatorischen Logik (Fundamentos de la lógica combinatoria).Curry (1930), Amer. J. Math.
Definición Los combinadores se definen como sigue:
B x y z = x (y z) C x y z = x z y K x y = x W x y = x y y
De forma intuitiva,
B x y z es la composición de los argumentos x e y aplicada al argumento z; C x y z intercambia los argumentos y y z; K x y descarta el argumento y; W x y duplica el argumento y.
Conexión con otros combinadores En las últimas décadas, el cálculo combinatorio SKI, con solo dos combinadores primitivos, K y S, se ha convertido en el enfoque canónico de la lógica combinatoria. B, C y W pueden expresarse en términos de S y K como sigue:
B = S (K S) K C = S (S (K (S (K S) K)) S) (K K) K = K W = S S (S K)
En la otra dirección, SKI puede definirse en términos de B, C, K, W como:
I = W K K = K S = B (B (B W) C) (B B) = B (B W) (B B C).Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press: 344, 3.6(d) and 3.7.
Conexión con la lógica intuicionista Los combinadores B, C, K y W corresponden a cuatro conocidos axiomas de la lógica proposicional:
AB: (B → C) → ((A → B) → (A → C)), AC: (A → (B → C)) → (B → (A → C)), AK: A → (B → A), AW: (A → (A → B)) → (A → B).
La aplicación de la función corresponde a la regla modus ponens:
MP: de A y A → B infiere B.
Los axiomas AB, AC, AK y AW, y la regla MP son completos para el fragmento implicacional de la lógica intuicionista. Para que la lógica combinatoria tenga como modelo:
El fragmento implicacional de la lógica clásica, requeriría el análogo combinatorio al principio del tercero excluido, por ejemplo, la ley de Peirce; La lógica clásica completa, requeriría el análogo combinatorio al axioma sentencial F → A.
Véase también
Lógica combinatoria Cálculo lambda
Bibliografía
Hendrik Pieter Barendregt (1984) The Lambda Calculus, Its Syntax and Semantics, Vol. 103 in Studies in Logic and the Foundations of Mathematics. North-Holland. Haskell Curry (1930) "Grundlagen der kombinatorischen Logik," Amer. J. Math. 52: 509–536; 789–834.
Raymond Smullyan (1994) Diagonalization and Self-Reference. Oxford Univ. Press.
Referencias
Enlaces externos
Keenan, David C. (2001) "To Dissect a Mockingbird." Rathman, Chris, "Combinator Birds." ""Drag 'n' Drop Combinators (Java Applet)."
Categoría:Lógica matemática Categoría:Cálculo lambda