XQuery Formal Semantics

Normalization

XQuery core

            [Clause₁ Clause₂ return Expr]_Expr ==

                        [Clause₁ return [Clause₂ return Expr]_Expr]_Expr

            [for ForBinding₁, ForBinding₂ return Expr]_Expr ==

                        [for ForBinding₁ return [for ForBinding₂ return Expr]_Expr]_Expr

            [where Expr₁ return Expr₂]_Expr ==

                        [if  (Expr₁) then Expr₂ else ()]_Expr ==

if (fn:boolean([Expr₁]_Expr))then [Expr₂]_Expr else ()

            [PathExpr]_Expr == fs:distinct-doc-order([PathExpr]_Path)

            [StepExpr / RelativePathExpr]_Path ==

let $fs:sequence := fs:distinct-doc-order([StepExpr]_Path)return

let $fs:last := fn:count($fs:sequence) return

for $fs:dot at $fs:position in $fs:sequence return

                              [RelativePathExpr]_Path

Example

 [<biblio>

 {

  for $r in doc("eb-bib.xml")//cite

  where $r/author

  return

    <citation>{$r}</citation>

 }

</biblio>]_Expr  ==

element biblio

 {

 for $r in fs:distinct-doc-order

     (let $fs:seq := fs:distinct-doc-order(doc("eb-bib.xml")) return

      let $fs:last := fn:count($fs:seq) return

      for $fs:dot AT $fs:position in $fs:seq return

      descendant-or-self::cite) return

  if (fn:boolean(fs:distinct-doc-order

       (let $fs:seq := fs:distinct-doc-order($r) return

        let $fs:last := fn:count($fs:seq) return

        for $fs:dot AT $fs:position in $fs:seq return

        child::author)) then 

            element citation {$r}

     else ()

 }

Static Semantics

Typing

Judgements

statEnv ├ Expr : Type

in environment StatEnv, expression Expr has type Type

Atomic types (e.g., xs:integer, xs:decimal, xs:double, xs:string)

Union types (e.g., (xs:string | xs:decimal) )

Sequence types (e.g., xs:integer*, xs:string?, xs:double+, empty())

Complex types (e.g., element(biblio), element(biblio,myNames:biblio.type), attribute(@*,myNames:date.type))

xs:anyType

Inference rules

statEnv ├ Expr₀ : xs:integer

statEnv ├ Expr₁ : xs:integer

     -------------------------------

statEnv ├ Expr₀ < Expr₁ : xs:boolean

statEnv ├ Expr₀ : xs:boolean

statEnv ├ Expr₁ : Type₁

statEnv ├ Expr₂ : Type₂

     -------------------------------------------------

statEnv ├ if (Expr₀ )then Expr₁ else Expr₂ : (Type₁ | Type₂)

statEnv ├ Expr₀ : Type₀

statEnv  + varType(Var : Type₀)├ Expr₁:Type₁

     -------------------------------------------------

statEnv ├ let $Var := Expr₀ return Expr₁ : Type₁

Dynamic Semantics

dynEnv ├ Expr₀ => Integer₀

dynEnv ├ Expr₁ => Integer₁

     -------------------------------

dynEnv ├ Expr₀ < Expr₁ => Integer₀ <Integer₁

dynEnv ├ Expr₀ : fn:true()

dynEnv ├ Expr₁ => Value

     -----------------------------------------

dynEnv ├ if (Expr₀ )then Expr₁ else Expr₂ => Value

dynEnv ├ Expr₀ => Value₀

dynEnv  + varValue(Var => Value₀)├ Expr₁ =>Value₁

     -----------------------------------------

dynEnv ├ let $Var := Expr₀ return Expr₁ => Value₁

dynEnv ├ Expr₀ => (Item₁ , ... , Item_n)

dynEnv  + varValue(Var₀ =>Item₁,Var₁ =>1)├ Expr₁ =>Value₁

                           ...

dynEnv  + varValue(Var₀ =>Item_n,Var₁ =>n)├ Expr₁ =>Value_n

     ------------------------------------------------------------

dynEnv ├ for $Var₀  at $Var₁ in Expr₀ return Expr₁ => (Value₁ , ... , Value_n)

Dealing with data store

Store₀;dynEnv ├ Expr => Value₁; Store₁

Store₁;dynEnv ├ Value₁  erases to Value₂; Store₂

NodeId not in dom(Store₂)

Store₃=Store₂ U store(NodeId => element ElementName {Value₂})

Store₃; dynEnv ├ validate { element ElementName {Value₂} } => Value₃; Store₄

     --------------------------------------------------------

Store₀;dynEnv ├ element ElementName {Expr} => Value₃; Store₄

Relating static and dynamic environments

V  matches  T                            is a judgment that a value V is of type T

dynEnv  matches  statEnv      if  dom(dynEnv.varValue) = dom(statEnv.varType)

                                                              and x in dom(") implies

dynEnv.varValue(x) matches statEnv.varType(x)

            Type soundness for values

if        dynEnv matches statEnv           and

         dynEnv ├ Expr => Value              and

         statEnv ├ Expr : Type

then   Value matches Type

            Type soundness for errors

if        dynEnv matches statEnv           and

         dynEnv ├ Expr raises Error     and

         statEnv ├ Expr : Type

then   Error  ≠ typeErr

Example

Assume eb-bib.xml with data shown and query Q

<biblio>

 {

   for $r in doc("eb-bib.xml")//cite

   where $r/author

   return

    <citation>{$r}</citation>

 }

</biblio>

statEnv ├ Q : element (biblio, element(citation,  element(cite, fs:anyType) )* )

dynEnv ├ Q =>

<biblio><citation><cite type="full"><author>W.L. Morton</author><title edition="2" date="1969">The Kingdom of Canada</title></cite></citation><citation><cite type="full"><author>H.A. Innis</author><title edition="2" date="1956">The Fur Trade in Canada</title></cite></citation><citation><cite type="author><author>W.S. MacNutt</author></cite></citation><citation><cite type="author><author>Fernand Ouellet</author></cite></citation></biblio>

References and related reading

Querying XML, Chapter 10.8, XQuery from the Experts, Chapters 4-5

W3C Semantics

Simeon03