A Context Theory for Intensional Programming ? Kaiyu Wan, Vasu Alagar, and Joey Paquet Department of Computer Science and Software Engineering Concordia University Montreal, Quebec H3G 1M8, Canada {ky wan,alagar,paquet@cse.concordia.ca} Abstract. In this paper, we give an overview of our current work on introduc- ing context as first-class objects in Lucid. It allows us to write programs in Lucx (Lucid enriched with context) in a high level of abstraction which is closer to the problem domain. We include a discussion on context theory, representation of context aggregations, and the syntax and semantic rules of Lucx. The imple- mentation of Lucx in GIPSY, a platform under development for compiling Lucid family of languages, is also discussed. Keywords: Context, Context Theory, Intensional Programming 1 Introduction Context is a rich concept and is hard to define. The meaning of “context” is tacitly un- derstood and used by researchers in diverse disciplines. In modelling human-computer interaction [5], context includes the physical place of the user, the time constraints, and the system’s assumption about users interests. In Ubiquitous computing [3], context is understood as both situated and environmental. In natural language processing, con- texts arise as situations for interpreting natural language constructs. In imperative pro- gramming languages, context introduces index, constants, and pointers. In functional languages, static context introduces definitions and constraints, and dynamic context processes the executable information for evaluating expressions. In Artificial Intelli- gence(AI), the notion of context was introduced by McCarthy and later used by Guha [4] as a means of expressing assumptions made by natural language expressions. Hence, a formula, which is an expression combining a sentence in AI with contexts, can express the exact meaning of the natural language expression. Intensional logic [7] is a branch of mathematical logic which is used to describe precisely context-dependent entities. In Intensional Programming(IP) paradigm, which has its foundations in Intensional Logic, the real meaning of an expression, called intension, is a function from contexts to val- ues, and the value of the intension at any particular context, called the extension, is obtained by applying context operators to the intension. Although the notion of context was implicit in Lucid, an Intensional Programming Language, context cannot be explic- itly declared and manipulated in Lucid. By introducing context as a first class object in Lucid, we remove this limitation. The language, thus extended, is called Lucx(Lucid extended with contexts). ? This work is supported by grants from the Natural Sciences and Engineering Research Council of Canada. The goal of this paper is to illustrate how context is formally defined and introduced as first class objects in Lucx and as a result, how Lucx can be used for programming diverse application domains. The context theory that we are developing provides a se- mantic basis for context manipulation in Lucx. The paper is organized as follows: In Section 2 we review briefly contexts in Intensional Programming Paradigm. Section 3 discusses the context theory applied in Lucx. In Section 4 we discuss the syntax and semantics of Lucx. An example of Lucx programming and implementing Lucx are also illustrated. We conclude our work in Section 5. 2 Context in Intensional Programming Paradigm Intensional Logic, a family of mathematical formal systems that permits expressions whose value depends on hidden context, came into being from research in natural lan- guage understanding. Basically, intensional logics add dimensions to logical expres- sions, and non-intensional logics can be viewed as constant in all possible dimensions, i.e. their valuation does not vary according to their context of utterance. Intensional operators are defined to navigate in the context space. In order to navigate, some di- mension tags (or indexes) are required to provide place holders along dimensions. These dimension tags, along with the dimension names they belong to, are used to define the context for evaluating intensional expressions. For example, we can have an expression: E: the average temperature this month here is greater than 0◦ C. This expression is intensional because the truth value of this expression depends on the context in which it is evaluated. The two intensional natural language operators in this expression are this month and here, which refer respectively to the time and space dimension. If we evaluate the expression in different cities in Canada and in the months of a particular year, the extension of the expression varies. Hence, we have the following valuation for the expression: Ja Fe Mr Ap Ma Jn Jl Au Se Oc No De Montreal F F F F T T T T T F F F E0 = Ottawa F F F T T T T T T F F F Toronto F F T T T T T T T T F F Vancouver F T T T T T T T T T T T The intension of the expression is the above whole table; and the extension of the expression in the time point Ap and in the space point Ottowa is T. Intensional programming paradigm has its foundations on intensional logic. It re- tains two aspects from intensional logic: first, at the syntactic level, are context-switching operators, called intensional operators; second, at the semantic level, is the use of pos- sible worlds semantics [7]. Lucid was a data-flow language and evolved into a Multidimensional Intensional Programming Language [1]. In extending Lucid with contexts we preserve the inten- sionality in Lucx. Moreover, contexts exist independent of any objects in the system. That is, one context may be used to evaluate different expressions, at the same time expressions can also be evaluated at different contexts. This feature distinguishes the language Lucx from other imperative languages or functional languages, where index (for imperative languages) or evaluation environment(for functional language) are al- ways bound to statements or expressions. Because of the separation of the definition of expressions from contexts, Lucx has provided more power of representing problems in different application domains and given more flexibility of programming. 3 Context Theory in Lucx Context theory provides a semantic basis for Lucx programs. A context in the theory need not be finite. However, context in Lucx has a finite number of dimensions and along each dimension is associated a tag set, which is enumerable. This is in contrast to Guha’s notion, wherein contexts are infinite, rich, and generalized objects. We are motivated by Guha’s work. However not all contexts studied by Guha can be dealt within our language. On the other hand, every context that we can define in Lucx is indeed a context in Guha’s sense, but restricted to well-formed Lucx expressions. 3.1 Context Definition In Intensional Programming context is a reference to the representation of the “pos- sible worlds” relevant to the current discussion. The “possible world” is a multidi- mensional space enclosing all possible information pertaining to the discussion. Mo- tivated by this, we formalize contexts as a subset of a finite union of relations. The relations are defined over dimension and tag sets. Let DIM = {d1 , d2 , . . . , dn } denote a finite set of dimension names. We associate with each di ∈ DIM a unique enumerable tag set Xi . Let TAG = {X1 , . . . , Xr } denote the set of tag sets. There exists functions fdimtotag : DIM → TAG, such that the function fdimtotag associates with every di ∈ DIM exactly one tag Xj in TAG. Definition 1 Consider the relations Pi = {di } × fdimtotag (di ) 1≤i≤n Sn A context C, given (DIM, fdimtotag ), is a finite subset of i=1 Pi . The degree of the context C is | ∆ |, where ∆ ⊂ DIM includes the dimensions that appear in C. A context is written using enumeration syntax, as [d1 : x1 , . . . , dn : xn ], where d1 , . . . , dn are dimension names, and xi is the tag for dimension di . We say a context C is sim- ple (s context), if (di , xi ), (dj , xj ) ∈ C ⇒ di 6= dj . A simple context C of degree 1 is called a micro (m context) context. Example 1 As an example consider a system in which computations involve pressure, volume, and time, where pressure is observed by different sensors, volume is mea- sured by different devices, and the sampling frequencies are different. The three dis- tinguished dimensions are: (1).Sampling Time ST with index N; (2). Pressure P with index set {s1 , . . . , sk }, where s1 , . . . , sk are named sensory devices; and (3). Volume V with index set {m1 , . . . , mq }, where m1 , . . . , mq are named measuring devices. A con- text c = [ST : 1, P : s2 , V : m3 ] for one stream σ may be interpreted as a reference to the tuple ht1 , p2 , v3 i, where at the first sampling time t1 the value of volume mea- sured by m3 is v3 and the value of pressure observed by the sensor s2 is p2 . Supposing t1 , p2 , v3 ∈ R, the domain for the entities in the stream σ is R × R × R. The same context may also be used as a reference to another possible world containing the ex- p2 ?v3 pression σ 0 = p?vt . Such a reference will produce the result t1 , which is the result of 0 evaluating the expression σ with the substitution [t 7→ t1 ; p 7→ p2 ; v 7→ v3 ]. In this case, the domain for the entities in the stream σ 0 is R. Several functions on contexts are predefined in [2]. The basic functions dim and tag are to extract the set of dimensions and their associate tag values from a set of con- texts. Since we are still developing the Lucx language, the set of predefined functions is not exhaustive. Functions on contexts using functions already defined in Lucx can be introduced. 3.2 Context Operators In [9], we have formally defined the following context operators: the override ⊕ is sim- ilar to function override; difference , comparison =, conjunction u , and disjunction t are similar to set operators; projection ↓ and hiding ↑ are selection operators; con- structor [ : ] is used to construct an atomic context; substitution / is used to substitute values for selected tags in a context; choice | accepts a finite number of contexts and nondeterministically returns one of them; undirected range and directed range * produce a set of contexts. Example 2 illustrates an overall example for some of those operators. Example 2 : Let c1 = [X : 2, X : 3, Y : 4],c2 = [X : 2, Y : 4, Z : 5], c3 = [Y : 2], D = {Y, Z}, Then c1 ⊕ c2 = [X : 2, Y : 4, Z : 5], c1 c2 = [X : 3], c1 ↓ D = [Y : 4], c1 u c2 = [X : 2, Y : 4], c1 t c2 = [X : 2, X : 3, Y : 4, Z : 5], c2 ↑ D = [X : 2], c2 c3 = {[X : 2, Y : 2, Z : 5], [X : 2, Y : 3, Z : 5], [X : 2, Y : 4, Z : 5]}, c3 * c2 = {[X : 2, Y : 2, Z : 5], [X : 2, Y : 3, Z : 5], [X : 2, Y : 4, Z : 5]}, c2 /hY, 3i = [X : 2, Y : 3, Z : 5], c2 * c3 = ∅ In order to provide a precise meaning for a context expression, we have defined the precedence rules for all the operators in Figure 1[a] (right column) (from the highest precedence to the lowest) and described a set of evaluation rules for context expressions in [9]. Parentheses will be used to override this precedence when needed. Operators having the same precedence will be applied from left to right. The formal syntax of context expressions is shown in Figure 1[a](left column). 3.3 Box and Box Operators A context which is not a micro context or a simple context is called a non-simple con- text. For example, context c4 = [X : 3, X : 4, Y : 3, Y : 2, U : blue] is a non-simple context. In general, a non-simple context is equivalent to a set of simple contexts [2]. In several applications we deal with contexts that have the same dimension set ∆ ⊆ DIM and the tags satisfy a predicate formula p. The short hand notation for such a set is Box[∆ | p]. syntax precedence C ::= c |C=C syntax precedence 1. ↓, ↑, / | C⊇C |C⊆C 2. | B ::= b |B|B | C | C | C/C 1. ↓, ↑, / 3. u, t | B B | BB | C⊕C | C C 2. | 4. ⊕, | BB | B↓D | CuC | CtC 3. , ,  5. , * | B ↑ D | B/hd, ti | C C|C*C 6. =, ⊆, ⊇ | C↓D |C↑D (b) Rules for Box Expression (a) Rules for Context Expression Fig. 1. Rules for Contex and Box Expressions Definition 2 Let ∆ = {d1 , . . . , dk }, where di ∈ DIM i = 1, . . . , k, and p is a predicate formula defined on the tuples of the relation Πd ∈∆ fdimtotag (d). The syntax Box[∆ | p] = {s | s = [di1 : xi1 , . . . , dik : xik ]}, where the tuple (x1 , . . . , xk ), xi ∈ fdimtotag (di ), i = 1, . . . k satisfy the predicate formula p, introduces a set S of contexts of degree k. For each context s ∈ S the values in tag(s) satisfy the predicate formula p. The context operators projection (↓), hiding (↑), choice (|), and substitution (/) intro- duced in Section 3.2 can be naturally lifted to sets of contexts, in particular for Boxes. As an example : ↑ and ↓ can be lifted for Box B: B ↑ D = {c ↑ D | c ∈ B}, B ↓ D = {c ↓ D | c ∈ B}. However not all context operators have natural exten- sions. Instead, the following three operations  (join), (intersection), and  (union) are defined [2] for sets of contexts introduced by Box. Example 3 : Let DIM = {X, Y, Z}, fdimtotag (X) = fdimtotag (Y) = fdimtotag (Z) = N, B1 = Box[X, Y | x, y ∈ N ∧ x + y = 5], B2 = Box[Y, Z | y, z ∈ N ∧ y = z2 ∧ z ≤ 3]. Then B1 = {[X : 1, Y : 4], [X : 2, Y : 3], [X : 3, Y : 2], [X : 4, Y : 1]} B2 = {[Y : 1, Z : 1], [Y : 4, Z : 2], [Y : 9, Z : 3]}. Hence B1  B2 = Box[X, Y, Z | x + y = 5 ∧ (y = z2 ∧ z ≤ 3)] = {[X : 1, Y : 4, Z : 2], [X : 4, Y : 1, Z : 1]} B1 B2 = Box[Y | x + y = 5 ∧ (y = z2 ∧ z ≤ 3)] = {[Y : 1], [Y : 4]} B1  B2 = Box[X, Y, Z | x + y = 5 ∨ (y = z2 ∧ z ≤ 3)] = {[X : 1, Y : 4, Z : 1..3], [X : 2, Y : 3, Z : 1..3], [X : 3, Y : 2, Z : 1..3], [X : 4, Y : 1, Z : 1..3], [X : 1..3, Y : 1, Z : 1], [X : 2..4, Y : 4, Z : 2], [X : 1..4, Y : 9, Z : 3]} We define these three operators (, , and ) have equal precedence and have seman- tics analogous to relational algebra operators. Let B be a box expression and D be a dimension set. A formal syntax for box expression B is defined in Figure 1[b] (left column) and the precedence rules for box operators are defined in Figure 1[b] right column. 3.4 Context Category Context Regions A context region is a finite subset of a multidimensional space gen- erated by a set of dimensions. Boxes can be used to represent different context regions. For example, Figure 2[a] shows two different context regions, which can be repre- sented as follows: B1 = Box[X, Y, Z | x2 + z2 ≤ 16 ∧ x = 12 z ∧ z ≥ 0], B2 = Box[X, Y, Z | x2 + y2 + z2 ≤ 9 ∧ z ≥ 0]. Box B1 defines a cone, and Box B2 defines the upper half of hemisphere with the radius 3. If we restrict to integer in- dices, then the set of contexts defined by Box B1 consists of all the points with integer coordinates within the cone, and the set of contexts defined by Box B2 consists of all the points with integer coordinates within the hemisphere. v(c2)(y) α49 α50 α51 α52 α53 6 . . . . . . . α47 α54 5 . . . . . . . . α55 4 . . . . B1 . . . . α56 B2 3 . . . . . . . α57 α17 2 α10 . . α16 . . α58 α9 α15 1 α2 α4 α6 α8 α59 (a) Differ- α1 1 α3 2 α5 3 α7 4 v(c1)(x) ent Context Regions (b) Clock Regions Fig. 2. Context Category In timed systems having continuous time model, clock regions which are equiva- lence classes of clock valuations arise when several clocks are used. These clock re- gions are treated as context regions, and can be represented as boxes [8]. As an ex- ample, consider clocks c1 and c2 when the maximum duration that can elapse in the clocks are m1 = 4, and m2 = 6. This gives rise to 59 clock regions, as shown in Fig- ure 2[b]. The clock regions corresponding to a set of clocks is represented as a set of Boxes. Each Box is defined by the dimension set ∆ = {c1 , . . . , ck }, and a con- straint on the clock valuations. For example, Box[∆ | p1 ], where ∆ = {c1 , c2 } and p1 = (0 < v(c1 )(x) < 1) ∧ (0 < v(c2 )(y) < v(c1 )(x)) refers to the region α1 . The tag sets for clocks are reals. For discrete time modelled by multiple clocks the tag sets are integers, and regions become lattice points, vertices of convex regions. Nested Contexts Nested contexts define the meta relation between different contexts. This is similar to Guha’s definition of nested context [4]. In his definitions, nested con- text enables to nest ist(f , c) formulas, which define that formula f is true in context c, and ist(ci ist(cj , α)), ist(ck ist(cl . . . ist(cj α) . . .)) are all valid. In the former example ist(ci ist(cj , α)), context ci is outer or meta to context cj . Guha also provides entering and exiting actions to migrate the interpretation of formulas from contexts. Similarly, we provide @∗ operator to navigate the evaluation of expressions between nested con- texts. Definition 3 Let p(x, y) and q(x, y, z) be two predicate formulas. If ∀ a, b for which p(a, b) is true, and if ∃ c such that q(a, b, c) is true, then we call p(x, y) as a projection of the predicate formula q(x, y, z) and write p(x, y) =↓z q(x, y, z). Conversely, we say z q(x, y, z) is a simple extension of p(x, y) and write p(x, y) → q(x, y, z). In general, a predicate formula extended with s > 1 arguments can be inductively defined as follows: xr+1 1. p(x1 , . . . , xr ) → q(x1 , . . . , xr , xr+1 ) xr+1 ,...,xr+s 2. p(x1 , . . . , xr ) −→ q(x1 , . . . , xr , . . . , xr+s ) ∆ xr+1 xr+2 = p0 (x1 , . . . , xr ) → p1 (x1 , . . . , xr , xr+1 ) → p2 (x1 , . . . , xr+2 ) . . . xr+s → ps (x1 , . . . , xr+s ), where p0 ≡ p, ps ≡ q. Definition 4 We define a relation @ on a set of boxes B as follows: for b1 , b2 ∈ B, b1 = Box[∆1 | p1 ], b2 = Box[∆2 | p2 ], b1 @ b2 iff ∆1 ⊂ ∆2 and p2 is an extension of the logic expression p1 . It is easy to see that @ is an irreflexive partial order on B. We define a partially order chain b1 @ b2 . . . @ bk to be nested, and refer to the boxes in the chain as nested contexts. We want to study the relationship between nested contexts and sets of expressions obtained by evaluating a given expression E at the boxes in the nested chain. Definition 5 Let B = {b1 , b2 , . . .} be a finite set of boxes, bi = Box[∆i | pi ], and E be an expression. Define the relation  on the set {E@∗ b1 , E@∗ b2 , . . .} as follows: E@∗ bi  E@∗ bk iff for Eij0 = E@cij0 , cij0 ∈ bi , there exists Ekj = E@ckj , ckj ∈ bk , such that ckj ↑ {∆k − ∆i } = cij0 , and Ekj = Eij0 @(ckj cij0 ). Theorem If b1 @ b2 then E@∗ b1  E@∗ b2 . Proof Let b1 = Box[∆1 | p1 ], b2 = Box[∆2 | p2 ], ∆1 = {X1 , X2 , . . . , Xk }, and ∆2 = {X1 , X2 , . . . , Xk , Xk+1 , . . . , Xm }, ∃(a1 , . . . , ak ), p1 (a1 , . . . , ak ) is true, then c1j0 = [X1 : a1 , . . . , Xk : ak ] ∈ b1 . By property b1 @ b2 , ∃ ak+1 , . . . , am such that p2 (a1 , . . . , ak , ak+1 , . . . , am ) is true. Hence c2j = [X1 : a1 , . . . , Xk : ak , Xk+1 : ak+1 , . . . , Xm : am ] ∈ b2 . It is easy to verify that c1j0 and c2j satisfy c2j ↑ {∆2 − ∆1 } = c1j0 and E1j0 = E@c1j0 , E2j = E@c2j satisfy E2j = E1j0 @(c2j c1j0 ). Hence it follows that E@∗ b1  E@∗ b2 . In general if b1 @ b2 . . . @ bk is a chain of nested contexts, we get a corresponding chain of cascading expressions: E@∗ b1  E@∗ b2 . . .  E@∗ bk . This rule gives the base for the reasoning and reducing rules for constraint programming solver mentioned in [9]. Context Dependent Expressions Contexts can be passed as parameters to functions. Definition 6 Let B1 = Box[∆1 | p1 ], and B2 = Box[∆2 | p2 ] define the context regions in the space generated by the dimensions ∆1 ∪ ∆2 . The context-dependent expression E is defined differently in different regions:   E1 in B1 B2 λ ·E = E2 in B2 B1 E3 in B1 u B2  µ ·E is defined to indicate corresponding context regions, namely, µ ·E = {B1 B2 , B2 B1 , B1 u B2 } An application of Definition 6 is to use contexts as parameters in a function defini- tion. Let f : X × Y × Z × C → W, where C is a set of contexts; and f (x, y, z, c), x ∈ X, y ∈ Y, z ∈ Z, c ∈ C, be defined such that for different context values, the function’s definitions are different. For example, function f (x, y, z, c) is defined according to dif- ferent context regions shown in Figure 2[a]. Hence µ ·f = {B1 B2 , B2 B1 , B1 u B2 }, and λ ·f = {2x3 + y − 6, x + y2 , z3 + y}. The evaluation of functions f varies depending on the actual context value given as input when f is called. Given contexts as input, context-dependent functions can be used to produce a new context as a result to achieve adaptation in context-aware system [9]. Dependent Context We define context dependency analogous to the functional depen- dency in relational data models. Definition 7 Let ∆ = {X1 , . . . , Xk } be a dimension set. If there exists a function φij : fdimtotag (Xi ) → fdimtotag (Xj ), we say φij is a functional dependency in the set ∆. In general, a functional dependency exists in ∆, if A ⊂ ∆, B ⊂ ∆, A ∩ B = ∅, and there exists a function : φAB : ΠXi ∈A fdimtotag (Xi ) → ΠXj ∈B fdimtotag (Xj ). For a given functional dependency φij in ∆, we define dependent contexts as the set of contexts: S∆ = {c | dim(c) = ∆0 ∧ ({Xi , Xj } ⊆ ∆0 ⊆ ∆)} As an example, c = [Xi : a, Xj : φij (a)] ∈ S∆ , a ∈ fdimtotag (Xi ). This definition is easy to generalize for the general functional dependency φAB . Dependent context effectively reduces the possible worlds that are relevant to eval- uate expressions. As an example, let a function φ: V → ST be defined as follows: φ(m1 ) = φ(m2 ) = 1; φ(m3 ) = φ(m4 ) = 2. Hence context of this form [P : s1 , V : m3 , ST : 1] need not be considered for evaluating expressions in the example. Moreover, dependent contexts also help to represent context sets compactly. In [9], we proved the following: starting with a set S∆ of contexts, whose dimensions are subsets of ∆ and a finite set of functional dependencies on ∆, we can represent S∆ 0 0 as an expression S∆ = S∆k  S∆ k , where there is no dependency in S∆k and S∆ k = b1  b2 . . .  bk , each bi is a Box representing one dependency. Since a box has a compact representation, the representation for S∆ given above is a compact way to manage the contexts in this S∆ . The substitutions for tags in b1 , . . . , bk are subject to dependencies. However, those tags corresponding to dimension in S∆k can be done freely. This is analogous to substitution principle in functional languages. 4 Intensional Language Lucx Lucx is a conservative extension of Lucid, with context becoming a first-class object in the language. This way, contexts can be manipulated, assigned values and passed as parameters dynamically. Syntax and Semantics of Lucx The syntax of Lucx is shown below. E ::= id S ::= {E1 , . . . , Em } | E(E1 , . . . , En ) | Box[E | E0 ] | if E then E0 else E00 Q ::= dimension id |# | id = E | E @ E0 | id(id1 , . . . , idn ) = E | [E1 : E01 , . . . , En : E0n ] |QQ | hE1 , . . . , En iE | select(E, E0 ) | E @∗ S | E where Q The difference between Lucx and original Lucid is highlighted in bold in the above syntax rules. The symbols @ and # are context navigation and query operators. The non-terminals E and Q respectively refer to expressions and definitions. The abstract semantics of evaluation in Lucx is D, P 0 ` E : v, which means that in the definition environment D, and in the evaluation context P 0 , expression E evaluates to v. The definition environment D retains the definitions of all of the identifiers that appear in a Lucid program. Formally, D is a partial function D : Id → IdEntry, where Id is the set of all possible identifiers and IdEntry has five possible kinds of value such as: Dimensions, Constants, Data Operators, Variables, and Functions[7]. The evaluation context P 0 , is the result of P †c, where P is the initial evaluating context, c is the defined context expression, and the symbol†denotes the overriding function. A complete operational semantics for Lucid is defined in [7]. The new semantic rules for Lucx are given below. D, P ` E0 : P 0 D, P 0 ` E : v Eat(c) : D, P ` E @E0 : v E# : D, P ` # : P D, P ` E2 : id2 D(id2 ) = (dim) E. : D, P ` E1 .E2 : tag(E1 ↓ {id2 }) D, P ` E : id D†[id 7→ (dim)] P †[id 7→ 0] D, P ` Ei : vi Etuple : D, P ` hE1 , E2 , . . . , En iE : v1 fby.id v2 fby.id . . . vn fby.id eod E = [d : v0 ] E0 = hE1 , . . . , En id P 0 = P † [d 7→ v0 ] D, P 0 ` E0 :v Eselect : D, P ` select(E, E0 ) : v D, P ` S : {P1 , . . . , Pm } D, Pi:1..m ` E : vi Eat(s) : D, P ` E @∗ S : {v1 , . . . , vm } D, P ` Ew:1..m : Pm Eset : D, P ` {E1 , . . . , Em } : {P1 , . . . , Pw } D, P ` E : ∆ ∆ = {v01 , . . . , v0n } = dim(P1 ) = . . . = dim(Pm ) Ebox : D(v0k:1..n ) = (dim) D, P ` E0 : fp (tag(Pi:1..m )) = true D, P ` Box[E | E0 ] : {P1 , . . . , Pm } D, P ` Edj : idj D(idj ) = (dim) Econtext : D, P ` Eij : vj P 0 = P0 † [id1 7→ v1 ] † . . . † [idn 7→ vn ] D, P ` [Ed1 : Ei1 , Ed2 : Ei2 , . . . , Edn : Ein ] : P 0 The evaluation rule for the navigation operator, Eatc , which corresponds to the syn- tactic expression E @ E0 , evaluates E in context E0 , where E0 is a context defined in Section 3.1. The evaluation rule for the set navigation operator Eats , which corresponds to the syntactic expression E @∗ S, evaluates E in a set of contexts S. Hence, the eval- uation result should be a collection of results of evaluating E at each element of S. Semantically speaking, the symbol # is a nullary operator, which evaluates to the cur- rent evaluation context P. And the symbol . is a binary operator, whose left operand is an expression and the right operand is a single dimension. The semantic rule Etupid evaluates a tuple as a finite stream whose dimension is explicitly indicated as E in the corresponding syntax rule hE1 , . . . , En iE. Accordingly, the semantic rule Eselect picks up one element indexed by E from the tuple E0 . The semantic rule Ebox evaluates a Box to a set of contexts according to the definition in Section 3.3. fp (tag(Pi )i=1..m ) is a boolean function. The rule Eset evaluates {E1 , . . . , Em } to a set of contexts. Examples of Lucx Programs We give two examples. 1. The example models the problem of heat transfer in a solid. There is a metal rod which initially has temperature 0 and whose left-hand end touches a heat source with temperature 100. As the heat is transfered, the temperature at the various points of the rod changes. That is, the temperature depends on the time point and the spatial position on the rod. The following equations illustrate the temperature of the rod as a function of time and space (where k is a small constant related to the physical properties of the rod): Tempt+1,s+1 = k × Tempt,s − (1 − 2 × k) × Tempt,s+1 + k × Tempt,s+2 Tempt,0 = 100 Temp0,s+1 = 0 The Lucx program that models the above equations and queries the temperature at the space 10 at time 10 is the following: Temp @ [Time : 10, Space : 10] where Temp @ [Time : t + 1, Space : s + 1] = k × Temp @ [Time : t, Space : s] −(1 − 2 × k) × Temp @ [Time : t, Space : s + 1] +k × Temp @ [Time : t, Space : s + 2] Temp@[Time : t, Space : 0] = 100 Temp@[Time : 0, Space : s + 1] = 0 end 2. Consider the problem of finding the solution in positive integers that satisfy the following constraints: x3 + y3 + z3 + u3 = 100 x