Global, Regional, and Local Contexts
Rabe F (2025)
Publication Type: Conference contribution
Publication year: 2025
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 16136 LNCS
Pages Range: 240-257
Conference Proceedings Title: Lecture Notes in Computer Science
Event location: Brasilia, BRA
ISBN: 9783032070203
DOI: 10.1007/978-3-032-07021-0_14
Abstract
We introduce UniFormal, a formal language for mathematical knowledge representation that continues the evolution of OpenMath and MMT. It is motivated by the lack of identifiers in these languages that exhibit the scoping behavior needed for, e.g., the fields in a record or the variables in a polynomial. Its core feature is a separation of identifiers and associated contexts into three levels: The global context maintains the usual toplevel declarations that can be imported across libraries and nested packages via qualified names. The local context maintains the usual α-renamable bound variables with narrow syntactic scope. The novel regional context sits in between these and maintains the identifiers of the current theory. A stack of regional contexts is used to allow for expressions that move between regions, e.g., when applying a theory morphism to transport an expression from one theory to another. We present a minimal language in this style, focusing on the general intuitions underlying the design. We anticipate it to be extended flexibly towards specialized aspects of mathematical knowledge such as programming languages or theorem provers to enable interoperability through their shared core concepts. This approach has already proved successful in the design and implementation of a UniFormal programming language.
Authors with CRIS profile
How to cite
APA:
Rabe, F. (2025). Global, Regional, and Local Contexts. In Valeria de Paiva, Peter Koepke (Eds.), Lecture Notes in Computer Science (pp. 240-257). Brasilia, BRA, BR: Springer Science and Business Media Deutschland GmbH.
MLA:
Rabe, Florian. "Global, Regional, and Local Contexts." Proceedings of the 18th International Conference on Intelligent Computer Mathematics, CICM 2025, Brasilia, BRA Ed. Valeria de Paiva, Peter Koepke, Springer Science and Business Media Deutschland GmbH, 2025. 240-257.
BibTeX: Download