<style type="text/css">CODE { font-family: sans-serif; font-weight: bold; }</style>
The *(term) for that which gives, or completes, the meaning of an _(object).

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 <em>object</em> described in a <em>_(language)</em> within a particular <em>_(scope)</em> has a context, which is defined by the total state of the evaluator when defined.

<p class="comment">This definition is a bit naive, especially when considered that the _(Tunes HLL) _(architecture| http://tunes.org/HLL/architecture.html) defines several types of re-usable components which interact in various ways to produce what we would call a "language".</p>

<ul class="links">
<li>_("Context Research Home Page"|http://context.umcs.maine.edu/)
<li>_("Modeling and using context: Past, present and future"|http://www.lip6.fr/reports/lip6.2002.010.html)
<li>_("Sasa Buvac: FORMALIZING CONTEXT"|http://www-formal.stanford.edu/buvac/)
</ul>

In a term algebra, a context <code>C</code> for a term <code>t</code> is a term <code>t<sup>1</sup></code> having <code>t</code> as a subterm, where (one of) the occurrence(s) of <code>t</code> 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 <code>[]</code>. Congruences in algebras are defined as equivalences which are preserved by any context. As an example, in the _(lambda calculus) <code>&#955;x.[]</code> is a context for the terms <code>x</code> and <code>((&#955;y.x) a)</code> (indeed, for any term). The substitution of the hole with these terms yields the terms <code>&#955;x.x</code> and <code>&#955;x.((&#955;y.x) a)</code> 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 <code>&#955;x.[]</code> is an evaluation context, given the reduction <code>(&#955;y.x) a &#8594; x</code>, we can infer from it the reduction <code>&#955;x.((&#955;y.x) a) &#8594; &#955;x.x</code>. If, on the other hand, we restrain evaluation context by excluding all the <code>&#955;x.[]</code> 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 <code>a.[]</code> contexts are not reactive: By the very definition of the dot (<code>.</code>) continuation operator, the term in the slot will be able to perform its computations only after the <code>a</code> valence has been consumed.
 
<hr>

To edit this page see _(HTML special characters and symbols).

<strong>Nota bene:</strong> if you have a UNICODE-aware text editor than ignore the _("SGML entities bug"|http://cliki.tunes.org/Text%20Formatting#SGML bug); you can edit, copy&paste from such an editor without problems.
