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 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

Naive set theory is any of several theories of sets used in the discussion of the foundations of mathematics. Unlike axiomatic set theories, which are defined using formal logic, naive set theory is defined informally, in natural language. It describes the aspects of mathematical sets familiar in discrete mathematics, and suffices for the everyday use of set theory concepts in contemporary mathematics.

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.

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. Propositions that contain no logical connectives are called atomic propositions.

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 mathematics, there are several equivalent ways of defining the real numbers. One of them is that they form a complete ordered field that does not contain any smaller complete ordered field. Such a definition does not prove that such a complete ordered field exists, and the existence proof consists of constructing a mathematical structure that satisfies the definition.

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 (1935). Smooth Moufang loops have an associated algebra, the Malcev algebra, similar in some ways to how a Lie group has an associated Lie algebra.

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" of points.

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.

In mathematics, set-theoretic topology is a subject that combines set theory and general topology. It focuses on topological questions that are independent of Zermelo–Fraenkel set theory (ZFC).

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.

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.