KnowledgeBase » SEMINAR » ID = 390

Formalizing the Theory Mechanism in NuPRL

by Jason Hickey
1993-1994

A "theory" in NuPRL is a collection of axioms, theorems, and definitions about a topic being studied formally. The mechanism we use currently is informal (a theory is whatever lies between theory_delimiters), and the namespace is flat. This presents a problem when we wish to extend theories. For instance, if we have a theory about monoids, we may wish to extend the theory by adding an axiom about commutativity, so we can study Abelian monoids. Ideally, the theorems, axioms, and definitions of the theory of monoids would be inherited automatically by the new theory.

Some of these problems can be solved by formalizing the theory mechanism. Borrowing from ideas in object-oriented programming, and pushing the type theory very hard, we can give a type to a theory that provides a hierarchical namespace and automatic inheritance. Furthermore, given formal theories, we can reason about them, and ask questions like "when are two theories equal?" The properties of the formal theory become especially clear in the context of abstract algebra, which I will use for most of my examples.