[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]
Subject: Re: [xacml-comment] Inconsistent definition for the any-of-all function
Thanks Steven, You are right. The Haskel and English language definitions do not appear to match. I think the English language version is the intended one. I am currently preparing a list of current known issues in the CS-01 and the TC will include this issue in the review. Best regards, Erik On 2011-01-25 01:10, Steven Legg wrote: > > 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 > > >
[Date Prev] | [Thread Prev] | [Thread Next] | [Date Next] -- [Date Index] | [Thread Index] | [List Home]