SKI Combinator Calculus - Formal Definition

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.

  1. S, K, and I are terms.
  2. If τ1 and τ2 are terms, then (τ1τ2) is a term.
  3. 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):

  1. If Δ is a derivation ending in an expression of the form α(Iβ)ι, then Δ followed by the term αβι is a derivation.
  2. If Δ is a derivation ending in an expression of the form α((Kβ)γ)ι, then Δ followed by the term αβι is a derivation.
  3. 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 spiritual kinship between Lincoln and Whitman was founded upon their Americanism, their essential Westernism. Whitman had grown up without much formal education; Lincoln had scarcely any education. One had become the notable poet of the day; one the orator of the Gettsyburg Address. It was inevitable that Whitman as a poet should turn with a feeling of kinship to Lincoln, and even without any association or contact feel that Lincoln was his.”
    —Edgar Lee Masters (1869–1950)

    “The man who knows governments most completely is he who troubles himself least about a definition which shall give their essence. Enjoying an intimate acquaintance with all their particularities in turn, he would naturally regard an abstract conception in which these were unified as a thing more misleading than enlightening.”
    —William James (1842–1910)