The article deals with the denotational seman- tegral part of the work, we have designed and develtics of a special query language called XML-Lambda oped a prototype of an XML- query processor for (abbreviated as XML- ), which is based on the simply typed validating the functional approach and experimenting lambda calculus. The exact semantics allows experimenta- with it. The main advantage of this concept is the tion with a language definition, prototyping of programs, possibility of a query optimizations in the XML- inand similar experiments. One of such experiment is the termediate form. It is much more easier than optimizaivmirpolnemmeenntt.aTtiohne mofatihneaXdvQaunetraygelaonfgouuargeapipnrothaechXiMstLh-e peons-- tions when we use the official W3C semantics ([3]). sibility of a query optimizations in the XML- intermedi- Since it is not possible to express the semantics of ate form. It is much more easier than optimizations based the whole XML- language in this contribution, the on the official W3C semantics. XML- is a part of more paper focuses chiefly on its main idea and concepts. complex XML- Framework which serves for experimenting with the tools for XML processing.
In this paper, we define formally the semantics of XML-Lambda Query Language. From now on we will use abbreviation XML- . XML- employs the func- 2.1 tional data model for XML data elaboration. The first idea for such an attitude was published in [5, 6]. This research brought in the key idea of a functional query processing with a wide potential that was later proven by a simple prototype implementation [7].
We can imagine two scenarios for this language; firstly, the language plays a role of a full-featured query language for XML (it has both formal syntax and semantics and there is also an existing prototype that acts as a proof-of-the-concept application). But there already exist standard approaches for XML querying – especially XQuery, with probably more appropriate syntax for users. So, there is no need to define any new query language.
In the second scenario, the XML- Query Language is utilized as an intermediate language for the description of XQuery semantics. In [4] we propose a novel method for XQuery evaluation based on the transformation of XQuery queries into their XMLequivalents and their subsequent evaluation. As an inIn this section, we briefly describe the XML- Query Language, a query language for XML based on the simply typed lambda calculus.
Typical query expression has a query part — an expression to be evaluated over data — and a constructor part that wraps a query result and forms the output.
The XML- Query Language is based on -terms defined over the type system TE as will be shown later.
-calculus is a formal mathematical system for investigation of function definition and application. It was introduced by Alonzo Church and has been utilized in many ways. In this work, we use a variant of this formalism, the simply-typed -calculus, as a core for the XML- Query Language. We have gathered the knowledge from [8] and [1]. Our realization is enriched by usage of tuples.
The main constructs of the language are variables, constants, tuples, projections, and -calculus operations — applications and abstractions. The syntax is similar to -calculus expressions, thus the queries are structured as nested -expressions, i.e.:
Language of terms is defined inductively as the least set containing all terms created by the application of the following rules. Let T; T1; : : : ; Tn, n 1 be members of TE . Let F be a set of typed constants, and V an at most countable set of typed variables. Then: 1. variable: each variable (member of V) of type T is
a term of type T 2. constant: each constant (member of F ) of type T
is a term of type T 3. application: if M is a term of type ((T1;: : :; Tn) ! T ) and N1; : : : ; Nn are terms of the types T1; : : : ; Tn, then M (N1; : : : ; Nn) is a term of the type T 4. -abstraction: if x1; : : : ; xn are distinct variables of types T1; : : : ; Tn and M is a term of type T , then x1 : T1; : : : ; xn : T1:(M ) is a term of type ((T1; : : : ; Tn) ! T ) 5. n-tuple: if N1;: : :; Nn are terms of types T1;: : :; Tn,
then (N1; : : : ; Nn) is a term of type (T1; : : : ; Tn) 6. projection: if (N1; : : : ; Nn) is a term of type (T1; : : : ; Tn), then N1; : : : ; Nn are terms of types
T1; : : : ; Tn 7. tagged term: if N is a term of type N AM E and
M is a term of type T then N : M is a term of type (E ! T ).
The set of abstract elements E serves as a notation for abstract positions in XML trees. Terms can be interpreted in a standard way by means of an interpretation assigning to each constant from F an object of the same type, and by a semantic mapping from the language of terms to all functions and Cartesian products given by the type system TE . Speaking briefly, an application is evaluated as an application of the associated function to given arguments, an abstraction ’constructs’ a new function of the respective type. The tuple is a member of Cartesian product of sets of typed objects. A tagged term is interpreted as a function defined only for one e 2 E. It returns again a function. 3 As for evaluation of a query, we do not need its complete derivation tree; such information is too complex and superfluous. Therefore, in order to diminish the domain that needs to be described without any loss of 4 Denotational semantics precision, we employ the abstract syntax. With the abstract syntax, we break up the query into logical pieces We use denotational semantics for the description of that forming an abstract syntax tree carrying all orig- the meaning of each XML- query. The approach is inal information constitute an internal representation based on the idea that for each correct syntactic consuitable for query evaluation. We introduce syntactic struct of the language we can define a respective meandomains for the language, i.e., logical blocks a query ing of it as a formal expression in another, well-known, may consist of. Subsequently, we list all production notation. We can say that the program is the denotarules. These definitions are later utilized in Section 4 tion of its meaning. The validity of the whole approach within the denotational semantics. is based on structural induction; i.e, that the meaning of more complex expressions is defined on the basis 3.1
By the term syntactic domain, we understand a logical part of a language. In Table 1, we list all syntactic domains of the XML- Query Language with their informal meaning. Notation Q : Query stands for the symbol Q representing a member of the Query domain.
Q : Query XML- queries, O : Options XML input attachements, C : Constructor constructors of output results, E : Expression general expressions, SQ : SubQuery (nested) subqueries, T : T erm sort of expression, F : F ragment sub-parts of a T erm, As : Assignment variable assignments, F lt : F ilter set pruning conditions, F C : F unctionCall either built-in or user-de ned functions, BinOp : BinOperator binary logical operators, RelOp : RelOperator binary relational operators, N F : N ullary identi ers of nullary functions (subset of Identif ier), P roj : P rojection identi ers for projections (subset of Identif ier), B : Boolean logical values, N : N umeral numbers, D : Digits digits, S : String character strings, Id : Identif ier strings conforming to the
N ame syntactic rule in [2]. The abstract production rules listed in Table 2 (written using EBNF) connect the terms of syntactic domains from the previous section into logical parts with suitable level of details for further processing. On the basis of these rules, we will construct the denotational semantics of the language. of their simpler parts. As the notation we employ the simply typed lambda calculus. It is a well-known and formally verified tool for such a purpose. 4.1
The denotational semantics utilizes a set of functions for the definition of the language meaning. For this purpose, we formulate all necessary mathematical definitions. We start with the data types and specification of the evaluation context followed by the outline of bindings to the TE type system. Then, all auxiliary and denotation functions are introduced.
Data Types. Each value computed during the process of the query evaluation is of a type from T ype. Let E be a type from the type system TE , we define T ype as: T ype ::= BaseT ype j Seq(T ype) Seq(T ype) ::= ? j BaseT ype Seq(T ype) BaseT ype ::= E j P rimitiveT ype
P rimitiveT ype ::= Boolean j String j N umber Primitive types, Boolean, String, and N umber, are defined with their set of allowed values as usual. The type constructor Seq stands for the the type of ordered sequences of elements of values of the type T ype3. We use it only for base types, so Seq(T ype) is the type of all ordered sequences of elements of base types. We do not permit sequences of sequences. The symbol ? stands for the empty sequence of types – represents an unknown type. More precisely, we interpret types as algebraic structures, where for each type 2 T ype there is exactly one carrier V , whose elements are the values of the respective type .
Variables. An XML- query can use an arbitrary (countable) number of variables. We model variables as pairs name : , where name refers to a variable name and is the data type of the variable – any member of T ype. Syntactically, variable name is always prepended by the dollar sign. Each expression in XML- has a recognizable type, otherwise both the type and the value are undefined.
Query Evaluation Context. During the process of query evaluation we need to store variables inside a working space known as a context. Formally, we denote this context as the State. We usually understand a state as the set of all active objects and their values at a given instance. We denote the semantic domain State of all states as a set of all functions from the set of identifiers Identif ier into their values of the type 2 T ype. Obviously, one particular state : State represents an immediate snapshot of the evaluation process; i.e., values of all variables at a given time. We denote this particular value for the variable x as [[x]]. Simply speaking, the state is the particular valuation of variables. We use the functor f [x v] for the definition of a function change in one point x to the value v. 4.2
Having defined all necessary prerequisites and auxiliary functions (recalling that the SeqT ype represents any permitted type of value), we formalize semantic functions over semantic domains as: SemQuery : Query → Seq(XM LDoc) → Seq(T ype) SemOptions : Options → (State → State) SemExpr : Expression → State → Seq(T ype) SemT erm : T erm → (State → Boolean) SemF rag : F ragment → State → Seq(T ype) SemAssign : F ragment×Identif ier → State → State SemRelOper : F ragment×RelOperator×F ragment →
→ (State → Boolean) SemBinOper : T erm × BinOperator × T erm →
→ (State → Boolean) SemAttrCons : AttrConstr × State → Seq(T ype) SemElemCons : ElemConstr × State → Seq(T ype) We start with the semantic equations for the expres3 We suppose usual functions nil, cons, append, null, head, sions, then we will continue with the semantics and tail for sequences. of queries. Terms. Terms are logical expressions. It means, that the meaning of any term in a given state is the Boolean value.
! State !
Terms are constructed with help of relational operators (we call it f ilter, but we do not distinguise it here), binary operators, negation sign, or primitive Boolean literals (denoted as B in the definition).
SemT erm[[B]] = :bool[[B]]
if B is a constant of the type Boolean SemT erm[[F1 RelOp F2]] =
:SemRelOper[[F1 RelOp F2]] SemT erm[[ ′not′ T ]] =
:not(SemT erm[[T ]] ) SemT erm[[T1 BinOp T2]] = = :SemBinOper[[T1 BinOp T2]]
Relational Operators. Relational operators can be applied to any two fragments and the meaning of resulting expression is the mapping from the current state to Boolean values. They serve in filters. Binary Operators. Binary operators can be applied to any two terms and the meaning of resulting expression is the mapping from the current state to Boolean values. XML- uses clasical logical conectives – logical ’or’ and logical ’and’ Fragments. Fragments are logical parts of filters and have the same meaning as expressions.
SemF rag : F ragment ! State ! Seq(T ype) SemF rag[[Id]] =
: [[Id]] SemF rag[[f (E1; :::; En)]] = = :f (SemExpr[[E1]] ; :::; SemExpr[[En]] ) SemF rag[[F P ]] = = :(SemF rag[[F ]] ◦ SemF rag[[P ]]) SemF rag[[(subquery)(arg)]] = = :(SemExpr[[subquery]]( )(SemExpr[[arg]]( ))) SemF rag[[I1I2:::InE]] = = SemExpr[[I2:::InE]]( [SemExpr[[E]] ← I1]) SemF rag[[N ]] = = :num[[N ]] if N is a constant of the type N umeral SemF rag[[S]] = = :str[[S]] if S is a constant of the type String SemF rag[[B]] = = :bool[[B]] if B is a constant of the type Boolean
Assignments. An assignment expression is a mandatory part of a query. It sets the initial context of the evaluation, more precisely, such expression evaluates a nullary function and stores the result into a variable. Then, the evaluation process will filter results and than iterates over all values and computes remaining results.
! State ! State
SemAssign[[Id '=' F ]] =
: [Id ← SemF rag[[F ]] ]
Expressions. Each expression e has a defined value SemExpr[[e]]( )( ) in a state and in an environment . The state represents the values of variables, the environment represents XML document that is elaborated. The result is a state SemExpr[[e]]( )( ), where all interesting values are bound into local variables. We do not need the environment in the next computation, because all information is in the state. We can model input data as a mapping Env from identifiers to XML documents, formally:
Env : Identif ier ! XM Ldoc
Seq(T ype)
Env ! SemExpr[[A1A2:::AnF1F2:::Fm]] =
= SemExpr[[A2:::AnF1F2:::Fm]](SemAssign[[A1]] ) SemExpr[[F1F2:::Fm]]
= = append(SemExpr[[F1]] ; SemExpr[[F2:::Fm]] )
if SemRelOper[[F1]] = true SemExpr[[F1F2:::Fm]] = SemExpr[[F2:::Fm]]
if SemRelOper[[F1]] SemExpr[[]] = nil = = f alse SemElemCons[[N A1:::AnI]] = = element(N; [[I]]; SemAttrCons[[A1]] ; :::;
SemAttrCons[[An]] ) SemElemCons[[N A1:::AnE]] = = element(N; SemExpr[[E]] ; SemAttrCons[[A1]] ; :::;
SemAttrCons[[An]] ) SemElemCons[[N I]] = element(N; [[I]]; nil) SemElemCons[[N E]] =
= element(N; SemExpr[[E]] ; nil) Constructors. Resulting values are created by constructors. A constructor is a list of items which can be either a variable identifier or a constructing expres- returning in the given state the string sion. :element(′book′; [[a]]; attribute(′title′; [[b]]))
State ! Seq(T ype) SemCons[[E1E]] = append(SemElemCons[[E1]] ;
SemCons[[E]] ) SemCons[[I1E]] = cons( [[I1]]; SemCons[[E]] ) SemCons[[ ]] = nil Element Constructors. The most common kind of resulting value is undoubtedly the element constructor; obviously, all its alternatives are supported – either with empty content, textual content or more complex (i.e. “mixed”) content. For all cases we can also attach attributes to elements. In the definition we use abstract functions element and attribute, which serves to construct output XML values from arguments. element(book,"the value of a",
attribute(title,"the value of b")) Options. The only allowed option in the language is now the specification of input XML documents.
Env ! Env SemOptions[[ ]](E) = E SemOptions[[ xmldata( X ) Y ]] =
= :SemOptions[[Y ]]( [Dom(X) ← X#])
We explore a function Dom(X) that converts an input XML document X into its internal representation accessible under identification X#.
Query. A query (denoted as Q) consists of query options (denoted as O), where input XML documents are
SemElemCons : ElemConstr State ! Seq(T ype) ebvoaulnudatteodi(tdsefnoormteadlansaEm)e,sa,ntdhethqeueoruytpeuxtprceosnssiotrnutcotiobne Attribute Constructors. Elements can have attributes commands (denoted as C). At first, input files are elabassigned by attribute constructors orated, than an initial variable assignment takes place, followed by evaluation of expression. Finally, the outSemAttrCons : AttrConstr State ! Seq(T ype) put is constructed. This idea is inbuilt into the definition of SemQuery[[O C E]] bellow. The whole meaning SemQuery[[Q]] of a query Q can be modeled as a mapping from the sequence of input XML documents into a sequence of output values of the type of T ype. The definition is carried by the structural induction on the possible forms of an input sequence.
SemQuery[[Q]] : Seq(XM LDoc) ! Seq(T ype)
SemQuery[[O C E]] : XM LDoc ! Seq(T ype) SemQuery[[Q]](nil) = nil SemQuery[[Q]](cons(H; T )) =
= append(SemQuery[[Q]](H); SemQuery[[Q]](T )) SemQuery[[O C E]] = =
:(SemCons[[C]](SemExpr[[E]]( :⊥) (SemOptions[[O]]( :⊥)( ))) The following example illustrates the computations performed in order to evaluate given XML- queries inside a virtual machine. It just computes a simple numerical term. More complex examples could be found in [4]. 5.1
Let us suppose the following simple query in the
XML- and its evaluation.
lambda $v1 ($v1 = plus(
( :?)(′$v1′) =
= 1: 1[′$v1′ SemF rag[[′plus(
(
( :?)](′$v1′) = = ( :?)[′$v1′ 2:plus(SemExpr[[′3′]] ( 2:?); SemExpr[[′2′]]( 2:?)) ( :?)](′$v1′) = = ( :?)[′$v1′ 2:plus(num[[′3′]]
( 2:?); num[[′2′]]( 2:?))( :?)](′$v1′) = = ( :?)[′$v1′ 2:plus(3; 2)( :?)](′$v1′) = = ( :?)[′$v1′ 2:5( :?)](′$v1′) = = ( :?)[′$v1′ :5](′$v1′) = = ( :?)[′$v1′ 5](′$v1′) = = 5 6
In this paper, we have presented syntax and denotational semantics of the XML- Query Language, a query language for XML based on simply typed lambda calculus. We use this language within the special XML- Framework as an intermediate form of XQuery expressions for description of its semantics. Nevertheless the language in its current version does not support all XML features, e.g. comments, processing instructions, and deals only with type information available in DTD, it can be successfully utilized for fundamental scenarios both for standalone query evaluation or as a tool for XQuery semantics description.