% $Id: WadlerProps.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
WadlerProps: trait
includes
XPathWadler
introduces
M': Pattern, Node → Bool
% Wadler writes Pattern x Node -> Bool, but then uses
% it as a higher-order function. odd.
asserts forall p, p1: Pattern,
x, x1, x2: Node,
s: String
M'(p, x) = ∃ x1 (x1 ∈ (parent*)[x]
∧ x ∈ S(p)[x1]);
implies forall p, p1: Pattern, x: Node, s: String
%@@ p not containing id(p), ancestor(p), ancestor-or-self(p), ..
%M(p, x) = M'(p, x);
p = !p1 ∨ p = id(s) ⇒
S(p)[x] = S(p)[root(x)];
% p @@ not containing /p, id(s), ancestor(p), anc-or-self(p), ..
%S(p)[x] \subseteq (subnodes\superstar)[x];
%@@ save this for later...
% S(p!id(dot))[x] = S(id(p))[x];
[Index]
HTML generated using lsl2html.