La B, C, K, W sistema es una variante de lógica combinatoria que toma como primitiva la combinadores B, C, K , y W . Este sistema fue descubierto por Haskell Curry en su tesis doctoral Grundlagen der kombinatorischen Logik , cuyos resultados se exponen en Curry (1930).
Definición
Los combinadores se definen de la siguiente manera:
- B x yz = x ( yz )
- C x yz = xzy
- K x y = x
- W x y = xyy
Intuitivamente
- B x yz es la composición de los argumentos x y y aplicada a la argumento z ;
- C x yz intercambia los argumentos y y z ;
- K x y descarta el argumento y ;
- W x y duplica el argumento y .
Conexión a otros combinadores
En las últimas décadas, el cálculo del combinador 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 se pueden expresar en términos de S y K de la siguiente manera:
- B = S ( KS ) K
- C = S ( S ( K ( S ( KS ) K )) S ) ( KK )
- K = K
- W = SS ( SK )
Yendo en la otra dirección, SKI se puede definir en términos de B, C, K, W como:
- I = WK
- K = K
- S = B ( B ( BW ) C ) ( BB ) = B ( BW ) ( BBC ). [1]
Conexión con la lógica intuicionista
Los combinadores B , C , K y W corresponden a cuatro axiomas bien conocidos de la lógica oracional :
- AB : ( B → C ) → (( A → B ) → ( A → C )),
- CA : ( 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 inferir 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 de la ley del medio excluido , por ejemplo, la ley de Peirce ;
- La lógica clásica completa , requeriría el análogo combinatoria con el axioma oracional C → A .
Ver también
Notas
- ^ Raymond Smullyan (1994) Diagonalización y autorreferencia . Universidad de Oxford. Presione: 344, 3.6 (d) y 3.7.
Referencias
- Hendrik Pieter Barendregt (1984) El cálculo Lambda, su sintaxis y semántica , vol. 103 en Estudios de Lógica y Fundamentos de las Matemáticas . Holanda Septentrional. 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). Lógica combinatoria . Vol. II. Amsterdam: Holanda Septentrional. ISBN 0-7204-2208-6.
|volume=
tiene texto extra ( ayuda ) - Raymond Smullyan (1994) Diagonalización y autorreferencia . Universidad de Oxford. Prensa.
enlaces externos
- Keenan, David C. (2001) " Diseccionar un ruiseñor " .
- Rathman, Chris, " Combinator Birds " .
- " " Combinadores de arrastrar y soltar (subprograma Java). "