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 ❙
❚
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?
view v : ?S -> ?T =
include ?someInclude ❙
a = u ❙
b = v ❙
❚
Like option 1, but with implicit view ...
.
theory T =
include ?S = ?v ❙
❚
theory T =
include ?R ❙
u ❙
v ❙
total structure s : ?S =
include ?someInclude ❙
a = u ❙
b = v ❙
❚
❚
theory T =
include ?R ❙
u ❙
v ❙
realize ?S ❙
a = s ❙
b = t ❙
❚
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 ❙
❚