Re: defining correctness for an XML transformation - how?
Hans-Juergen Rennau <[email protected]> Wed, 3 Jul 2024 20:45:00 +0000 (UTC)
| Newsgroups | gmane.text.xml.devel |
|---|---|
| Message-ID | <[email protected]> |
------=_Part_1586042_1783233005.1720039500697
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Yes and no, I think. First, API integration is a huge topic and a major pa=
rt of it is really the translation of information itself - not enhancement;=
second, if the ambition is limited to a partial validation, a contribution=
to validation, then you can regard any results concerning the semantic ali=
gnment as valuable pieces of information to be assembled. It is somewhat li=
ke logical chemistry: A is mapped to its semantic content A', B is mapped t=
o B', then A' and B' are poured into one pot and we can measure what happen=
s. An important aspect is the independence of the A to A' and B to B' mappi=
ngs, as they are usable in combination with any C, D, ... for which a corre=
sponding alignment has been defined.
Am Mittwoch, 3. Juli 2024 um 20:22:03 MESZ hat Michael Kay <mike@saxoni=
ca.com> Folgendes geschrieben: =20
=20
>The correctness of the transformation can then be assessed by comparing t=
he information content of source and target.=C2=A0
Only for transformations that aren't designed to remove any information or =
add any information. Those must surely be in a minority.
Michael KaySaxonica
On 3 Jul 2024, at 19:13, Hans-Juergen Rennau <[email protected]> wrote:
A most interesting question. My thoughts tend in a direction different fro=
m pre- and post-conditions. The focus should be on the comparison of struct=
ured information. As you are speaking of "translation from one format to an=
other", I consider information content as a possible yardstick. Imagine sou=
rce and target formats can be mapped to their semantic information content =
- expressed e.g. by RDF or some other representation as recently presented =
at xmlprague 2024 [1]. The correctness of the transformation can then be as=
sessed by comparing the information content of source and target. I think t=
he possibility of mapping tree-structured information (XML, JSON, ...) to t=
ree-independent information content does not receive the interest which it =
deserves.
Kind regards,Hans-J=C3=BCrgen
[1] Kottmann,=C2=A0Renzo; Cedric Pauken;=C2=A0 Andreas=C2=A0Schmitz:=C2=A0S=
imple Semantic Data Modeling in XML (SeMoX), xmlprague 2024https://archive.=
xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf=C2=A0, p. 231 f
Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M. Sperberg-McQueen <=
[email protected]> Folgendes geschrieben: =20
=20
Roger Costello's recent question about how to show the correctness of a
translation from one XML format to another very similar one suggests a
related question.=C2=A0 Forget *showing* that an XML transformation is
correct -- how would you define correctness formally, if you wanted to
be able in principle to provide a machine-checkable proof of
correctness?
For imperative languages, one way is to define a pre-condition which the
caller of a program or function must guarantee, and a post-condition
which describes what the program or function will achieve.=C2=A0 Written in=
a
Hoare triple, pre-condition P, post-condition Q, and code S can be
depicted as {P}S{Q}.
But the logical world illustrated by typical descriptions of Hoare
triples feels remarkably simple -- atomic values assigned to variables.
What language would one need in order to formulate plausible pre- and
post-conditions on XML transformations, or more generally on functions
or procedures that operate on XDM instances?
Asking for a friend.
--=20
C. M. Sperberg-McQueen
Black Mesa Technologies LLC
http://blackmesatech.com
_______________________________________________________________________
XML-DEV is a publicly archived, unmoderated list hosted by OASIS
to support XML implementation and development. To minimize
spam in the archives, you must subscribe before posting.
[Un]Subscribe/change address: http://www.oasis-open.org/mlmanage/
Or unsubscribe: [email protected]
subscribe: [email protected]
List archive: http://lists.xml.org/archives/xml-dev/
List Guidelines: http://www.oasis-open.org/maillists/guidelines.php
=20
=20
------=_Part_1586042_1783233005.1720039500697
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
<html><head></head><body><div class=3D"ydpf609ccc3yahoo-style-wrap" style=
=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;font-size:13px=
;"><div></div>
<div dir=3D"ltr" data-setdir=3D"false">Yes and no, I think. First, =
API integration is a huge topic and a major part of it is really the transl=
ation of information itself - not enhancement; second, if the ambition is l=
imited to a partial validation, a contribution to validation, then you can =
regard any results concerning the semantic alignment as valuable pieces of =
information to be assembled. It is somewhat like logical chemistry: A is ma=
pped to its semantic content A', B is mapped to B', then A' and B' are pour=
ed into one pot and we can measure what happens. An important aspect is the=
independence of the A to A' and B to B' mappings, as they are usable in co=
mbination with any C, D, ... for which a corresponding alignment has been d=
efined.</div><div><br></div>
=20
</div><div id=3D"yahoo_quoted_0482204425" class=3D"yahoo_quoted">
<div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
=20
<div>
Am Mittwoch, 3. Juli 2024 um 20:22:03 MESZ hat Mich=
ael Kay <[email protected]> Folgendes geschrieben:
</div>
<div><br></div>
<div><br></div>
=20
=20
<div><div id=3D"yiv9600196079"><div>><span style=3D"font=
-family:Helvetica, Arial, sans-serif;">The correctness of the transformatio=
n can then be assessed by comparing the information content of source and t=
arget. </span><div><font face=3D"Helvetica Neue, Helvetica, Arial, san=
s-serif"><br clear=3D"none"></font></div><div><font face=3D"Helvetica Neue,=
Helvetica, Arial, sans-serif">Only for transformations that aren't designe=
d to remove any information or add any information. Those must surely be in=
a minority.</font></div><div><font face=3D"Helvetica Neue, Helvetica, Aria=
l, sans-serif"><br clear=3D"none"></font></div><div><font face=3D"Helvetica=
Neue, Helvetica, Arial, sans-serif">Michael Kay</font></div><div><font fac=
e=3D"Helvetica Neue, Helvetica, Arial, sans-serif">Saxonica<br clear=3D"non=
e" id=3D"yiv9600196079lineBreakAtBeginningOfMessage"></font><div id=3D"yiv9=
600196079yqt34232" class=3D"yiv9600196079yqt1799670175"><div><br clear=3D"n=
one"><blockquote type=3D"cite"><div>On 3 Jul 2024, at 19:13, Hans-Juergen R=
ennau <[email protected]> wrote:</div><br clear=3D"none" class=3D"yiv9=
600196079Apple-interchange-newline"><div><div><div style=3D"font-family:Hel=
vetica Neue, Helvetica, Arial, sans-serif;font-size:13px;" class=3D"yiv9600=
196079ydp36b3e5cayahoo-style-wrap"><div></div>
<div dir=3D"ltr"><div><div dir=3D"ltr" style=3D"font-family:Helveti=
ca Neue, Helvetica, Arial, sans-serif;">A most interesting question. My tho=
ughts tend in a direction different from pre- and post-conditions. The focu=
s should be on the comparison of structured information. As you are speakin=
g of "translation from one format to another", I consider information conte=
nt as a possible yardstick. Imagine source and target formats can be mapped=
to their semantic information content - expressed e.g. by RDF or some othe=
r representation as recently presented at xmlprague 2024 [1]. The correctne=
ss of the transformation can then be assessed by comparing the information =
content of source and target. I think the possibility of mapping tree-struc=
tured information (XML, JSON, ...) to tree-independent information content =
does not receive the interest which it deserves.</div><div dir=3D"ltr" styl=
e=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;"><br clear=
=3D"none"></div><div dir=3D"ltr" style=3D"font-family:Helvetica Neue, Helve=
tica, Arial, sans-serif;">Kind regards,</div><div dir=3D"ltr" style=3D"font=
-family:Helvetica Neue, Helvetica, Arial, sans-serif;">Hans-J=C3=BCrgen</di=
v><div dir=3D"ltr" style=3D"font-family:Helvetica Neue, Helvetica, Arial, s=
ans-serif;"><br clear=3D"none"></div><div dir=3D"ltr" style=3D"font-family:=
Helvetica Neue, Helvetica, Arial, sans-serif;">[1] Kottmann, Renzo; Ce=
dric Pauken; Andreas <span style=3D"">Schmitz: </span>Simpl=
e Semantic Data Modeling in XML (SeMoX), xmlprague 2024</div><div dir=3D"lt=
r" style=3D"font-family:Helvetica Neue, Helvetica, Arial, sans-serif;"><a r=
el=3D"nofollow noopener noreferrer" shape=3D"rect" target=3D"_blank" href=
=3D"https://archive.xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf"=
style=3D"color:rgb(25, 106, 212);text-decoration-line:underline;">https://=
archive.xmlprague.cz/2024/files/xmlprague-2024-proceedings.pdf</a> , p=
. 231 f</div></div><br clear=3D"none"></div><div><br clear=3D"none"></div>
=20
</div><div id=3D"yiv9600196079ydp173f1a58yahoo_quoted_0923868499" c=
lass=3D"yiv9600196079ydp173f1a58yahoo_quoted">
<div style=3D"font-family:'Helvetica Neue', Helvetica, Arial, s=
ans-serif;font-size:13px;color:#26282a;">
=20
<div>
Am Mittwoch, 3. Juli 2024 um 15:47:59 MESZ hat C. M=
. Sperberg-McQueen <[email protected]> Folgendes geschrieben:
</div>
<div><br clear=3D"none"></div>
<div><br clear=3D"none"></div>
=20
=20
<div><div dir=3D"ltr">Roger Costello's recent question abou=
t how to show the correctness of a<br clear=3D"none"></div><div dir=3D"ltr"=
>translation from one XML format to another very similar one suggests a<br =
clear=3D"none"></div><div dir=3D"ltr">related question. Forget *showi=
ng* that an XML transformation is<br clear=3D"none"></div><div dir=3D"ltr">=
correct -- how would you define correctness formally, if you wanted to<br c=
lear=3D"none"></div><div dir=3D"ltr">be able in principle to provide a mach=
ine-checkable proof of<br clear=3D"none"></div><div dir=3D"ltr">correctness=
?<br clear=3D"none"></div><div dir=3D"ltr"><br clear=3D"none"></div><div di=
r=3D"ltr">For imperative languages, one way is to define a pre-condition wh=
ich the<br clear=3D"none"></div><div dir=3D"ltr">caller of a program or fun=
ction must guarantee, and a post-condition<br clear=3D"none"></div><div dir=
=3D"ltr">which describes what the program or function will achieve. W=
ritten in a<br clear=3D"none"></div><div dir=3D"ltr">Hoare triple, pre-cond=
ition P, post-condition Q, and code S can be<br clear=3D"none"></div><div d=
ir=3D"ltr">depicted as {P}S{Q}.<br clear=3D"none"></div><div dir=3D"ltr"><b=
r clear=3D"none"></div><div dir=3D"ltr">But the logical world illustrated b=
y typical descriptions of Hoare<br clear=3D"none"></div><div dir=3D"ltr">tr=
iples feels remarkably simple -- atomic values assigned to variables.<br cl=
ear=3D"none"></div><div dir=3D"ltr"><br clear=3D"none"></div><div dir=3D"lt=
r">What language would one need in order to formulate plausible pre- and<br=
clear=3D"none"></div><div dir=3D"ltr">post-conditions on XML transformatio=
ns, or more generally on functions<br clear=3D"none"></div><div dir=3D"ltr"=
>or procedures that operate on XDM instances?<br clear=3D"none"></div><div =
dir=3D"ltr"><br clear=3D"none"></div><div dir=3D"ltr">Asking for a friend.<=
br clear=3D"none"></div><div dir=3D"ltr"><br clear=3D"none"></div><div dir=
=3D"ltr">-- <br clear=3D"none"></div><div dir=3D"ltr">C. M. Sperberg-McQuee=
n<br clear=3D"none"></div><div dir=3D"ltr">Black Mesa Technologies LLC<br c=
lear=3D"none"></div><div dir=3D"ltr"><a rel=3D"nofollow noopener noreferrer=
" shape=3D"rect" target=3D"_blank" href=3D"http://blackmesatech.com/">http:=
//blackmesatech.com</a><br clear=3D"none"></div><div dir=3D"ltr"><br clear=
=3D"none"></div><div dir=3D"ltr">__________________________________________=
_____________________________<br clear=3D"none"></div><div dir=3D"ltr"><br =
clear=3D"none"></div><div dir=3D"ltr">XML-DEV is a publicly archived, unmod=
erated list hosted by OASIS<br clear=3D"none"></div><div dir=3D"ltr">to sup=
port XML implementation and development. To minimize<br clear=3D"none"></di=
v><div dir=3D"ltr">spam in the archives, you must subscribe before posting.=
<br clear=3D"none"></div><div dir=3D"ltr"><br clear=3D"none"></div><div dir=
=3D"ltr">[Un]Subscribe/change address: <a rel=3D"nofollow noopener noreferr=
er" shape=3D"rect" target=3D"_blank" href=3D"http://www.oasis-open.org/mlma=
nage/">http://www.oasis-open.org/mlmanage/</a><br clear=3D"none"></div><div=
dir=3D"ltr">Or unsubscribe: <a rel=3D"nofollow noopener noreferrer" shape=
=3D"rect" ymailto=3D"mailto:[email protected]" target=3D"_b=
lank" href=3D"mailto:[email protected]">xml-dev-unsubscribe=
@lists.xml.org</a><br clear=3D"none"></div><div dir=3D"ltr">subscribe: <a r=
el=3D"nofollow noopener noreferrer" shape=3D"rect" ymailto=3D"mailto:xml-de=
[email protected]" target=3D"_blank" href=3D"mailto:xml-dev-subscri=
[email protected]">[email protected]</a><br clear=3D"none"></d=
iv><div dir=3D"ltr">List archive: <a rel=3D"nofollow noopener noreferrer" s=
hape=3D"rect" target=3D"_blank" href=3D"http://lists.xml.org/archives/xml-d=
ev/">http://lists.xml.org/archives/xml-dev/</a><br clear=3D"none"></div><di=
v dir=3D"ltr">List Guidelines: <a rel=3D"nofollow noopener noreferrer" shap=
e=3D"rect" target=3D"_blank" href=3D"http://www.oasis-open.org/maillists/gu=
idelines.php">http://www.oasis-open.org/maillists/guidelines.php</a><br cle=
ar=3D"none"></div><div dir=3D"ltr"><br clear=3D"none"></div></div>
</div>
</div></div></div></blockquote></div></div><br clear=3D"none"></div=
></div></div></div>
</div>
</div></body></html>
------=_Part_1586042_1783233005.1720039500697--