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)
| Identifer | oai:union.ndltd.org:mcmaster.ca/oai:macsphere.mcmaster.ca:11375/26272 |
| Date | January 2021 |
| Creators | Sharoda, Yasmine |
| Contributors | Carette, Jacques, Farmer, William, Computer Science |
| Source Sets | McMaster University |
| Language | English |
| Detected Language | English |
| Type | Thesis |
Page generated in 0.0017 seconds