The Forest through the Trees

We have introduced several powerful techniques and formal tools: normalization rules that define a large language in terms of a smaller core ; inference rules for defining both the dynamic evaluation of and static typing of expressions; and judgments for relating external values, internal values, and types.

The foundations of the techniques presented in this chapter are in logic and programming language theory. The main technique we use to specify XQuery's semantics is widely used, so much so that it goes by several names , including natural semantics, big-step semantics , and evaluation semantics ; it is a special case of what is called operational semantics . The technique was originally proposed by Plotkin [STRUCTURAL] and Kahn [SEMANTICS], and used to good effect in the formal semantics of Standard ML [STANDARD-ML]. The notation for inference rules goes back to Frege's seminal work on logic [FORMULA-LANG; see also DDJ]. Natural semantics is covered in numerous introductory texts [PROG-FOUNDATIONS; PROG-LANG; THEORIES; and FS-PROG].

The process of formalizing XQuery gives us confidence in the correctness and completeness of XQuery's informal definition and can serve as the basis for formulating correct and semantics- preserving optimization techniques. Most important, we hope that the formal semantics can inform XQuery implementers in their day-to-day work, and that this chapter provides them the instruction necessary to use the XQuery Formal Semantics effectively.