Armstrong's axioms

Last updated

Armstrong's axioms are a set of references (or, more precisely, inference rules) used to infer all the functional dependencies on a relational database. They were developed by William W. Armstrong in his 1974 paper. [1] The axioms are sound in generating only functional dependencies in the closure of a set of functional dependencies (denoted as ) when applied to that set (denoted as ). They are also complete in that repeated application of these rules will generate all functional dependencies in the closure .

Contents

More formally, let denote a relational scheme over the set of attributes with a set of functional dependencies . We say that a functional dependency is logically implied by , and denote it with if and only if for every instance of that satisfies the functional dependencies in , also satisfies . We denote by the set of all functional dependencies that are logically implied by .

Furthermore, with respect to a set of inference rules , we say that a functional dependency is derivable from the functional dependencies in by the set of inference rules , and we denote it by if and only if is obtainable by means of repeatedly applying the inference rules in to functional dependencies in . We denote by the set of all functional dependencies that are derivable from by inference rules in .

Then, a set of inference rules is sound if and only if the following holds:

that is to say, we cannot derive by means of functional dependencies that are not logically implied by . The set of inference rules is said to be complete if the following holds:

more simply put, we are able to derive by all the functional dependencies that are logically implied by .

Axioms (primary rules)

Let be a relation scheme over the set of attributes . Henceforth we will denote by letters , , any subset of and, for short, the union of two sets of attributes and by instead of the usual ; this notation is rather standard in database theory when dealing with sets of attributes.

Axiom of reflexivity

If is a set of attributes and is a subset of , then holds . Hereby, holds [] means that functionally determines .

If then .

Axiom of augmentation

If holds and is a set of attributes, then holds . It means that attribute in dependencies does not change the basic dependencies.

If , then for any .

Axiom of transitivity

If holds and holds , then holds .

If and , then .

Additional rules (Secondary Rules)

These rules can be derived from the above axioms.

Decomposition

If then and .

Proof

1. (Given)
2. (Reflexivity)
3. (Transitivity of 1 & 2)

Composition

If and then .

Proof

1. (Given)
2. (Given)
3. (Augmentation of 1 & A)
4. (Decomposition of 3)
5. (Augmentation of 2 & X)
6. (Decomposition of 5)
7. (Union 4 & 6)

Union

If and then .

Proof

1. (Given)
2. (Given)
3. (Augmentation of 2 & X)
4. (Augmentation of 1 & Z)
5. (Transitivity of 3 and 4)

Pseudo transitivity

If and then .

Proof

1. (Given)
2. (Given)
3. (Augmentation of 1 & Z)
4. (Transitivity of 3 and 2)

Self determination

for any . This follows directly from the axiom of reflexivity.

Extensivity

The following property is a special case of augmentation when .

If , then .

Extensivity can replace augmentation as axiom in the sense that augmentation can be proved from extensivity together with the other axioms.

Proof

1. (Reflexivity)
2. (Given)
3. (Transitivity of 1 & 2)
4. (Extensivity of 3)
5. (Reflexivity)
6. (Transitivity of 4 & 5)

Armstrong relation

Given a set of functional dependencies , an Armstrong relation is a relation which satisfies all the functional dependencies in the closure and only those dependencies. Unfortunately, the minimum-size Armstrong relation for a given set of dependencies can have a size which is an exponential function of the number of attributes in the dependencies considered. [2]

Related Research Articles

First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.

The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives representing the truth functions of conjunction, disjunction, implication, equivalence, and negation. Some sources include other connectives, as in the table below.

The relational model (RM) is an approach to managing data using a structure and language consistent with first-order predicate logic, first described in 1969 by English computer scientist Edgar F. Codd, where all data is represented in terms of tuples, grouped into relations. A database organized in terms of the relational model is a relational database.

Cox's theorem, named after the physicist Richard Threlkeld Cox, is a derivation of the laws of probability theory from a certain set of postulates. This derivation justifies the so-called "logical" interpretation of probability, as the laws of probability derived by Cox's theorem are applicable to any proposition. Logical probability is a type of Bayesian probability. Other forms of Bayesianism, such as the subjective interpretation, are given other justifications.

In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.

In relational database theory, a functional dependency is a constraint between two sets of attributes in a relation from a database. In other words, a functional dependency is a constraint between two attributes in a relation. Given a relation R and sets of attributes , X is said to functionally determineY if and only if each X value in R is associated with precisely one Y value in R; R is then said to satisfy the functional dependency XY. Equivalently, the projection is a function, i.e. Y is a function of X. In simple words, if the values for the X attributes are known, then the values for the Y attributes corresponding to x can be determined by looking them up in any tuple of R containing x. Customarily X is called the determinant set and Y the dependent set. A functional dependency FD: XY is called trivial if Y is a subset of X.

In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.

In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collection of sets defined by a formula whose quantifiers range only over sets. NBG can define classes that are larger than sets, such as the class of all sets and the class of all ordinals. Morse–Kelley set theory (MK) allows classes to be defined by formulas whose quantifiers range over classes. NBG is finitely axiomatizable, while ZFC and MK are not.

In functional analysis and related branches of mathematics, the Banach–Alaoglu theorem states that the closed unit ball of the dual space of a normed vector space is compact in the weak* topology. A common proof identifies the unit ball with the weak-* topology as a closed subset of a product of compact sets with the product topology. As a consequence of Tychonoff's theorem, this product, and hence the unit ball within, is compact.

In mathematics, a Moufang loop is a special kind of algebraic structure. It is similar to a group in many ways but need not be associative. Moufang loops were introduced by Ruth Moufang. Smooth Moufang loops have an associated algebra, the Malcev algebra, similar in some ways to how a Lie group has an associated Lie algebra.

The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus.

Tarski's axioms are an axiom system for Euclidean geometry, specifically for that portion of Euclidean geometry that is formulable in first-order logic with identity. As such, it does not require an underlying set theory. The only primitive objects of the system are "points" and the only primitive predicates are "betweenness" and "congruence". The system contains infinitely many axioms.

In set theory, -induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In database theory, a multivalued dependency is a full constraint between two sets of attributes in a relation.

<span class="mw-page-title-main">Ordered vector space</span> Vector space with a partial order

In mathematics, an ordered vector space or partially ordered vector space is a vector space equipped with a partial order that is compatible with the vector space operations.

In abstract algebra, a partially ordered ring is a ring (A, +, ·), together with a compatible partial order, that is, a partial order on the underlying set A that is compatible with the ring operations in the sense that it satisfies:

A canonical cover for F is a set of dependencies such that F logically implies all dependencies in , and logically implies all dependencies in F.

The counting lemmas this article discusses are statements in combinatorics and graph theory. The first one extracts information from -regular pairs of subsets of vertices in a graph , in order to guarantee patterns in the entire graph; more explicitly, these patterns correspond to the count of copies of a certain graph in . The second counting lemma provides a similar yet more general notion on the space of graphons, in which a scalar of the cut distance between two graphs is correlated to the homomorphism density between them and .

In mathematics, specifically the field of abstract algebra, Bergman's Diamond Lemma is a method for confirming whether a given set of monomials of an algebra forms a -basis. It is an extension of Gröbner bases to non-commutative rings. The proof of the lemma gives rise to an algorithm for obtaining a non-commutative Gröbner basis of the algebra from its defining relations. However, in contrast to Buchberger's algorithm, in the non-commutative case, this algorithm may not terminate.

References

  1. William Ward Armstrong: Dependency Structures of Data Base Relationships , page 580-583. IFIP Congress, 1974.
  2. Beeri, C.; Dowd, M.; Fagin, R.; Statman, R. (1984). "On the Structure of Armstrong Relations for Functional Dependencies" (PDF). Journal of the ACM. 31: 30–46. CiteSeerX   10.1.1.68.9320 . doi:10.1145/2422.322414. Archived from the original (PDF) on 2018-07-23.