Trace monoid

Last updated

In computer science, a trace is a set of strings, wherein certain letters in the string are allowed to commute, but others are not. It generalizes the concept of a string, by not forcing the letters to always be in a fixed order, but allowing certain reshufflings to take place. Traces were introduced by Pierre Cartier and Dominique Foata in 1969 to give a combinatorial proof of MacMahon's master theorem. Traces are used in theories of concurrent computation, where commuting letters stand for portions of a job that can execute independently of one another, while non-commuting letters stand for locks, synchronization points or thread joins. [1]

Contents

The trace monoid or free partially commutative monoid is a monoid of traces. In a nutshell, it is constructed as follows: sets of commuting letters are given by an independency relation. These induce an equivalence relation of equivalent strings; the elements of the equivalence classes are the traces. The equivalence relation then partitions up the free monoid (the set of all strings of finite length) into a set of equivalence classes; the result is still a monoid; it is a quotient monoid and is called the trace monoid. The trace monoid is universal, in that all dependency-homomorphic (see below) monoids are in fact isomorphic.

Trace monoids are commonly used to model concurrent computation, forming the foundation for process calculi. They are the object of study in trace theory. The utility of trace monoids comes from the fact that they are isomorphic to the monoid of dependency graphs; thus allowing algebraic techniques to be applied to graphs, and vice versa. They are also isomorphic to history monoids, which model the history of computation of individual processes in the context of all scheduled processes on one or more computers.

Trace

Let denote the free monoid, that is, the set of all strings written in the alphabet . Here, the asterisk denotes, as usual, the Kleene star. An independency relation on then induces a (symmetric) binary relation on , where if and only if there exist , and a pair such that and . Here, and are understood to be strings (elements of ), while and are letters (elements of ).

The trace is defined as the reflexive transitive closure of . The trace is thus an equivalence relation on , and is denoted by , where is the dependency relation corresponding to that is and conversely Clearly, different dependencies will give different equivalence relations.

The transitive closure implies that if and only if there exists a sequence of strings such that and and for all . The trace is stable under the monoid operation on (concatenation) and is therefore a congruence relation on .

The trace monoid, commonly denoted as , is defined as the quotient monoid

The homomorphism

is commonly referred to as the natural homomorphism or canonical homomorphism. That the terms natural or canonical are deserved follows from the fact that this morphism embodies a universal property, as discussed in a later section.

One will also find the trace monoid denoted as where is the independency relation. Confusingly, one can also find the commutation relation used instead of the independency relation (it differs by including all the diagonal elements).

Examples

Consider the alphabet . A possible dependency relation is

The corresponding independency is

Therefore, the letters commute. Thus, for example, a trace equivalence class for the string would be

The equivalence class is an element of the trace monoid.

Properties

The cancellation property states that equivalence is maintained under right cancellation. That is, if , then . Here, the notation denotes right cancellation, the removal of the first occurrence of the letter a from the string w, starting from the right-hand side. Equivalence is also maintained by left-cancellation. Several corollaries follow:

A strong form of Levi's lemma holds for traces. Specifically, if for strings u, v, x, y, then there exist strings and such that for all letters and such that occurs in and occurs in , and

[2]

Universal property

A dependency morphism (with respect to a dependency D) is a morphism

to some monoid M, such that the "usual" trace properties hold, namely:

1. implies that
2. implies that
3. implies that
4. and imply that

Dependency morphisms are universal, in the sense that for a given, fixed dependency D, if is a dependency morphism to a monoid M, then M is isomorphic to the trace monoid . In particular, the natural homomorphism is a dependency morphism.

Normal forms

There are two well-known normal forms for words in trace monoids. One is the lexicographic normal form, due to Anatolij V. Anisimov and Donald Knuth, and the other is the Foata normal form due to Pierre Cartier and Dominique Foata who studied the trace monoid for its combinatorics in the 1960s. [3]

Unicode's Normalization Form Canonical Decomposition (NFD) is an example of a lexicographic normal form - the ordering is to sort consecutive characters with non-zero canonical combining class by that class.

Trace languages

Just as a formal language can be regarded as a subset of , the set of all possible strings, so a trace language is defined as a subset of all possible traces.

Alternatively, but equivalently, a language is a trace language, or is said to be consistent with dependency D if

where

is the trace closure of a set of strings.

See also

Notes

  1. Sándor & Crstici (2004) p.161
  2. Proposition 2.2, Diekert and Métivier 1997.
  3. Section 2.3, Diekert and Métivier 1997.

Related Research Articles

<span class="mw-page-title-main">Original proof of Gödel's completeness theorem</span>

The proof of Gödel's completeness theorem given by Kurt Gödel in his doctoral dissertation of 1929 is not easy to read today; it uses concepts and formalisms that are no longer used and terminology that is often obscure. The version given below attempts to represent all the steps in the proof and all the important ideas faithfully, while restating the proof in the modern language of mathematical logic. This outline should not be considered a rigorous proof of the theorem.

In algebra, a homomorphism is a structure-preserving map between two algebraic structures of the same type. The word homomorphism comes from the Ancient Greek language: ὁμός meaning "same" and μορφή meaning "form" or "shape". However, the word was apparently introduced to mathematics due to a (mis)translation of German ähnlich meaning "similar" to ὁμός meaning "same". The term "homomorphism" appeared as early as 1892, when it was attributed to the German mathematician Felix Klein (1849–1925).

<span class="mw-page-title-main">Monoid</span> Algebraic structure with an associative operation and an identity element

In abstract algebra, a branch of mathematics, a monoid is a set equipped with an associative binary operation and an identity element. For example, the nonnegative integers with addition form a monoid, the identity element being 0.

<span class="mw-page-title-main">Pauli matrices</span> Matrices important in quantum mechanics and the study of spin

In mathematical physics and mathematics, the Pauli matrices are a set of three 2 × 2 complex matrices which are Hermitian, involutory and unitary. Usually indicated by the Greek letter sigma, they are occasionally denoted by tau when used in connection with isospin symmetries.

In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set A can be thought of as being a "generic" algebraic structure over A: the only equations that hold between elements of the free object are those that follow from the defining axioms of the algebraic structure. Examples include free groups, tensor algebras, or free lattices.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

In mathematics and computer science, the syntactic monoid of a formal language is the smallest monoid that recognizes the language .

<span class="mw-page-title-main">Fermi's interaction</span> Mechanism of beta decay proposed in 1933

In particle physics, Fermi's interaction is an explanation of the beta decay, proposed by Enrico Fermi in 1933. The theory posits four fermions directly interacting with one another. This interaction explains beta decay of a neutron by direct coupling of a neutron with an electron, a neutrino and a proton.

Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.

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, the Fubini–Study metric is a Kähler metric on projective Hilbert space, that is, on a complex projective space CPn endowed with a Hermitian form. This metric was originally described in 1904 and 1905 by Guido Fubini and Eduard Study.

In mathematical physics, the gamma matrices, , also called the Dirac matrices, are a set of conventional matrices with specific anticommutation relations that ensure they generate a matrix representation of the Clifford algebra Cl1,3(). It is also possible to define higher-dimensional gamma matrices. When interpreted as the matrices of the action of a set of orthogonal basis vectors for contravariant vectors in Minkowski space, the column vectors on which the matrices act become a space of spinors, on which the Clifford algebra of spacetime acts. This in turn makes it possible to represent infinitesimal spatial rotations and Lorentz boosts. Spinors facilitate spacetime computations in general, and in particular are fundamental to the Dirac equation for relativistic spin-1/2 particles.

In quantum mechanics, notably in quantum information theory, fidelity is a measure of the "closeness" of two quantum states. It expresses the probability that one state will pass a test to identify as the other. The fidelity is not a metric on the space of density matrices, but it can be used to define the Bures metric on this space.

In computer science, in particular in concurrency theory, a dependency relation is a binary relation on a finite domain , symmetric, and reflexive; i.e. a finite tolerance relation. That is, it is a finite set of ordered pairs , such that

In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process. The history monoid provides a set of synchronization primitives for providing rendezvous points between a set of independently executing processes or threads.

<span class="mw-page-title-main">Stokes' theorem</span> Theorem in vector calculus

Stokes's theorem, also known as Kelvin–Stokes theorem after Lord Kelvin and George Stokes, the fundamental theorem for curls or simply the curl theorem, is a theorem in vector calculus on R3. Given a vector field, the theorem relates the integral of the curl of the vector field over some surface, to the line integral of the vector field around the boundary of the surface. The classical Stokes' theorem can be stated in one sentence: The line integral of a vector field over a loop is equal to the flux of its curl through the enclosed surface.

ACE — the collection of units, implementing both a public key encryption scheme and a digital signature scheme. Corresponding names for these schemes — «ACE Encrypt» and «ACE Sign». Schemes are based on Cramer-Shoup public key encryption scheme and Cramer-Shoup signature scheme. Introduced variants of these schemes are intended to achieve a good balance between performance and security of the whole encryption system.

<span class="mw-page-title-main">Symmetry in quantum mechanics</span> Properties underlying modern physics

Symmetries in quantum mechanics describe features of spacetime and particles which are unchanged under some transformation, in the context of quantum mechanics, relativistic quantum mechanics and quantum field theory, and with applications in the mathematical formulation of the standard model and condensed matter physics. In general, symmetry in physics, invariance, and conservation laws, are fundamentally important constraints for formulating physical theories and models. In practice, they are powerful methods for solving problems and predicting what can happen. While conservation laws do not always give the answer to the problem directly, they form the correct constraints and the first steps to solving a multitude of problems.

In mathematical physics, the Gordon decomposition of the Dirac current is a splitting of the charge or particle-number current into a part that arises from the motion of the center of mass of the particles and a part that arises from gradients of the spin density. It makes explicit use of the Dirac equation and so it applies only to "on-shell" solutions of the Dirac equation.

In first-order arithmetic, the induction principles, bounding principles, and least number principles are three related families of first-order principles, which may or may not hold in nonstandard models of arithmetic. These principles are often used in reverse mathematics to calibrate the axiomatic strength of theorems.

References

General references

Seminal publications