Theories are simply named groups of declarations. Examples for theories are first-order or higher-order theories, logics, type theories, logical frameworks. Their conrete syntax is
<body> is a sequence of declarations. The context available to any specific declaration is everything provided by previous declarations, specifically theory inclusions and everything provided by the meta theory.
The meta theory statement is optional and behaves like a theory inclusion.
Theories can be nested, like this:
in which case the visible context of both the inner theory as well as
<previousbody>, i.e. the inner theory can see all previous declarations of the outer theory, but at no point can the outer theory see inside the inner theory (unless explicitely included).
Given two theories
B, a view from
B maps all declarations in
A to expressions over symbols in
B, while preserving typing judgments. i.e. if
|- a : tpA in
v:A->B is a view, then
|- v(a) : v(tpA). Hence, views are truth preserving.
A is the domain of
B is the codomain.
Their conrete syntax is
<assignments> is a list of assignment declarations. Their syntax looks like this:
<name> has to be a symbol declared in (the dependency closure of)
<term> has to be a well-formed term over symbols in
<codomain> preserving typing judgments.
Modules can have arbitrary metadata, similar to how declarations can have arbitrary metadata associated to them:
theory MyTheory = myAnnotationKey ❙ myAnnotationKey2 ❙ myAnnotationValue ❙ myAnnotationValue2❙ meta ?myAnnotationKey ?myAnnotationValue ❙ meta ?myAnnotationKey2 ?myAnnotationValue2❙ ❚ // Also possible in views: ❚ view v : ?MyTheory -> ... = // Do the symbols come from the domain theory? ❙ meta ?myAnnotationKey ?myAnnotationValue ❙ meta ?myAnnotationKey2 ?myAnnotationValue2❙ ❚
See the corresponding section on metadata for declarations on how each meta line is structured. Note that you can have multiple metadatums on the same theory with the same key. In the implementation the metadatums form a list, hence this is allowed.
The semantics of the large scale structure of developments in MMT is computed in the category of theories and theory morphisms.
Every development in MMT yields a specific category of theories and morphisms.
Among those, MMT distinguishes the implicit morphisms.
For any two theories
B, there may be at most one implicit morphism from
The implicit morphisms are the following:
Thus, technically the implicit morphisms form a thin broad subcategory of the category of theories and morphisms.
The semantics of an implicit morphism
B is that every declaration of
A is also visible to
B, i.e., any well-formed term
A is also well-formed over
The meaning of
Bis an implicit morphism, which maps every term to itself. Thus, the effect of an include from
Bis that every term of
Acan be used in
Bwith the same meaning.
c:a=tto a theory
Tthat she does not have write access to. She could declare a theory
T. But then the new declaration would only be available in theories that use
T2. Instead, she would like to extend
Titself from the outside, i.e., without changing it. She can achieve that by declaring a theory
c:aand an implicit view from
c=t. Then she can use