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:

    “On every formal visit a child ought to be of the party, by way of provision for discourse.”
    —Jane Austen (1775–1817)

    “Beauty, like all other qualities presented to human experience, is relative; and the definition of it becomes unmeaning and useless in proportion to its abstractness. To define beauty not in the most abstract, but in the most concrete terms possible, not to find a universal formula for it, but the formula which expresses most adequately this or that special manifestation of it, is the aim of the true student of aesthetics.”
    —Walter Pater (1839–1894)