The MMT Language and System


Modules occur in documents level, contain declarations and have an associated MMT URI of the form <NAMESPACE>?<NAME>, with the namespace of the current document. Modules are delimited with the symbol `\GS`


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

`theory <name> : <metatheory> = <body> \GS`

, where <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:

`theory <outer> : <metatheory1> =	<previousbody> theory <inner> : <metatheory2> =	<innerbody>	\GS	<laterbody> \GS`

in which case the visible context of both the inner theory as well as <laterbody> is <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 A and B, a view from A to B maps all declarations in A to expressions over symbols in B, while preserving typing judgments. i.e. if |- a : tpA in A and v:A->B is a view, then |- v(a) : v(tpA). Hence, views are truth preserving. A is the domain of v and B is the codomain.

Their conrete syntax is

`view <name> : <domain> -> <codomain> = <assignments> \GS`

, where <assignments> is a list of assignment declarations. Their syntax looks like this:

`<name> = <term> \RS`

In assignments, <name> has to be a symbol declared in (the dependency closure of) <domain>, whereas <term> has to be a well-formed term over symbols in <codomain> preserving typing judgments.