Re: [xml-dev] n-Queens Problem

[u123724 <u123724@gmail.com>]

Schematron is undoubtly useful, even though its undecidability prevent it
from being used for eg. static type checking of programs (eg. roughly,
checking if all successful executions of a program produce schema-valid
result markup, which was a somewhat hot topic in academia around 2002/2003,
and which seems a desirable property of a query/validation language to know).
Obviously, the language being used for the program and it's querying
and manipulation power play a role here.

A question that may be worth answering is whether there exist decidable
Schematron fragments eg. if Schematron can be made decidable when
restricted to XPath subsets (like eg. XML Schema, which restricts predicates
for unique and key constraints to only basic XPath constructs, but which is
unfortunately still undecidable).

I haven't checked lately, but is there a formal characterization of Schematron's
power vs. grammar-based schema formalisms? Supposedly, this comes down
to the question of whether XPath expressions can encode Glushkov and/or other
automata constructions (or rather, if in general the minimal length of an XPath
expression encoding a regular expression check is bounded by a polynomial
rather than general exponential function in terms of the input regular
expression size).

On Mon, Apr 3, 2017 at 8:40 AM, Rick Jelliffe <rjelliffe@allette.com.au> wrote:
> I think what has not been demonstrated is that undecidability is an
> important property for a pragmatic schema language.
>
> In fact, since we know that Schematron is useful and more powerful than the
> other schema languages, why isn't that (non-mathematical) proof that
> undecidability (if using some particular constructs) is actually not an
> important property?
>
> Regards,
> Rick
>
>
> On 3 Apr 2017 00:02, "u123724" <u123724@gmail.com> wrote:
>>
>> A solution to the N-queens problem in XSLT was discussed on this
>> mailing list as early as 1999 ("Can solve the N-queens - but can't count!"
>> cf. https://www.oxygenxml.com/archives/xsl-list/199906/msg00289.html)
>> in the context of XSLT language design.
>>
>> Now and then, the question for document query and validation languages
>> was to strike a balance between decidability, complexity (Big-O)
>> and power. Traditionally, it was consensus that schema languages
>> shouldn't be undecidable. That is, the problem to determine if there is a
>> document that satisfies all the constraints the validation language
>> can express should be solvable, and moreover should be solvable in
>> time and space bounded by a polynomial in terms of the input problem's
>> eg. symbol length.
>>
>> So while being able to check the N-queens constraints is nice, it hints at
>> the fact that Schematron is leaning on the "too powerful to be useful"
>> side
>> of things as a validation language. But note that already XML Schema is
>> undecidable because of eg. interaction with identity constraints and
>> occurence indicators if I recall correctly; http://www.unidex.com/scp/
>> links to these results and also contains a proof of Schematron
>> undecidablity. Notably, only DTDs (and possibly Relax NG) are considered
>> decidable according to it.
>>
>> On Sun, Apr 2, 2017 at 3:12 PM, Costello, Roger L. <costello@mitre.org>
>> wrote:
>> > David Carlisle wrote a very cool:
>> >
>> >
>> >
>> > … solution that works for
>> >     any size chessboard …
>> >
>> >
>> >
>> > Thank you David!
>> >
>> >
>> >
>> > Here is how David models the chessboard:
>> >
>> >
>> >
>> > <n-queens>
>> >     <queen column="1" row="3"/>
>> >     <queen column="2" row="1"/>
>> >     <queen column="3" row="4"/>
>> >     <queen column="4" row="2"/>
>> > </n-queens>
>> >
>> >
>> >
>> > And here is his (mind-blowing) Schematron schema:
>> >
>> >
>> >
>> > <sch:schema xmlns:sch="http://purl.oclc.org/dsdl/schematron";
>> >                       queryBinding="xslt2">
>> >
>> >     <sch:pattern id="n-Queens-Problem">
>> >
>> >         <sch:rule context="n-queens">
>> >             <sch:assert test="every $c in 1 to count(queen) satisfies
>> > exists(queen[@column=$c])">
>> >                 There cannot be two queens in the same column.
>> >             </sch:assert>
>> >             <sch:assert test="every $r in 1 to count(queen) satisfies
>> > exists(queen[@row=$r])">
>> >                 There cannot be two queens on the same row.
>> >             </sch:assert>
>> >             <sch:assert
>> > test="count(queen)=count(distinct-values(queen/(number(@row) -
>> > number(@column))))">
>> >                 There cannot be two queens on a (falling) diagonal.
>> >             </sch:assert>
>> >             <sch:assert
>> > test="count(queen)=count(distinct-values(queen/(number(@row) +
>> > number(@column))))">
>> >                 There cannot be two queens on a (rising) diagonal.
>> >             </sch:assert>
>> >         </sch:rule>
>> >     </sch:pattern>
>> >
>> > </sch:schema>
>> >
>> >
>>
>> _______________________________________________________________________
>>
>> 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: xml-dev-unsubscribe@lists.xml.org
>> subscribe: xml-dev-subscribe@lists.xml.org
>> List archive: http://lists.xml.org/archives/xml-dev/
>> List Guidelines: http://www.oasis-open.org/maillists/guidelines.php