Notes about my work
NEWS! (2021 Nov 30) The unabridged version of our TYPES2021 submission is now available on the arXiv (preprint link). The paper describes our new formal proof of Birkhoff's variety theorem in Martin-Löf type theory using the Agda proof assistant.
More complete documentation of the Agda Universal Algebra Library (agda-algebras) is available on the main ualib.org website.
The library is open source and downloadable from the ualib/agda-algebras GitHub repository.
(2021 Jan 20) I'm pleased to announce that on 12 January 2021 I achieved my goal of constructing a formal, machine-checked proof of Birkhoff's variety theorem in dependent type theory using the Agda programming language.
Birkhoff's celebrated theorem asserts that a class K of algebraic structures is closed under the taking of homomorphic images, subalgebras, and arbitrary products if and only if K is defined by a set of equations.
To the best of my knowledge, this is the first time Birkhoff's Theorem has been formulated and proved in dependent type theory and verified with a proof assistant.
The Agda Universal Algebra Library has undergone a makeover to make it more concise and elegant and to correct some flaws in the previous version. The latest release is version 2.03.
The main project webpage (ualib.org) is the best source for up-to-date documentation.
the Agda Universal Algebra Library gitlab repository is where one can download (clone or fork) and install the source code of the Agda UALib.
- The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory; (CoRR) available on arXiv [cs.LO] abs/2101.10166.
- Constraint Satisfaction Problems over Finite Structures, with Libor Barto and Antoine Mottet; (submitted to LICS 2021) available on arXiv [cs.LO] abs/2010.04958.
- Bounded homomorphisms and finitely generated fiber products of lattices, with Peter Mayr and Nik Ruskuc; International Journal of Algebra and Computation, (30):693--710, 2020; available on arXiv [math.LO] abs/1907.08046.
- Polynomial-time tests for difference terms in idempotent varieties, with Ralph Freese and Matthew Valeriote; International Journal of Algebra and Computation, (29):927--949, 2019; available on arXiv [math.LO] abs/2011.07879.
- Universal algebraic methods for constraint satisfaction problems, with Clifford Bergman; (accepted for publication in Logical Methods in Computer Science) available on arXiv [cs.LO] abs/1611.02867.
- Isotopic algebras with nonisomorphic congruence lattices; Algebra Universalis, (72):295--298, 2014; available on arXiv [math.RA] abs/1301.7481
- Expansions of finite algebras & their congruence lattices; Algebra Universalis, (69):257--278, 2013; available on arXiv [math.RA] abs/1205.1106.
- Proceedings of Algebras and Lattices in Hawaii 2018, (editor) with Kira Adaricheva, Jennifer Hyndman; available at Lulu.com
- Topics in nonabelian harmonic analysis and dsp applications; (best paper award) Proceedings of the International Symposium on Musical Acoustics, Nara, Japan 2004.
- Characterizing musical signals with Wigner-Ville interferences; Proceedings of the International Computer Music Conference, Gothenburg, Sweden 2002.
- Approximating eigenvalues of large stochastic matrices; Proceedings of the 8th Copper Mt. Conference on Iterative Methods, Colorado, 1998.
Summary of Research Activities
Research areasThese are the areas I'm most passionate about.
- Logic, universal algebra, model theory, category theory;
- Formalization of mathematics in Agda and Lean;
- Computational complexity of constraint satisfaction problems and deciding properties of general structures;
- Functional programming in Scala/Spark for algebra, machine learning, and Big Data.
- Logic and Foundations. The Agda Universal Algebra Library and Birkhoff's Theorem in Martin-Löf Dependent Type Theory (PREPRINT)
- Computational Complexity. The Complexity of the Homomorphism Problem for Boolean structures, with Libor Barto and Antoine Motet (PREPRINT)
- Lattice Theory. Bounded homomorphisms and finitely generated fiber products of lattices, with Peter Mayr and Nik Ruskuc (PREPRINT)
- Equational Logic. Polynomial-time Tests for Difference Terms in Idempotent Varieties, with Ralph Freese and Matt Valeriote (PREPRINT)
- Computational Complexity. Universal Algebraic Methods for Constraint Satisfaction Problems, with Cliff Bergman (PREPRINT)
Formal Foundations for Informal Mathematics ResearchAgda proof assistant and programming language. The project title is Formal Foundations for Informal Mathematics Research and two significant outputs of the project are the paper The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory and the software library that paper describes.
Bounded Lattices and Fiber Productsthe book by Freese, Jezek and Nation for the definition of a bounded lattice homomorphism.) and I presented a proof of one direction of the conjecture at the Algebras and Lattices in Hawaii conference in 2018. By early 2019 we proved the converse and thus confirmed our conjecture. Mayr and Ruskuc had in mind an application for the fact that our new result is equivalent to a characterization of fiber products of lattices. A paper presenting our theorem characterizing bounded lattices was published in January of 2020 in the International Journal of Algebra and Computation, 30 (4):693--710, 2020. (PREPRINT)
Equational Logic and ComplexityPREPRINT)
Algebras and Algorithms, Structure and Complexity
In 2015, I joined a group of 8 other scientists to form a universal algebra research group and secure a 3-year NSF grant for the project, Algebras and Algorithms, Structure and Complexity Theory. Our focus is on fundamental problems at the confluence of logic, algebra, and computer science, and our main goal is to deepen understanding of how to determine the complexity of certain types of computational problems. We focus primarily on classes of algebraic problems whose solutions yield new information about the complexity of CSPs. These include scheduling problems, resource allocation problems, and problems reducible to solving systems of linear equations. CSPs are theoretically solvable, but some are not solvable efficiently. Our work provides procedures for deciding whether a given instance of a CSP is tractable or intractable, and we develop efficient algorithms for finding solutions in the tractable cases.40-page manuscript co-authored with Cliff Bergman (Iowa State Univ) and entitled Universal Algebraic Methods for Constraint Satisfaction Problems. This was recently accepted for publication in the journal Logical Methods in Computer Science (LMCS) (PREPRINT)
The Universal Algebra Calculator
See this post