% $Id: XMLWadler.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
XMLWadler: trait
    includes
        Relation(Node, R[Node],
         __ \< __ \> __ for __ 〈 __ 〉 __, %@@ LP doesn't grok lslinit.ini
        bot for ⊥, top for ⊤),
        Set(Node, FiniteSet[Node] for Set[E]),
        RelSet(String, Set[String]),
        TotalOrder(Node),
        MinMax(Node)

    introduces
% section 2: Sets and relations
% where Wadler writes y \in rel[x], larch folks write
% x \langle rel \rangle y
% @@hmm... LP doesn't seem to understand \langle as
% a bracket symbol, so I'll use \<.
        __ [ __ ] : R[Node], Node → FiniteSet[Node]
        
        first, last: FiniteSet[Node] → FiniteSet[Node] % Set1 below

% section 3: A data model for XML
        isRoot, isElement, isAttribute, isText, isComment, isPI: Node → Bool
% why not make those disjoint types? hm...
        parent: → R[Node]
        children: → R[Node]
        attributes: → R[Node]
        root: Node → Node

        subnodes: → R[Node]

        name: Node → String
        value: Node → String        

        id: String → FiniteSet[Node] % Set1... see below
        split: String → Set[String]


    asserts ∀ x, y, x1, x2: Node,
                    r:R[Node],
                    n, s, s1: String,
                    ns: FiniteSet[Node]

% section 2: Sets and relations
% where Wadler writes y \in rel[x], larch folks write
% x \langle rel \rangle y
        y ∈ r[x] = (x \< r \> y);

        first({}) = {};
        last({}) = {};
        first({x}) = {x};
        last({x}) = {x};
        first(ns) = {y} ⇒ first(insert(x, ns)) = {min(x,y)};
        last(ns) = {y} ⇒ last(insert(x, ns)) = {max(x,y)};

% section 3: A data model for XML
        functional(parent);
        isRoot(x) ⇒ parent[x] = {};

        children[x] ≠ {} ⇒ isRoot(x) ∨ isElement(x);
        attributes[x] ≠ {} ⇒ isElement(x);
        y ∈ children[x] ⇒
         isElement(y) ∨ isText(y) ∨ isComment(y) ∨ isPI(y);
        y ∈ attributes[x] ⇒ isAttribute(y);
        y = root(x) ⇒ isRoot(y); % i.e. isRoot(root(x))

        subnodes[x] = children[x] ∪ attributes[x];

% @@ name/value table

        x ∈ id(n) ∧ y ∈ id(n) ⇒ x=y; % Set1

        y ∈ subnodes[x] = (parent[y] = {x}); % p. 5

        x ∈ (subnodes*)[root(x)] ; % p. 5
% @@hmm... I thought I could use
% Node generated by root, children, attributes
% but children and attributes aren't Node->Node operators.
% Hm... a more natural larch definition might go bottom-up:
% makeElement : List[Node], List[Node] -> Node
% Node generated by makeElement, root

% @@ I added this specification of root
        isRoot(x) ⇒ root(x) = x;
         x \< subnodes \> y ⇒ root(x) = root(y);

    implies
        ∀ x: Node
             root(root(x)) = root(x)
%@@? converts first, last, __[__]:Node->FiniteSet[Node], root

[Index]

HTML generated using lsl2html.