sTeX-MMT-Discrepancies

[Jazzpirate]

Here's the list I promised, @mkohlhase @frabe :

• Terms in sTeX can occur outside of declaration components - i.e. anywhere ("top-level terms"), but should be checked by the Solver, (possibly) have URIs etc.

  • current solution: Signature/Language module split; top-level terms are represented as definientia for constants in the language module (only if term is a ComplexTerm)

• sTeX has \usemodule

  • current solution: \usemodule is represented as an include in the language module. This makes sense in that the symbols imported via usemodule should not occur in components of declared symbols (which would imply a "real" dependency) - but maybe we would want them to be allowed to? e.g. they could be allowed in (formal) definientia, but just not further exported in TeX. Could add the includes to the signature theory instead.

• statements (definition/example/theorem/sparagraph/...) - narrative elements that should be queryable for, amenable to (to some extent) being modified by "narrative theory morphisms" and/or document context (numbering, possibly choice of notations etc.)

  • current solution: as with top-level terms; add them to the language module as constants with the HTML as OMFOREIGN-definiens, add relational for e.g. is-example-of, is-definition-of etc.

• notations for any symbol can be introduced anywhere where the symbol is in scope; this includes language-specific notations (e.g. ggT(...) vs gcd(...))

  • current solution: again constants with HTML of the notation as OMFOREIGN-definiens + relational info

• variables can be declared and used local to the current TeX-Group

  • current solution: declarations are tracked during import and references are abstracted away according to MMT rules (or roles?) at the outside of top-level terms and components; e.g. by lambda in definientia, pi/forall in types, by default, by \bind in the sTeX meta theory. The binder symbols used should be set depending on e.g. a precise meta theory: \importmodule{?HOL} would give me the symbols, \begin{smodule}[meta=?HOL] would do the same, but also set HOLs lambda/pi symbols as the ones to use for abstracting away variables. Drawback: the declaration of the variable itself is not represented as OMDoc.

• implicit variables: in MMT surface syntax, these are determined by notations. In sTeX, semantic macros have fixed arities though, so either we force users to always provide all arguments and hide them in the notations, or we allow for the same semantic macro to have different arities depending on the notation (dangerous, ugly to implement, unintuitive to use), or:

  • current solution: variables not occuring in terms directly, but in types/definientia of other variables are considered implicit arguments; they are abstracted away on the outside of a component using \implicitbind and become part of the type or definiens of a constant, rather than the notation. This means that every occurence of a symbol in a term requires a loopup of the type/definens to check for an implicitbind and introduce fresh variables to be solved accordingly.

• sTeX allows for bound variables in any argument position; this is incompatible with OMBINDC currently

  • current solution: sTeX-specific HOAS with wrapper SOMB() for a OMBINDC(...) where the argument positions are attached to the bound variables

• Module types: will become more ubiquitous in sTeX as the most convenient way to represent structured dependent data. Should be represented as a structural feature that generates a module/record type, but derived declarations can't "include" other derived declarations, because MMT currently does not support theory morphisms between derived declarations.

  • current solution: nested theory instead, add a constant for the MOD type (marked as GeneratedFrom the nested module)

• need conservative extensions; primarily for module types (e.g. to subsequently add the defined subtraction/division-operation to a group)

  • current solution: tracked in TeX, a conservative extension bar to a module type ?foo redefines \foo from generatingOMS(foo) to RecordMerge(?foo, MOD ?bar) instead. This is necessary, since there can be multiple conservative extensions distributed among multiple modules, so we can't guarantee that the current usage of \foo in a given document context corresponds to any specific nested module with precisely all the conservative extensions of ?foo.

• Notable: can fully or partially instantiate module types, either way represented as a RecordMerge of the module type with an anonymous record, which gives us a (structural) subtype. An actual instance is identified with the (structural) subtype with all fields defined, i.e. a singleton type.

• More stuff related to statements:

  • terms t in a sdefinition marked with \definiens{t} are attached to the corresponding constant c as definiens, iff c does not yet have a definiens and c is declared in the same module as the definition. Otherwise, it generates an equality rule t==c.
  • the sassertion environment with name= and (optionally) \assume{t1}...\assume{tn} and \conclusion{t} generates a new constant of type DED t1 -> ... -> DED tn -> t for some -> and DED provided via MMT rules (or roles, as above) => can also be used to provide types to declarations.
  • the proof-environment behaves basically like sdefinition, but with intermediate steps; structural feature will/should build up the proof term from individual steps

• More stuff related to HOAS et al:

  • lots of metadata on all (sub)terms to keep track of e.g. the term before applying HOAS things (for subsequent presentation as MathML), the precise notation used etc.