Archive for the ‘formal methods’ Category

There must be fifty ways …

Wednesday, April 7th, 2010

[7 April 2010]

The old Paul Simon song “There must be fifty ways to leave your lover” keeps running through my head. I can see close to fifty ways to define the XPath 1.0 data model in terms of (a) a set of nodes and (b) two relations defined on that set, which are taken as primitive; all other relations (i.e. all the other axes of XPath) are defined in terms of those two primitive relations.

Strictly speaking, I make it forty-eight ways. First, pick any single relation from any of the following four groups:

  1. parent, child, ancestor, descendant
  2. prevsib, nextsib, preceding-sibling, following-sibling
  3. prevnode, nextnode, document-order preceding (>>), document-order-following (<<)

That’s twelve possibilities.

Second, pick any single relation from either of the other two groups; that makes eight possible choices, times twelve first choices, for ninety-six ordered pairs of relations. But the order doesn’t matter, so we have forty-eight distinct pairs.

In recent days, taking some pairs not quite at random, defining the constraints they must satisfy in order to be a suitable basis for defining an XPath 1.0 tree, and defining all the other relations in terms of the chosen primitives, I have learned a couple of mildly interesting things.

  • It’s more convenient to take parent as a primitive, than child.
  • It’s more convenient to take one of the single-step relations (parent, child, nextsib, prevsib, nextnode, prevnode) than one of their transitive closures (ancestor, descendant, etc.).

The nextsib relation, for example, needs to be acyclic, functional, injective, and not transitive. If it is, then its transitive closure following-sibling will automatically be suitable. But if you start with following-sibling and specify (as you will need to) that it is transitive and acyclic, that does not suffice to guarantee that its transitive reduction nextsib is functional and injective. You can of course simply say that a following-sibling relation is suitable if and only if (a) it’s transitive, (b) it’s acyclic, and (c) its transitive reduction is functional and injective, but now you’re forcing the reader to work with two relations, not just one: both following-sibling and its transitive reduction. It would be interesting either to find a way to constrain the closure directly to ensure the necessary properties in the reduction, or else to find a proof that there is no way to constrain a closure to ensure that its reduction is functional and injective without explicitly referring to the reduction.

  • From any relation in any group, the other relations in that group are (relatively) easy to derive in terms of inversion, transitive closure, or transitive reduction. Defining a relation in the third group typically proves more interesting. And while it’s more convenient to choose the primitive relations from among the reductions, it turns out that at least in some cases it’s easiest to define the third group in terrms of one of the closures. For example, given the parent and next-sibling relations, it proves easier to define document-order-following in terms of the primitives than to define next-node.

It occurs to me to wonder whether there are ways to define XPath 1.0 trees that don’t reduce to or include one of these forty-eight.

One way to define the XPath data model

Tuesday, April 6th, 2010

[6 April 2010; addenda and copy editing 7-8 April 2010]

After discovering earlier this year that the definition of the XPath 1.0 data model falls short of the goal of guaranteeing the desired properties to all instances of the data model, I’ve been spending some time experimenting with alternative definitions, trying to see what must be specified a priori and what properties can be left to follow from others.

It’s no particular surprise that the data model can be defined in a variety of different ways. I’ve worked out three with a certain degree of precision. Here is one, which is not the usual way of defining things. For simplicity, it ignores attributes and namespace nodes; it’s easy enough to add them in once the foundations are a bit firmer.

Assume a non-empty finite set S and two binary relations R and Q on S, with the following properties [Some constraints are shown here as deleted: they were included in the first version of this list but later proved to be redundant; see below] :

  1. R is functional, acyclic, and injective (i.e. for any x and y, R(x) = R(y) implies x = y).
  2. There is exactly one member of S which is not in the domain of R (i.e. R(e) has no value), and exactly one which is not in the range of R (i.e. there is one element e such that for no element f do we have e = R(f)).
  3. Q is transitive and acyclic.
  4. The transitive reduction of Q is functional and injective.
  5. It will be observed that R essentially places the elements of S in a sequence without duplicates. For all elements e, f, g, h of S, if Q includes the pairs (e, f) and (g, h) and if g falls between e and f in the sequence defined by R (or, more formally, if the transitive closure of R contains the pairs (e, f), (e, g), and (g, f)), then h also falls between e and f in that sequence.
  6. The transitive closure of the inverse of R (i.e. R-1*) contains Q as a subset.
  7. The single element of S which is not in the domain of R is also neither in the domain nor the range of Q.

It turns out that if we have any relations R and Q defined on some set S, then we have an instance of the XPath 1.0 data model. The nodes in the model instance, the axes defining their interrelations, and so on can all be defined in terms of S, R, and Q.

For the moment, I’ll leave the details as an exercise for the reader. (I also realize, as I’m about to click “Publish”, that I have not actually checked to see whether the set of constraints given above is minimal. I started with a short list and added constraints until S, R, and Q sufficed to determine a unique data model instance, but I have not checked to see whether any of the later additions rendered any of the earlier additions unnecessary. So points for any reader who identifies redundant constraints in the list given above.)

[When I did check for minimality, it turned out that several of the constraints included in the list above are redundant. The fact that relation R is functional and injective, for example, follows from the others shown. Actually it follows from a subset of them. The deletions above show one way of reducing the number of a priori constraints: they all follow from the others and can be dropped. None of the remaining items follows from the others; if any of them are deleted, the constraints no longer suffice to ensure the properties required by XPath.]

Alloy as logical desk calculator

Friday, March 26th, 2010

[26 March 2010]

Long ago I used a wonderful file-oriented database system called Watfile, which was designed as a sort of desk-calculator for data. It was designed for personal use, not industrial-strength data management, and its designers successfully resisted the temptation to add more features and more power at the cost of a more complex user interface. Watfile was to a full enterprise-class database as a desk calculator of the 1960s was to … oh, perhaps to Fortran. For suitable problems, the ease of setup far outweighed any considerations of power or completeness.

The experience of using Watfile for data manipulation tasks established in my mind the class of ‘desk-calculator-like’ packages for various kinds of problem.

Today I experimented with Alloy as a sort of logical desk calculator, and I’m happy to report that it passed the test with flying colors.

For reasons I won’t go into here, I’ve wondered a bit recently what it might look like to apply the technique of distinctive-feature analysis (originally developed for phonological descriptions of sound systems of language) to writing systems. When I sat down a few months ago with pencil and paper to see if I could devise a smallish set of typographic features which could (say) distinguish the twenty-six letters of the alphabet as I was taught it in first grade, I rapidly found that working solely with pen and paper made me impatient: it was too tedious to look at the set of features already identified and see which letters could not yet be distinguished (because they had the same value for all the features in question).

When I came back to this problem this afternoon, I thought for a few minutes about what questions I’d like to be able to ask the machine. Given a specified set of graphemes (as a first exercise, I chose the lower-case alphabet) and a specified set of binary features (does the letter have an ascender? a descender? a vertical stroke? a full or partial circle or bowl? Is the stroke to the left of the bowl? …), with information about which graphemes have the feature in question, I want to be able to ask, first, whether a particular set of features suffices to distinguish each individual grapheme? Or are there two or more graphemes which have the same value for all features in the set? And of course, if there are such sets of indistinct graphemes, what are they?

It occurred to me to solve the problem in Prolog; it would take just a relatively simple set of Prolog predicates to do what I wanted. But as I was preparing to launch X Windows, so that I could launch Prolog, I realized that I already had the Alloy Analyzer running. And so I wrote the predicates I wanted in Alloy instead of Prolog, to see whether it would work.

The upshot is: yes, it worked, and it was probably a bit easier to do than it would have been in Prolog. When I was thinking about how to set up the problem in Prolog, I found myself wondering about the best data representation to choose, and so on, almost as much as about the structure of the problem. I won’t say that Alloy posed no analogous problems — I did have to think for a moment or two about the best way to describe graphemes and distinctive features. But the high level of abstraction afforded by Alloy made the decision feel less binding, and made me feel a bit more comfortable experimenting. (It sounds strange to put it this way: after all, Prolog’s high level of abstraction is one of its great design strengths. But Prolog is also designed to be an efficient and effective programming language, which means that some details are exposed which have only procedural significance, and sometimes you find yourself thinking about them, even in situations where questions of execution efficiency don’t arise.

In very short order, I found it possible to define a suitably abstract representation of graphemes and features, specify some useful functions and predicates for asking the questions described above, and specify a small set of features (ten) which have a certain degree of typographic plausibility and which suffice to distinguish the graphemes in question. (Ten binary features for twenty-six graphemes may seem high, given that the theoretical minimum is only five, and that ten bits suffice to distinguish a thousand objects, not just twenty-six. But writing, like natural language, has some redundancy. Feature sets used to analyse natural language sound systems are also often very inefficient.) The visualization tools did not prove very helpful, but the Evaluator feature of the Alloy Analyzer was a great help.

If I pursue this work any further, I probably will put it into Prolog, where the interactive interface for expression evaluation is perhaps a bit more convenient than in Alloy. But it’s nice to know that Alloy can be used for this kind of problem, too.

Interested readers can find both the generic definitions and the specific graphemes and features for lower-case Latin letters (as used in Anglophone countries) on the Black Mesa Technologies web site.

The axes of XPath

Thursday, March 25th, 2010

[25 March 2010; error noticed by Dimitre Novatchev fixed 29 March 2010]

Steve DeRose and I have been discussing the XPath [1.0] data model recently (among other things), and in the course of the discussion an interesting observation has emerged.

it’s obvious that some of the axes in XPath expressions are inverses of each other, and also that some are transitive closures of others (or, going the other way, that some are transitive reductions of others). What surprised me a little was that (if for the moment you leave out of account the self and the XYZ-or-self axes, the attribute axis, and the namespace axis [and also preceding and following) all of the XPath axes fit naturally into a pattern that can be represented by three squares. (Will table markup work here? I wonder.) The first square represents the up/down axes:

Up/down
parent ancestor
child descendant

The next square covers sibling relations. Unlike parent and child, which are just short-hand for single steps along the up or down axis, XPath provides no syntactic sugar for preceding-sibling :: * [1] and following-sibling :: * [1], so I’ve invented the names “nextsib” and “prevsib” (marked with a star here to signal that they are invented):

Sideways
*prevsib preceding-sibling
*nextsib following-sibling

The third square describes overall document order; again, I’ve invented names for the single-step relations [note that the names used here for the transitive relations are given by XPath 2.0; XPath 1.0 doesn't provide notation for them]:

Overall document order
*prevnode >>
*nextnode <<

[In the first version of this post, the right-hand columns were labeled preceding and following, but Dimitre Novatchev reminded me gently that these axes do not in fact correspond to document order: preceding excludes andestors and following excludes descendants. That's a plausible exclusion, since no one in their right mind would say that chapter one of Moby Dick precedes the first paragraph of Moby Dick. Contains, yes; precedes, no. In fact, I remember getting into an argument with Phil Wadler about this, early on in the days of the XML Query working group, not realizing (a) that the document ordering he was describing was actually prescribed by XPath 1.0, nor (b) that saying that ancestors precede their descendants in document order didn't mean that the ancestors would have to be present on the preceding axis. Thank you, Dimitre! And sorry, Phil!]

In each table row, the relation on the right is the positive transitive closure of the one on the left, and the one on the left is the transitive reduction of the one on the right.

In each table column, the relations in the top and bottom rows are inverses of each other.

The tables make it easy to see that it suffices to take a single pair of relations on nodes as primitive (e.g. child [or better first-child] and nextsib, or parent and prevsib); everything else in the tree can be defined in terms of the two primitive relations. (It’s not completely clear to me yet whether any two relations will do as long as they are from different tables, or not. Taking nextnode and parent seems to work, as does the pair nextnode and child but nextnode and first-child seems to pose problems — why can child be replaced by first-child in some situations but not others? Hmm.)

There seem to be implications for the formalization of the data model (which is how we got here in the first place), but maybe also for teaching new users how to think about or learn XPath.

A small gotcha in Alloy’s closure operator

Wednesday, March 24th, 2010

[24 March 2010]

Consider the following Alloy model:

sig Node {}
one sig gl { r, s : Node -> Node }{ s = *r }
run {}

It has no instances, and the Alloy Analyzer comments laconically “Predicate may be inconsistent.” But the similar model below does have instances. Why?

sig Node {}
one sig gl { r, s : univ -> univ }{ s = *r }
run {}

I ran into this phenomenon today, when I was trying to do some work relating to the definition of document order in the XPath data model. It’s convenient to have both a relation like the successor relation of arithmetic on the natural numbers, which gives you the next item in document order, and a relation like the less-than-or-equals relation of arithmetic, which is the reflexive transitive closure of the successor relation. And if you want to have both, you will want to specify, as is done above, that the one is the reflexive transitive closure of the other. And when you do, it’s a bit alarming to be told (and mostly very quickly) that nothing in your model has any instances at all.

It took me a couple hours to reduce the problem to the terms shown above (there were several complications which looked more likely to be the cause of the trouble, and which took time to eliminate), and then a little more time to realize that declaring the relations in question as Node -> Node or as univ -> univ made a difference.

I invite the interested reader, if a user of Alloy, to consider the two models and explain why one has instances and the other doesn’t. No peeking at what follows until you have a theory.

Found it? If you found it without spending a couple hours on it, my hat’s off to you.

The * operator produces the reflexive transitive closure of a binary relation r by essentially taking the union of the positive transitive closure of r and the identity relation iden. That is, for all relations r, *r is defined as ^r + iden.

The problem is that iden covers everything in the model, including the gl (globals) object and the automatically included integers. And the upshot is that s cannot satisfy the constraint s = *r while also satisfying its declaration (Node -> Node).

In his book Software Abstractions, Daniel Jackson remarks on the oddity of * including ‘irrelevant’ tuples in the relation, but (as he points out) it almost never matters, because in many context the irrelevant tuples are dropped out during evaluation of the containing expression. The consequence is that it’s possible to work with Alloy (as I have obviously been doing) with a mental model in which * is somehow smart enough to add only those tuples which are ‘relevant’ to the relation whose closure is being taken. That mental model proves to be an over-complexification.

One reason I like Alloy a lot is that it allows the user to operate at a fairly high level of abstraction, if you can just find the right level. Working in Alloy presents fewer of the small issues of syntax and data typing and so on that can bedevil attempts to explore problems even in high-level programming languages, and so you mostly get to your results a lot faster. But I guess no formal system is ever completely free of cases where the user stares blankly at the screen for some indefinite period of time, trying to figure out why the system is producing such a counter-intuitive and obviously wrong result.

In the words of the old MVS error message: Probable user error. Solution: correct and re-submit.

How formal can you get?

Tuesday, January 26th, 2010

[26 January 2010; updated a URI 28 Jan 2010]

In a recent comment on an earlier post here, David Carlisle wrote of proofs concerning properties of the XPath 1.0 data model

It’s not clear how formal any such proof could be, given that the XPath model and even more so, XML itself are defined so informally.

It’s true that the XPath spec defines the data model in prose and not in formulas. But on the whole it’s relatively formal and explicit prose, and I would expect it to be relatively easy to translate the prose into a formal notation.

As a test of that proposition, I recently improved a shining hour or four by translating section 5 of the XPath 1.0 spec into Alloy, the modeling tool developed by Daniel Jackson and others in the MIT Software Design Group. (I would describe Alloy briefly here, but I’ve written about Alloy often enough in this blog that I won’t describe it again now; regular readers of this blog will already know about it, and those who don’t can search the Web for information, or search this blog for what I’ve said about it before.)

The full Alloy model of XPath 1.0 is available from the Black Mesa Technologies web site. It will be of most interest, of course, for those familiar with Alloy, or wanting to learn more about it. But Alloy’s formalism is simple enough that anyone with a taste for formal methods will find it easy going, and the document paraphrases all the important things in English prose.

The net result, I think, is that there are (unsurprisingly) some places where the definition of the XPath 1.0 data model could or should be more explicit, and a few places where it seems a rule or two given explicitly is strictly speaking redundant, but by and large the definition is pretty clean and seems to mean what its creators meant it to mean. By and large, the definition of the data model is formulated without reliance on the XML spec (there are a few places where this separation could be cleaner), so that the informality of the XML spec (or what I prefer to think of as its programmatic promiscuity regarding models) does not in fact make it hard to formalize the XPath 1.0 data model.

In the current version, there are a couple of rough bits that I hope to sand down before I use this model in any other contexts. The ones I’m currently aware of are these:

  • The definition of the parent relation does not require that whenever parent(c,p) is true, either child(p,c) or attribute(p,c) is true. The XPath 1.0 spec doesn’t say this explicitly, but I think its authors probably felt that it would be pedantic to say something like that for a relation with a name like parent.
  • Similarly, the relations parent and ch are not guaranteed acyclic, though I think the original spec assumes that the names parent and child make clear that the relations should be acyclic. (But see the song “I’m my own Grandpa” and the Alloy models illustrating it, developed in Daniel Jackson’s Software Abstractions and shipped with Alloy in the samples directory.)
  • The predicate precedes intended to model document order is defined recursively; this is not legal in Alloy. So a conventional relation on nodes will need to be defined instead, with appropriate constraints. It is still not clear whether the rules given in the spec suffice to make the order total (at least in the absence of multiply occurring children); if they don’t, I’d like to propose an additional predicate which has that effect.

Two, four, three, who’s counting?

Monday, January 25th, 2010

[25 January 2010; correct botched formulation, 26 January]

The XPath 1.0 puzzle introduced and discussed in earlier posts continues to occupy some of my thoughts. Consider the document which can be written

  <a><b/><b/><b/></a>

The central question is this: given an instance of the XPath 1.0 data model corresponding to this document (or to any equivalent document), how many element nodes are present in the instance?

It turns out that not only are the answers four and two both consistent (as far as I can tell) with the definition of the XPath 1.0 data model, but that other answers are possible as well. Well, another answer.

Consider the document

<!DOCTYPE a [
<!ELEMENT a ANY>
<!ELEMENT b ANY>
<!ENTITY b '<b/>' >
]>
<a>&b;&b;<b/></a>

This is not the same serial-form XML document as the one at the top of the page, and the data-model equivalent is not necessarily the same, either, I think. But they both have a document element of type ’a’, whose ordered list of children has length three, with each child being of type ‘b’.

If we take token as denoting some physical object, marks on paper or some other way of writing a character type (here, pixels on screens, magnetic fields on suitable media, or optical effects on other media), which I am told is its proper meaning as it was introduced by Peirce, then here there appear to me to be three string tokens matching the element production (one ‘a’ and two ‘b’s), not four and not two, and thus three element nodes in the data model, not four and not two.

I’m not really at all sure that the right way to define XML documents (and by extension XML elements) is as strings. But if we do wish to say that an element is a string (of some kind), there seem to be at least three different approaches we can take:

  1. a sequence of character types (i.e. a string-type)
  2. a sequence of character tokens (i.e. a string-token)
  3. an occurrence, within some context, of a sequence of character types

Some of the issues relating to these concepts are very well laid out in the article “Types and Tokens” written by Linda Wetzel for the Stanford Encyclopedia of Philosophy. It is interesting to know that SGML and XML accomplish simply, through entity references, what some philosophers have regarded as impossible: we have more occurrences of a thing than we have tokens for it. In the second document given above, it seems clear (at least to me, but I am no philosopher) that there are two string-tokens of type “<b/>” — one in the entity declaration and one in the document content — and three occurrences of that string-type in the document body. When entity expansion is performed by a machine, we are quite likely to be able to identify different tokens with the different occurrences of the string-type (as long as we are willing to entertain time-slices as part of our definition of string-token), but when I just look at the document and count the occurrences of the string-type, I don’t create new tokens in the physical world (unless you want to include mental acts as tokens, but I am pretty sure that that would be a bad idea).

The good news is that there is plenty of philosophical light to throw on these issues, and the issues are well understood by philosophers. Also good news is that the XPath 1.0 data model appears to be consistent with all three possible views.

The bad news, I think, is that while the philosophers understand the issues quite well, they don’t agree on what to do about them. Also bad news is that the XPath 1.0 spec is consistent with all three views, even though it clearly wants to have a single answer to questions like “How many elements are in this document?”. Also, it seems clear that the XPath 1.0 spec really wants to view elements as occurrences (or, at least, the occurrence story produces the results the XPath 1.0 spec relies on its data model producing), but the notion of occurrence appears to be regarded by philosophers as easily the most problematic of the three concepts competing for our patronage.

Fortunately, to make the XPath 1.0 data model do what its creators wanted it to do, all that is necessary is to say explicitly that no node occurs more than once (there’s that word again!) in its parent’s ordered list of children. Or, equivalently, that the cardinality of the set of child nodes is the same as the length of the ordered list of children.

[In full XPath terms, we may also think of it as forbidding any node to appear among the result of evaluating the expression “preceding-sibling::* | following-sibling::*” with that node as the context item. But the data model does not provide a primitive definition of sibling-hood, so it can't conveniently be formulated that way in the data model.]

Tell me, Captain Yossarian, how many elements do you see?

Friday, January 22nd, 2010

[22 January 2010]

In an earlier post, I asked how many element nodes are present in the following XML document’s representation in the XPath 1.0 data model.

  <a><b/><b/><b/></a>

I think the spec clearly expects the answer “four” (a parent and three children). More than that, I think the spec reflects the belief of its authors and editors that that answer follows necessarily from the properties of the data model as defined in section 5 of the spec.

But I don’t think “four” is the only answer consistent with the data model as defined.

In particular, consider the answer “two”: one ‘a’ element node, and one ‘b’ element node (which for brevity I’ll just call A and B from here on out; note that A and B are element nodes, whose generic identifiers happen to be ‘a’ and ‘b’.). As far as I can tell, the abstract object just defined obeys all the rules which define the XPath 1.0 model. The rules which seem to apply to this document are these:

  1. “The tree contains nodes.”

    Check.

  2. “Some types of nodes … have an expanded-name …”

    Check: here the names are “a” and “b”.

  3. “There is an ordering, document order, defined on all the nodes in the document …”

    Check: in the model instance I have in mind the nodes are ordered. (In fact they have a total order, which is more than the spec explicitly requires here.) The root node is first, A second, and B third.

  4. “… corresponding to the order in which the first character of the XML representation of each node occurs in the XML representation of the document after expansion of general entities.”

    Check.

  5. “Thus, the root node will be the first node.”

    Check.

  6. “Element nodes occur before their children.”

    Check: The element node A occurs before its child B in the ordering.

  7. “Thus, document order orders element nodes in order of the occurrence of their start-tag in the XML (after expansion of entities).”

    Check: the start-tags for B begin at positions 4, 8, and 12 of the document’s serial form (counting from 1), and the start-tag for A begins at position 1. So the order of the start-tags in the XML matches the order of the nodes in the model.

    If we had several elements with multiple occurrences and thus multiple start-tags, and the positions of the start-tags were intermingled (as in <a> <b/> <c/> <b/> <c/> <b/> </a>), then it would appear that we had only a partial order on them. if the spec specified that document order was a total ordering over all nodes, we might have a problem. But it doesn’t actually say that; it just speaks of an “ordering”; it would seem strange to argue that a partial ordering is not an “ordering”.

  8. “Root nodes and element nodes have an ordered list of child nodes.”

    Check: the root node’s list of children is {1 → A}, A has the list {1 → B, 2 → B, 3 → B}, and B has the empty list {}.

  9. “Nodes never share children: if one node is not the same node as another node, then none of the children of the one node will be the same node as any of the children of another node.”

    Check: the sets {A}, {B}, and {} (representing the children, respectively, of the root node, A, and B) are pairwise disjoint.

  10. “Every node other than the root node has exactly one parent, which is either an element node or the root node.”

    Check. A has the root node as its parent, B has A as its parent.

  11. “A root node or an element node is the parent of each of its child nodes.”

    Check: the root’s only child is A, and A’s parent is the root. A’s only child is B, and B’s parent is A.

  12. “The descendants of a node are the children of the node and the descendants of the children of the node..”

    Check. The descendants of the root node are {A, B}, those of A are {B}, those of B are {}.

That’s it for the general rules; I think it’s clear that the construction we are describing satisfies them. The subsections of section 5 have some more specific rules, including one that is relevant here.

  1. “There is an element node for every element in the document.” (Sec. 5.2.)

    This rule was cited by John Cowan in his answer to the earlier post; it seems to me it can be taken in either of two ways.

    First, we can take it (as John did, and as I did the first time through this analysis) as saying that for each element node in an instance of the data model, there is an element in the corresponding serial-form XML document, and conversely (I read it as claiming a one to one correspondence) for every element in the serial-form document, there is an element node in the data model instance.

    In this case, the rule seems to me to have two problems. The first problem is that the rule assumes a mapping between XML serial-form documents and data model instances and further assumes (if we take the word “the” and the use of the singular seriously — we are, after all, dealing with a formal specification written by a group of gifted spec-writers, and edited by two of the best in the business) that the mapping from data model instance to serial-form document is a function. But how can it be a function, given that the data model does not model insignficant white space? There are infinitely many serial-form XML documents equivalent to any given data model instance. Serialization will not be a function unless additional rules are specified. And in any case, when we set out to define a formal data model as is done in the XPath 1.0 spec, I think the usual idea is that we should define the data model in such a way as to make it possible to prove that every data-model instance corresponds to a class of XML documents treated as equivalent for XPath purposes, and that every XML document corresponds to a data model instance. If the rule really does appeal to the number of elements in the serial-form XML document, then it’s assuming, rather than establishing, the correspondence. It’s hard to believe that either Steve DeRose or James Clark could make that mistake.

    The second problem, on this reading of the rule, is that it’s hard to say whether a given data model instance obeys the rule, because it’s not clear that XML gives a determinate answer for the question.

    Some argue that XML documents are, by definition, strings that match the relevant production of the XML spec (on this see my post of 5 March 2008); by the same logic we can infer that an element is a string matching the element production.

    [Note: For what it's worth I don't think the XML spec explicitly identifies either documents or elements with strings; the argument that XML documents and elements are strings rests on the claim that they can't be anything else, or that making them anything else would make the spec inconsistent. As I noted in my blog post of 2008, there is at least one passage which seems to assume that documents are strings (it speaks of a document matching the document production), but I believe that passage is just a case of bad drafting.]

    If for discussion’s sake we accept this argument, then it seems we must ask ourselves: is the string consisting of the four characters U+003C, U+0062, U+002F, U+003E, in order, one string or three strings?

    The answer, as students of philosophy will have been shouting out at home for some moments now, is “yes”. If by character you mean ‘character type’, then one string (or string type). If on the other hand you mean ‘character token’, then for the document shown above, I think pretty clearly three strings (string tokens).

    So, on this first reading of the rule, check. Two distinct elements in the XML (counting string types), two in the data model instance. (To show that this rule excludes the model instance we’re discussing, it would be necessary to show that the serialized XML document has four elements, and that counting only two elements is inconsistent with the XML spec. Given how coy the XML spec is on the nature of XML documents, I don’t believe such a showing possible.)

    The second reading of the rule is that “document” does not mean, in this sentence, something different from the data model instance, but is just a way of referring to the entirety of the data model instance itself. A quick glance at the usage of the word “document” in the XPath 1.0 spec suggests that that is in fact its most common usage. In recent years, influenced perhaps by the work on the XPath 2.0 data model, with formalists of the caliber of Mary Fernández and Phil Wadler, many people have begun to think it natural to define an abstract model independently of the XML spec, and then (as I suggested above) establish in separate steps that there is a correspondence between the set of all XML documents viewed as character sequences and the set of all instances of the data model.

    The XPath 1.0 spec seems to take a slightly different tack, rhetorically. The definition of the data model begins

    XPath operates on an XML document as a tree. This section describes how XPath models an XML document as a tree.

    I take this as a suggestion that the data model instance operated on by XPath 1.0 can be thought of not as a thing separate from the XML document (whatever that is) but as a particular way of looking at and thinking about the XML document. I think it’s true that there was (historically speaking) no consensus among the XML community at that time that the term XML document referred to a string, as opposed to a tree. I think the idea would have met fierce resistance.

    On this reading, the rule quoted above is either a vacuous statement, or a statement about usage, establishing the correspondence (or equivalence) between the terms element and element node.

    So, on this second reading, check. Two elements, two element nodes. Same thing, really, element node and element.

As I say, I think it’s quite clear which answer the XPath 1.0 spec intends the question to have: plenty of places in the spec clearly rely on element nodes never having themselves as siblings, just as plenty of places rely on element nodes never having more than one parent. Both properties are a common-sensical interpretation of the element structure of XML. I believe the point of defining the data model explicitly is to eliminate, as far as possible, the need to appeal to common sense and “what everyone knows”, to get the required postulates down on paper so that any implementation which respects those postulates and obeys the constraints will conform and inter-operate. For the parent relation, the definition of the model makes the common-sense interpretation of XML explicit. But not (as far as I can see) for the sibling relation.

Perhaps the creators of the XPath 1.0 spec felt that no explicit statement about no elements being their own siblings was necessary, because it followed from other properties of the model as specified. If so, I think either I must have missed something, or (less likely, but still possible) they did. If the property is to hold for all instances of the model, and if it does not follow from the current definition of the model, then perhaps it needs to be stated explicitly as part of the definition of the model.

[When he reached the end of this post, my evil twin Enrique turned to me and asked “Who's Yossarian? Was he a member of the XSL Working Group?” “No, he was a character in Joseph Heller's novel Catch 22. The title of the post is a reference to an elaborate bit in chapter 18 of the novel.” “And by ‘elaborate,’” mused Enrique, “you mean —” “Exactly: that it's too long to quote here and still claim fair use. Besides, this isn't a commentary on Catch 22. Just search the Web (or the book) for the phrase ‘I see everything twice.’”]

An XPath 1.0 puzzle

Wednesday, January 20th, 2010

[20 January 2010]

Consider the XML document shown below, and in particular consider its representation in the XPath 1.0 data model.

  <a><b/><b/><b/></a>

How many element nodes are there in this document, regarded as an instance of the XPath 1.0 data model? I think it’s clear that, for purposes of XPath 1.0, the expected answer is four: one of type ‘a’ and three of type ‘b’, all children of the ‘a’ element.

I am finding it unexpectedly difficult to prove that conclusion formally on the basis of the definition of the data model given in the spec. I wonder if anyone else will have better luck.

Binary adder in ACL2 and Alloy

Monday, January 11th, 2010

[11 January 2010]

Not too long ago, I wrote about cross training in programming languages, and the pleasure of rewriting things from one language into another.

Recently I had another occasion to think about that. I’ve been doing some work lately with two systems which I think of as similar, though they have different goals and emphases. ACL2 (‘a computational logic for applicative Common Lisp’) is an industrial-strength theorem prover, with a history of use for proofs of correctness for chip designs, programming languages, and mathematical propositions like the fundamental theorem of calculus. It’s a lot like a high-performance car, both in its power and in the fact that it spends a lot of time in the shop. Er, uh, I mean, it requires close, intelligent attention from the user. And its learning curve looks a lot like the approach to Mesa Verde. Alloy, by contrast, is an instance of what its designer calls “light-weight formal methods”; the language is kept simple for analysability’s sake, and no theorem prover is provided: instead, exhaustive searches through all the models of a system up to a given size are made, to find counter-examples to an assertion. It’s got a learning curve, too, but in my experience it’s pretty manageable.

I’m interested in both ACL2 and Alloy because both seem to me to offer help in making designs and specifications correct, and keeping them that way when changes are made. It would be nice to have a better sense of when one tool is more appropriate to a problem, and when the other. One conjecture I’ve entertained: Alloy for initial playing around with a design, ACL2 for fuller proofs of correctness (when real proofs are desired) after the design has settled down a bit. Solving the same problem using both tools seems like an obvious way to test that conjecture and get a sense of how the two compare.

So in a spirit of exploration, I recently took an example from the ACL2 textbook* and experimented with making an Alloy model of the same thing, which I finished the other day and have now published on the Alloy community site. The example covers a binary adder constructed from simple sub-units which add single-bit numbers. (I found it enlightening to read the Wikipedia article on adders; if you’re not an electrical engineer, you may, too.)

* Matt Kaufmann, Panagiotis Manolios, and J Strother Moore, Computer-Aided Reasoning: An Approach ([Austin]: [n.p.], 2002), section 10.5.1.

The experience poses a bit of a challenge to the conjecture just mentioned: although ACL2 does require some help proving that the relevant function terminates and that it’s correct, in some ways the ACL2 description seems simpler than the Alloy description. Certainly it’s more compact. To ensure that models are analysable, Alloy forbids recursive functions; finding an Alloy equivalent to the recursive ACL2 specification of the adder took me some head-scratching, and the result uses a lot of machinery that feels kind of ad hoc to me. But in a way, the fact that a non-recursive formulation can be found also feels like a demonstration of Alloy’s expressive power. (Short version: recursion can be changed to iteration, right? So think about using sequences.)

A really good comparative sense of the two systems will require a lot more than one exercise of this kind; ideally, I’d like a whole series of ACL2-to-Alloy and Alloy-to-ACL2 translations. Currently, my Alloy seems to be up to translating at least some ACL2 exercises into Alloy; I am not certain my ACL2 skills are up to finding ACL2 equivalents for standard Alloy exercises. If you are interested in formal methods (and who else will still be reading at this point?), all I can say is: stay tuned. And if you do any cross-translation exercises of this kind, think about sharing them!