Formal Definition
We can augment the definition of a lambda expression to gain one in the context of lambda-mu calculus. The three main expressions found in lambda calculus are as follows:
- V, a variable, where V is any identifier.
- λV.E, an abstraction, where V is any identifier and E is any lambda expression.
- (E E′), an application, where E and E′ are any lambda expressions.
For details, see the corresponding article.
In addition to the traditional λ-variables, the lambda-mu calculus includes a distinct set of μ-variables. These μ-variables can be used to name or freeze arbitrary subterms, allowing us to later abstract on those names. The set of terms contains unnamed (all traditional lambda expressions are of this kind) and named terms. The terms that are added by the lambda-mu calculus are of the form:
- t is a named term, where α is a μ-variable and t is an unnamed term.
- (μ α. E) is an unnamed term, where α is a μ-variable and E is a named term.
Read more about this topic: Lambda-mu Calculus
Famous quotes containing the words formal and/or definition:
“There must be a profound recognition that parents are the first teachers and that education begins before formal schooling and is deeply rooted in the values, traditions, and norms of family and culture.”
—Sara Lawrence Lightfoot (20th century)
“The physicians say, they are not materialists; but they are:MSpirit is matter reduced to an extreme thinness: O so thin!—But the definition of spiritual should be, that which is its own evidence. What notions do they attach to love! what to religion! One would not willingly pronounce these words in their hearing, and give them the occasion to profane them.”
—Ralph Waldo Emerson (1803–1882)