Formal Definition
The terms and derivations in this system can also be more formally defined:
Terms: The set T of terms is defined recursively by the following rules.
- S, K, and I are terms.
- If τ1 and τ2 are terms, then (τ1τ2) is a term.
- Nothing is a term if not required to be so by the first two rules.
Derivations: A derivation is a finite sequence of terms defined recursively by the following rules (where all Greek letters represent valid terms or expressions with fully balanced parentheses):
- If Δ is a derivation ending in an expression of the form α(Iβ)ι, then Δ followed by the term αβι is a derivation.
- If Δ is a derivation ending in an expression of the form α((Kβ)γ)ι, then Δ followed by the term αβι is a derivation.
- If Δ is a derivation ending in an expression of the form α(((Sβ)γ)δ)ι, then Δ followed by the term α((βδ)(γδ))ι is a derivation.
Assuming a sequence is a valid derivation to begin with, it can be extended using these rules.
Read more about this topic: SKI Combinator Calculus
Famous quotes containing the words formal and/or definition:
“True variety is in that plenitude of real and unexpected elements, in the branch charged with blue flowers thrusting itself, against all expectations, from the springtime hedge which seems already too full, while the purely formal imitation of variety ... is but void and uniformity, that is, that which is most opposed to variety....”
—Marcel Proust (1871–1922)
“The very definition of the real becomes: that of which it is possible to give an equivalent reproduction.... The real is not only what can be reproduced, but that which is always already reproduced. The hyperreal.”
—Jean Baudrillard (b. 1929)