Re: [xml-dev] defining correctness for an XML transformation - how?

["C. M. Sperberg-McQueen" <cmsmcq@blackmesatech.com>]

Thank you, Liam.  Some responses interspersed.

"Liam R. E. Quin" <liam@fromoldbooks.org> writes:

> On Wed, 2024-07-03 at 07:40 -0600, C. M. Sperberg-McQueen wrote:
>> 
>> What language would one need in order to formulate plausible pre- and
>> post-conditions on XML transformations, or more generally on
>> functionsor procedures that operate on XDM instances?
>
> XSLT maybe.
>
> Unfortunately there are two difficult aspects here and i am not sure
> either has been (or can be?) solved.
>
> First, ensuring that a Turing-complete computation will terminate is of
> course the halting problem (unlike the problem of getting Bodin the Dog
> to stop pulling during walks, which is the Halter problem). Since a
> computation that does not terminate is (1) possible and (2) presumably
> not correct, i think we have to abandon the idea of a complete
> solution.

Quite true.  If it's true that I can't abandon that idea now, it's
because I abandoned it long ago.  In general, I believe it's true that
there are many programs which cannot be proven correct or incorrect,
just because they include constructs which defy (current capacities of)
analysis.

But the insolubility of the Halting Problem does not mean that no
programs can be proven to terminate (just as the Halter Problem does not
mean we don't go for walks with our dogs).

> ...

> I wrote that there are two difficult aspects; the second is that the
> notion of correctness can often be tied to domain-level interpretation
> - that is, to the relationship between the digital and the physical,
> the imaginary and the imaged.

True.  In some domains, of course, arithmetic can be used as a
substitute: we may not be able to express directly that the result of a
particular function should denote the force at a particular moment, but
we can say that it should be the product of variables m (mass) and a
(acceleration).  For lots of XML transformations, arithmetic doesn't get
us very far.

> To make it harder, our transformations
> operate in a world of speculation: we specify not what shall be but
> what might be:
>     <xsl:template match="chapter/section/glossary/title">
>
> So we cannot easily mark our input to say, There isn’t a glossary here,
> but there might have been. Nor can we easily identify the place in the
> output where a transformed glossary does not appear.

Here I think you're partly right and partly wrong.  A multiplication
routine in a machine's microcode must be prepared for large number of
multiplications it will never be asked to perform, just because it
*might* be asked to perform them.

Just as reasoning about correctness of imperative programs works both
with post-conditions and with pre-conditions (m and a had better be
numbers in the expected range), I think we can say that a stylesheet
with that template may or may not depend on the presence of at least one
glossary with a title -- schema-validity of the input is at least one
possible part of a pre-condition.

> If you can come up with anything better than Schematron, for any
> pragmatically useful definition of better :), i’m for sure very
> interested. “Validates against a target schema” is at least part-way,
> too.

Yes.  Sometimes I think our schema languages -- both the grammatical
components and the assertion components -- may be our current best
answer to my question.  I think, though, that we may need more, in the
general case, because as you say sometimes correctness involves
interpretation in a given domain.  An XSLT transformation that
translates an ixml grammar into an equivalent ixml grammar in a
restricted form (BNF) is correct if and only if L(G) = L(G').  To say
that meaningfully, I guess we may need the ability to define predicates
of our own.  If we use a version of XPath in which we can define
functions, I guess we have that.

> It’s too hot here today

My sympathies.  We were lucky and had a short rainstorm.  (And here, a
rainstorm normally helps relieve the heat, instead of just making
everything even muggier.)

Michael

-- 
C. M. Sperberg-McQueen
Black Mesa Technologies LLC
http://blackmesatech.com