During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries. Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Lightweight Realms

  • Michael Kohlhase,
  • Florian Rabe,
  • Marcel Schütz

摘要

During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries. Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.