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:
“It is in the nature of allegory, as opposed to symbolism, to beg the question of absolute reality. The allegorist avails himself of a formal correspondence between ideas and things, both of which he assumes as given; he need not inquire whether either sphere is real or whether, in the final analysis, reality consists in their interaction.”
—Charles, Jr. Feidelson, U.S. educator, critic. Symbolism and American Literature, ch. 1, University of Chicago Press (1953)
“Im beginning to think that the proper definition of Man is an animal that writes letters.”
—Lewis Carroll [Charles Lutwidge Dodgson] (18321898)