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:
“The conviction that the best way to prepare children for a harsh, rapidly changing world is to introduce formal instruction at an early age is wrong. There is simply no evidence to support it, and considerable evidence against it. Starting children early academically has not worked in the past and is not working now.”
—David Elkind (20th century)
“Scientific method is the way to truth, but it affords, even in
principle, no unique definition of truth. Any so-called pragmatic
definition of truth is doomed to failure equally.”
—Willard Van Orman Quine (b. 1908)