Return to search

Leveraging Information Contained in Theory Presentations

Building a large library of mathematical knowledge is a complex and labour-intensive
task. By examining current libraries of mathematics, we see that the human effort put
in building them is not entirely directed towards tasks that need human creativity.
Instead, a non-trivial amount of work is spent on providing definitions that could
have been mechanically derived.
In this work, we propose a generative approach to library building, so definitions
that can be automatically derived are computed by meta-programs. We focus our
attention on libraries of algebraic structures, like monoids, groups, and rings. These
structures are highly inter-related and their commonalities have been well-studied
in universal algebra. We use theory presentation combinators to build a library of
algebraic structures. Definitions from universal algebra and programming languages
meta-theory are used to derive library definitions of constructions, like homomorphisms
and term languages, from algebraic theory presentations. The result is an
interpreter that, given 227 theory expressions, builds a library of over 5000 definitions.
This library is, then, exported to Agda and Lean. / Dissertation / Doctor of Philosophy (PhD)

Identiferoai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/26272
Date January 2021
CreatorsSharoda, Yasmine
ContributorsCarette, Jacques, Farmer, William, Computer Science
Source SetsMcMaster University
LanguageEnglish
Detected LanguageEnglish
TypeThesis

Page generated in 0.0021 seconds