Patterns & Idioms in Formalizations - UniFormal/uniformal.github.io Wiki

Original URL: https://github.com/UniFormal/uniformal.github.io/wiki/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: 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 ❙
❚