scholarly journals Unification and Anti-unification modulo Equational Theories

10.29007/65sh ◽  
2018 ◽  
Author(s):  
Santiago Escobar
Keyword(s):  
Automated Reasoning ◽  
Equational Theory ◽  
Unification Algorithm ◽  
Equational Unification ◽  
Equational Theories

Automated reasoning modulo an equational theory E is a fundamental technique in many applications. In this talk, we would present a narrowing-based equational unification algorithm for theories satisfying the finite variant property. We also talk about equational generalization, also called anti-unification

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.

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

scholarly journals Unification of Higher-order Patterns modulo Simple Syntactic Equational Theories

2000 ◽  
Vol Vol. 4 no. 1 ◽  
Author(s):  
Alexandre Boudet
Keyword(s):  
Higher Order ◽  
Unification Algorithm ◽  
First Order ◽  
Equational Theories ◽  
Order Case ◽  
International Audience ◽  
Syntactic Theories

International audience We present an algorithm for unification of higher-order patterns modulo simple syntactic equational theories as defined by Kirchner [14]. The algorithm by Miller [17] for pattern unification, refined by Nipkow [18] is first modified in order to behave as a first-order unification algorithm. Then the mutation rule for syntactic theories of Kirchner [13,14] is adapted to pattern E-unification. If the syntactic algorithm for a theory E terminates in the first-order case, then our algorithm will also terminate for pattern E-unification. The result is a DAG-solved form plus some equations of the form λ øverlinex.F(øverlinex) = λ øverlinex. F(øverlinex^π ) where øverlinex^π is a permutation of øverlinex When all function symbols are decomposable these latter equations can be discarded, otherwise the compatibility of such equations with the solved form remains open.

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.

scholarly journals Hierarchical Combination of Unication Algorithms (Extended Abstract)

10.29007/vb87 ◽  
2018 ◽  
Author(s):  
Serdar Erbatur ◽  
Deepak Kapur ◽  
Andrew M Marshall ◽  
Paliath Narendran ◽  
Christophe Ringeissen
Keyword(s):  
Combination Method ◽  
Critical Question ◽  
Unification Algorithm ◽  
Unification Theory ◽  
Combination Problem ◽  
Equational Theories ◽  
Novel Approach ◽  
Unification Algorithms

A critical question in unification theory is how to obtaina unification algorithm for the combination of non-disjointequational theories when there exists unification algorithmsfor the constituent theories. The problem is known to bedifficult and can easily be seen to be undecidable in thegeneral case. Therefore, previous work has focused onidentifying specific conditions and methods in which theproblem is decidable.We continue the investigation in this paper, building onprevious combination results and our own work.We are able to develop a novel approach to the non-disjointcombination problem. The approach is based on a new set ofrestrictions and combination method such that if the restrictionsare satisfied the method produces an algorithm for the unificationproblem in the union of non-disjoint equational theories.

scholarly journals Symbolic Analysis of Maude Theories with Narval

2019 ◽  
Vol 19 (5-6) ◽  
pp. 874-890
Author(s):  
MARÍA ALPUENTE ◽  
SANTIAGO ESCOBAR ◽  
JULIA SAPIÑA ◽  
DEMIS BALLIS
Keyword(s):  
Logic Programming ◽  
Reachability Analysis ◽  
Software Systems ◽  
Symbolic Computations ◽  
Fine Grained ◽  
Equational Unification ◽  
Symbolic Reasoning ◽  
Equational Theories ◽  
Graphical Tool ◽  
High Level

AbstractConcurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

Sign in / Sign up

Export Citation Format

Share Document