Showing 1–13 of 13 results for author: DeMeo, W

The Agda Universal Algebra Library, Part 2: Structure

Authors: William DeMeo

Abstract: The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from universal algebra, equational logic, and model theory, and as such… ▽ More The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from universal algebra, equational logic, and model theory, and as such provides many examples that exhibit the power of inductive and dependent types for representing and reasoning about mathematical structures and equational theories. In this paper, we describe the the types and proofs of the UALib that concern homomorphisms, terms, and subalgebras. △ Less

Submitted 16 March, 2021; originally announced March 2021.

Comments: 33 pages

MSC Class: 68V20 (Primary) 03C05 (Secondary) ACM Class: F.4.1

The Agda Universal Algebra Library, Part 1: Foundation

Authors: William DeMeo

Abstract: The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from general algebra and equational logic, including many examples that ex… ▽ More The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from general algebra and equational logic, including many examples that exhibit the power of inductive and dependent types for representing and reasoning about relations, algebraic structures, and equational theories. In this paper we discuss the logical foundations on which the library is built, and describe the types defined in the first 13 modules of the library. Special attention is given to aspects of the library that seem most interesting or challenging from a type theory or mathematical foundations perspective. △ Less

Submitted 20 April, 2021; v1 submitted 9 March, 2021; originally announced March 2021.

Comments: 32 pages + references

MSC Class: 68V20 (Primary) 03C05 (Secondary) ACM Class: F.4.1

A Machine-checked proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory

Authors: William DeMeo, Jacques Carette

Abstract: The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a… ▽ More The Agda Universal Algebra Library (agda-algebras) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. In this paper we draw on and explain many components of the agda-algebras library, which we extract into a single Agda module in order to present a self-contained formal and constructive proof of Birkhoff's HSP theorem in Martin-Löf dependent type theory. In the course of our presentation, we highlight some of the more challenging aspects of formalizing the basic definitions and theorems of universal algebra in type theory. Nonetheless, we hope this paper and the agda-algebras library serve as further evidence in support of the claim that dependent type theory and the Agda language, despite the technical demands they place on the user, are accessible to working mathematicians (such as ourselves) who possess sufficient patience and resolve to formally verify their results with a proof assistant. Indeed, the agda-algebras library now includes a substantial collection of definitions, theorems, and proofs from universal algebra, illustrating the expressive power of inductive and dependent types for representing and reasoning about general algebraic and relational structures. △ Less

Submitted 30 November, 2021; v1 submitted 25 January, 2021; originally announced January 2021.

Comments: This is the long (35 page) version of a paper submitted to TYPES 2021; the previous draft, [v2], was a comprehensive description of an old version of the Agda Universal Algebra Library (called UALib; ver. 1.0.0); the library was rewritten and renamed agda-algebras (ver. 2.0.0); this paper describes only a subset of the agda-algebras library that we used to prove Birkhoff's HSP theorem in Agda

MSC Class: 68V20 (Primary) 03C05 (Secondary) ACM Class: F.4.1

Polynomial-time Tests for Difference Terms in Idempotent Varieties

Authors: William DeMeo, Ralph Freese, Matthew Valeriote

Abstract: We consider the following practical question: given a finite algebra A in a finite language, can we efficiently decide whether the variety generated by A has a difference term? We answer this question (positively) in the idempotent case and then describe algorithms for constructing difference term operations. We consider the following practical question: given a finite algebra A in a finite language, can we efficiently decide whether the variety generated by A has a difference term? We answer this question (positively) in the idempotent case and then describe algorithms for constructing difference term operations. △ Less

Submitted 16 November, 2020; originally announced November 2020.

Journal ref: International Journal of Algebra and Computation, 29 (6):927--949, 2019

Constraint Satisfaction Problems over Finite Structures

Authors: Libor Barto, William DeMeo, Antoine Mottet

Abstract: We initiate a systematic study of the computational complexity of the Constraint Satisfaction Problem (CSP) over finite structures that may contain both relations and operations. We show the close connection between this problem and a natural algebraic question: which finite algebras admit only polynomially many homomorphisms into them? We give some sufficient and some necessary conditions for a f… ▽ More We initiate a systematic study of the computational complexity of the Constraint Satisfaction Problem (CSP) over finite structures that may contain both relations and operations. We show the close connection between this problem and a natural algebraic question: which finite algebras admit only polynomially many homomorphisms into them? We give some sufficient and some necessary conditions for a finite algebra to have this property. In particular, we show that every finite equationally nontrivial algebra has this property which gives us, as a simple consequence, a complete complexity classification of CSPs over two-element structures, thus extending the classification for two-element relational structures by Schaefer (STOC'78). We also present examples of two-element structures that have bounded width but do not have relational width (2,3), thus demonstrating that, from a descriptive complexity perspective, allowing operations leads to a richer theory. △ Less

Submitted 29 January, 2021; v1 submitted 10 October, 2020; originally announced October 2020.

ACM Class: F.1.3; F.4.1

Journal ref: LICS 2021 pages 1--13

Bounded homomorphisms and finitely generated fiber products of lattices

Authors: William DeMeo, Peter Mayr, Nik Ruskuc

Abstract: We investigate when fiber products of lattices are finitely generated and obtain a new characterization of bounded lattice homomorphisms onto lattices satisfying a property we call Dean's condition (D) which arises from Dean's solution to the word problem for finitely presented lattices. In particular, all finitely presented lattices and those satisfying Whitman's condition satisfy (D). For lattic… ▽ More We investigate when fiber products of lattices are finitely generated and obtain a new characterization of bounded lattice homomorphisms onto lattices satisfying a property we call Dean's condition (D) which arises from Dean's solution to the word problem for finitely presented lattices. In particular, all finitely presented lattices and those satisfying Whitman's condition satisfy (D). For lattice epimorphisms $g\colon A\to D$, $h\colon B\to D$, where $A$, $B$ are finitely generated and $D$ satisfies (D), we show the following: If $g$ and $h$ are bounded, then their fiber product (pullback) $C=\{(a,b)\in A\times B\ |\ g(a)=h(b)\}$ is finitely generated. While the converse is not true in general, it does hold when $A$ and $B$ are free. As a consequence we obtain an (exponential time) algorithm to decide boundedness for finitely presented lattices and their finitely generated sublattices satisfying (D). This generalizes an unpublished result of Freese and Nation. △ Less

Submitted 26 November, 2019; v1 submitted 18 July, 2019; originally announced July 2019.

Journal ref: International Journal of Algebra and Computation Vol. 30, No. 04, pp. 693-710 (2020)

The Commutator as Least Fixed Point of a Closure Operator

Authors: William DeMeo

Abstract: We present a description of the (non-modular) commutator, inspired by that of Kearnes in~\cite[p.~930]{MR1358491}, that provides a simple recipe for computing the commutator. We present a description of the (non-modular) commutator, inspired by that of Kearnes in~\cite[p.~930]{MR1358491}, that provides a simple recipe for computing the commutator. △ Less

Submitted 8 March, 2017; originally announced March 2017.

Universal Algebraic Methods for Constraint Satisfaction Problems

Authors: Clifford Bergman, William DeMeo

Abstract: After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if the algebra has a Taylor term operation. Despite the tremendous achievements in this area (including recently announce proofs of the general conjecture), there… ▽ More After substantial progress over the last 15 years, the "algebraic CSP-dichotomy conjecture" reduces to the following: every local constraint satisfaction problem (CSP) associated with a finite idempotent algebra is tractable if and only if the algebra has a Taylor term operation. Despite the tremendous achievements in this area (including recently announce proofs of the general conjecture), there remain examples of small algebras with just a single binary operation whose CSP resists direct classification as either tractable or NP-complete using known methods. In this paper we present some new methods for approaching such problems, with particular focus on those techniques that help us attack the class of finite algebras known as "commutative idempotent binars" (CIBs). We demonstrate the utility of these methods by using them to prove that every CIB of cardinality at most 4 yields a tractable CSP. △ Less

Submitted 17 January, 2022; v1 submitted 9 November, 2016; originally announced November 2016.

MSC Class: Primary: 08A70; Secondary: 03C05; 08A30; 08A40

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 19, 2022) lmcs:2568

Isotopic algebras with non-isomorphic congruence lattices

Authors: William DeMeo

Abstract: We give examples of pairs of isotopic algebras with non-isomorphic congruence lattices. This answers the question of whether all isotopic algebras have isomorphic congruence lattices. We give examples of pairs of isotopic algebras with non-isomorphic congruence lattices. This answers the question of whether all isotopic algebras have isomorphic congruence lattices. △ Less

Submitted 10 February, 2013; v1 submitted 30 January, 2013; originally announced January 2013.

Comments: 3 pages; comments welcome

Journal ref: Algebra universalis volume 72, pages 295--298 (2014)

Dedekind's Transposition Principle for lattices of equivalence relations

Authors: William DeMeo

Abstract: We prove a version of Dedekind's Transposition Principle that holds in lattices of equivalence relations. We prove a version of Dedekind's Transposition Principle that holds in lattices of equivalence relations. △ Less

Submitted 28 January, 2013; originally announced January 2013.

Comments: 3 pages; comments welcome

Interval enforceable properties of finite groups

Authors: William DeMeo

Abstract: We propose a classification of group properties according to whether they can be deduced from the assumption that a group's subgroup lattice contains an interval isomorphic to some lattice. We are able to classify a few group properties as being "interval enforceable" in this sense, and we establish that other properties satisfy a weaker notion of "core-free interval enforceable." We also show tha… ▽ More We propose a classification of group properties according to whether they can be deduced from the assumption that a group's subgroup lattice contains an interval isomorphic to some lattice. We are able to classify a few group properties as being "interval enforceable" in this sense, and we establish that other properties satisfy a weaker notion of "core-free interval enforceable." We also show that if there exists a group property and its negation that are both core-free interval enforceable, this would settle an important open question in universal algebra. △ Less

Submitted 7 April, 2014; v1 submitted 9 May, 2012; originally announced May 2012.

Comments: 11 pages

MSC Class: 20E15 (Primary) 20D30; 20B10; 06B15; 08A30

Expansions of finite algebras and their congruence lattices

Authors: William DeMeo

Abstract: We present a novel approach to the construction of new finite algebras and describe the congruence lattices of these algebras. Given a finite algebra $(B_0, \dots)$, let $B_1, B_2, \dots, B_K$ be sets that either intersect $B_0$ or intersect each other at certain points. We construct an \emph{overalgebra} $(A, F_A)$, by which we mean an expansion of $(B_0, \dots)$ with universe… ▽ More We present a novel approach to the construction of new finite algebras and describe the congruence lattices of these algebras. Given a finite algebra $(B_0, \dots)$, let $B_1, B_2, \dots, B_K$ be sets that either intersect $B_0$ or intersect each other at certain points. We construct an \emph{overalgebra} $(A, F_A)$, by which we mean an expansion of $(B_0, \dots)$ with universe $A = B_0 \cup B_1 \cup \cdots \cup B_K$, and a certain set $F_A$ of unary operations that includes mappings $e_i$ satisfying $e_i^2 = e_i$ and $e_i(A) = B_i$, for $0\leq i \leq K$. We explore two such constructions and prove results about the shape of the new congruence lattices $Con(A, F_A)$ that result. Thus, descriptions of some new classes of finitely representable lattices is one contribution of this paper. Another, perhaps more significant contribution is the announcement of a novel approach to the discovery of new classes of representable lattices, the full potential of which we have only begun to explore. △ Less

Submitted 8 October, 2013; v1 submitted 5 May, 2012; originally announced May 2012.

Comments: 22 pages, 10 figures

MSC Class: 08A30 (Primary) 06B10; 08A60 (Secondary)

Journal ref: Algebra Universalis, 69, pp. 257--278, 2013

Congruence lattices of finite algebras

Authors: William J. DeMeo

Abstract: An important and long-standing open problem in universal algebra asks whether every finite lattice is isomorphic to the congruence lattice of a finite algebra. Until this problem is resolved, our understanding of finite algebras is incomplete, since, given an arbitrary finite algebra, we cannot say whether there are any restrictions on the shape of its congruence lattice. By a well known result of… ▽ More An important and long-standing open problem in universal algebra asks whether every finite lattice is isomorphic to the congruence lattice of a finite algebra. Until this problem is resolved, our understanding of finite algebras is incomplete, since, given an arbitrary finite algebra, we cannot say whether there are any restrictions on the shape of its congruence lattice. By a well known result of Palfy and Pudlak, the problem would be solved if we could prove the existence of a finite lattice that is not an interval in the lattice of subgroups of a finite group. Thus the problem of characterizing congruence lattices of finite algebras is closely related to the problem of characterizing intervals in subgroup lattices. In this work, we review a number of methods for finding a finite algebra with a given congruence lattice, including searching for intervals in subgroup lattices. We also consider methods for proving that algebras with a given congruence lattice exist without actually constructing them. By combining these well known methods with a new method we have developed, and with much help from computer software like the UACalc and GAP, we prove that with one possible exception every lattice with at most seven elements is isomorphic to the congruence lattice of a finite algebra. As such, we have identified the unique smallest lattice for which there is no known representation. We examine this exceptional lattice in detail, and prove results that characterize the class of algebras that could possibly represent this lattice. We conclude with what we feel are the most interesting open questions surrounding this problem and discuss possibilities for future work. △ Less

Submitted 7 May, 2012; v1 submitted 19 April, 2012; originally announced April 2012.

Comments: Ph.D. Thesis, 114 pages, 29 figures

MSC Class: 08A30 (Primary) 06B15; 20E15 (Secondary)