Reference. Leveraging the Information Contained in Theory Presentations
A theorem prover without an extensive library is much less useful to its potential users. Algebra, the study of algebraic structures, is a core component of such libraries. Algebraic theories also are themselves structured, the study of which was started as Universal Algebra. Various constructions (homomorphism, term algebras, products, etc) and their properties are both universal and constructive. Thus they are ripe for being automated. Unfortunately, current practice still requires library builders to write these by hand. We first highlight specific redundancies in libraries of existing systems. Then we describe a framework for generating these derived concepts from theory definitions. We demonstrate the usefulness of this framework on a test library of 227 theories.
Cite
Cited by (1)
Frex: Dependently Typed Algebraic Simplification allais-2025-frex
We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library’s dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.
Cites 35 works (1 here)
With notes (1)
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages carette-2009-finally
We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
External (34)
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (2020)
- Haskell: an advanced, purely functional programming language (website) (2020)
- List of mathematical structures (2020)
- Haskell lens library, version 4.19.1 (2020)
- A language feature to unbundle data at will (short paper) (2019)
- Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal (2019)
- The Lean mathematical library (2019)
- Universal Algebra and Applications in Theoretical Computer Science (2018)
- Formalization of Universal Algebra in Agda (2018)
- Building on the Diamonds between Theories: Theory Presentation Combinators (2018)
- Deriving via: or, how to turn hand-written instances into an anti-pattern (2018)
- Type checking through unification (2016)
- Experience Implementing a Performant Category-Theory Library in Coq (2014)
- Theory Presentation Combinators (2012)
- Universal Algebra (chapter of Foundations of Algebraic Specification and Formal Software Development) (2012)
- A generative geometric kernel (2011)
- The MathScheme Library: Some Preliminary Experiments (2011)
- A generic deriving mechanism for Haskell (2010)
- Developing the Algebraic Hierarchy with Type Classes in Coq (2010)
- Packaging Mathematical Structures (2009)
- Template meta-programming for Haskell (2002)
- A Constructive Algebraic Hierarchy in Coq (2002)
- Universal Algebra in Type Theory (1999)
- Principles of Maude (1996)
- Little theories (1992)
- Universal algebra in higher types (1992)
- Telescopic mappings in typed lambda calculus (1991)
- Universal algebra (Meinke and Tucker) (1991)
- Fundamentals of Algebraic Specification 1 (1985)
- A Course in Universal Algebra (1981)
- A Treatise on Universal Algebra: With Applications (1898)
- Logic system interrelationships
- Tog, a prototypical implementation of dependent types
- Coq user contributions - algebra library