rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model: The implicational fragment of classical logic, would require the combinatory analog to the law of excluded middle, i.e., Peirce's law; Complete classical logic, would require the combinatory analog to the sentential axiom . This connection between the types of combinators and the corresponding logical axioms is an instance of the Curry–Howard isomorphism. Examples of reduction There may be multiple ways to do a reduction. All are equivalent, as long as you don't break order of operations See also Combinatory logic B, C, K, W system Fixed point combinator Lambda calculus Functional programming Unlambda programming language The Iota and Jot programming languages, designed to be even simpler than SKI. To Mock a Mockingbird References A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors. are a more formal introduction to combinatory logic, with a special emphasis on fixed point results. External links O'Donnell, Mike "The SKI Combinator Calculus as a Universal System." Keenan, David C. (2001) "To Dissect a Mockingbird." Rathman, Chris, "Combinator Birds." ""Drag 'n' Drop Combinators (Java Applet)." A Calculus of Mobile Processes, Part I (PostScript) (by Milner, Parrow, and Walker) shows a scheme for combinator graph reduction for the SKI calculus in pages 25–28. the Nock programming language may be seen as an assembly language based on SK combinator calculus in the same way that traditional assembly language is based on Turing machines. Nock instruction 2 (the "Nock operator") is the S combinator and Nock instruction 1 is the K combinator. The other primitive instructions in Nock (instructions 0,3,4,5, and the pseudo-instruction "implicit cons") are not necessary for universal computation, but make programming more convenient by providing facilities for dealing with binary tree data structures and arithmetic; Nock also provides 5 more instructions (6,7,8,9,10) that could have been built out of these primitives. Lambda calculus Combinatory logic