Approximate Functional Dependencies---Implication Problem Revisited

Approximate Functional Dependencies—Implication Problem Revisited Nicolas Fröhlich1,† , Matilda Häggblom2,† , Åsa Hirvonen2,† and Minna Hirvonen1,† 1 2

Leibniz Universität Hannover, Germany University of Helsinki, Finland

Abstract Functional dependencies are an important and well-studied class of database constraints that correspond to a notion expressed by dependence atoms in team logic. In practice, data often contain errors, so in some cases it might be useful to allow the database to have a small number of tuples that violate the desired dependency. Väänänen (2017) studied the axiomatisation of a notion of approximate dependence that specifies for each dependence atom how much of the database can be disregarded. We demonstrate that the interaction of approximate dependence atoms is more complicated than previously thought in the sense that there is a semantic consequence that is not captured by the inference rules introduced before. We show that Väänänen’s axiomatisation is still complete in the restricted case of unary dependencies. We also consider the complexity of model checking for approximate dependence: it is NP-complete for disjunctions of two atoms and LOGSPACE-hard for individual atoms.

Keywords Database, functional dependency, approximation, team semantics, axiomatisation, model checking.

1. Introduction Functional dependencies were introduced in database theory by Codd in the 1970’s [1], and axiomatised by Armstrong [2] a few years later. In the unirelational case they are equivalent to dependence atoms in team logic. Teams were originally defined by Hodges [3, 4] to give a compositional semantics for so-called independence-friendly logic. Väänänen [5] introduced dependence logic, allowing the explicit study of relationships between variables. The rise of big data offers strong motivation to study dependencies that disregard statistical outliers in the data set. Approximate notions of dependence are also motivated by considerations of natural language, such as ‘most’, ‘all but a few’, and were formalised for functional dependencies by Kivinen and Mannila [6] with various measures of the part of the information allowed to be erroneous. Väänänen adapted one of the definitions as approximate dependence atoms in the team semantic setting [7], and proposed an axiomatisation of its implication problem. Unfortunately, the axiomatisation in [7] disregards a subtle point in dependence that only turns up in the approximate notion. Where in pure functional dependencies, a tuple 𝑦𝑧 depends on 𝑥 exactly when both 𝑦 and 𝑧 depend on 𝑥, in an approximate version, where small errors are allowed, the distribution of errors between variables introduces interplay between the variables that is hard to axiomatise. In this paper, we illustrate this phenomenon by presenting a ‘missing rule’ - a semantic consequence that cannot be obtained from the axiomatisation in [7]. Väänänen’s axiomatisation is still complete in the restricted case of unary dependencies, where simple dependence statements ‘𝑦 depends on 𝑥’ are considered for single variables 𝑥 and 𝑦. We extract the necessary rules for unary and constant dependencies, and prove completeness (there was an error in the proof in [7]). Such axiomatizations could help speed up algorithms for discovering approximate dependencies in databases (see, e.g., [8]), with applications in data mining. We also examine the complexity of the model checking problem for approximate dependence. †

These authors contributed equally. $ nicolas.froehlich@thi.uni-hannover.de (N. Fröhlich); matilda.haggblom@helsinki.fi (M. Häggblom); asa.hirvonen@helsinki.fi (Å. Hirvonen); minna.hirvonen@thi.uni-hannover.de (M. Hirvonen)  0009-0003-5413-1823 (N. Fröhlich); 0009-0003-6289-7853 (M. Häggblom); 0000-0003-2149-4153 (Å. Hirvonen); 0000-0002-2701-9620 (M. Hirvonen)

2. Definitions We recall basic team semantic definitions together with the approximate dependence atoms from [7]. Let 𝐷 and 𝑀 be sets of variables and values, respectively. An assignment 𝑠 over 𝐷 is a function 𝑠 : 𝐷 → 𝑀 . A team 𝑋 over 𝐷 is a set of assignments 𝑠 : 𝐷 → 𝑀 . For a team 𝑋 over 𝐷 and a tuple 𝑥 = 𝑥1 . . . 𝑥𝑛 of variables from D, we define the notation 𝑋[𝑥] := {𝑠(𝑥) ∈ 𝑀 𝑛 | 𝑠 ∈ 𝑋}, where 𝑠(𝑥) = 𝑠(𝑥1 ) . . . 𝑠(𝑥𝑛 ). For 𝑥 = 𝑥1 . . . 𝑥𝑛 and 𝑦 = 𝑦1 . . . 𝑦𝑚 , we write 𝑥𝑦 for the tuple 𝑥1 . . . 𝑥𝑛 𝑦1 . . . 𝑦𝑚 . The notation |𝑥| refers to the length of the tuple 𝑥, e.g, |𝑥| = 𝑛 for 𝑥 = 𝑥1 . . . 𝑥𝑛 . Let 𝑥 and 𝑦 be finite tuples of variables from 𝐷 such that 𝑦 is nonempty, i.e., |𝑦| ≥ 1. An expression =(𝑥, 𝑦) is called a dependence atom. The satisfaction relation between a team 𝑋 over 𝐷 and the atom =(𝑥, 𝑦) is defined by 𝑋 |= =(𝑥, 𝑦) if and only if for all 𝑠, 𝑠′ ∈ 𝑋, 𝑠(𝑥) = 𝑠′ (𝑥) implies 𝑠(𝑦) = 𝑠′ (𝑦). Since 𝑋 |= =(𝑥, 𝑦) if and only if there is a function 𝑓 : 𝑋[𝑥] → 𝑋[𝑦] such that 𝑓 (𝑠(𝑥)) = 𝑠(𝑦) for all 𝑠 ∈ 𝑋, dependence atoms are often called functional dependencies, especially in database theory. Note that the tuple 𝑥 is allowed to be empty1 , and in that case, we write =(𝑦) instead of =(, 𝑦). The atom =(𝑦) is called the constancy atom, as it states that the value of 𝑦 is constant in the team. Let Σ ∪ {𝜏 } be a set of atoms with variables from 𝐷. We write 𝑋 |= Σ, if 𝑋 |= 𝜎 for all 𝜎 ∈ Σ. We say that Σ semantically entails 𝜏 , written as Σ |= 𝜏 , if for all 𝑋 over 𝐷, we have that 𝑋 |= Σ implies 𝑋 |= 𝜏 . We consider a notion of approximate dependence that states that a dependence must hold in a team when we are allowed to remove some assignments (usually a small portion of the whole team). Definition 2.1 ([7]). Let 𝑝 be a real number, 0 ≤ 𝑝 ≤ 1. For finite teams, 𝑋 |= =𝑝 (𝑥, 𝑦) if there is a subteam 𝑌 ⊆ 𝑋, |𝑌 | ≤ 𝑝 · |𝑋|, such that 𝑋 ∖ 𝑌 |= =(𝑥, 𝑦). The following set of rules is sound for approximate dependencies. Definition 2.2 ([7]). Rules 𝐴1-𝐴7 form the system A for approximate dependencies. (A1) =0 (𝑥𝑦, 𝑥). (A5) If =𝑝 (𝑥𝑢, 𝑦𝑣), then =𝑝 (𝑢𝑥, 𝑦𝑣) and =𝑝 (𝑥𝑢, 𝑣𝑦). (A2) =1 (𝑥, 𝑦). (A3) If =𝑝 (𝑥, 𝑦𝑣), then =𝑝 (𝑥𝑢, 𝑦).

(A6) For 𝑟 = 𝑚𝑖𝑛{𝑝 + 𝑞, 1}, if =𝑝 (𝑥, 𝑦) and =𝑞 (𝑦, 𝑣), then =𝑟 (𝑥, 𝑣).

(A4) If =𝑝 (𝑥, 𝑦), then =𝑝 (𝑥𝑢, 𝑦𝑢).

(A7) For 𝑝 ≤ 𝑞 ≤ 1, if =𝑝 (𝑥, 𝑦), then =𝑞 (𝑥, 𝑦).

For a set of approximate dependencies Σ and a system of rules B, we write Σ ⊢B =𝑝 (𝑥, 𝑦) if we can apply the rules in B to the dependencies in Σ to derive the conclusion =𝑝 (𝑥, 𝑦). A system B is sound if whenever Σ ⊢B =𝑝 (𝑥, 𝑦), also Σ |= =𝑝 (𝑥, 𝑦). As shown in [7], the rules are sound, but we challenge the claim that they are complete in the sense claimed in [7], i.e., that for a finite set of approximate dependence atoms, Σ |= =𝑝 (𝑥, 𝑦) would imply that Σ ⊢A =𝑝 (𝑥, 𝑦). First, let us note a minor issue that arises when the dependence is defined on sequences rather than on sets of variables/attributes, as is common in the database theory literature. Using system A, we cannot derive =𝑝 (𝑥, 𝑥𝑦) from =𝑝 (𝑥, 𝑦). Instead, we can derive =𝑝 (𝑥, 𝑦) ⊢A =𝑝 (𝑥𝑥, 𝑥𝑦), so if we consider 𝑥𝑥 as different from 𝑥, the set of rules is not complete even for usual dependencies with approximation 0. To solve this, as pointed out in [9], we can replace the rules 𝐴3 and 𝐴4 with the rule 𝐴34 : (𝐴34 )

If =𝑝 (𝑥, 𝑦), then =𝑝 (𝑥, 𝑥𝑦).

System A* consisting of rules 𝐴1, 𝐴2, 𝐴34 , 𝐴5, 𝐴6 and 𝐴7 is complete for usual dependencies sensitive to repetition of variables (see e.g., [10] for a completeness proof in the team semantic setting). However, we show in the next section that there are semantic entailments specific to the approximate setting that are not derivable even in this modified set of rules A* . 1

In the dependence atom =(𝑥, 𝑦), the tuple 𝑦 is assumed to be nonempty, because otherwise the atom =(𝑥, 𝑦) would be trivially satisfied by any team over 𝐷 that contains the variables 𝑥.

Table 1 5 (𝑥, 𝑦). Example team for Example 3.1. The team satisfies all approximation atoms in Σ, while also satisfying = 16 * 5 (𝑥, 𝑦) cannot be derived from Σ given the rules in system A . However = 16 𝑥

𝑣1

𝑣2

𝑣3

𝑦

𝑧0

𝑠0 𝑠1 𝑠2 𝑠3 𝑠4 𝑠5 𝑠6 .. .

0 0 0 0 0 0 0 .. .

0 0 0 1 0 0 0 .. .

0 0 0 0 1 0 0 .. .

1 2 3 4 0 0 0 .. .

1 2 3 4 5 0 0 .. .

0 1 2 3 4 5 6 .. .

𝑠15

0

0

0

0

0

15

3. Missing Rule We aim to show that there is a semantic entailment among approximate dependence atoms that is not derivable using rules from the system A* , proving that the system is incomplete. First, we exemplify this semantic entailment by examining a specific team. Example 3.1. Let Σ = {=0 (𝑥), = 1 (𝑥, 𝑣1 𝑣2 ), = 2 (𝑥, 𝑣1 𝑣3 ), = 2 (𝑣1 , 𝑦), =0 (𝑣2 𝑣3 , 𝑦)} be a set of approxi8 8 8 mate atoms. Consider the team 𝑋 depicted in Table 1. We have that 𝑋 |= Σ, while having to remove the maximum number of assignments in each approximation atom in Σ. Next, consider the dependence atom =(𝑥, 𝑦). For =(𝑥, 𝑦) to be true, five assignments in 𝑋 need to be removed; therefore 𝑋 |= = 5 (𝑥, 𝑦) holds. 16 However = 5 (𝑥, 𝑦) cannot be derived by the rules in system A* . The best approximation atom derivable is 16

6 = 6 (𝑥, 𝑦) via transitivity of = 1 (𝑥, 𝑣1 𝑣2 ) and = 2 (𝑣1 , 𝑦). While 𝑋 |= = 6 (𝑥, 𝑦) is obvious, the ratio 16 16 8 8 16 is clearly not optimal.

The next result shows that this example is not an isolated case, but that all teams satisfying Σ must also satisfy = 5 (𝑥, 𝑦). 16

Proposition 3.2. Let Σ = {=0 (𝑥), = 1 (𝑥, 𝑣1 𝑣2 ), = 2 (𝑥, 𝑣1 𝑣3 ), = 2 (𝑣1 , 𝑦), =0 (𝑣2 𝑣3 , 𝑦)} be a set of ap8 8 8 proximate atoms. If 𝑋 |= Σ for any team 𝑋, then 𝑋 |= = 5 (𝑥, 𝑦). 16

However, since Σ ̸⊢A* = 5 (𝑥, 𝑦), we conclude that A* is an incomplete set of rules. 16 It is worth noting that the missing rule does not only show incompleteness in the case with tuples as dependent variables (i.e., in the right part of the atom). If one studies right unary dependence atoms, i.e., atoms of the form =𝑝 (𝑥1 . . . 𝑥𝑛 , 𝑦1 ), one can simulate atoms of the form =𝑝 (𝑥, 𝑦1 𝑦2 ) by introducing a new variable 𝑧 and using dependencies =0 (𝑧, 𝑦1 ), =0 (𝑧, 𝑦2 ), =0 (𝑦1 𝑦2 , 𝑧), =𝑝 (𝑥, 𝑧).

4. Restricted Completeness Theorem We prove the completeness of the original system in Definition 2.2 for a restricted set of approximate dependence atoms. Namely, when we restrict to rational approximations 𝑝 ∈ Q ∩ [0, 1] and to unary and so-called 1-constancy atoms of the form =𝑝 (𝑥, 𝑦), where |𝑥| ≤ 1 and |𝑦| = 1. Due to the arity restrictions, we can omit rules 𝐴4 and 𝐴5. We denote the remaining rules restricted to unary and 1-constancy atoms by 𝐴11 , 𝐴21 , 𝐴31 , 𝐴61 and 𝐴71 and obtain system A1 . In particular, 𝐴11 takes the simple form ‘=0 (𝑥, 𝑥)’, and 𝐴31 is of the form ‘if =𝑝 (𝑦), then =𝑝 (𝑢, 𝑦)’.

Table 2 Suppose that = 14 (𝑥, 𝑦) is not derivable from Σ using rules from system A1 , where Σ is {= 14 (𝑥, 𝑤), = 14 (𝑤, 𝑦)}. Then 𝑑(𝑥) = 0, 𝑑(𝑤) = 41 , and 𝑑(𝑦) = 12 and we can construct counterexample teams 𝑋 and 𝑌 as illustrated. 𝑋

𝑥

𝑤

𝑦

𝑧0

𝑌

𝑥

𝑤

𝑦

𝑠0 𝑠1 𝑠2 𝑠3 𝑠4

0 0 0 0 0

0 1 1 1 1

0 1 2 2 2

0 1 2 3 4

𝑠0 𝑠1 𝑠2 𝑠3 𝑠4

0 0 0 𝑎 𝑏

0 1 1 𝑎 𝑏

0 1 2 𝑎 𝑏

Theorem 4.1. Let Σ∪{=𝑝 (𝑥, 𝑦)} be a finite set of unary and 1-constancy rational approximate dependence atoms. If Σ |= =𝑝 (𝑥, 𝑦), then Σ ⊢A1 =𝑝 (𝑥, 𝑦). To prove completeness under these restrictions, we construct a counterexample team 𝑋 similar to the one in [7], but with some core differences, one of which we discuss next. Let Σ ∪ {=𝑝 (𝑥, 𝑦)} be as in the above Theorem. Our goal is to show, under the assumption Σ ̸⊢A1 =𝑝 (𝑥, 𝑦), that there is a team 𝑋 that satisfies all atoms in Σ but not =𝑝 (𝑥, 𝑦). Like in [7], for each variable 𝑢 we find the smallest approximation 𝑑(𝑢) for which =𝑑(𝑢) (𝑥, 𝑢) is derivable from Σ. Differing from [7], we can find the least common denominator 𝑛 − 1 for the approximations appearing in Σ ∪ {=𝑝 (𝑥, 𝑦)}, since they 𝑘 are rational numbers. We then construct a team of size 𝑛 such that the approximations 𝑑(𝑢) = 𝑛−1 are 𝑘 uniformly encoded with a slightly better approximation, namely 𝑛 . This type of uniformity is missing from [7], making that completeness proof erroneous even for unary atoms, possibly because of the attempt to cover real-numbered approximations. Two examples of counterexample teams are presented in Table 2, one of which takes advantage of a dummy variable 𝑧0 and the other does not. A similar construction for unary approximate inclusion atoms with rational approximations also appeared in [11].

5. Model Checking Model checking is a central decision problem in every logic. It asks the simple question whether a formula of the logic is true in a structure. One often considers the data complexity variant where the formula is fixed and the input consists of only the structure. For dependence logic, model checking is NP-complete in general, even for quantifier-free disjunctions of only three dependence atoms, but in NL, when restricted to disjunctions of two atoms [12]. However, with approximations even simpler formulas can have intractable model checking, as was shown for the approximate operator in [13]. Our first result demonstrates that with a single approximate dependence atom, disjunctions of just two atoms become NP-complete. In the setting of dependence logic, disjunctions are not defined globally over the whole team but rather split the team into two parts, each satisfying one of the two disjuncts. Formally, 𝑋 |= 𝜑1 ∨ 𝜑2 if there are teams 𝑋1 , 𝑋2 such that 𝑋 = 𝑋1 ∪ 𝑋2 and 𝑋𝑖 |= 𝜑𝑖 for 𝑖 ∈ {1, 2}. Theorem 5.1. The model checking problem for = 3 (𝑢, 𝑣) ∨ =0 (𝑥, 𝑦) is NP-complete. 13

Next, consider the complexity of a single approximate dependence atom. It is well known that single dependence atoms are first-order definable. This is no longer true for approximate dependence atoms. Theorem 5.2. The model checking problem for = 1 (𝑥, 𝑦) is LOGSPACE-hard. 2

6. Conclusion and Future Work We introduced a semantic entailment that cannot be deduced by using system A* , meaning that the system is not complete in the general case of approximate dependencies. It seems likely that there are

other similar semantic entailments involving different approximations, so the system might actually have several missing rules. This raises the question whether the implication problem is finitely axiomatisable or whether every complete system necessarily involves an infinite number of rules. If the problem is not finitely axiomatisable, a natural goal for future work would be to prove that this is indeed the case. It might still be possible to represent the axioms in a nice way that expresses the infinite rules in the form of a rule schema, e.g., as in [14, 15, 16]. Investigating this is also a relevant question for further research. Since the implication problem for dependencies with real (or even rational) number approximations seems difficult to axiomatise, one may ask if this has something to do with some specific properties of these structures. Therefore, it might be useful to investigate the approximate dependence in the setting of monoids, where we may consider structures with different properties. A monoid is a tuple 𝐾 = (𝐾, +, 0𝐾 ) where 𝐾 is a set, + is an associative binary operation on 𝐾, and 0𝐾 is an identity element of +. A monoid 𝐾 is positive if 𝑎 + 𝑏 = 0𝐾 implies 𝑎 = 0𝐾 and 𝑏 = 0𝐾 , and commutative if 𝑎 + 𝑏 = 𝑏 + 𝑎 for all 𝑎, 𝑏 ∈ 𝐾. An ordered monoid is a commutative monoid 𝐾 with a partial order ≤ such that 0𝐾 ≤ 𝑎 for all 𝑎 ∈ 𝐾, and 𝑎 ≤ 𝑏 implies 𝑎 + 𝑐 ≤ 𝑏 + 𝑐 for all 𝑎, 𝑏, 𝑐 ∈ 𝐾. The idea is that we consider a totally ordered positive commutative monoid 𝐾 = (𝐾, ≤, +, 0𝐾 ), and for a finite team 𝑋 ⊆ {𝑠 | 𝑠 : 𝐷 → 𝑀 }, define a 𝐾-team X as a function X : 𝑋 → 𝐾. A 𝐾-team is essentially an annotated database relation or a 𝐾-relation, as introduced in [17] in the setting of semiring provenance. Denote supp(X) := {𝑠 ∈ 𝑋 | X(𝑠) ̸= 0𝐾 }. Then for any 𝑎 ∈ 𝐾, we can define a 𝐾-approximate dependence ∑︀ atom =𝑎 (𝑥, 𝑦) with the following satisfaction relation: X |= =𝑎 (𝑥, 𝑦) iff there is 𝑌 ⊆ 𝑋 for which 𝑠∈𝑌 X(𝑠) ≤ 𝑎 and supp(X ↾𝑋∖𝑌 ) |= =(𝑥, 𝑦). Note that we define ∑︀ 𝑠∈∅ X(𝑠) = 0𝐾 , so X |= =0𝐾 (𝑥, 𝑦) iff supp(X) |= =(𝑥, 𝑦). If 𝐾 is the Boolean monoid B = ({0, 1}, ≤, ∨, 0), the 𝐾-approximate dependencies correspond to the usual dependencies, where each =0 (𝑥, 𝑦) corresponds to =(𝑥, 𝑦) and each =1 (𝑥, 𝑦) is trivially satisfied. If 𝐾 is the probability monoid P = ([0, 1], ≤, +, 0), where ≤ is the usual order of the unit interval [0, 1] and 𝑎 + 𝑏 = max{𝑎 + 𝑏, 1}, then the 𝐾-approximate dependencies correspond to the approximate dependencies over 𝐾-teams X that are uniform distributions, i.e., X(𝑠) = 1/|𝑋| for all 𝑠 ∈ 𝑋. Different dependency notions over 𝐾-teams have been studied, e.g., in [18, 19]2 . In the setting of monoids, the satisfaction of the 𝐾-approximate dependencies is defined in such a way that the number of tuples that can be removed is measured as an absolute value instead of a team ratio. One possible line of future research on real approximations is to examine whether considering approximation as an absolute value instead of a ratio could help with obtaining a complete axiomatisation. Already in [6], variants of both absolute value approximations and ratio approximations were introduced. One can also consider other definitions, such as a local variant where 𝑋 |= =𝑝 (𝑥, 𝑦) if there is a subteam 𝑌 ⊆ 𝑋, |𝑌 | ≤ 𝑝 · |𝑋 ↾{𝑥𝑦} |, such that 𝑋 ∖ 𝑌 |= =(𝑥, 𝑦), where 𝑋 ↾{𝑥𝑦} is the team restricted to the variables 𝑥 and 𝑦. With this definition, {=𝑝 (𝑥, 𝑤), =𝑞 (𝑤, 𝑦)} ̸|= =𝑝+𝑞 (𝑥, 𝑦), meaning any complete system, even restricted to unary atoms, would be different from the one in [7]. To take advantage of the team semantic framework, we could situate the approximate dependence atom in a language with connectives and quantifiers as in first-order dependence logic [5]. Some first steps in this direction are taken in [13]. With our gained understanding of unary and 1-constancy approximate dependence atoms, they could serve as the first building blocks of an approximate variant of first-order dependence logic. Acknowledgements The authors want to thank Jouko Väänänen and the anonymous reviewers of LINDA 2026 for many helpful suggestions. The authors appreciate the project support by a Finnish-German co-operation Grant: DAAD (German Exchange Service, project id 57710940), Research Council of Finland (project id 359650). The first author appreciates funding by the German Research Foundation (DFG) under the 2

Note that these works also consider (conditional) independence atoms whose semantics is defined using both addition and multiplication, so their structure 𝐾 is a semiring instead of a monoid.

grant ME2479/3-1 and project id 511769688. The fourth author appreciates funding by the Magnus Ehrnrooth Foundation.

References [1] E. F. Codd, Further normalization of the data base relational model, IBM Research Report, San Jose, California RJ909 (1971). [2] W. W. Armstrong, Dependency structures of data base relationships, in: IFIP Congress, 1974. URL: https://api.semanticscholar.org/CorpusID:38788061. [3] W. Hodges, Compositional semantics for a language of imperfect information, Logic Journal of IGPL 5 (1997) 539–563. doi:10.1093/jigpal/5.4.539. [4] W. Hodges, Some strange quantifiers, in: J. Mycielski, G. Rozenberg, A. Salomaa (Eds.), Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, Lecture Notes in Computer Science, Springer, Berlin, Heidelberg, 1997, pp. 51–65. doi:10.1007/3-540-63246-8_ 4. [5] J. Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic, London Mathematical Society Student Texts, Cambridge University Press, 2007. [6] J. Kivinen, H. Mannila, Approximate inference of functional dependencies from relations, Theoretical Computer Science 149 (1995) 129–149. doi:10.1016/0304-3975(95)00028-U, fourth International Conference on Database Theory (ICDT ’92). [7] J. Väänänen, The logic of approximate dependence, in: C. Başkent, L. S. Moss, R. Ramanujam (Eds.), Rohit Parikh on Logic, Language and Society, Springer International Publishing, Cham, 2017, pp. 227–234. doi:10.1007/978-3-319-47843-2_12. [8] Y. Huhtala, J. Kärkkäinen, P. Porkka, H. Toivonen, Tane: An efficient algorithm for discovering functional and approximate dependencies, The Computer Journal 42 (1999) 100–111. doi:10. 1093/comjnl/42.2.100. [9] M. Hannula, J. Kontinen, F. Yang, Logics in Team Semantics, 2026. Unpublished manuscript. [10] P. Galliani, J. Väänänen, On dependence logic, in: A. Baltag, S. Smets (Eds.), Johan van Benthem on Logic and Information Dynamics, Springer International Publishing, Cham, 2014, pp. 101–119. doi:10.1007/978-3-319-06025-5_4. [11] M. Häggblom, Axiomatizing variants of approximate inclusion, in: A.-Y. Turhan, J. Virtema (Eds.), Foundations of Information and Knowledge Systems, Springer Nature Switzerland, Cham, 2026, pp. 341–346. [12] J. Kontinen, Coherence and computational complexity of quantifier-free dependence logic formulas, Stud Logica 101 (2013) 267–291. doi:10.1007/S11225-013-9481-8. [13] A. Durand, M. Hannula, J. Kontinen, A. Meier, J. Virtema, Approximation and dependence via multiteam semantics, Ann. Math. Artif. Intell. 83 (2018) 297–320. doi:10.1007/S10472-017-9568-4. [14] S. S. Cosmadakis, P. C. Kanellakis, M. Y. Vardi, Polynomial-time implication problems for unary inclusion dependencies, J. ACM 37 (1990) 15–46. doi:10.1145/78935.78937. [15] M. Hirvonen, The implication problem for functional dependencies and variants of marginal distribution equivalences, ACM Trans. Comput. Logic 25 (2024). doi:10.1145/3677120. [16] T. Barlag, M. Hannula, J. Kontinen, N. Pardal, J. Virtema, Locally consistent k-relations: Entailment and axioms of functional dependence, 2026. arXiv:2505.11057. [17] T. J. Green, G. Karvounarakis, V. Tannen, Provenance semirings, in: Proceedings of the TwentySixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’07, Association for Computing Machinery, New York, NY, USA, 2007, p. 31–40. doi:10.1145/ 1265530.1265535. [18] M. Hannula, Conditional Independence on Semiring Relations, in: G. Cormode, M. Shekelyan (Eds.), 27th International Conference on Database Theory (ICDT 2024), volume 290 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2024, pp. 20:1–20:20. doi:10.4230/LIPIcs.ICDT.2024.20.

[19] M. Hirvonen, Implication problems over positive semirings, in: Foundations of Information and Knowledge Systems: 14th International Symposium, FoIKS 2026, Hanover, Germany, March 23–26, 2026, Proceedings, Springer-Verlag, Berlin, Heidelberg, 2026, p. 29–47. doi:10.1007/ 978-3-032-21540-6_3. [20] M. R. Garey, D. S. Johnson, L. J. Stockmeyer, Some simplified NP-complete graph problems, Theor. Comput. Sci. 1 (1976) 237–267. [21] N. Fröhlich, P. G. Kolaitis, A. Meier, Disjunctions of two dependence atoms, in: S. Guerrini, B. König (Eds.), 34th EACSL Annual Conference on Computer Science Logic, CSL 2026, Paris, France, February 23-28, 2026, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, pp. 10:1–10:21. doi:10.4230/LIPICS.CSL.2026.10.

Table 3 Types of error for 𝑣1 , 𝑣2 and 𝑣3 . We denote by ∙ any non zero value. type

𝑥

𝑣1

𝑣2

𝑣3

𝒜 ℬ 𝒞 𝒟 ℰ ℱ 𝒢

0 0 0 0 0 0 0

∙ ∙ ∙ ∙ 0 0 0

0 ∙ ∙ 0 0 ∙ ∙

0 0 ∙ ∙ ∙ ∙ 0

A. Proofs The appendix includes the proofs omitted from the main part of the paper. Proposition 3.2. Let Σ = {=0 (𝑥), = 1 (𝑥, 𝑣1 𝑣2 ), = 2 (𝑥, 𝑣1 𝑣3 ), = 2 (𝑣1 , 𝑦), =0 (𝑣2 𝑣3 , 𝑦)} be a set of ap8 8 8 proximate atoms. If 𝑋 |= Σ for any team 𝑋, then 𝑋 |= = 5 (𝑥, 𝑦). 16

Proof. Fix any team 𝑋 |= Σ. Notice that there are seven different types of ‘error’ assignments in 𝑋 for variables 𝑣1 , 𝑣2 and 𝑣3 , i. e., assignments which need to be removed to make = 1 (𝑥, 𝑣1 𝑣2 ) or = 2 (𝑥, 𝑣1 𝑣3 ) 8 8 true. These ‘error types’ are depicted in Table 3 and labelled 𝒜 to 𝒢. Note that each type corresponds to a non-empty subset of the set {𝑣1 , 𝑣2 , 𝑣3 }. We denote by 𝑎 the ratio of error type 𝒜 occurring in 𝑋, i. e., 𝑎=

|{𝑠 ∈ 𝑋 | 𝑠 is of error type 𝒜}| . |𝑋|

Likewise define the ratios 𝑏 to 𝑔. We have two constraints on these ratios given by Σ: 𝑎+𝑏+𝑐+𝑑+𝑓 +𝑔 ≤

1 8

the ratio of assignments which have to be removed for = 1 (𝑥, 𝑣1 𝑣2 ), and 8

2 𝑎+𝑏+𝑐+𝑑+𝑒+𝑓 ≤ . 8 the ratio of assignments which have to be removed for = 2 (𝑥, 𝑣1 𝑣3 ). 8

5 We now show, that 𝑝 = 16 is the smallest ratio to guarantee 𝑋 |= =𝑝 (𝑥, 𝑦). Here, there are two ways to show 𝑋 |= =𝑝 (𝑥, 𝑦). First, via =𝑞 (𝑥, 𝑣2 𝑣3 ) and =0 (𝑣2 𝑣3 , 𝑦) with unknown ratio 𝑞 = 𝑏 + 𝑐 + 𝑑 + 𝑒 + 𝑓 + 𝑔. Second, via =𝑟 (𝑥, 𝑣1 ) and = 2 (𝑣1 , 𝑦) with unknown ratio 𝑟 = 𝑎 + 𝑏 + 𝑐 + 𝑑. 8

5 With transitivity it follows that 𝑝 = min(𝑞 + 0, 𝑟 + 28 ). We need to show that 𝑝 ≤ 16 for any 𝑋, i. e., 5 we want to show the maximum value 𝑝 can take is less than or equal to 16 . Thus, we assume 𝑞 = 𝑟 + 82 as the worst case for 𝑝 and try to find the maximum. If we plug in the lower bounds we get

𝑏+𝑐+𝑑+𝑒+𝑓 +𝑔 =𝑎+𝑏+𝑐+𝑑+

2 8

which implies 𝑒 + 𝑓 + 𝑔 = 82 + 𝑎. From the first constraint, it follows that 𝑓 + 𝑔 ≤ 18 − 𝑟. Thus 𝑒 ≥ 18 + 𝑟 + 𝑎. From the second constraint, it follows that 𝑒 ≤ 28 − 𝑟 − 𝑓 . Together we have 2 1 −𝑟−𝑓 ≥ +𝑟+𝑎 8 8

1 − 𝑎 − 𝑓 ≥ 2𝑟 8 1 𝑎+𝑓 − ≥𝑟 16 2 1 1 5 Since we want to maximize 𝑟, assume 𝑎 = 𝑓 = 0 and 𝑟 = 16 . So we get 𝑝 = 28 + 16 as desired. = 16 Therefore any team 𝑋 that satisfies Σ must also satisfy = 5 (𝑥,𝑦) . 16

Theorem 4.1. Let Σ∪{=𝑝 (𝑥, 𝑦)} be a finite set of unary and 1-constancy rational approximate dependence atoms. If Σ |= =𝑝 (𝑥, 𝑦), then Σ ⊢A1 =𝑝 (𝑥, 𝑦). Proof. Let 𝐷0 be the set of variables in Σ ∪ {=𝑝 (𝑥, 𝑦)}, and let 𝑧0 be a variable that does not occur in any of the atoms in the set. We write ⊢ for a derivation using rules 𝐴11 , 𝐴21 , 𝐴31 , 𝐴61 and 𝐴71 . Suppose that Σ ̸⊢ =𝑝 (𝑥, 𝑦). By 𝐴11 and 𝐴71 , we can derive ⊢ =0 (𝑥, 𝑥) ⊢ =𝑝 (𝑥, 𝑥) and by 𝐴21 we can derive ⊢ =1 (𝑥, 𝑦), so it follows that 𝑦 is different from 𝑥 and that 𝑝 < 1. For each variable 𝑢 in 𝐷0 , define 𝑑(𝑢) to be the smallest rational number for which Σ ⊢ =𝑑(𝑢) (𝑥, 𝑢), which is guaranteed to exist since Σ is finite and ⊢ =1 (𝑥, 𝑢) always holds by 𝐴21 (also in the case that 𝑥 is the empty sequence). Let 𝑛 − 1 be the least common denominator for the approximations appearing in Σ ∪ {=𝑝 (𝑥, 𝑦)}. For ′ 𝑞′ each approximation 𝑞, let 𝑞 ′ be such that 𝑞 = 𝑛−1 , and similarly, we write 𝑑(𝑢)′ whenever 𝑑(𝑢) = 𝑑(𝑢) 𝑛−1 , etc. We build the counterexample team 𝑋 = {𝑠0 , . . . 𝑠𝑛−1 } such that for each variable 𝑤 ∈ 𝐷0 , {︃ 𝑖 if 𝑖 ≤ 𝑑(𝑤)′ , 𝑠𝑖 (𝑤) = 𝑑(𝑤)′ otherwise. Additionally, let 𝑠𝑖 (𝑧0 ) = 𝑖 for all 𝑖 ∈ {0, . . . , 𝑛 − 1}. The team is constructed such that for 𝑤 ∈ 𝐷0 , |𝑋[𝑤]| = 𝑑(𝑤)′ + 1, see Table 2 for an example. As a consequence, we have the equivalences: 𝑋 |= =𝑞 (𝑢, 𝑣) iff 𝑑(𝑣)′ − 𝑑(𝑢)′ ≤ 𝑞𝑛 iff |𝑋[𝑣] ∖ 𝑋[𝑢]| ≤ 𝑞𝑛.

(*)

Now, let us show that 𝑋 ̸|= =𝑝 (𝑥, 𝑦). Observe that Σ ⊢ =0 (𝑥, 𝑥) by 𝐴11 , so 𝑋[𝑥] = {0} if 𝑥 is a nonempty sequence and otherwise ∅, so |𝑋[𝑥]| ≤ 1. Furthermore, since Σ ̸⊢ =𝑝 (𝑥, 𝑦), we have by construction of 𝑋 that |𝑋[𝑦]| ≥ 𝑝′ + 2, hence |𝑋[𝑦] ∖ 𝑋[𝑥]| ≥ 𝑝′ + 1. Now, |𝑋[𝑦] ∖ 𝑋[𝑥]| 𝑝′ + 1 𝑝′ ≥ > = 𝑝, 𝑛 𝑛 𝑛−1 thus 𝑋 ̸|= =𝑝 (𝑥, 𝑦) follows by (*). It remains to show that for each =𝑟 (𝑢, 𝑣) ∈ Σ, 𝑋 |= =𝑟 (𝑢, 𝑣). By construction of the team, |𝑋[𝑢] ∖ 𝑋[𝑥]| = 𝑑(𝑢)′ . By rule 𝐴61 we have that Σ ⊢ =𝑑(𝑢)+𝑟 (𝑥, 𝑣), hence |𝑋[𝑣] ∖ 𝑋[𝑥]| ≤ 𝑑(𝑢)′ + 𝑟′ . Now |𝑋[𝑣] ∖ 𝑋[𝑢]| ≤ (𝑑(𝑢)′ + 𝑟′ ) − 𝑑(𝑢)′ = 𝑟′ = 𝑟(𝑛 − 1) < 𝑟𝑛, from which 𝑋 |= =𝑟 (𝑢, 𝑣) follows by (*). If we want to avoid the dummy variable 𝑧0 , identify the smallest 𝑘 for which 𝑠𝑘 ∈ 𝑋 and 𝑠𝑘 , 𝑠𝑙 are the same assignments restricted to the variables in 𝐷0 whenever 𝑘 < 𝑙 ≤ 𝑛 − 1. For each such 𝑠𝑙 , replace it with the assignment 𝑠𝑎𝑙 such that 𝑠𝑎𝑙 (𝑤) = 𝑎𝑙 for all 𝑤 ∈ 𝐷0 , where 𝑎𝑙 is a fresh value. Let 𝑌 be the team {𝑠0 , . . . , 𝑠𝑘 , 𝑠𝑎𝑘+1 , . . . 𝑠𝑎𝑛−1 }. Checking that 𝑌 is a counterexample team is similar to the proof for 𝑋. Theorem 5.1. The model checking problem for = 3 (𝑢, 𝑣) ∨ =0 (𝑥, 𝑦) is NP-complete. 13

Proof. Membership in NP is quite obvious. A non-deterministic machine can guess the split into 𝑋1 3 and 𝑋2 for the disjunction and additionally guess the removed 13 assignments 𝑌1 ⊆ 𝑋1 . Then the only thing left to do is to check whether 𝑋1 ∖ 𝑌1 |= =(𝑢, 𝑣) and 𝑋2 |= =(𝑥, 𝑦) is true. We continue with showing NP-hardness. To this end, we present a reduction from 3SAT. This reduction will use a similar construction as the reduction to the decision problem of Max2SAT presented in [20]. Let 𝜑 be an instance of 3SAT, i. e., a set of clauses (𝑎𝑖 ∨ 𝑏𝑖 ∨ 𝑐𝑖 ) for 𝑖 ∈ 𝐼, where each 𝑎𝑖 , 𝑏𝑖 and 𝑐𝑖 corresponds to a variable or its negation. First, split each clause (𝑎𝑖 ∨ 𝑏𝑖 ∨ 𝑐𝑖 ) into four subclauses of size 1 and six subclauses of size 2: (𝑎𝑖 ), (𝑏𝑖 ), (𝑐𝑖 ), (𝑑𝑖 ), (¯ 𝑎𝑖 ∨ ¯𝑏𝑖 ), (¯ 𝑎𝑖 ∨ 𝑐¯𝑖 ), (¯𝑏𝑖 ∨ ¯𝑏𝑖 ), (𝑎𝑖 ∨ 𝑑¯𝑖 ), (𝑏𝑖 ∨ 𝑑¯𝑖 ), (𝑐𝑖 ∨ 𝑑¯𝑖 ). The variable 𝑑𝑖 is a fresh variable introduced for each clause. As noted in [20] exactly seven of these ten clauses can be true when the original clause was satisfied, while at most six can be true if 𝑎𝑖 , 𝑏𝑖 and 𝑐𝑖 are false. We now construct a team 𝑋𝑖 such that the clause is satisfied if and only if a split between 17 of 20 assignments is possible. Let 𝑝 : Lit → {0, 1} be the function determining the parity of literals; while 𝑝¯ denotes the opposite, i.e., 𝑝¯(𝑥) = 1 − 𝑝(𝑥) for all 𝑥 ∈ Lit. Now, the team 𝑋𝑖⋃︀ is as depicted in Table 4. The full team of this reduction is then the union of all 𝑋𝑖 for 𝑖 ∈ 𝐼, i.e. 𝑋 = 𝑖∈𝐼 𝑋𝑖 . Correctness follows from [20] in a mostly straightforward manner. First, observe that =0 (𝑥, 𝑦) corresponds to assignments of the variables. That is, in the split 𝑋2 |= =0 (𝑥, 𝑦), each variable has to agree on its parity. Second, the split of = 3 (𝑢, 𝑣) can take one assignment from each subclause without 13 considering the approximation. Taking the approximation into account, this side of the split can take three additional assignments for a total of 13. Ordinarily, these three assignments would violate the dependence atom; however, they can be removed using the approximation. Thus, if seven of the ten subclauses are true by an assignment team, 𝑋𝑖 can be split. If this is true for all 𝑋𝑖 , then this also holds for 𝑋. In contrast, if only six assignments are true (as is the case for the non-satisfying assignment of the clause), then the team 𝑋𝑖 cannot be split, and therefore also 𝑋 cannot be split. Theorem 5.2. The model checking problem for = 1 (𝑥, 𝑦) is LOGSPACE-hard. 2

Proof. Define 𝑋 ⇆ as the team that swaps and renames the values of 𝑥 and 𝑦 in every assignment of 𝑋. For example, if 𝑠(𝑥) = 0, 𝑠(𝑦) = 1 is an assignment in 𝑋, then 𝑋 ⇆ contains 𝑠¯(𝑥) = 1̄, 𝑠¯(𝑦) = 0̄ as an assignment. Let 𝑋 be a team over {𝑥, 𝑦}. We reduce from the model checking problem for =(𝑥, 𝑦) ∨ =(𝑦, 𝑥), which is LOGSPACE-complete [21], by mapping 𝑋 to 𝑋 ∪ 𝑋 ⇆ . It is easy to see that this can be done by a first-order reduction. Table 4 Team 𝑋𝑖 given a clause over variables {𝑎, 𝑏, 𝑐}, with 𝑝(𝑥) the parity of 𝑥 in the clause; and 𝑝¯ the opposite.

𝑢

𝑣

𝑥

𝑦

𝑢

𝑣

𝑥

𝑦

𝑢

𝑣

𝑥

𝑦

𝑖0 𝑖0 𝑖1 𝑖1 𝑖2 𝑖2 𝑖3 𝑖3

0 1 0 1 0 1 0 1

𝑎 𝑎 𝑏 𝑏 𝑐 𝑐 𝑑𝑖 𝑑𝑖

𝑝(𝑎) 𝑝(𝑎) 𝑝(𝑏) 𝑝(𝑏) 𝑝(𝑐) 𝑝(𝑐) 1 1

𝑖4 𝑖4 𝑖5 𝑖5 𝑖6 𝑖6

0 1 0 1 0 1

𝑎 𝑏 𝑎 𝑐 𝑏 𝑐

𝑝¯(𝑎) 𝑝¯(𝑏) 𝑝¯(𝑎) 𝑝¯(𝑐) 𝑝¯(𝑏) 𝑝¯(𝑐)

𝑖7 𝑖7 𝑖8 𝑖8 𝑖9 𝑖9

0 1 0 1 0 1

𝑎 𝑑𝑖 𝑏 𝑑𝑖 𝑐 𝑑𝑖

𝑝(𝑎) 0 𝑝(𝑏) 0 𝑝(𝑐) 0

Assume 𝑋 |= =(𝑥, 𝑦) ∨ =(𝑦, 𝑥). Then there exists a split 𝑋 = 𝑋1 ∪ 𝑋2 such that 𝑋1 |= =(𝑥, 𝑦) and 𝑋2 |= =(𝑦, 𝑥). The same split also witnesses satisfaction for 𝑋 ⇆ , when swapping the teams, i.e., 𝑋2⇆ |= =(𝑥, 𝑦) and 𝑋1⇆ |= =(𝑦, 𝑥). Since the values in 𝑋 and 𝑋 ⇆ are disjoint 𝑋1 ∪ 𝑋2⇆ |= =(𝑥, 𝑦). Now, for the size of these subteams we have that |𝑋1 | + |𝑋2 | ≥ |𝑋| |𝑋1 | + |𝑋2⇆ | ≥ |𝑋|

(|𝑋2 | = |𝑋2⇆ |)

|𝑋1 ∪ 𝑋2⇆ | ≥ |𝑋| 1 |𝑋1 ∪ 𝑋2⇆ | ≥ · (|𝑋| + |𝑋 ⇆ |) 2 1 ⇆ |𝑋1 ∪ 𝑋2 | ≥ · |𝑋 ∪ 𝑋 ⇆ | 2

(𝑋1 ∩ 𝑋2⇆ = ∅) (|𝑋| = |𝑋 ⇆ |) (𝑋 ∩ 𝑋 ⇆ = ∅)

Therefore 𝑋 ∪ 𝑋 ⇆ |= = 1 (𝑥, 𝑦). 2 For the other direction assume 𝑋 ̸|= =(𝑥, 𝑦) ∨ =(𝑦, 𝑥). Then for all subteams 𝑋1 , 𝑋2 ⊆ 𝑋 with 𝑋1 |= =(𝑥, 𝑦) and 𝑋2 |= =(𝑦, 𝑥) we have that 𝑋 ∖ (𝑋1 ∪ 𝑋2 ) ̸= ∅. Therefore |𝑋1 | + |𝑋2 | < |𝑋|. The same is true for 𝑋 ⇆ , 𝑋1⇆ and 𝑋2⇆ . Thus |𝑋1 | + |𝑋2 | + |𝑋1⇆ | + |𝑋2⇆ | < |𝑋| + |𝑋 ⇆ | 2|𝑋1 | + 2|𝑋2⇆ | < |𝑋| + |𝑋 ⇆ | 1 |𝑋1 | + |𝑋2⇆ | < (|𝑋| + |𝑋 ⇆ |) 2 1 ⇆ |𝑋1 ∪ 𝑋2 | < |𝑋 ∪ 𝑋 ⇆ | 2 holds and implies 𝑋 ∪ 𝑋 ⇆ ̸|= = 1 (𝑥, 𝑦). 2

Related documents

• Approximate Functional Dependencies---Implication Problem Revisited#625150
• Approximate Functional Dependencies---Implication Problem Revisited#622877
• Generics and Weak Necessity#772724
• 16 CFR Part 1009 — General Statements of Policy or Interpretation#506100
• Ineliminable underdetermination and context-shifting arguments#87417