Patterns & Idioms in Formalizations

Common Patterns of writing MMT theories and views

Expressing views and assignments

Consider the theories below. The goal is to map a = u and b = v somehow. We discuss several options in the following.

theory R = // ... ❙ ❚

theory S =
  include ?R ❙
  a ❙
  b ❙
❚

theory T =
  include ?R ❙
  u ❙
  v ❙
❚

Discussion

		Constants from S?	Allowed Partiality	Partiality Semantics
1	view	translatable via view (not supported so far)	only dependency-closed partiality	unassigned constants cannot be mapped
2	implicit view	implicitly translated	^	^
3	T + defined include		^	unassigned constants not included?
4	T + structure		arbitrary partiality	unassigned constants get copied over to a qualified copy
5	T + realize	translatable by induced view and duplicate constants	none	N/A

When to use which?

• option 1: should be the default option to use
• option 2: ?
• option 3: ?
• option 4: if you want to to include another theory, but set one constant to something within the current theory ("amalgation", "pushout" semantics)
• option 5: ?

Option 1: a view

view v : ?S -> ?T =
  include ?someInclude ❙
  a = u ❙
  b = v ❙
❚

Option 2: implicit view

Like option 1, but with implicit view ....

Option 4: view + defined include

theory T =
  include ?S = ?v ❙
❚

Option 4: a structure

theory T =
  include ?R ❙
  u ❙
  v ❙
  
  total structure s : ?S =
    include ?someInclude ❙
    a = u ❙
    b = v ❙
  ❚
❚

Option 5: a realize

theory T =
  include ?R ❙
  u ❙
  v ❙

  realize ?S ❙
  a = s ❙
  b = t ❙
❚

"Union in View Codomain" Pattern

Imagine you want to do a view v : ?S -> (?T union ?SomeMoreCodomain). That isn't possible in MMT (yet). Instead you can do:

theory SomeMoreCodomain = // ... ❙ ❚

theory S =
  include ?R ❙
  a ❙
  b ❙
❚

theory T =  
  u ❙
  v ❙

  include ?SomeMoreCodomain ❙

  realize ?S ❙
  a = u ❙
  b = v ❙
❚