Commit 7776e94a authored by ComFreek's avatar ComFreek

add theories on semantics equivalence

parent 1c44128e
namespace latin:/wuvtest/structurecolimit❚
fixmeta ur:?LF❚
theory Syntax =
theory Semantics =
include ?Syntax ❙
theory EquivalenceOfSemantics =
structure syn : ?Syntax = ❚
structure sem1 : ?Semantics =
include ?Syntax ❘ = ?EquivalenceOfSemantics?syn ❙
structure sem2 : ?Semantics =
include ?Syntax ❘ = ?EquivalenceOfSemantics?syn ❙
theory EquivalenceOfSemantics2 =
// include ?Syntax ❙
structure sem1 : ?Semantics =
include ?Syntax ❙
structure sem2 : ?Semantics =
include ?Syntax ❙
\ No newline at end of file
......@@ -67,10 +67,29 @@ theory CompositionalTranslations =
// Notions of equivalence ❚
theory DeductionEquivalence =
structure L : ?FormalSystem = ❚
theory FormalSystemEquivalence =
include ?ScratchSFOL ❙
structure L : ?FormalSystem =
// here and below in the other structures force that we maintain the same base logic
as in the outer theory ❙
include ?ScratchSFOL ❙
// can I force Sem1|?FormalSystem = L? same for Sem2? ❙
structure Sem1 : ?FormalSystem =
include ?ScratchSFOL ❙
include ?FormalSystem ❘ = ?FormalSystemEquivalence?L ❙
structure Sem2 : ?FormalSystem =
include ?ScratchSFOL ❙
include ?FormalSystem ❘ = ?FormalSystemEquivalence?L ❙
theory DeductionEquivalence =
include ?FormalSystemEquivalence ❙
structure Sem1 : ?Deduction = ❚
structure Sem2 : ?Deduction = ❚
......@@ -78,9 +97,8 @@ theory DeductionEquivalence =
theory ComputationEquivalence =
structure L : ?FormalSystem = ❚
include ?FormalSystemEquivalence ❙
// can I force Sem1|?FormalSystem = L? same for Sem2? ❙
structure Sem1 : ?Computation = ❚
structure Sem2 : ?Computation = ❚
......@@ -88,9 +106,8 @@ theory ComputationEquivalence =
theory ConcretizationEquivalence =
structure L : ?FormalSystem = ❚
include ?FormalSystemEquivalence ❙
// can I force Sem1|?FormalSystem = L? same for Sem2? ❙
structure Sem1 : ?Concretization = ❚
structure Sem2 : ?Concretization = ❚
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment