Overview
The combinatory logic consists of a set of terms and rules for manipulating combinatory expressions to produce new expressions. It forms one of the simplest models of computation.
Specification
The combinatory language consists of a set of terms called variables. {% v_0, v_{1}, ... %} and terms called basic combinators: {% I,K,S %}
The following are the rules for well formed combinatory expressions.
- All variables and combinators are terms
- {% (XY) %} is a term if both {% X %} and {% Y %} are terms.
Substitution
Substitution in a term, written as {% [U/x]Y %} is defined by the following rules.
-
{% [U/x]x = U %}
-
{% [U/x]a = a %}
-
{% [U/x](XY) = ([U/x]X [U/x]Y) %}
Substitution effectively just replaces all occurences of a given term in the target.
Reduction
Reduction is the essence of computation. It takes a term and replaces it by some other term. The following are the three reduction rules of combinatory logic.
- {% IX \to X %}
- {% KXY \rightarrow X %}
- {% SXYZ \rightarrow XZ(YZ) %}