Editing Combinatory logic (section)

==In computing==
In [[computer science]], combinatory logic is used as a simplified model of [[computation]], used in [[computability theory]] and [[proof theory]]. Despite its simplicity, combinatory logic captures many essential features of computation.

Combinatory logic can be viewed as a variant of the [[lambda calculus]], in which lambda expressions (representing functional abstraction) are replaced by a limited set of ''combinators'', primitive functions without [[free variables and bound variables|free variable]]s. It is easy to transform lambda expressions into combinator expressions, and combinator reduction is much simpler than lambda reduction. Hence combinatory logic has been used to model some [[non-strict programming language|non-strict]] [[functional programming]] languages and [[graph reduction machine|hardware]]. The purest form of this view is the programming language [[Unlambda]], whose sole primitives are the S and K combinators augmented with character input/output. Although not a practical programming language, Unlambda is of some theoretical interest.

Combinatory logic can be given a variety of interpretations. Many early papers by Curry showed how to translate axiom sets for conventional logic into combinatory logic equations.{{sfn|Hindley|Meredith|1990}} [[Dana Scott]] in the 1960s and 1970s showed how to marry [[model theory]] and combinatory logic.