Editing SKI combinator calculus (section)

==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 τ<sub>1</sub> and τ<sub>2</sub> are terms, then (τ<sub>1</sub>τ<sub>2</sub>) 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 α and ι are words over the alphabet {'''S''', '''K''', '''I''', (, )} while β, γ and δ are terms):
# 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. All derivations of length 1 are valid derivations.