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:
“That anger can be expressed through words and non-destructive activities; that promises are intended to be kept; that cleanliness and good eating habits are aspects of self-esteem; that compassion is an attribute to be prized—all these lessons are ones children can learn far more readily through the living example of their parents than they ever can through formal instruction.”
—Fred Rogers (20th century)
“Perhaps the best definition of progress would be the continuing efforts of men and women to narrow the gap between the convenience of the powers that be and the unwritten charter.”
—Nadine Gordimer (b. 1923)