The parametric expressibility of functions is a generalization of the expressibility via composition. All parametrically closed classes of functions (p-clones) form a lattice. For finite domains the lattice is shown to be finite, however straight-forward iteration over all functions is infeasible, and so far the p-indecomposable functions are only known for domains with two and three elements. In this work we show how pindecomposable functions can be computed more efficiently by means of an extended version of attribute exploration (AE). Due to the growing number of attributes standard AE is not able to guarantee the discovery of all p-indecomposable functions. We introduce an extension of AE and investigate its properties. We investigate the conditions allowing us to guarantee the success of exploration. In experiments the lattice of pclones on three-valued domain was reconstructed.
The expressibility of functions is a major topic in mathematics and has a long history of investigation. The interest is explainable: when one aims at investigating any kind of functional properties, which classes of functions should one consider? If a function f is expressible through a function h then it often means that f inherits properties of h and should not be treated separately. Moreover, if h in turn is expressible through f then both have similar or even the same properties. Therefore, partition with respect to expressibility is meaningful and can be the first step in the investigation of functions.
With the development of electronics and logical circuits a new question arises: if one wants to be able to express all possible functions which minimal set of functions should one have at hands? One of the first investigations in this direction was carried out in [Pos42]; in this work all the Boolean classes of functions closed under expressibility are found and described. Afterwards many important works were dedicated to related problems such as the investigation of the structure of the lattice of functional classes, for example, [Yab60,Ros70]. However, it is known that the lattice of classes of functions closed under expressibility is in general uncountably infinite. In [Kuz79] a more general type of functional expressibility was introduced – parametric expressibility. A significant advantage of this type of expressibility is that for any finite domain Ak, |A|= k the lattice of all classes closed under parametric expressibility classes of functions (p-clones) is finite [BW87]. However, finding this lattice is a complex task. For k = 3 in a thorough and tedious investigation [Dan77] it was proved that a system of 197 functions forms the lattice of all p-clones. The investigation was carried out without the use of computers.
In this paper we introduce, develop, and investigate the methods and tools for automation of the exploration of the lattice of p-clones. Therefore, this paper “applied” to A3 can be seen as complementing the work [Dan77] where a proof of the correctness of the results obtained using the elaborated in this paper tools can be found. Namely, in this paper we answer the question how to find all the p-clones, whereas in [Dan77] it is proved that certain functions allow us to construct the desired lattice. The presented methods and tools are extensible to larger domains as well.
Contributions – New original approach to exploring the lattice of p-clones introduced; – An extension of the standard exploration procedure is introduced and investigated; – The whole procedure is implemented and executed; the obtained results confirm with the previously known results; – It is proved that for certain starting conditions the desired lattice will necessarily be eventually discovered. 2
In what follows we keep to standard definitions of FCA [GW99]. Let G and M be sets and let I ⊆ G × M be a binary relation between G and M . The triple K := (G, M, I) is called a (formal) context. The set G is called the set of objects. The set M is called the set of attributes. A context (G∗, M∗, I∗) such that G∗ ⊆ G, M∗ ⊆ M , and I∗ = I ∩ G∗ × M∗ is called a subcontext of K.
Consider mappings ϕ: 2G → 2M and ψ: 2M → 2G: ϕ(X) := {m ∈ M | gIm for all g ∈ X}, ψ(A) := {g ∈ G | gIm for all m ∈ A}.
Mappings ϕ and ψ define a Galois connection between (2G, ⊆) and (2M , ⊆), i.e. ϕ(X) ⊆ A ⇔ ψ(A) ⊆ X. Usually, instead of ϕ and ψ a single notation (·)0 is used.
Let X ⊆ G, A ⊆ M . A formal concept C of a formal context (G, M, I) is a pair (X, A) such that X0 = A and A0 = X. The subset of objects X is called the extent of C and is denoted by ext(C), and the subset of attributes A is called the intent of C and is denoted by int(C). For a context (G, M, I), a concept C1 = (X, A) is a subconcept of a concept C2 = (Y, B) (C1 ≤ C2) if X ⊆ Y or, equivalently, B ⊆ A. This defines a partial order on formal concepts. The set of all formal concepts of (G, M, I) is denoted by B(G, M, I).
An implication of K = (G, M, I) is defined as a pair (A, B), where A, B ⊆ M , written A → B. A is called the premise, B is called the conclusion of the implication A → B. The implication A → B is respected by a set of attributes N if A * N or B ⊆ N . We say that the implication is respected by an object g if it is respected by the intent of g. If g does not respect an implication then g is called a counter-example. The implication A → B holds (is valid ) in K if it is respected by all g0, g ∈ G, i.e. every object, that has all the attributes from A, also has all the attributes from B (A0 ⊆ B0). A unit implication is defined as an implication with only one attribute in its conclusion, i.e. A → b, where A ⊆ M, b ∈ M . Every implication A → B can be regarded as a set of unit implications {A → b | b ∈ B}.
An implication basis of a context K is defined as a set LK of implications of K, from which any valid implication for K can be obtained as a consequence and none of the proper subsets of LK has this property. We call the set of all valid in K the implicative theory of K. A minimal in the number of implications basis was defined in [GD86] and is known as the canonical implication basis.
An object g is called reducible in a context K := (G, M, I) iff ∃X ⊆ G \ g : g0 = X0. Note that a new object is going to be reducible if in the context there already exists a formal concept with the same intent as the intent of the new object. Reducible objects neither contribute to any implication basis nor to the concept lattice [GW99], therefore, if one is only interested in the implicative theory or in the concept lattice of the context reducible objects can be eliminated. In what follows we introduce other types of reducibility, therefore, we refer to this type of reducibility as plain reducibility.
In what follows the canonical implication basis is used, however, the investigation could be performed using another implication basis.
Attribute Exploration (AE) consists in iterations of the following steps until stabilization: computing the implication basis of a context, finding counterexamples to implications, updating the context with counterexamples as new objects, recomputing the basis. AE has been successfully used for investigations in many mostly analytical areas of research. For example, in [KPR06] AE is used for studying Boolean algebras, in [Dau00] lattice properties are studied, in [Rev14] algebraic identities are studied. 3
Consider a set Ak, |A|= k, k ∈ N. Consider a function f : Aar(f) → A (ar(f ) denotes the arity of f ), the set of all possible functions over Ak of different arities is denoted by Uk. The particular functions pin(x1, . . . xn) = xi are called the projections. The set of all projections is denoted by P r. In what follows instead of writing (x1, . . . xn) we use a shorter notation (x).
Let H ⊆ Uk. We say that f is compositionally expressible through H (denoted f ≤ H) if the following condition holds: f (x) ≡ h(j1(x), . . . , jar(h)(x)), (1) for some h, j1, . . . jm ∈ H ∪ P r.
A functional clone is a set of functions containing all projections and closed under compositions. The set of all functional clones over a domain of size k = 2 forms a countably infinite lattice [Pos42]. However, if k > 2 then the set of all functional classes is uncountable [YM59].
Let H ⊆ Uk and for any i ∈ [1, m] : ti, si ∈ H ∪ P r. We say that f, f ∈ Uk is parametrically expressible through H (denoted f ≤p H) if the following condition holds: f (x) = y ⇐⇒
m ∃w ^ ti(x, w, y) = si(x, w, y).
i=1 (2) The notation J ≤p H means that every function from J is parametrically expressible through H. A parametric clone (or p-clone) is a set of functions closed under parametric expressibility and containing all projections. We consider a special relation f • of arity ar(f )+1 on Ak called the graph of function f . f • consists of the tuples of the form (x, f (x)). If function h is compatible with f •, i.e. if for all valuations of variables xij in Ak holds the identity (ar(f ) = n, ar(h) = m) f (h(x11, . . . , x1m), . . . h(xn1, . . . , xnm)) ≡ h(f (x11, . . . , xn1), . . . f (x1m, . . . , xnm)), then we say that functions f and h commute (denoted f ⊥ h). For a set of functions H we write f ⊥ H to denote that for all h ∈ H : f ⊥ h. The commutation property is commutative, i.e. f ⊥ h iff h ⊥ f .
The centralizer of H is defined by H⊥ = {g ∈ Uk | g ⊥ H}. In [Kuz79] it is shown that if f ≤p H then f ⊥ H⊥.
A function f is called p-indecomposable if each system H parametrically equivalent to {f } (i.e. f ≤p H and H ≤p f ) contains a function parametrically equivalent to f . Hence, for each p-indecomposable function there exists a class of p-indecomposable functions that are parametrically equivalent to it. From each such class we take only one representative (only one p-indecomposable function) and gather them in a set of p-indecomposable functions denoted by Fkp. A pclone H cannot be represented as an intersection of p-clones strictly containing H if and only if there exists a p-indecomposable function f such that H = f ⊥⊥. Hence, in order to construct the lattice of all p-clones it suffices to find all pindecomposable functions. The lattice of all p-clones for any finite k is finite [BW87], hence, Fkp is finite.
In [BW87] it is proved that it suffices to consider p-indecomposable functions of arity at most kk, however, the authors conjecture that the actual arity should be equal to k for k ≥ 3. The conjecture is still open. Nevertheless, thanks to results reported in [Dan77], we know that the conjecture holds for k = 3. 4
The knowledge about the commutation properties of a finite set of functions F ⊆ Uk can be represented as a formal context KF = (F, F, ⊥F ), where ⊥F ⊆ F 2, a pair (f1, f2) ∈ F 2 belongs to the relation ⊥F iff f1 ⊥ f2. Note that the relation ⊥F is symmetric, hence, the objects and the attributes of the context are the same functions.
The goal of this paper is to develop methods for constructing the lattice of all p-clones on A3. As already noted, for the purpose of constructing the lattice of p-clones it suffices to find all p-indecomposable functions Fkp. The set of supremum-irreducible elements of the lattice of p-clones is exactly the set {f ∗∗ | f ∈ Fkp}.
For any domain of size k there exist kkk functions of arity k. Therefore, to compute the context of all commuting functions KUk one has to perform O(kkk ∗ kkk ∗ kk2 ) operations (taking into consideration only functions of arity k and the cost of commutation check in the worst case). For k = 3 we count about 1030 operations. Therefore, already for k = 3 a brute-force solution is infeasible.3
We intend to apply AE to commuting functions. For this purpose we developed and implemented methods for finding counter-examples to implications over functions from Uk [Rev15]. These methods are not presented in this paper for the sake of compactness. However, as the number of attributes is not fixed, the success of applying AE is not guaranteed, i.e. it is not guaranteed that the complete lattice of p-clones will eventually be discovered using AE. 4.1
We now describe which commuting properties a new function g 6∈ F should possess in order to alter the concept lattice of the original context K = (F, F, ⊥) despite the fact that the intent of g is equal to an intent from B(F, F, ⊥F ). 3 Of course one can use dualities, but it does not give a feasible solution as well as there exist only k ∗ (k − 1) dualities.
To distinguish between binary relations on different sets of functions we use subscripts. The commutation relation on F is denoted by ⊥F , i.e. ⊥F = {(h, j) ∈ F 2 | h ⊥ j}. The context with the new function (F ∪ g, F ∪ g, ⊥F ∪g) is denoted by KF ∪g. The derivation operator for the context KF ∪g is denoted by (·)⊥F ∪g . Proposition 1. Let C ∈ B(F, F, ⊥) such that ext(C) * int(C). Let g ∈ Uk, g ∈/ F be a function such that g⊥F ∪g ∩ F = int(C) (g is reducible in KF ).
g is irreducible in KF ∪g ⇔ g ⊥ g.
Proof. As ext(C) * int(C) and for all f ∈ F \ int(C) : g 6⊥ f it follows that g 6⊥ ext(C). We prove the contrapositive statement: g is reducible in KF ∪g ⇔ g 6⊥ g. ⇐ As g 6⊥ g we have g⊥F ∪g = int(C) = ext(C)⊥F ∪g . Therefore, g is reducible. ⇒ As g is reducible we obtain g⊥F ∪g = H⊥F ∪g for some H ⊆ F . Fix this H.
As H⊥F ∪g = int(C) we have H⊥F ∪g⊥F ∪g = ext(C). Suppose H ⊆ int(C), then H⊥F ∪g⊥F ∪g ⊆ int(C)⊥F ∪g⊥F ∪g = int(C). As H⊥F ∪g⊥F ∪g = ext(C) and ext(C) * int(C) we arrive at a contradiction. Therefore, H * int(C). Hence, g 6⊥ H, therefore, g 6∈ H⊥F ∪g , hence, g 6∈ g⊥F ∪g .
Corollary 1. If g is reducible in KF , but irreducible in KF ∪g and g ⊥ g then ext(C) → g holds in KF ∪g.
Proof. As g⊥F ∪g = int(C)∪{g} and ext(C)⊥F ∪g = int(C) we have ext(C)⊥F ∪g ⊂ g⊥F ∪g , therefore, ext(C) → g.
The statement dual to Proposition 1 holds as well.
Proposition 2. Let C ∈ B(F, F, ⊥F ) such that ext(C) ⊆ int(C). Let g ∈ Uk, g ∈/ F be a function such that g⊥F ∪g ∩ F = int(C) (g is reducible in KF ).
g is irreducible in KF ∪g ⇔ g 6⊥ g.
Proof. As ext(C) ⊆ int(C) and g ⊥ int(C) then g ⊥ ext(C). We prove the contrapositive statement: g is reducible in KF ∪g ⇔ g ⊥ g. ⇐ As g ⊥ g and g ⊥ ext(C) we have ext(C)⊥F ∪g = int(C) ∪ {g} = g⊥F ∪g .
Hence, g is reducible. ⇒ As g is reducible we obtain g⊥F ∪g = H⊥F ∪g for some H ⊆ F . Fix this H.
As g ⊥ int(C) we have H ⊥ int(C), hence, H ⊆ ext(C). As g ⊥ ext(C) we have g ⊥ H, hence, g ∈ H⊥F ∪g , therefore, g ∈ g⊥F ∪g and g ⊥ g. Corollary 2. If g is reducible in KF , but irreducible in KF ∪g and g 6⊥ g then g → ext(C) holds in KF ∪g.
Proof. As g⊥F ∪g = int(C) and ext(C)⊥F ∪g = int(C) ∪ {g} we have g⊥F ∪g ⊂ ext(C)⊥F ∪g , therefore, g → ext(C).
In order to distinguish reducibility in the old context KF and in the new context KF ∪g we introduce a new notation. Definition 1. We call a function g that is reducible in KF , but irreducible in KF ∪g, first-order irreducible for KF . If g is reducible for KF and reducible in KF ∪g we call it first-order reducible for KF .
We remind that if g is irreducible in (F ∪g, F, ⊥F ∪{(g, f ) ∈ {g}×F | f ⊥ g}) we call it plainly irreducible. Hence, if function is first-order reducible for KF then it is also plainly reducible in KF . Note that g is plainly irreducible in KF iff g is a counter-example to some valid in KF implication.
Next we present an example with functions from U3, in order to explicitly show this we add 3 in the subscript of every function. The numbering of the functions is induced by the lexicographic ordering on the outputs of the functions [Rev15]. We use superscripts ·u for unary, ·b for binary, and ·t for ternary functions.
Example 1. The context under consideration K(03) is presented in Figure 2. The implication basis of K(03) is empty, therefore, there exist no plainly irreducible functions. The function f3b,756 has the following commuting properties: f3b,756 ⊥ {f3u,0, f3b,12015} and f3b,756 6⊥ f3u,1. Moreover, f3b,756 6⊥ f3b,756 and for the corresponding concept C holds ext(C) = {f3u,0} ⊂ {f3u,0, f3b,12015} = int(C). As follows from Proposition 2, the function f3b,756 is first-order irreducible for K(03). f3u,0 f3u,1 f3,12015
b Corollary 3. Let C ∈ B(F, F, ⊥F ), g ∈ Uk, g ∈/ F , and g be first-order reducible for KF .
ext(C) ⊥ g ⇔ g ⊥ g.
Proof. Follows from Propositions 1 and 2 and the fact that ext(C) ⊥ g ⇔ ext(C) ⊆ int(C).
There remains a possibility that a union of sets of reducible functions is irreducible. We proceed with the simplest case when there are only two sets each containing a single first-order reducible function for the current context. We prove several propositions about such pairs of first-order reducible functions. The consequences of these propositions are deeper investigated in Section 4.2.
We consider a context KF and new functions g1, g2 ∈ Uk, g1, g2 6∈ F . We denote {g1, g2} by G, ⊥F ∪G= {(h, j) ∈ (F ∪ G)2 | h ⊥ j}, the context (F ∪ G, F ∪ G, ⊥F ∪G) is denoted by KF ∪G, the corresponding derivation operator is denoted by (·)⊥F∪G . As in the case with one function, for i ∈ {1, 2} : gi is not a counter-examples to a valid implication iff gi⊥F∪G ∩ F ∈ int(G, M, I). We denote the corresponding intents by int(C1) and int(C2), respectively.
Proposition 3. Let C1, C2 ∈ B(F, F, ⊥F ) and g1, g2 ∈/ F be first-order reducible for KF . Suppose g1 ⊥ g2.
Both g1, g2 are irreducible in KF ∪G ⇔ ext(C1) * int(C2).
Proof. As g1 is irreducible it holds that g1⊥F∪G 6= ext(C1)⊥F∪G . From Corollary 3 follows that g1 ∈ ext(C1)⊥F∪G iff g1 ∈ g⊥F∪G . Therefore, ext(C1)⊥F∪G = 1 g1⊥F∪G \ {g2}. Hence, ext(C1) 6⊥ g2, hence, ext(C1) * int(C2). Similarly for g2, ext(C2) * int(C1).
Proposition 4. Let C1, C2 ∈ B(F, F, ⊥F ) and g1, g2 ∈/ F be first-order reducible for KF . Suppose g1 6⊥ g2.
Both g1, g2 are irreducible in KF ∪G ⇔ ext(C1) ⊆ int(C2).
Proof. As g1 is irreducible it holds that g1⊥F∪G 6= ext(C1)⊥F∪G . From Corollary 3 follows that g1 ∈ ext(C1)⊥F∪G iff g1 ∈ g⊥F∪G . Therefore, ext(C1)⊥F∪G = 1 g1⊥F∪G ∪ {g2}. Hence, ext(C1) ⊥ g2, hence, ext(C1) ⊆ int(C2). By the properties of derivation operators, ext(C2) ⊆ int(C1).
The functions mentioned in Propositions 4 and 3 can be called second-order irreducible for KF . In the next proposition we show that it is not necessary to look for three functions at once in order to find all p-indecomposable functions. Therefore, we do not need to define third-order irreducibility.
Here we use the notation: for I ⊆ {1, 2, 3} : LI = {gi | i ∈ I}. We omit the curly brackets in I, i.e. L{1,2} = L12 = {g1, g2}.
Proposition 5. Let G = {g1, g2, g3} be a set of functions such that G ∩ F = ∅ and for i ∈ {1, 2, 3} : gi⊥F∪G ∩ F = int(Ci). If not all functions from G are reducible in KF ∪G then there exists L ⊂ G such that not all functions from L are reducible in KF ∪L.
Proof. Let g1 be reducible in KF ∪L12 and in KF ∪L13 . Then there exists H ⊆ F ∪ {g2} : H⊥F∪L12 = g⊥F∪L12 and J ⊆ F ∪ {g3} : J ⊥F∪L13 = g⊥F∪L13 . Fix 1 1 these H and J . If either g2 is irreducible in KF ∪L2 or g3 is irreducible in KF ∪L3 then the proposition is proved. Therefore, we can assume that they are reducible in corresponding context. Hence, without loss of generality, we can assume that H, J ⊆ F (i.e. H ∩ G = J ∩ G = ∅). Note that g1⊥F∪G = g1⊥F∪L13 ∪ g1⊥F∪L12 = J ⊥F∪L13 ∪ H⊥F∪L12 . (3)
Let g3 ∈ H⊥F∪G . Then g3 ⊥ H. As g3⊥F∪G ∩ F = int(C3) we obtain H ⊆ int(C3). Moreover, as int(C3) is an intent in KF we have H⊥F ⊥F ⊆ int(C3). As g1⊥F∪G ∩ F = H⊥F = J ⊥F = int(C1) we have J ⊥F ⊥F ⊆ int(C3) and, by properties of closure operators, J ⊆ int(C3). Therefore, g3 ⊥ J and g3 ∈ J ⊥F ∪G . Similarly, if g2 ∈ J ⊥F ∪G then g2 ∈ H⊥F ∪G . Hence,
H⊥F ∪L12 ∪ J ⊥F ∪L13 = H⊥F ∪G ∪ J ⊥F ∪G . (4)
Combining (3) and (4) we obtain g1⊥F ∪G = H⊥F ∪G ∪ J ⊥F ∪G . Therefore, g⊥F ∪G = (H ∩ J )⊥F ∪G . Hence, g1 is reducible in KF ∪G and we arrive at a 1 contradiction with initial assumption.
Therefore, if g1, g2 are in KF ∪L12 then at least g1 is irreducible in KF ∪L13 . If g3 is reducible in KF ∪L13 then g1 is reducible in KF ∪L1 . Otherwise, both g1, g3 are irreducible in KF ∪L13 .
Suppose that a context KF contains all p-indecomposable functions, however, the task is to prove this fact, i.e. that no further p-indecomposable functions exist. Suppose it has been checked that no counter-examples exist and every single function g ∈ Uk is first-order reducible for KF . According to the above propositions it is necessary to look for exactly two functions at once in order to prove the desired statement. Therefore, in order to complete the proof for every C1, C2 ∈ B(KF ) one has to find all the functions g1, g2 such that g1⊥F ∪g1 ∩ F = int(C1) and g2⊥F ∪g2 ∩ F = int(C2) and then check if g1 commutes with g2. Therefore, one has to check the commutation property between all functions (if the context indeed contains all p-indecomposable functions). As already discussed, this task is infeasible. This result is discouraging. However, having the knowledge about the final result in some cases we can guarantee that all pindecomposable functions will be found even without looking for two functions at once. 4.2
During the exploration of p-clones one can discover such a subcontext of functions that no further function is a counter-example to existing implications. We shall say that such a subcontext is implicatively closed, meaning that all the valid in this subcontext implications are valid in the final context as well. Analysis of similar constructions can be found in [Gan07].
In order to guarantee the discovery of all p-indecomposable functions (success of exploration) it would suffice to find such a subcontext that it is neither implicatively closed nor contained in any other implicatively closed subcontext. Suppose the context KF = (F, F, ⊥F ), F ⊆ Uk is discovered. As earlier, we denote the context of all p-indecomposable functions on Uk by KFkp . Let S = Fkp\F . It would be desirable to be able to guarantee the discovery of functions S by considering only the discovered part of relation ⊥F and the part ⊥F S (=⊥S−F1 ), see Figure 3. Unfortunately, as the next example shows, in general it is not possible. Example 2. Consider the context in Figure 4. The context contains all the pindecomposable functions from U2 and three additional objects g1, g2, g3. Functions with commutation properties as of g1, g2, g3 do not exist. However, if functions with commutation properties as of g1, g2, g3 existed then the functions g1, g2
F S
F ⊥F
S ⊥F S ⊥SF
⊥S would not be counter-examples to any valid in KF2p∪g3 implication. Note that g3 is a counter-example to a valid in KF2p implication. Therefore, the subcontext containing functions F2p ∪ g3 would be implicatively closed. Moreover, it is even closed with respect to finding first-order irreducible functions as g1 is reducible in KF2p∪{g1,g3} and g2 is reducible in KF2p∪{g2,g3}.
However, if instead of g3 we consider the function g4, which differs from g3 only in that g4 commutes with both g1 and g2, then the subcontext containing F2p ∪ g4 is neither implicatively closed nor contained in any implicatively closed subcontext of the context KF2p∪{g1,g2,g4}. The difference between g3 and g4 is contained in ⊥S in Figure 3. Therefore, in general it is not possible to guarantee the discovery of functions S without considering ⊥S . Definition 2. Let KH be a context, KF ⊆ KH , S = H \ F . An object s ∈ S is called an essential counter-example for KF if there exists a valid in KF implication Imp such that 1. s is a counter-example to Imp; 2. there does not exist an object p ∈ S \ {s} such that p is a counter-example to Imp.
It is clear that all the essential counter-examples will necessarily be added to the context during the exploration. The next proposition suggests how one can check if a counter-example is essential or not.
In the context KF3p there are several pairs of functions (f1, f2) such that they commute with the same functions except for one commutes with itself and the other does not commute with itself. These functions cannot be essential counterexamples, because they are counter-examples to the same implications, if any. However, if they are the only counter-examples to some valid implication then these functions will eventually be discovered by object-attribute exploration. Proposition 6. Let s1, s2 ∈ S such that s2 6⊥ s2 and s1⊥Uk = s2⊥Uk ∪ {s2}. If there exists a valid in KF implication Imp such that the counter-examples are exactly s1, s2 ∈ S then s1 is first-order irreducible for KF ∪s2 and s2 is first-order irreducible for KF ∪s1 .
Proof. s1 in KF ∪s2 . As Imp is valid in KF the set s2⊥F ∪s1 is closed in KF . Therefore, as follows from Proposition 1 for the object concept of s2 (ext(Cs2 ) * int(Cs2 )), the function s1 (s1 ⊥ s1) is first-order irreducible. s2 in KF ∪s1 . As Imp is valid in KF the set s1⊥F ∪s2 is closed in KF . Therefore, as follows from Proposition 2 for the object concept of s1 (ext(Cs1 ) ⊆ int(Cs1 )), the function s2 (s2 6⊥ s2) is first-order irreducible.
We have investigated different types of reducibilities, we have shown, that there do not exist third-order irreducible functions. However, the task of finding second-order irreducible functions is infeasible. Fortunately, it is possible to find not only zero-order irreducible functions, but also first-order irreducible functions. Moreover, if it would be possible to prove that the functions undiscovered at the moment are not second-order irreducible then we can guarantee that all the p-indecomposable functions will eventually be discovered. 5
We take all unary functions as the starting point. Thanks to earlier investigation in [Dan77] we know the final context. When we investigate all possible implicatively closed partitions such that the implicatively closed subcontext contains all unary functions we find the following: – We start with 27 unary functions, 26 of them are p-indecomposable; – After adding all essential counter-examples we obtain 147 functions; – After using Proposition 6 we obtain 155 functions; – There remain 42 functions to be discovered. By direct check we find that there does not exist an implicatively closed subcontext containing 155 mentioned above functions such that all the undiscovered functions are secondorder irreducible. Hence, if we start from all unary functions on A3 all the functions F3p will eventually be discovered.
The experiment was conducted three times starting from different initial contexts, all three times the exploration was successful. The exploration stating from a single constant function f3u,0 took 207 steps.