Inconsistent definition for the any-of-all function

[Steven Legg <steven.legg@enitiatives.com.au>]

In appendix A.3.12 of the XACML 3 core specification (Higher-order bag
functions), the English description of the any-of-all function is not
consistent with the Haskell formal definition.

The English description is (including the typo at the beginning of the first
URN):

     The expression SHALL be evaluated as if the
     "rn:oasis:names:tc:xacml:1.0:function:any-of" function had been applied to
     each value of the second bag and the whole of the first bag using the
     supplied xacml:Function, and the results were then combined using
     "urn:oasis:names:tc:xacml:1.0:function:and".

This suggests a corresponding Haskell definition such as:

     any_of_all f xs [] = True
     any_of_all f xs (y:ys) = (any_of f xs y) && (any_of_all f xs ys)

The formal Haskell definition for the any-of-all function is actually:

     any_of_all f [] ys = False
     any_of_all f (x:xs) ys = (all_of f x ys) || (any_of_all f xs ys)

These two Haskell definitions are not equivalent! Note that if the second
definition evaluates to true, then the first definition must also evaluate to
true, but the reverse case does not hold.

Either the English description or the Haskell definition must be changed for
the sake of consistency (the example happens to work either way though it is
described in terms of the English description), but there is a deeper issue
here. Both interpretations are perfectly reasonable to have as higher-order bag
functions. In fact, there are four reasonable combinations of any-of and all-of
for a higher-order bag function of two bag arguments:

(1) x_of_x f [] ys = True
     x_of_x f (x:xs) ys = (any_of f x ys) && (x_of_x f xs ys)

(2) x_of_x f xs [] = False
     x_of_x f xs (y:ys) = (all_of f xs y) || (x_of_x f xs ys)

(3) x_of_x f xs [] = True
     x_of_x f xs (y:ys) = (any_of f xs y) && (x_of_x f xs ys)

(4) x_of_x f [] ys = False
     x_of_x f (x:xs) ys = (all_of f x ys) || (x_of_x f xs ys)

Definition (1) corresponds to the current all-of-any function, the any-of-all
function is confused between (3) and (4), and definition (2) is not supported
at all. It seems to me that there are only two functions where there ought to
be four. I don't have any great ideas on what they should be called - perhaps:

     (1) all-of-any
     (2) reverse-any-of-all
     (3) reverse-all-of-any
     (4) any-of-all

I will detail an alternative to defining the missing functions in a separate
email.

Separately, the Haskell definitions for the all-of-any and any-of-all functions
refer to the Haskell definitions of any_of and all_of, but these haven't been
defined.

Regards,
Steven