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:

    “Good gentlemen, look fresh and merrily.
    Let not our looks put on our purposes,
    But bear it as our Roman actors do,
    With untired spirits and formal constancy.”
    —William Shakespeare (1564–1616)

    “Although there is no universal agreement as to a definition of life, its biological manifestations are generally considered to be organization, metabolism, growth, irritability, adaptation, and reproduction.”
    —The Columbia Encyclopedia, Fifth Edition, the first sentence of the article on “life” (based on wording in the First Edition, 1935)