% $Id: XPathWadler.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
A formal semantics of patterns in XSLT 16 July 1999 by Philip Wadler
XPathWadler: trait
    includes
        XMLWadler % sections 2, 3 of the paper

    introduces
% 5 A semantics for Patterns
        __ | __: Pattern, Pattern → Pattern
% default larch config doesn't have / as an op char, so we use !
        ! __ : Pattern → Pattern
        !! __ : Pattern → Pattern
        __ ! __ : Pattern, Pattern → Pattern
        __ !! __ : Pattern, Pattern → Pattern
        __ [__] : Pattern, Qualifier → Pattern
        [__] : String → Pattern % Wadler's notation doesn't need []
% @@isName: where does the Name set comefrom?
% is it a subset of String?
        star : → Pattern % *
        @ __ : String → Pattern % isName@@
        atStar : → Pattern
        text : → Pattern
        comment : → Pattern
        pi: String → Pattern % isName
        pi: → Pattern
        id: Pattern → Pattern
        id: String → Pattern
        ancestor: Pattern → Pattern
        ancestor_or_self: Pattern → Pattern
        dot : → Pattern
        dotdot : → Pattern

        and: Qualifier, Qualifier → Qualifier
        or: Qualifier, Qualifier → Qualifier
        notq: Qualifier → Qualifier
        first_of_type: → Qualifier
        last_of_type: → Qualifier
        first_of_any: → Qualifier
        last_of_any: → Qualifier
        __ \equal __ : Pattern, String → Qualifier
        [ __ ] : Pattern → Qualifier % wadler's notation doesn't need []


        M: Pattern, Node → Bool
% Wadler's formulation is M : Pattern -> Node -> Boolean
% but larch is 1st order, so I (un?)curried it.

        S: Pattern → R[Node]

        Q: Qualifier, Node → Bool
% again, curried

        siblingElements: Node → FiniteSet[Node]

        ancAux: Pattern, Node → FiniteSet[Node]
        ancSelfAux: Pattern, Node → FiniteSet[Node]

        firstAux: Node → FiniteSet[Node]

    asserts
        Pattern generated by
          | , !__, __ ! __ , !! __, __!!__,
          __ [__], [__],
          star, @, atStar,
          text, comment, pi:String→Pattern, pi:→Pattern,
          id:Pattern→Pattern, id:String→Pattern,
          ancestor, ancestor_or_self, dot, dotdot
        Qualifier generated by
          and, or, notq,
          first_of_type, last_of_type, first_of_any, last_of_any,
          \equal, [__]

        ∀ p, p1, p2: Pattern, x, y, x1, x2, x3: Node,
                    q, q1, q2: Qualifier,
                    n, s, s1: String,
                    ns: FiniteSet[Node]


% Figure 1: Semantics of patterns ...
        M(p, x)       = ∃ x1 (x1 ∈ (subnodes*)[root(x)]
                                ∧ x ∈ S(p)[x1]);

        S(p1 | p2)[x] = S(p1)[x] ∪ S(p2)[x];

        S(!p)[x]      = S(p)[root(x)];

% where wadler writes S ::= { x | P(x) }
% we write x \in S = P(x)
% @@c.f. comp.specification.larch discussion
        x2 ∈ S(!!p)[x]     = ∃ x1 (x1 ∈ (subnodes*)[root(x)]
                                        ∧ x2 ∈ S(p)[x1]);

        x2 ∈ S(p1!p2)[x]   = ∃ x1 (x1 ∈ S(p1)[x] ∧ x2 ∈ S(p2)[x1]);

        x3 ∈ S(p1!!p2)[x]  = ∃ x1 ∃ x2 (x1 ∈ S(p1)[x]
                                             ∧ x2 ∈ (subnodes*)[x1]
                                             ∧ x3 ∈ S(p2)[x2]);

        x1 ∈ S(p[q])[x]    = x1 ∈ S(p)[x] ∧ Q(q, x1);

        x1 ∈ S([n])[x]     = x1 ∈ subnodes[x] ∧ isElement(x1)
                                ∧ name(x1) = n;

        x1 ∈ S(star)[x]    = x1 ∈ subnodes[x] ∧ isElement(x1);

        x1 ∈ S(@ n)[x]     = x1 ∈ subnodes[x] ∧ isAttribute(x1)
                                ∧ name(x1) = n;

        x1 ∈ S(atStar)[x]  = x1 ∈ subnodes[x] ∧ isAttribute(x1);

        x1 ∈ S(text)[x]    = x1 ∈ subnodes[x] ∧ isText(x1);

        x1 ∈ S(comment)[x] = x1 ∈ subnodes[x] ∧ isComment(x1);

        x1 ∈ S(pi(n))[x]   = x1 ∈ subnodes[x] ∧ isPI(x1) ∧ name(x1) = n;

        x1 ∈ S(pi)[x]      = x1 ∈ subnodes[x] ∧ isPI(x1);

        x2 ∈ S(id(p))[x]   = ∃ x1 (x1 ∈ S(p)[x]
                                      ∧ ∃ s (s ∈ split(value(x1))
                                               ∧ x2 ∈ id(s)));

        x1 ∈ S(id(s))[x]   = ∃ s1 (s1 ∈ split(s) ∧ x1 ∈ id(s1));

        S(ancestor(p))[x]    = last(ancAux(p, x));
        x1 ∈ ancAux(p, x)  = x1 ∈ (parent\superplus)[x] ∧ M(p, x1);

        S(ancestor_or_self(p))[x]  = last(ancSelfAux(p, x));
        x1 ∈ ancSelfAux(p, x)  = x1 ∈ (parent*)[x] ∧ M(p, x1);

        S(dot)[x]            = {x};

        S(dotdot)[x]         = parent[x];

        Q(and(q1, q2), x)     = Q(q1, x) ∧ Q(q2, x);

        Q(or(q1, q2), x)     = Q(q1, x) ∨ Q(q2, x);

        Q(notq(q), x)        = ¬ Q(q, x);

        Q(first_of_type, x) = x ∈ first(firstAux(x));
        x1 ∈ firstAux(x)  = x1 ∈ siblingElements(x) ∧ name(x1) = name(x);
% Wadler paper missing x1 \in before siblingElements???

        Q(last_of_type, x)  = x ∈ last(firstAux(x));

        Q(first_of_any, x)  = x ∈ first(siblingElements(x));

        Q(last_of_any, x)   = x ∈ last(siblingElements(x));

        Q(p \equal s, x)    = ∃ x1 (x1 ∈ S(p)[x] ∧ value(x1) = s);

        Q([p], x)           = (S(p)[x] ≠ {});

        x2 ∈ siblingElements(x) = ∃ x1 (x1 ∈ parent[x]
                                           ∧ x2 ∈ subnodes[x]
                                           ∧ isElement(x2));
    implies
        converts
            siblingElements,
            ancAux, ancSelfAux, firstAux,
            M, S, Q

[Index]

HTML generated using lsl2html.