Redundancy is an error?

Hi Folks,

I am learning the Alloy modelling language. It is so cool. One interesting aspect of Alloy is this rule:

An expression is erroneous if it can be shown
to be redundant, using types alone.

A common and simple case of redundancy is an expression that is equal to the empty relation (set). For example, if sets A and B are disjoint, then (A intersect B) is empty and therefore redundant (and therefore erroneous).

I am trying to see if any of the XML technologies have an equivalent rule.

It seems that XSD does not. Consider: the following schema says that an XML instance document can never have a <Foo> element:

<xs:element name="Book">
    <xs:complexType>
        <xs:sequence>
            <xs:element name="Title" type="xs:string"/>
            <xs:element name="Author" type="xs:string"/>
            <xs:element name="Date" type="xs:string"/>
            <xs:element name="Foo" minOccurs="0" maxOccurs="0" type="xs:string"/>
        </xs:sequence>
    </xs:complexType>
</xs:element>

The Foo element declaration is redundant – it declares an element that can never manifest in XML instances. Redundancy is not an error in XSD.

It also seems that redundancy is not an error in XSLT/XPath. Consider: the following XSLT has an XPath expression that can never be satisfied:

<xsl:template match="/">
    <xsl:choose>
        <xsl:when test="name(/*[position() eq 0]) eq 'foo'">foo</xsl:when>
        <xsl:when test="name(/*[position() eq 1]) eq 'bar'">bar</xsl:when>
        <xsl:when test="name(/*[position() eq 1]) eq 'blah'">blah</xsl:when>
    </xsl:choose>
</xsl:template>

In the vast universe of XML technologies, is there anywhere a rule that requires redundancy be treated as an error?

/Roger