B, C, K, W system

B , C, K, W- systemet är en variant av kombinatorisk logik som tar kombinatorerna B, C, K och W som primitiva . Detta system upptäcktes av Haskell Curry i sin doktorsavhandling Grundlagen der kombinatorischen Logik , vars resultat anges i Curry (1930).

Definition

Kombinatorerna definieras enligt följande:

• B x yz = x ( yz )
• C x yz = xzy
• K x y = x
• W x y = xyy

Intuitivt,

• B x y är sammansättningen av x och y ;
• C x är x med den vända argumentordningen ;
• K x är funktionen "konstant x ", som förkastar nästa argument;
• W duplicerar sitt andra argument för den dubbla tillämpningen till det första. Således "förenar" det sitt första arguments två förväntningar på input till en.

Anslutning till andra kombinatorer

Under de senaste decennierna har SKI-kombinatorkalkylen , med endast två primitiva kombinatorer, K och S , blivit den kanoniska metoden för kombinatorisk logik . B, C och W kan uttryckas i termer av S och K enligt följande:

• B = S ( KS ) K
• C = S ( S ( K ( S ( KS ) K )) S ) ( KK )
• K = K
• W = SS ( SK )

Ett annat sätt är, efter att ha definierat B enligt ovan, att ytterligare definiera C = S(BBS)(KK) och W = CSI .

Om man går åt andra hållet kan SKI definieras i termer av B,C,K,W som:

• I = WK
• K = K
• S = B ( B ( BW ) C ) ( BB ) = B ( BW ) ( BBC ).

Också att notera, Y -kombinator har ett kort uttryck i detta system som Y = BU(CBU) där U = WI = SII är självtillämpningskombinatorn.

Koppling till intuitionistisk logik

Kombinatorerna B , C , K och W motsvarar fyra välkända axiom för sententiallogik :

AB : ( B → C ) → (( A → B ) → ( A → C )),

AC : ( A → ( B → C )) → ( B → ( A → C )),

AK : A → ( B ) → A ),

AW : ( A → ( A → B )) → ( A → B ).

Funktionstillämpningen motsvarar regeln modus ponens :

MP : från A → B och A sluter B .

Axiomen AB , AC , AK och AW , och regeln MP är kompletta för det implikationsfragment av intuitionistisk logik . För att kombinatorisk logik ska ha som modell:

• Det implikativa fragmentet av klassisk logik skulle kräva den kombinatoriska analogen till lagen om utesluten mitt, t.ex. Peirces lag ;
• Fullständig klassisk logik skulle kräva den kombinatoriska analogen till meningsakxiomet F → A.

Se även

• Kombinationslogik
• SKI kombinatorkalkyl
• Lambdakalkyl
• Att håna en Mockingbird

Anteckningar

•   Hendrik Pieter Barendregt (1984) The Lambda Calculus, Its Syntax and Semantics, Vol. 103 i Studies in Logic and the Foundations of Mathematics . Nord-Holland. ISBN 0-444-87508-5
• Haskell Curry (1930) "Grundlagen der kombinatorischen Logik," Amer. J. Math. 52 : 509-536; 789–834. https://doi.org/10.2307/2370619
•   Curry, Haskell B. ; Hindley, J. Roger ; Seldin, Jonathan P. (1972). Kombinationslogik . Vol. II. Amsterdam: Norra Holland. ISBN 0-7204-2208-6 .
• Raymond Smullyan (1994) Diagonalization and Self-Reference . Oxford Univ. Tryck.

externa länkar

• Keenan, David C. (2001) " To Dissect a Mockingbird. "
• Rathman, Chris, " Kombinatorfåglar. "
• " "Drag 'n' Drop Combinators (Java Applet). "