An approach for studying relations between properties of functions on ordered sets is proposed. The approach is based on Attribute Exploration. 16 properties of functions are considered, among them monotonicity, idempotency, path independence, exchange properties, convexity, etc. Example functions are partially automatically generated on the powersets of sets with 2, 3 and 4 elements. The protocol of Attribute Exploration, which is run on examples of functions as objects and 16 function properties as attributes, is considered. The current Duquenne-Guigues implication base is presented. The list of proved implications is presented and discussed.
Many authors have investigated interrelations between properties of functions. For example, in [AM81], [AA95] this issue was studied within choice theory, in [Bir67], [GW96] the authors considered properties of functions in the lattice theory and formal concept analysis, in [Kos99], [MR00] problems about relations between properties arise when considering connection between choice and lattice theories. In this work we propose a clear and easy way for generating statements about properties of functions. For this purpose we use the method called "Attribute exploration" described in [GW96]; an application of this method to boolean algebras and lattices can be found in works [KPR06] and [Dau00].
The result of applying the method is a set of rules which should further be proved or rejected theoretically. If all the rules are either proved or rejected, we will have the complete set of all possible implications between sets of properties under investigation. For making easier the proofs or rejections of implications from the Duquenne-Guigues base, we compute minimal generators of their premises.
The paper is organized as follows. In section 2 we recall some important properties of functions, de nitions of implication, their bases, introduce Attribute Exploration. A modi cation of implication bases is proposed in 2.1. In subsection 2.2 we present and discuss the main results. The list of proved implications is given in subsection 2.3.
A
f 2(A) = f (A) f (A) A A f (A) A B ) f (A) f (B) A B ) f (B) f (A) f (B) A B ) f (B) = f (A) A B ) f (B) \ A f (A) f (A) \ f (B) f (A [ B)
(f (B) = ; ) f (A) = ;; B )
Let S be a nite set. A function f on 2S is a map from 2S to 2S (f : 2S ! 2S), where 2S is the set of all subsets of S (so-called powerset of S).
Denote by f g the composition of two functions f and g on set 2S, f g(A) = f (g(A)). If f = g, then instead of f g, one usually writes f 2.
De nition 1 ([AA95], [AM81], [Sen71], [Kos99], [Mou85], [Plo73]). Let f be a function on 2S (f : 2S ! 2S). Consider the following properties for arbitrary A; B; C S; x; y 2 S; x 6= y, f (B) \ A 6= ; ) f (A) = f (B) \ A IT Intransigence A B ) f (A) = f (B) \ A EX Exchange property x; y 2= f (A), y 2 f (A [ fxg) ) x 2 f (A [ fyg) AEX Anti-exchange property x; y 2= f (A), y 2 f (A [ fxg) ) x 2= f (A [ fyg) IAEX Inverse anti-exchange x; y 2 f (A), y 2= f (A x) ) x 2 f (A y) property
[f (A) = f (B) and A C f (A [ B) = f (f (A) [ f (B)) f (A) = f (B) ) f (A [ C) = f (B [ C)
B] ) f (A) = f (C)
In the work [Plo73] property PI was de ned as: f (A [ B) = f (f (A) [ B), but in this work we follow [MR00].
Remark 1. Authors do not claim this list of properties is complete. One can easily nd properties not included in this list. Authors have chosen the properties that they nd most useful and studied by many authors.
Let G, M be sets. Let I G M - be a binary relation between G and M . Triple K := (G; M; I) is called a (formal) context. Set G is called a set of objects, set M - a set of attributes.
Consider mappings ' : 2G ! 2M and : 2M ! 2G: '(A) := fm 2 M j gIm for all g 2 Ag; (B) := fg 2 G j gIm for all m 2 Bg: Any A1; A2 G, B1; B2 M satisfy:
Mappings ' and de ne Galois connection between (2G; ) and (2M ; ). Usually, instead of ' and a single notation ( )0 is used.
(Formal) concept is a pair (A; B): A G; B M; A0 = B and B0 = A: Concepts are partially ordered by relation (A1; B1) (A2; B2) () A1 A2 (B2 B1).
Implication A ! B, where A; B M takes place if A0 B0, i.e. every object, that has all the attributes from A, also has all the attributes from B. Implications satisfy Armstrong rules :
; X ! Y ; X ! Y; Y [ Z ! W
X ! X X [ Z ! Y X [ Z ! W
Implication base is a set of implications, from which using Armstrong rules any correct implication for a given context can be deduced and none of the subsets of this set of implications is an implication base.
A minimal in the size implication base was de ned in [GD86] and is known as Duquenne-Guigues implication base. In paper [Gan84] the premises of implications from the minimal base were characterized in terms of pseudo-intents. A subset of attributes P M is called pseudo-intent, if P 6= P 00 and for every such pseudo-intent Q such that Q P , one has Q00 P . Duquenne-Guigues implication base looks then as follows: fP ! (P 00 n P ) j P - pseudo-intentg. 2.1
Proposition 1. Let G be a Duquenne-Guigues implication base for a context K that contains an implication H ! H00 n H. If X H and X00 = H00 then an implications set G0, constructed from G by substitution implication X ! H00 n H for implication H ! H00 n H, is a minimal implications base for the context K. Proof. 1. Implication X ! H00 is correct in context K. Indeed, X0 =
X000 = H000. 2. G0 is an implications base. Indeed, as X H then (using second Arm
X!Y ) from X ! H00 can be deduced H ! H00 and, consesqtureonntglyr,ufrleomX[GZ0!cYan be deduced any implication, that can be deduced from G. Moreover, as shown above implication X ! H00 is correct in the context K, so there doesn't appear any implication that can be deduced from G0 but cannot be deduced from G. 3. Implication base G0 is minimal in the number of implications. Indeed, the size of G0 is equal to the size of the Duquenne-Guigues base G which is minimal in the number of implications.
As proved in proposition 1 the implication base can be changed, namely the premises of the implications can be reduced. It is worth saying that conditions X H and X00 = H00 may be satis ed by di erent subsets of the set of attributes M . Hence, there may be a certain level of freedom in choosing the exact form of an implication base with reduced premises.
If an implication with reduced premise is proved, then, obviously, a proof is correct for an implication with a bigger premise as well. If a counter-example has been found, then it changes both bases; indeed, any implications base de nes the whole set of correct implications, so the changes in the set of correct implications result in changes in the implication base.
Hence, one may change the form of the base depending on personal needs. Studying relations between function properties, it is of course easier to prove implications with reduced premises and to nd counter-examples for implications with reduced premises.
The pseudocode of the programme we used for nding minimal premises looks as follows (we already had Duquenne-Guigues base computed): consider implication a ! b, 1. i := 1; x := ; 2. while q(x ! 3. x := next(x; i) 4. return x
a00) do next(x; i) = (y; if y is lexicographically next element of 2a of size i;
next(x; i + 1); if y is not de ned. 2.2
In this work we study Duquenne-Guigues implication bases for contexts, where objects are example functions, attributes are properties of functions (de nition 1) and a binary relation indicates whether a function has or does not have a property. Example functions were generated on sets M2 = 2f0;1g, M3 = 2f0;1;2g and M4 = 2f0;1;2;3g, where 0; 1; 2; 3 are incomparable elements.
Functions f : Mi ! Mi can be represented as Mi-tuples of outputs, if we make an agreement about the input tuple. As sets Mi can be lexicographically ordered, Mi-tuples can be also lexicographically ordered. For each set M3 and M4, due to resource constraints we have taken rst 100000 lexicographically ordered Mi-tuples and, rst ordered the input tuple lexicographically and obtained rst 100000 functions, then reversed the input tuple and obtained another 100000 functions. On set M2 all the functions were generated. Functions generated on M4 did not add new implications to the implication base generated for M2 and M3.
The context of functions on M2 after row reducing is shown in Table 2. The context of functions on both sets M2 and M3 after row reduction is shown in Table 1. The functions in the tables are numbered, the properties are written on the top of every column (for de nitions see de nition 1). Row reduction was performed for both contexts.
Implications that we obtain are rules of the form "if a function has a set of properties A, then it also has a set of properties B", where A; B M; A\B = ;.
Though the Duquenne-Guigues base is minimal in the number of implications, it is not guaranteed that the premises of implications are minimal. However, as shown in proposition 1, the premises of implications in the base may be made smaller. Below the bases with reduced premises for contexts in Table 1 and Table 2 are presented.
The Duquene-Guigues base with reduced premises for context of functions on sets M2 and M3 (Table 1):
The Duquene-Guigues base with reduced premises for context of functions on set M2 (Table 2): 1. H ! IAEX 2. CG ! CV 3. M ! C, CV 4. AT ! H, EX, IAEX, AEX, CV 5. INT ! AEX, C(+) 6. INT, EX ! H, ID, IAEX 7. H, INT ! EX, ID 8. AT, C ! CG 9. (-EX, AEX) (-EX, CV) ! C 10. INT, ! ID, CV 11. , AEX, CG ! IAEX, (-C) 12. CS ! H, IAEX, AEX, C, 13. PI ! ID, IAEX, CG, C, CV, 14. EXT ! H, IAEX, C(+), 15. IT ! H, EX, CS, ID, IAEX, PI, CG, M, AEX, C, INT, CV, 16. ID, CV ! , C(+) 17. INT, CG ! H, EX, CS, ID, IAEX, PI, (-C) 18. M, EX ! 19. H, M ! , CG(+) 20. EXT, CS ! EX, ID 21. INT, H, ! CS, PI, CG 22. ID, CG ! IAEX, PI (-C) 23. M, AEX, EX ! IAEX 24. PI, EX ! H 25. PI, EXT ! M 26. M, CS ! ID, PI(+) 27. M, AT ! ID, PI 28. AT, EXT ! ID, PI, M 29. PI, AT ! M 30. INT, M, PI ! IT 31. M, EXT, CS ! IT, INT 32. ID, EX (-AEX) ! IAEX, C(+) 33. AT, CG ! C(*) 34. M, INT, CG ! IAEX(*) 35. AEX, EX, CG ! IAEX(*)
The implications that are not in the base for context of functions on M2 and M3 ( rst list in this subsection) are marked with "(*)". The properties that are present in some implication in the base of functions on M2, but are absent in corresponding implication in the base for context of functions on M2 and M3 are marked with "(+)". Finally, "(-)" marks the properties that are absent in some implication in the base of functions on M2, but are present in corresponding implication in the base for context of functions on M2 and M3.
Implication 9 has two corresponding implications in the base of functions on M2 and M3 ( rst list in this subsection): implication 10 and implication 13.
The list of implications that are present in the base for the context of functions on M2 and M3 (Table 1), but are absent in the base for the context of functions on M2 (Table 2): 1. H, ID, , AEX ! C 2. H, ID, CV ! C 3. ID, M, EX ! IAEX 4. M, EXT ! CG 5. H, M, EX ! CG
As the context of functions on M2 and M3 (Table 1) is an extension of context of functions on M2 (Table 2) in some sense, then the above implications list should be possible to derive from the base on M2. Indeed, the implication "H, ID, , AEX ! C" can be derived from the implication " ! C" (implication 9). Implication "H, ID, CV ! C" can be derived from implication "ID, CV ! , C" (implication 16). Implication "ID, M, EX ! IAEX" can be derived from implication "ID, EX ! IAEX, C" (implication 32). Implication "M, EXT ! CG" can be derived from implication "EXT ! H, IAEX, C, " (implication 14) and implication "H, M ! , CG" (implication 19). Finally, implication "H, M, EX ! CG" can be derived from implication "H, M ! , CG" (implication 19).
Now we prove a proposition that helps to explain the di erence between bases.
Proposition 2. If function f on M2 has a property it also has a property C. Proof. First we recall the properties:
Concordance (C): f (A) \ f (B) Let us consider all possible cases:
B ) f (B) = f (A) f (A [ B) 1. A B: then f (A [ B) = f (B), property C is satis ed. 2. A is incomparable with B: then let A = f0g and B = f1g. f (A [ B) = f (f0; 1g); A; B f0; 1g, (a) f (f0; 1g) = f0; 1g, property C is satis ed. (b) f (f0; 1g) f0; 1g ) f (f0; 1g) A f0; 1g (A is taken for certainty, but if the condition is satis ed for B, then in every expression below we should substitute B for A), considering property O: f (A) = f (f0; 1g) ) f (A) \ f (B) f (f0; 1g) = f (A [ B), which was to be proved.
The proved proposition accounts for the changes in implications 9, 5, 11, 14, 16, 19, 22, 32 in the base for the context of functions on M2. The proved proposition is only correct for the functions on M2, there are counter-examples for functions on M3 (see Table 1 26th function). Function H EX CS ID IAEX PI CG EXT M IT AEX C AT INT CV O 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 50 18 19 20 51 21 52 22 23 24 25
X X X X X X X X X
X X X X X X X
X
X X X
X X X X X X X X
X X X X X X X X X X X X X
X X X X X X X
X
X X X
X X X X X X X X
X X X X X X X X X X X X X X X X X
X X X X X X X X X X X X
X
X X X
X
X X X
X X X X
X X X
X X X X
X X X X
X X X
X X X X X X X X X X X X X X X X X X X X
X X X X X X X X X X X X X X X
X X X X X X X X X
X X X X
X X X X X X X X
X X X X X X X X X X
X X X
X
X
Currently we know that the following implications hold: { EXT ! O, H, IAEX { INT ! AEX { M ! CV, C { IT ! INT, CS, ID, PI, O, C, H, M { PI ! ID, CG [MR00], [DK06] { H ! IAEX { ID, CV ! O { ID, M ! O [MR00] { ID, CG ! PI { CS ! O, H, C [AA95] { INT, PI $ INT, CG [DK06] { INT, ID, CV $ INT, O [MR00] { INT, PI $ INT, H, O [AM81] { EXT, PI $ EXT, ID, M [MR00] { INT, H, M $ INT, IT
Let us prove the implications that are not proved in the literature.
As can be seen from the de nitions of properties, property IT is stronger than property CS, so property IT also implies properties H, C, O ([AA95]).
Choice functions are called functions that have property INT.
Theorem 1. Let f be a choice function on 2S. Then the following conditions are equivalent: { f has properties H and M; { f has property IT.
Proof. INT, H, M ! INT, IT. Having M and INT we obtain A B ) f (A) f (B) ) f (A) \ A f (B) \ A ) f (A) f (B) \ A. Having H we obtain f (B) \ A f (A). Hence, we have f (B) \ A f (A) f (B) \ A, then f (A) = f (B) \ A, which is property IT.
INT, IT ! INT, H, M. Conversely, IT implies A B ) f (A) = f (B) \ A ) f (A) f (B), which is property M. Moreover, IT implies f (A) = f (B) \ A ) f (B) \ A f (A), which is property H.
Remark 2. Note that implication IT ! H, M holds for every function. Theorem 2. Let f be a function on 2S, then the following statements hold:
Proof. 1. Having EXT A f (A) we obtain f (B)\A f (A), which is property H.
H implies IAEX, so EXT implies IAEX (see 3 in this theorem). If f (B) A B, then, having EXT B f (B) we obtain f (B) = A = B, therefore f (A) = f (B), which is property O. 2. If x; y 2= f (A) and f has property INT, then f (A) A ) x; y 2= A, so x 2= A [ fyg; f (A [ fyg) 2 A [ fyg ) x 2= f (A [ fyg). 3. Having H we obtain (A x) A ) f (A) \ (A x) f (A x), and, if x; y 2 f (A); y 2= f (A x), then y 2= A x, and, as x 6= y, y 2= A, then f (A y) = f (A), so x 2 f (A y) = f (A), q.e.d. 4. If f (B) A B, having ID f (f (B)) = f (B) and CV we obtain f (f (B)) = f (A) = f (B), which is property O. 5. Having ID and CG we obtain f (f (A)) = f (A) ) f (f (A) [ f (B)) = f (A [ f (B)), applying the same conversion once more we obtain f (f (B)) = f (B) ) f (A [ f (B)) = f (A [ B), nally we get f (f (A) [ f (B)) = f (A [ f (B)) = f (A [ B), q.e.d. 6. Having M we obtain f (A) f (A [ B) and f (B) f (A [ B) 8A; B S, then f (A) \ f (B) f (A [ B), which is property C.
If A X B, then, having M we obtain f (A) f (X) f (B), but f (A) = f (B), so f (X) = f (A) = f (B). 7. Having IT we obtain A B ) f (A) = f (B) \ A ) f (A) f (B), which is property M.
Having IT we obtain A B ) f (A) = f (B) \ A ) f (A) A, which is property INT.
Property IT implies properties H, O and INT, and these three properties imply property PI ([AM81]). 3
Implication bases for context of functions on the powerset of two-element set and for context of functions on powerset of two- and three-element sets were obtained. The di erence in bases is presented and partly explained. Some implications in these bases were proved in the literature, for some of implications we gave the proofs. The remaining implications are to be either proved or rejected. We computed minimal generators of the premises closures as alternative to pseudointents. The use of minimal generators instead of pseudo-intents may make proofs and counterexamples of implications easier. We presented the complete list of proved implications and the contexts used in our study, so one can test the results and continue proving or refuting the implications between function properties. Acknowledgements We thank Florent Domenach for his careful reading, useful comments, helping with references and useful suggestions. We thank Daniel Borchmann for providing us with a useful FCA library in Clojure dialect of LISP and useful suggestions.
We also thank Fuad Aleskerov, Bernhard Ganter and Gleb Koshevoy for helpful discussions.