Context

There are many different aspects to context, but there is a single notion that encompasses the whole which can be defined. We say that an object described in a language within a particular scope has a context, which is defined by the total state of the evaluator when defined.

This definition is a bit naive, especially when considered that the Tunes HLL architecture defines several types of re-usable components which interact in various ways to produce what we would call a "language".

• Context Research Home Page
• Modeling and using context: Past, present and future
• Sasa Buvac: FORMALIZING CONTEXT

In a term algebra, a context C for a term t is a term t1 having t as a subterm, where (one of) the occurrence(s) of t has been replaced by a "hole". The hole is a special-purpose term whose role is just marking an empty slot in a term, and is usually indicated as []. Congruences in algebras are defined as equivalences which are preserved by any context. As an example, in the lambda calculus λx.[] is a context for the terms x and ((λy.x) a) (indeed, for any term). The substitution of the hole with these terms yields the terms λx.x and λx.((λy.x) a) respectively.

Rewrite rules are usually defined for a class of elementary terms and recursively extended to all the term by means of a class of context named the evaluation, or applicative, contexts. As an example, if λx.[] is an evaluation context, given the reduction (λy.x) a → x, we can infer from it the reduction λx.((λy.x) a) → λx.x. If, on the other hand, we restrain evaluation context by excluding all the λx.[] contexts, like in Mendhekar and Friedman's reflective lambda calculus, the latter reduction cannot be performed. Restraining evaluation contexts is equivalent to establishing an evaluation order. On the other hand, in calculi for concurrent distributed processes, like the pi calculus, evaluation contexts are usually named reactive contexts, and express the computational loci where distributed computing entities may interact. In this case, restraining evaluation contexts is necessary to express the fact that not every hole where a term modelling a process may appear is meant as a place where the process can compute. As an example, all the a.[] contexts are not reactive: By the very definition of the dot (.) continuation operator, the term in the slot will be able to perform its computations only after the a valence has been consumed.

To edit this page see HTML special characters and symbols.

Nota bene: if you have a UNICODE-aware text editor than ignore the SGML entities bug; you can edit, copy&paste from such an editor without problems.

This page is linked from: Abstraction   Congruence   Continuation   Escape   Functional   Meta-Space   process migration   Referential Transparency and State   Reification   Resilient   Scope   Semantics   Side Effect   Virtual Machine