Equational Theories of Tropical Semirings

2001 ◽  
Vol 8 (21) ◽  
Author(s):  
Luca Aceto ◽  
Zoltán Ésik ◽  
Anna Ingólfsdóttir
Keyword(s):  
Equational Theory ◽  
Finite Basis ◽  
Free Algebras ◽  
Real Numbers ◽  
Binary Operations ◽  
Equational Theories ◽  
Tropical Semiring

This paper studies the equational theory of various exotic semirings presented in the literature. Exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. Two prime examples of such structures are the <em> (max,+) semiring</em> and the <em>tropical semiring</em>. It is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. For each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.

scholarly journals On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers

1999 ◽  
Vol 6 (22) ◽  
Author(s):  
Luca Aceto ◽  
Zoltán Ésik ◽  
Anna Ingólfsdóttir
Keyword(s):  
Process Algebra ◽  
Equational Theory ◽  
Finite Basis ◽  
Alternative Proof ◽  
Equational Logic ◽  
Basic Process ◽  
Natural Numbers ◽  
Binary Operations ◽  
Keywords And Phrases ◽  
Trace Equivalence

<p>This paper shows that the collection of identities in two variables<br />which hold in the algebra N of the natural numbers with constant<br />zero, and binary operations of sum and maximum does not have a<br />finite equational axiomatization. This gives an alternative proof of the<br />non-existence of a finite basis for N - a result previously obtained by<br />the authors. As an application of the main theorem, it is shown that<br />the language of Basic Process Algebra (over a singleton set of actions),<br />with or without the empty process, has no finite omega-complete equational<br />axiomatization modulo trace equivalence.</p><p><br />AMS Subject Classification (1991): 08A70, 08B05, 03C05, 68Q70.<br />ACM Computing Classification System (1998): F.4.1.<br />Keywords and Phrases: Equational logic, varieties, complete axiomatizations,<br />process algebra, trace equivalence.</p>

Finite axiomatizability for equational theories of computable groupoids

1989 ◽  
Vol 54 (3) ◽  
pp. 1018-1022 ◽  
Author(s):  
Peter Perkins
Keyword(s):  
Binary Operation ◽  
Finite Algebra ◽  
Equational Theory ◽  
Natural Numbers ◽  
Finite Axiomatizability ◽  
Finite Algebras ◽  
Equational Theories ◽  
Primitive Recursive ◽  
Positive Integers ◽  
Recursive Set

A computable groupoid is an algebra ‹N, g› where N is the set of natural numbers and g is a recursive (total) binary operation on N. A set L of natural numbers is a computable list of computable groupoids iff L is recursive, ‹N, ϕe› is a computable groupoid for each e ∈ L, and e ∈ L whenever e codes a primitive recursive description of a binary operation on N.Theorem 1. Let L be any computable list of computable groupoids. The set {e ∈ L: the equational theory of ‹N, ϕe› is finitely axiomatizable} is not recursive.Theorem 2. Let S be any recursive set of positive integers. A computable groupoid GS can be constructed so that S is inifinite iff GS has a finitely axiomatizable equational theory.The problem of deciding which finite algebras have finitely axiomatizable equational theories has remained open since it was first posed by Tarski in the early 1960's. Indeed, it is still not known whether the set of such finite algebras is recursively (or corecursively) enumerable. McKenzie [7] has shown that this question of finite axiomatizability for any (finite) algebra of finite type can be reduced to that for a (finite) groupoid.

A note on equational theories

2000 ◽  
Vol 65 (4) ◽  
pp. 1705-1712 ◽  
Author(s):  
Markus Junker
Keyword(s):  
Equational Theory ◽  
Order Theory ◽  
Point Of View ◽  
Unpublished Manuscript ◽  
Positive Information ◽  
Closed Sets ◽  
First Order Theory ◽  
Equational Theories ◽  
Definable Sets ◽  
Image Position

Several attempts have been done to distinguish “positive” information in an arbitrary first order theory, i.e., to find a well behaved class of closed sets among the definable sets. In many cases, a definable set is said to be closed if its conjugates are sufficiently distinct from each other. Each such definition yields a class of theories, namely those where all definable sets are constructible, i.e., boolean combinations of closed sets. Here are some examples, ordered by strength:Weak normality describes a rather small class of theories which are well understood by now (see, for example, [P]). On the other hand, normalization is so weak that all theories, in a suitable context, are normalizable (see [HH]). Thus equational theories form an interesting intermediate class of theories. Little work has been done so far. The original work of Srour [S1, S2, S3] adopts a point of view that is closer to universal algebra than to stability theory. The fundamental definitions and model theoretic properties can be found in [PS], though some easy observations are missing there. Hrushovski's example of a stable non-equational theory, the first and only one so far, is described in the unfortunately unpublished manuscript [HS]. In fact, it is an expansion of the free pseudospace constructed independently by Baudisch and Pillay in [BP] as an example of a strictly 2-ample theory. Strong equationality, defined in [Hr], is also investigated in [HS].

scholarly journals Polynomial density of commutative semigroups

1993 ◽  
Vol 48 (1) ◽  
pp. 151-162 ◽  
Author(s):  
Andrzej Kisielewicz ◽  
Norbert Newrly
Keyword(s):  
Commutative Semigroup ◽  
Equational Theory ◽  
Full Description ◽  
Commutative Semigroups ◽  
Equational Theories

An algebra is said to be polynomially n−dense if all equational theories extending the equational theory of the algebra with constants have a relative base consisting of equations in no more than n variables. In this paper, we investigate polynomial density of commutative semigroups. In particular, we prove that, for n > 1, a commutative semigroup is (n − 1)-dense if and only if its subsemigroup consisting of all n−factor-products is either a monoid or a union of groups of a bounded order. Moreover, a commutative semigroup is 0-dense if and only if it is a bounded semilattice. For semilattices, we give a full description of the corresponding lattices of equational theories.

scholarly journals THE FINITE BASIS PROBLEM FOR THE MONOID OF TWO-BY-TWO UPPER TRIANGULAR TROPICAL MATRICES

2016 ◽  
Vol 94 (1) ◽  
pp. 54-64 ◽  
Author(s):  
YUZHU CHEN ◽  
XUN HU ◽  
YANFENG LUO ◽  
OLGA SAPIR
Keyword(s):  
Finite Basis ◽  
Finite Basis Problem ◽  
Basis Problem ◽  
Tropical Semiring ◽  
Bicyclic Monoid ◽  
Nonfinitely Based

For each positive $n$, let $\mathbf{u}_{n}\approx \boldsymbol{v}_{n}$ denote the identity obtained from the Adjan identity $(xy)(yx)(xy)(xy)(yx)\approx (xy)(yx)(yx)(xy)(yx)$ by substituting $(xy)\rightarrow (x_{1}x_{2}\ldots x_{n})$ and $(yx)\rightarrow (x_{n}\ldots x_{2}x_{1})$. We show that every monoid which satisfies $\mathbf{u}_{n}\approx \boldsymbol{v}_{n}$ for each positive $n$ and generates a variety containing the bicyclic monoid is nonfinitely based. This implies that the monoid $U_{2}(\mathbb{T})$ (respectively, $U_{2}(\overline{\mathbb{Z}})$) of two-by-two upper triangular tropical matrices over the tropical semiring $\mathbb{T}=\mathbb{R}\cup \{-\infty \}$ (respectively, $\overline{\mathbb{Z}}=\mathbb{Z}\cup \{-\infty \}$) is nonfinitely based.

The Uniqueness of the Field of Complex Numbers

1969 ◽  
Vol 62 (5) ◽  
pp. 369-372
Author(s):  
William Wynne Willson
Keyword(s):  
Complex Numbers ◽  
Real Numbers ◽  
Binary Operations ◽  
Ordered Pairs

IN A recent paper in this journal Dorman, Tollefson, and Stein1 considered under what binary operations of addition and multiplication the set S of ordered pairs of real numbers becomes a field. In particular they showed that the three following assumptions lead to infinitely many possible fields, which they classified into three types. The assumptions are these:

scholarly journals On equational theories of semilattices with operators

1990 ◽  
Vol 42 (1) ◽  
pp. 57-70 ◽  
Author(s):  
J. Ježek ◽  
P. PudláK ◽  
J. Tůma
Keyword(s):  
Equational Theory ◽  
Algebraic Lattice ◽  
Equational Theories ◽  
Algebraic Lattices

In 1986, Lampe presented a counterexample to the conjecture that every algebraic lattice with a compact greatest element is isomorphic to the lattice of extensions of an equational theory. In this paper we investigate equational theories of semi-lattices with operators. We construct a class of lattices containing all infinitely distributive algebraic lattices with a compact greatest element and closed under the operation of taking the parallel join, such that every element of the class is isomorphic to the lattice of equational theories, extending the theory of a semilattice with operators.

The equational theory of CA3 is undecidable

1980 ◽  
Vol 45 (2) ◽  
pp. 311-316 ◽  
Author(s):  
Roger Maddux
Keyword(s):  
Equational Theory ◽  
Cylindric Algebra ◽  
Relation Algebras ◽  
Cylindric Algebras ◽  
3 Dimensional ◽  
First Order ◽  
Equational Theories ◽  
Order Language ◽  
Theoretic Proof

There is no algorithm for determining whether or not an equation is true in every 3-dimensional cylindric algebra. This theorem completes the solution to the problem of finding those values of α and β for which the equational theories of CAα and RCAβ are undecidable. (CAα and RCAβ are the classes of α-dimensional cylindric algebras and representable β-dimensional cylindric algebras. See [4] for definitions.) This problem was considered in [3]. It was known that RCA0 = CA0 and RCA1 = CA1 and that the equational theories of these classes are decidable. Tarski had shown that the equational theory of relation algebras is undecidable and, by utilizing connections between relation algebras and cylindric algebras, had also shown that the equational theories of CAα and RCAβ are undecidable whenever 4 ≤ α and 3 ≤ β. (Tarski's argument also applies to some varieties K ⊆ RCAβ with 3 ≤ β and to any variety K such that RCAα ⊆ K ⊆ CAα and 4 ≤ α.)Thus the only cases left open in 1961 were CA2, RCA2 and CA3. Shortly there-after Henkin proved, in one of Tarski's seminars at Berkeley, that the equational theory of CA2 is decidable, and Scott proved that the set of valid sentences in a first-order language with only two variables is recursive [11]. (For a more model-theoretic proof of Scott's theorem see [9].) Scott's result is equivalent to the decidability of the equational theory of RCA2, so the only case left open was CA3.

Two Unusual Representations for the Set of Real Numbers

1970 ◽  
Vol 63 (8) ◽  
pp. 665
Author(s):  
Sanderson M. Smith
Keyword(s):  
Rational Numbers ◽  
Real Numbers ◽  
The Real ◽  
Binary Operations

The rational numbers and the real numbers are both fields under the binary operations of addition and multiplication.

How to prove decidability of equational theories with second-order computation analyser SOL

2019 ◽  
Vol 29 ◽  
Author(s):  
MAKOTO HAMANA
Keyword(s):  
Programming Language ◽  
Equational Theory ◽  
Second Order ◽  
Language Theory ◽  
Analysis Tool ◽  
Monoidal Categories ◽  
Equational Theories ◽  
Algebraic Theories ◽  
Order Algebraic ◽  
Π Calculus

Abstract We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool, i.e. Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories. To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of the second-order computation in a non-trivial manner. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and λ-calculi, Plotkin and Power’s theory of states and bits, and Stark’s theory of π-calculus. We also demonstrate how this methodology can solve the coherence of monoidal categories.

Sign in / Sign up

Export Citation Format

Share Document