- From: Dan Connolly <connolly@w3.org>
- Date: Thu, 07 Sep 2006 03:31:13 -0500
- To: www-tag@w3.org
The 26 July draft says:
[Definition: A language change is backwards compatible if newer
processors can process all instances of the old language. ]
-- http://www.w3.org/2001/tag/doc/versioning
http://www.w3.org/2001/tag/doc/versioning-20060726.html
which is OK as an intuitive gloss, but it makes no use
of all the terminology that is set up in the diagram.
I'm pretty sure that the term "backwards compatible"
can be completely defined in terms of intent, text, etc.
and a bit of logic. I worked out the details of an
example tonight.
The change from HTML 2 to HTML 4 is backward compatible,
right? Using the informal definition above: if I write
chap2.html in HTML 2, an HTML 4 user agent will grok just fine.
We can elaborate this formally, using the terms
in our UML diagram.
I have an Act_of_Production in HTML 2; let's call it _:act1,
and let's call the intent of that act of production ex:chap1in .
_:act1 a ev:Act_of_Production
ev:language ex:HTML2;
ev:text "<html>...</html>";
ev:intent ex:chap1in.
Now suppose you consume that same text in HTML 4:
_:act2 a Act_of_Consumption;
ev:language ex:HTML4;
ev:text "<html>...</html>" .
What we mean by backward compatible is that the impact
of _:act2 is the same as the intent of _:act1, i.e. ex:chap1in.
That's how we can express "newer processors can process all instances
of the old language" using the terms from the UML diagram.
The definitions of backward and forward compatible are inverses
of each other; we really only need to define one. TimBL
offered this definition a while ago:
one language is a sublanguage (or "profile") of a
second language if any text in the first language is also a
valid text in the second language and has the same
interpretation in the second language.
To say that HTML 4 is also forward-compatible with HTML 2,
we'd say that HTML 4 is a sublanguage of HTML 2. Now this
feels a little funny, but as we've discussed at a couple
TAG ftf meetings, the syntax of HTML 2 really does include
the syntax of HTML 4 by way of the "ignore tags you
don't understand" convention. It's not _quite_ correct,
because there may be some loss of fidelity/meaning when
an HTML 2 user agent deals with an HTML 4 document.
I haven't formalized that stuff yet. More on that
later, I hope. Meanwhile, back to the example where
I have all the details worked out.
The 26 July draft does have an "Act of Interpretation"
box, but I didn't use it; I'm pretty sure it's redundant
w.r.t. intent/impact (not in a harmful way; it's just
that the one can be defined in terms of the other; they're
not independent). I just used intent/impact. And I actually
only formalized a corollary of the above definition
of sublanguage; that is;
If the language of some act of production
is a sublanguage of some act of consumption,
and they have the same text, then the impact
of the consumption is the intent of the production.
In N3:
{
[] ev:text ?TXT; :language [ is :sublanguage of ?BIG ]; :intent ?I.
?COMM a ev:Act_of_Consumption;
ev:text ?TXT; :language ?BIG.
} => { ?COMM :impact ?I }.
That rule, combined with the cardinality constraints
in the UML diagram, converted to OWL, is enough to
justify the conclusion that
_:act2 ev:impact ex:chap1in .
Oh... I had to add one more rule that it's quite
expressible in OWL nor UML, but is what we talked
about when we built the diagram:
# A language and a text determine the intent/impact of a communication
{
?C1 ev:text ?D; :language ?L; :intent ?I.
?C2 ev:text ?D; :language ?L.
} => { ?C2 :intent ?I }.
The gory details are checked in under
http://www.w3.org/2001/tag/2006/ext-vers/
To produce the proof, I do...
~/w3ccvs/WWW/2001/tag/2006/ext-vers$ make ex-html24-pf.n3
python ../../../../2000/10/swap/cwm.py ex-html24.n3 ext-vers-rules.n3
--think \
--filter=ex-html24-goal.n3 --why >ex-html24-pf.n3
and if you run check.py on it, it checks the proof and
shows you the conclusion:
_:act2 :impact ex:chap1in;
:language ex:HTML4;
:text "<html>...</html>" .
As part of checking this stuff, I wrote some code for producing
a somewhat conventional/readable version of cwm's proofs.
a CE step is going from "A and B and ..." to just A (or just B...).
a GMP step is application of a rule. In some steps,
the formula is abbreviated as ... . Hm... now that I look
at this, I wonder about cwm's use of @forSome in proofs...
1: ...
[by parsing <ex-html24.n3>]
2: @forSome :_g2 . :_g2 a ev:Act_of_Consumption .
[by CE on 1]
3: @forSome :_g2 . :_g2 ev:text "<html>...</html>" .
[by CE on 1]
4: @forSome :_g2 . :_g2 ev:language ex:HTML4 .
[by CE on 1]
5: :HTML4 ev:sublanguage :HTML2 .
[by CE on 1]
6: @forSome :_g3 . :_g3 ev:intent ex:chap1in .
[by CE on 1]
7: @forSome :_g3 . :_g3 ev:text "<html>...</html>" .
[by CE on 1]
8: @forSome :_g3 . :_g3 ev:language ex:HTML2 .
[by CE on 1]
9: ...
[by parsing <ext-vers-rules.n3>]
10: @forAll :BIG, :COMM, :I, :TXT . { @forSome run:_g4 . [ ev:intent :I;
ev:language run:_g4; ev:text :TXT ]. :BIG ev:sublanguage run:_g4 . :COMM
a ev:Act_of_Consumption; ev:language :BIG; ev:text :TXT . } log:implies
{:COMM ev:impact :I . } .
[by CE on 9]
11: ...
[by GMP on 10, [2, 3, 4, 5, 6, 7, 8]]
12: @forSome :_g2 . :_g2 ev:impact ex:chap1in .
[by CE on 11]
13: @forSome :_g2 . :_g2 ev:text "<html>...</html>" .
[by CE on 1]
14: @forSome :_g2 . :_g2 ev:language ex:HTML4 .
[by CE on 1]
15: @forSome :_g2 . ex:chap2 ev:stateCommunication :_g2 .
[by CE on 1]
16: ...
[by parsing <ex-html24-goal.n3>]
17: @forAll e:C . { ex:chap2 :stateCommunication e:C . e:C :impact
ex:chap1in; :language ex:HTML4; :text "<html>...</html>" . } log:implies
{e:C :impact ex:chap1in; :language ex:HTML4; :text
"<html>...</html>" . } .
[by CE on 16]
18: run:_g2 :impact ex:chap1in; :language ex:HTML4; :text
"<html>...</html>" .
[by GMP on 17, [12, 13, 14, 15]]
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
D3C2 887B 0F92 6005 C541 0875 0F91 96DE 6E52 C29E
Received on Thursday, 7 September 2006 08:31:24 UTC