Commit fe7d1a19 authored by Florian Rabe's avatar Florian Rabe

no message

parent 6e0eb1f1
dataconstructor http://cds.omdoc.org/examples/linear?Contraction?idem
theory http://cds.omdoc.org/examples/linear?Contraction
HasMeta http://cds.omdoc.org/examples/linear?Contraction http://cds.omdoc.org/examples?FOLEQNatDed
Includes http://cds.omdoc.org/examples/linear?Contraction http://cds.omdoc.org/examples/linear?Syntax
Includes http://cds.omdoc.org/examples/linear?Contraction http://cds.omdoc.org/examples/linear?Worlds
Declares http://cds.omdoc.org/examples/linear?Contraction http://cds.omdoc.org/examples/linear?Contraction?idem
constant http://cds.omdoc.org/examples/linear?Contraction?idem
......@@ -2,12 +2,13 @@ dataconstructor http://cds.omdoc.org/examples/linear?Exchange?comm
dataconstructor http://cds.omdoc.org/examples/linear?Exchange?test
theory http://cds.omdoc.org/examples/linear?Exchange
HasMeta http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples?FOLEQNatDed
Includes http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Syntax
Includes http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Worlds
Declares http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Exchange?comm
constant http://cds.omdoc.org/examples/linear?Exchange?comm
Declares http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?NormalizeWorlds]
constant http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?NormalizeWorlds]
Declares http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?EquateWorlds]
constant http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?EquateWorlds]
Declares http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Exchange?test
constant http://cds.omdoc.org/examples/linear?Exchange?test
Declares http://cds.omdoc.org/examples/linear?Exchange http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?EquateWorlds]
constant http://cds.omdoc.org/examples/linear?Exchange?[scala://examples.mmt.kwarc.info?EquateWorlds]
dataconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?at
judgementconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?At
datatypeconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?valid
dataconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?weaken
dataconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?⊗_R
dataconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?⊗_L
dataconstructor http://cds.omdoc.org/examples/linear?ResourceSemantics?1_R
......@@ -36,14 +32,6 @@ HasMeta http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.
Includes http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?Syntax
Includes http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?Worlds
Includes http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?Exchange
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?at
constant http://cds.omdoc.org/examples/linear?ResourceSemantics?at
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?At
constant http://cds.omdoc.org/examples/linear?ResourceSemantics?At
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?valid
constant http://cds.omdoc.org/examples/linear?ResourceSemantics?valid
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?weaken
constant http://cds.omdoc.org/examples/linear?ResourceSemantics?weaken
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?⊗_R
constant http://cds.omdoc.org/examples/linear?ResourceSemantics?⊗_R
Declares http://cds.omdoc.org/examples/linear?ResourceSemantics http://cds.omdoc.org/examples/linear?ResourceSemantics?⊗_L
......
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?weaker
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?≤_refl
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?≤_antisym
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?≤_trans
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?≤_monotone
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?≤_least
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?weaken
dataconstructor http://cds.omdoc.org/examples/linear?Weakening?divisibility
theory http://cds.omdoc.org/examples/linear?Weakening
HasMeta http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples?FOLEQNatDed
Includes http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Syntax
Includes http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Worlds
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?weaker
constant http://cds.omdoc.org/examples/linear?Weakening?weaker
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?≤_refl
constant http://cds.omdoc.org/examples/linear?Weakening?≤_refl
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?≤_antisym
constant http://cds.omdoc.org/examples/linear?Weakening?≤_antisym
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?≤_trans
constant http://cds.omdoc.org/examples/linear?Weakening?≤_trans
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?≤_monotone
constant http://cds.omdoc.org/examples/linear?Weakening?≤_monotone
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?≤_least
constant http://cds.omdoc.org/examples/linear?Weakening?≤_least
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?weaken
constant http://cds.omdoc.org/examples/linear?Weakening?weaken
Declares http://cds.omdoc.org/examples/linear?Weakening http://cds.omdoc.org/examples/linear?Weakening?divisibility
constant http://cds.omdoc.org/examples/linear?Weakening?divisibility
......@@ -4,13 +4,12 @@ dataconstructor http://cds.omdoc.org/examples/linear?Worlds?empty
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?neutL
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?neutR
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?assoc
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?weaker
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?≤_refl
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?≤_antisym
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?≤_trans
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?≤_monotone
dataconstructor http://cds.omdoc.org/examples/linear?Worlds?at
judgementconstructor http://cds.omdoc.org/examples/linear?Worlds?At
datatypeconstructor http://cds.omdoc.org/examples/linear?Worlds?valid
theory http://cds.omdoc.org/examples/linear?Worlds
HasMeta http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples?FOLEQNatDed
Includes http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Syntax
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?world
constant http://cds.omdoc.org/examples/linear?Worlds?world
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?union
......@@ -23,13 +22,9 @@ Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/exampl
constant http://cds.omdoc.org/examples/linear?Worlds?neutR
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?assoc
constant http://cds.omdoc.org/examples/linear?Worlds?assoc
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?weaker
constant http://cds.omdoc.org/examples/linear?Worlds?weaker
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?≤_refl
constant http://cds.omdoc.org/examples/linear?Worlds?≤_refl
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?≤_antisym
constant http://cds.omdoc.org/examples/linear?Worlds?≤_antisym
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?≤_trans
constant http://cds.omdoc.org/examples/linear?Worlds?≤_trans
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?≤_monotone
constant http://cds.omdoc.org/examples/linear?Worlds?≤_monotone
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?at
constant http://cds.omdoc.org/examples/linear?Worlds?at
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?At
constant http://cds.omdoc.org/examples/linear?Worlds?At
Declares http://cds.omdoc.org/examples/linear?Worlds http://cds.omdoc.org/examples/linear?Worlds?valid
constant http://cds.omdoc.org/examples/linear?Worlds?valid
......@@ -23,10 +23,14 @@ theory Syntax : http://cds.omdoc.org/urtheories?LF =
= [x,y] !x ⊸ y❙
// We use untyped first-order logic with equality to define the sematnics.
The values of the first-order universe are the worlds, and propositions may hold at different worlds.❚
theory Worlds : /examples?FOLEQNatDed =
include ?Syntax❙
// worlds contain resources ❙
world : type❘= term❙
// union of worlds, corresponds to multiset union of resources ❙
// composition of worlds, corresponds to multiset union of resources ❙
union : world ⟶ world ⟶ world ❘# 1 * 2 prec 100❙
// empty world with no resources ❙
empty : world❘# ε❙
......@@ -36,56 +40,75 @@ theory Worlds : /examples?FOLEQNatDed =
neutR : {P} ⊦ P*ε ≐ P❙
assoc : {P,Q,R} ⊦ (P*Q)*R ≐ P*(Q*R)❙
// ordering with monotonicity
weaker : world ⟶ world ⟶ prop ❘ # 1 ≤ 2 prec 80
≤_refl : {P} ⊦ P ≤ P
≤_antisym: {P,Q} ⊦ P ≤ Q ⟶ ⊦ Q ≤ P ⟶ ⊦ P≐Q
≤_trans : {P,Q,R} ⊦ P≤Q ⟶ ⊦ Q≤R ⟶ ⊦ P≤R ❙
≤_monotone: {a,b,c,d} ⊦ a ≤ b ⟶ ⊦ c ≤ d ⟶ ⊦ a*c ≤ b*d❙
// A @ P: A can be produced by using all resources available in world P
at : o ⟶ world ⟶ prop
At : o ⟶ world ⟶ type❘ = [p,w] ⊦ at p w❘# 1 @ 2 prec 50❘role Judgment
// a formula is valid if it holds in the empty world
valid : o ⟶ type ❘= [A] A @ ε❘# valid 1 prec -10❙
// Apart from the monoid/multiset structure, there is no way to introduce worlds.
The set of worlds is the freely-generated T over the bound world variables.
Here T is the theory imposed on worlds, T is an extension of the monoid theory.
Different extensions allow modeling different structural rules.
The following gives three extensions, but only Exchange is used later on.❚
// Exchange corresponds to commutativity.❚
theory Exchange : /examples?FOLEQNatDed =
include ?Worlds❙
// exchange is commutativity❙
comm : {P,Q} ⊦ P*Q ≐ Q*P❙
// We add two special type-checking rules that mechanize the monoid+commutativity axiom.
Their mplementations are given in the folder scala (sibling of source).❙
// A simplification rule for *-terms: it normalizes bracketing of *, drops ε, and reorders the arguments❙
rule rules?NormalizeWorlds❙
rule rules?EquateWorlds❙
test : {p,q,r} ⊦ r*(p*q)*ε*r ≐ r*(r*(q*p)) ❘= [p,q,r] refl❙
// An equality-checking rule for equations involving *: it normalizes both sides and solves meta-variables of type world.
For example, it can reduce v*w=v*w' to w=w'.
Situations like this came up in several of the examples below.
This rule is admissible for solving meta-variables but not derivable from the monoid+commutativity axioms.
Effectively, it works in the freely-generated commutative monoid.
Because it is only admissible, it breaks modularity: e.g., it cannot be easily combined with a corresponding rule for idempotence.❙
rule rules?EquateWorlds❙
// Contraction corresponds to idempotence.❚
theory Contraction : /examples?FOLEQNatDed =
include ?Worlds❙
// contraction is idempotence ❙
idem : {P} ⊦ P*P ≐ P❙
// Weakening corresponds to the empty world being the least element.❚
theory Weakening : /examples?FOLEQNatDed =
include ?Worlds❙
// least world is weakening (without this, the order is trivial, i.e., there is no weakening)❙
// ordering with monotonicity❙
weaker : world ⟶ world ⟶ prop ❘ # 1 ≤ 2 prec 80❙
≤_refl : {P} ⊦ P ≤ P❙
≤_antisym: {P,Q} ⊦ P ≤ Q ⟶ ⊦ Q ≤ P ⟶ ⊦ P≐Q❙
≤_trans : {P,Q,R} ⊦ P≤Q ⟶ ⊦ Q≤R ⟶ ⊦ P≤R ❙
≤_monotone: {a,b,c,d} ⊦ a ≤ b ⟶ ⊦ c ≤ d ⟶ ⊦ a*c ≤ b*d❙
// least world (without this, the order is trivial, i.e., there is no weakening)❙
≤_least : {P} ⊦ ε ≤ P❙
// TODO: This should be a subtyping rule so that it does not occur in proofs.❙
weaken: {A,v,w} A @ v ⟶ ⊦v≤w ⟶ A @ w❙
divisibility: {P,Q} ⊦ P ≤ P*Q ❘
= [P,Q] congF neutR ([u]u≤P*Q) (≤_monotone ≤_refl ≤_least)❙
// Proofs of the linear sequent A1, ..., An |- A are represented as terms of type
(A1 ⊗ ... ⊗ An) ⊸ A @ ε❚
// Now proofs of the linear sequent A1, ..., An |- A are represented as terms of type
(A1 ⊗ ... ⊗ An) ⊸ A @ ε, where @ is the binary holds-at relation between propositions and worlds.
theory ResourceSemantics : /examples?FOLEQNatDed =
include ?Syntax❙
include ?Worlds❙
include ?Exchange❙
// A @ P: A can be produced by using all resources available in world P❙
at : o ⟶ world ⟶ prop❙
At : o ⟶ world ⟶ type❘ = [p,w] ⊦ at p w❘# 1 @ 2 prec 50❘role Judgment❙
// a formula is valid if it holds in the empty world❙
valid : o ⟶ type ❘= [A] A @ ε❘# valid 1 prec -10❙
// should be a subtyping rule❙
weaken: {A,v,w} A @ v ⟶ ⊦v≤w ⟶ A @ w❙
⊗_R : {A,B,a,b} A @ a ⟶ B @ b ⟶ A ⊗ B @ a*b❙
⊗_L : {A,B,C,u,v} A ⊗ B @ u ⟶ ({a}{b} A @ a ⟶ B @ b ⟶ C @ a*b*v) ⟶ C @ u*v❘
# ⊗_L 6 7❙
......@@ -116,6 +139,9 @@ theory ResourceSemantics : /examples?FOLEQNatDed =
!_R : {A} A @ ε ⟶ ! A @ ε❙
!_L : {A,C,u,v} ! A @ u ⟶ (A @ ε ⟶ C @ v) ⟶ C @ u*v❙
// In the remaineder, we prove some derivable rules to exercise the calculus.❙
⊗_commute : {A,B} valid A⊗B ⊸ B⊗A❘
= [A,B] ⊸_R [ab,h] ⊗_L h [a,b,p,q] ⊗_R q p❙
......@@ -148,7 +174,9 @@ theory ResourceSemantics : /examples?FOLEQNatDed =
= [A,B] ⊸_R [ab,h] ⊕_L h ([a,p] !_L p ([pE] !_R (⊕_Rl pE)))
([b,q] !_L q ([qE] !_R (⊕_Rr qE)))❙
!_over_& : {A,B} valid !(A&B) ⊸ (!A&!B)❘
// = [A,B] ⊸_R [ab,h] &_R (!_L h [pqE] &_Ll pqE ([a,p] !_R p))
// TODO: This proof unexpectedly does not type-check, eventually failing at a=ε and b=ε.
Further investigation is needed to determine if the proof is in fat wrong or if the type-checker is led astray by the EquateWorlds rules.❙
// = [A,B] ⊸_R [ab,h] &_R (!_L h [pqE] &_Ll pqE ([a,p] !_R p))
(!_L h [pqE] &_Lr pqE ([b,q] !_R q))❙
!_idempotent1 : {A} valid !!A ⊸ !A❘
= [A] ⊸_R [a,h] !_L h [k] !_L k [l] !_R l❙
......
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