Resource management for Lolli using strictness tags

Kevin Watkins

[draft of May 25, 1999]

1 Introduction

Note two difficulties with the CHP97 system RM_{3}. One, information about which resources are strict is destroyed in the left premise of rm_{3}-⊗_{0v} and must be recovered for the right premise using a linear-time search. This information can be retained by associating a tag with each resource. Two, the care taken to remove strict resources from the output context by the intersection in the conclusion of rm_{3}-⊗_{1v} is unnecessary. The system can delay the removal of a strict resource consumed by ⊤ until control reaches the rule at which the resource was placed in the strict context (rm_{st}-&_{1v} or rm_{st}-⊸).

Together these observations recover the simplicity of the original resource management system for the multiplicatives, typically the most used connectives in practice.

2 The strictness tag system RM_{ST}

The contexts of the original resource management systems are modified to contain a tag for each resource indicating whether it is strict. A resource D marked with tag s is written D^{s}. Marked contexts are denoted by the Greek letter Λ. Intuitionistic contexts are not marked. The same conventions regarding contexts are adhered to.

The tags associated with resources in the strictness tag system are taken to be unique markers of some kind which can be compared for equality. It must be possible to generate new tags dynamically. An implementation might use integers.

Each judgment is annotated with a tag. Resources in the linear input context with the same tag are considered strict, and other resources are lax. The new rule system for these judgments is presented in Figure 1. The notation s(Λ) denotes the tagged context obtained by setting the tags of all the resources in Λ to s.

There is additional notation to relate tagged and untagged contexts. [Λ] refers to the untagged context given by erasing all the tags of Λ. [Λ]_{s} refers to the untagged context consisting of all resources in Λ marked with tag s.

Similarly, [Λ]_{¬s} refers to the untagged context consisting of all resources in Λ marked with tags other than s.

The RM_{ST} system satisfies two important invariants. The first, Theorem 2.1, is that output contexts are subcontexts of input contexts. This is similar to but weaker than the subcontext property of RM_{3}, since in RM_{ST} the input context, and hence the output context, can contain both strict and lax resources. In fact, the RM_{ST} system takes advantage of this to delay the removal of strict resources consumed by ⊤.

However, when the ⊤-flag is zero, a stronger invariant holds. In this case, the output context contains only resources from the lax part of the input context, as shown in Theorem 2.2.

Theorem 2.1 (Subcontext property for RM_{ST}) If Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G, then Λ_{O} ⊆ Λ_{I}.

Proof The proof is by induction on (I :: Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G).

Case: I = {[Λ_{I}]_{s} = · \atop Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} a ≐ a} ^{rm^{st}-≐}

1. Λ_{I} ⊆ Λ_{I}

The rm_{st}-1, rm_{st}-⊤, and rm_{st}-! cases are similar.

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{O}) \ ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} & G_{2} ^{rm^{st}-&^{0v}}

1. Λ_{O} ⊆ Λ_{I}  inductive hypothesis on I_{1}

The rm_{st}-⊕_{1}, rm_{st}-⊕_{2}, rm_{st}-⊃, rm_{st}-∀, rm_{st}-∃, and rm_{st}-atm int cases are similar.

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{M}) + Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} − s(Λ_{I} − Λ_{M}) ⟹_{v}^{s} G_{1} & G_{2} ^{rm^{st}-&^{1v}}

1. Λ_{M} ⊆ Λ_{I}  inductive hypothesis on I_{1}
2. Λ_{O} ⊆ s(Λ_{I} − Λ_{M}) + Λ_{M}  inductive hypothesis on I_{2}
3. \begin{aligned}Λ_{O} − s(Λ_{I} − Λ_{M}) & ⊆ Λ_{M} \\ & ⊆ Λ_{I} \end{aligned}  {2 \atop 1}

\begin{matrix}D ≫ a \ G & D, Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G \\ D, Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} a \end{matrix} ^{rm^{st}-atm int}
\begin{matrix}D ≫ a \ G & Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G \\ Γ ; D^{t}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} a \end{matrix} ^{rm^{st}-atm lin}
{[Λ_{I}]_{s} = · \atop Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} a ≐ a} ^{rm^{st}-≐}

{[Λ_{I}]_{s} = · \atop Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} 1} rm_{st}-1
Γ ; Λ_{I} \ Λ_{I} ⟹_{1}^{s} ⊤ rm_{st}-⊤  (No rule for 0.)
Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} Γ ; s(Λ_{I} − Λ_{O}) \ ⟹_{v}^{s} G_{2}

Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} & G_{2}

rm^{st}-&^{0v}
Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{s} G_{1} Γ ; s(Λ_{I} − Λ_{M}) + Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}

Γ ; Λ_{I} \ Λ_{O} − s(Λ_{I} − Λ_{M}) ⟹_{v}^{s} G_{1} & G_{2}

rm^{st}-&^{1v}
t new Γ ; Λ_{I} \ Λ_{M} ⟹_{0}^{t} G_{1} Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}

Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊗ G_{2}

rm^{st}-⊗^{0v}
t new Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{t} G_{1} Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{t} G_{2}

Γ ; Λ_{I} \ Λ_{O} ⟹_{1}^{s} G_{1} ⊗ G_{2}

rm^{st}-⊗^{1v}
{Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊕ G_{2}} ^{rm^{st}-⊕^{1}}

{Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{2} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊕ G_{2}} ^{rm^{st}-⊕^{2}}
{Γ ; D^{s}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} G \atop Γ ; Λ_{I} \ Λ_{O} − D^{s} ⟹_{v}^{s} D ⊸ G} ^{rm^{st}-⊸}

{D, Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} D ⊃ G} ^{rm^{st}-⊃}
\begin{matrix}[Λ_{I}]_{s} = · & Γ ; · \ ⟹_{v}^{s} G \\ Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} ! G \end{matrix} ^{rm^{st}-!}
{Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} [c/x]G \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} ∀x.G} rm_{st}-∀

{Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} [t/x]G \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} ∃x.G} rm_{st}-∃

Figure 1: Lolli resource management with strictness tags.

Case: I = t new {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{0}^{t} G_{1}} {I_{2} \atop Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊗ G_{2} ^{rm^{st}-⊗^{0v}}

1. \begin{aligned}Λ_{O} & ⊆ Λ_{M} \\ & ⊆ Λ_{I} \end{aligned}

inductive hypothesis on I_{2} inductive hypothesis on I_{1}

The rm_{st}-⊗_{1v} case is similar.

Case: I = {I_{1} \atop Γ ; D^{s}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} G} ; Γ ; Λ_{I} \ Λ_{O} − D^{s} ⟹_{v}^{s} D ⊸ G ^{rm^{st}-⊸}

1. Λ_{O} ⊆ D^{s}, Λ_{I}  inductive hypothesis on I_{1}
2. Λ_{O} − D^{s} ⊆ Λ_{I}  1

Case: I = \begin{matrix}{I_{1} \atop D ≫ a \ G} & {I_{2} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G} \\ Γ ; D^{t}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} a \end{matrix} ^{rm^{st}-atm lin}

1. Λ_{O} ⊆ Λ_{I}  inductive hypothesis on I_{2}
2. Λ_{O} ⊆ (D^{t}, Λ_{I})  1
□

Theorem 2.2 (Limited strictness of RM_{ST}) If Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G, then [Λ_{O}]_{s} = ·. Proof The proof is by induction on (I :: Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G).

Case: I = {[Λ_{I}]_{s} = · \atop Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} a ≐ a} ^{rm^{st}-≐}

1. [Λ]_{s} = ·  side condition of I

The rm_{st}-1 and rm_{st}-! cases are similar.

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{O}) \ ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} & G_{2} ^{rm^{st}-&^{0v}}

1. [Λ_{O}]_{s} = ·  inductive hypothesis on I_{1}

The rm_{st}-⊗_{0v}, rm_{st}-⊕_{1}, rm_{st}-⊕_{2}, rm_{st}-⊃, rm_{st}-∀, rm_{st}-∃, rm_{st}-atm int, and rm_{st}-atm lin cases are similar.

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{M}) + Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} − s(Λ_{I} − Λ_{M}) ⟹_{v}^{s} G_{1} & G_{2} ^{rm^{st}-&^{1v}}

1. [Λ_{O}]_{s} = ·  inductive hypothesis on I_{2}
2. [Λ_{O} − s(Λ_{I} − Λ_{M})]_{s} = ·  1

Case: I = {I_{1} \atop Γ ; D^{s}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} G} ; Γ ; Λ_{I} \ Λ_{O} − D^{s} ⟹_{v}^{s} D ⊸ G ^{rm^{st}-⊸}

1. [Λ_{O}]_{s} = ·  inductive hypothesis on I_{1}
2. [Λ_{O} − D^{s}]_{s} = ·  1

The remaining cases cannot arise because the conclusion of the rule in each case has the ⊤-flag set. □

Theorem 2.2 allows an implementation of RM_{ST} to omit the context subtraction in the conclusions of rm_{st}-&_{1v} and rm_{st}-⊸ when v = 0.

An important fact is that the RM_{3} and RM_{ST} systems are very strongly related. In fact, it is claimed that the functions on proofs determined by the soundness and completeness theorems below determine a structure-preserving bijection between RM_{3} and RM_{ST} proofs. This ensures that the RM_{ST} system preserves the desirable operational behavior of the RM_{3} system.

The soundness of RM_{ST}relative to RM_{3} is straightforwardly stated. It makes no commitment about the presence of strict resources in the output context.

Theorem 2.3 (Soundness of RM_{ST} with respect to RM_{3}) If Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G then Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G.

Proof The proof is by induction on the derivation (I :: Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G).

Case: I = {[Λ_{I}]_{s} = · \atop Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} a ≐ a} ^{rm^{st}-≐}

1. ∃ J :: Γ ; ·; [Λ]_{¬s} \ [Λ]_{¬s} ⟹_{0} a ≐ a  rm_{3}-≐
2. [Λ]_{s} = ·  side condition of I

3. J :: Γ ; [Λ]_{s}; [Λ]_{¬s} \ [Λ]_{¬s} ⟹_{0} a ≐ a  1, 2

The rm_{st}-1 and rm_{st}-! cases are similar. Case: I = Γ ; Λ_{I} \ Λ_{I} ⟹_{1}^{s} ⊤ rm_{st}-⊤

1. Γ ; [Λ]_{s}; [Λ]_{¬s} \ [Λ]_{¬s} ⟹_{1} ⊤  rm_{3}-⊤

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{O}) \ ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} & G_{2} ^{rm^{st}-&^{0v}}

1. ∃ J_{1} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{0} G_{1} inductive hypothesis on I_{1}
2. ∃ J_{2} :: Γ ; [s(Λ_{I} − Λ_{O})]_{s}; [s(Λ_{I} − Λ_{O})]_{¬s} \ [Λ_{X}]_{¬s} ⟹_{v} G_{2}

inductive hypothesis on I_{2}

3. [Λ_{O}]_{s} = ·  theorem 2.2 on I_{1}
4. [s(Λ_{I} − Λ_{O})]_{s} = [Λ_{I} − Λ_{O}] = [Λ_{I} − Λ_{O}]_{s} + [Λ_{I} − Λ_{O}]_{¬s} = [Λ_{I}]_{s} + ([Λ_{I}]_{¬s} − [Λ_{O}]_{¬s})  3
5. [s(Λ_{I} − Λ_{O})]_{¬s} = ·
6. J_{2} :: Γ ; [Λ_{I}]_{s} + ([Λ_{I}]_{¬s} − [Λ_{O}]_{¬s}) ; · \ [Λ_{X}]_{¬s} ⟹_{v} G_{2}  2, 4, 5
7. Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{0} G_{1} & G_{2}  rm_{3}-&_{0v} on 1, 6

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{s} G_{1}} {I_{2} \atop Γ ; s(Λ_{I} − Λ_{M}) + Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} − s(Λ_{I} − Λ_{M}) ⟹_{v}^{s} G_{1} & G_{2} ^{rm^{st}-&^{1v}}

1. ∃ J_{1} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{M}]_{¬s} ⟹_{1} G_{1} inductive hypothesis on I_{1}
2. let Λ′_{I} ≡ s(Λ_{I} − Λ_{M}) + Λ_{M}
3. ∃ J_{2} :: Γ ; [Λ′_{I}]_{s}; [Λ′_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{2} inductive hypothesis on I_{2}
4. Λ_{M} ⊆ Λ_{I}  theorem 2.1 on I_{1}
5. [Λ′_{I}]_{s} = [Λ_{I} − Λ_{M}] + [Λ_{M}]_{s} = [Λ_{I} − Λ_{M}]_{s} + [Λ_{I} − Λ_{M}]_{¬s} + [Λ_{M}]_{s} = ([Λ_{I}]_{s} − [Λ_{M}]_{s} + [Λ_{M}]_{s}) + ([Λ_{I}]_{¬s} − [Λ_{M}]_{¬s}) = [Λ_{I}]_{s} + ([Λ_{I}]_{¬s} − [Λ_{M}]_{¬s})  {2 \atop 4}
6. [Λ′_{I}]_{¬s} = [Λ_{M}]_{¬s}  2
7. J_{2} :: Γ ; [Λ_{I}]_{s} + ([Λ_{I}]_{¬s} − [Λ_{M}]_{¬s}) ; [Λ_{M}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{2}  3, 5, 6
8. Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{1} & G_{2}  rm_{3}-&_{1v} on 1, 7

Case: I = t new {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{0}^{t} G_{1}} {I_{2} \atop Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊗ G_{2} ^{rm^{st}-⊗^{0v}}

1. Λ_{M} ⊆ Λ_{I}  theorem 2.1 on I_{1}
2. ∃ J_{1} :: Γ ; [Λ_{I}]_{t}; [Λ_{I}]_{¬t} \ [Λ_{M}]_{¬t} ⟹_{0} G_{1} inductive hypothesis on I_{1}
3. [Λ_{I}]_{t} = ·  side condition of I
4. \begin{aligned}[Λ_{I}]_{¬t} & = [Λ_{I}] \\ & = [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \end{aligned}  side condition of I

5. [Λ_{M}]_{¬t} = [Λ_{M}]  3, 1
6. J_{1} :: Γ ; ·; [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \ [Λ_{M}] ⟹_{0} G_{1}  2, 3, 4, 5
7. ∃ J_{2} :: Γ ; [Λ_{M}]_{s}; [Λ_{M}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{2} inductive hypothesis on I_{2}
8. [Λ_{M}]_{s} = [Λ_{I}]_{s} ∩ [Λ_{M}]  1
9. [Λ_{M}]_{¬s} = [Λ_{I}]_{¬s} ∩ [Λ_{M}]  1
10. J_{2} :: Γ ; [Λ_{I}]_{s} ∩ [Λ_{M}] ; [Λ_{I}]_{¬s} ∩ [Λ_{M}] \ [Λ_{O}]_{¬s} ⟹_{v} G_{2}  7, 8, 9
11. Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{1} ⊗ G_{2}  rm_{3}-⊗_{0v} on 6, 10

Case: I = t new {I_{1} \atop Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{t} G_{1}} {I_{2} \atop Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{t} G_{2}} Γ ; Λ_{I} \ Λ_{O} ⟹_{1}^{s} G_{1} ⊗ G_{2} ^{rm^{st}-⊗^{1v}}

1. Λ_{O} ⊆ Λ_{M} ⊆ Λ_{I}  theorem 2.1 on I_{2}, I_{1}
2. ∃ J_{1} :: Γ ; [Λ_{I}]_{t}; [Λ_{I}]_{¬t} \ [Λ_{M}]_{¬t} ⟹_{1} G_{1} inductive hypothesis on I_{1}
3. [Λ_{I}]_{t} = ·  side condition of I
4. \begin{aligned}[Λ_{I}]_{¬t} & = [Λ_{I}] \\ & = [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \end{aligned}  side condition of I

5. J_{1} :: Γ ; ·; [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \ [Λ_{M}]_{¬t} ⟹_{1} G_{1}  2, 3, 4
6. ∃ J_{2} :: Γ ; [Λ_{M}]_{t}; [Λ_{M}]_{¬t} \ [Λ_{O}]_{¬t} ⟹_{v} G_{2} inductive hypothesis on I_{2}
7. [Λ_{M}]_{t} = ·  1, 3
8. J_{2} :: Γ ; ·; [Λ_{M}]_{¬t} \ [Λ_{O}]_{¬t} ⟹_{v} G_{2}  6, 7
9. ∃ J_{3} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{I}]_{¬s} ∩ [Λ_{O}]_{¬t} ⟹_{1} G_{1} ⊗ G_{2} rm_{3}-⊗_{1v} on 5, 8
10. [Λ_{O}]_{¬t} = [Λ_{O}]  1, 3
11. \begin{aligned}[Λ_{I}]_{¬s} ∩ [Λ_{O}]_{¬t} & = [Λ_{I}]_{¬s} ∩ [Λ_{O}] \\ & = [Λ_{I}]_{¬s} ∩ [Λ_{O}]_{¬s} \\ & = [Λ_{O}]_{¬s} \end{aligned}  {10 \atop 1}

12. J_{3} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{1} G_{1} ⊗ G_{2}  9, 11

Case: I = {I_{1} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1}} ; Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊕ G_{2} ^{rm^{st}-⊕^{1}}

1. ∃ J_{1} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{1} inductive hypothesis on I_{1}
2. Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{1} ⊕ G_{2}  rm_{3}-⊕_{1} on 1

The rm_{st}-⊕_{2}, rm_{st}-⊃, rm_{st}-∀, rm_{st}-∃, and rm_{st}-atm int cases are similar.

Case: I = {I_{1} \atop Γ ; D^{s}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} G} ; Γ ; Λ_{I} \ Λ_{O} − D^{s} ⟹_{v}^{s} D ⊸ G ^{rm^{st}-⊸}

1. ∃ J_{1} :: Γ ; [D^{s}, Λ_{I}]_{s}; [D^{s}, Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G_{1}

inductive hypothesis on I_{1}

2. J_{1} :: Γ ; D, [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G  1
3. ∃ J_{2} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} D ⊸ G  rm_{3}-⊸ on 2
4. J_{2} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O} − D^{s}]_{¬s} ⟹_{v} D ⊸ G  3

Case: I = \begin{matrix}{I_{1} \atop D ≫ a \ G} & {I_{2} \atop Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G} \\ Γ ; D^{t}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} a \end{matrix} ^{rm^{st}-atm lin}

There are two cases, depending on whether t = s.

When t ≠ s:

1. ∃ J_{2} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G  inductive hypothesis on I_{2}
2. ∃ J_{3} :: Γ ; [Λ_{I}]_{s}; D, [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} a  rm_{3}-atm lax on I_{1}, 1
3. J_{3} :: Γ ; [D^{t}, Λ_{I}]_{s}; [D^{t}, Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} a  2

When t = s:

1. ∃ J_{2} :: Γ ; [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} G  inductive hypothesis on I_{2}
2. ∃ J_{3} :: Γ ; D, [Λ_{I}]_{s}; [Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} a  rm_{3}-atm strict on I_{1}, 1
3. J_{3} :: Γ ; [D^{t}, Λ_{I}]_{s}; [D^{t}, Λ_{I}]_{¬s} \ [Λ_{O}]_{¬s} ⟹_{v} a  2
□

The statement of the completeness theorem for RM_{ST} relies on the inputoutput behavior of the resource management systems in order to relate the contexts of RM_{3} and RM_{ST} derivations. A tagging of the input contexts of the RM_{3} proof is provided via an extra assumption, and the theorem generates a tagged output context as well as the RM_{ST} proof. The lax resources contained in the RM_{ST} output context are the same as those in the RM_{3} output context. However, the RM_{ST} output context may contain strict resources as well, which are not present in the RM_{3} output context. These spurious resources are always removed before proof search proceeds to another branch.

Theorem 2.4 (Completeness of RM_{ST} with respect to RM_{3}) Given an RM_{3} derivation (I :: Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G) and a tagged context Λ_{I} such that [Λ_{I}]_{s} = Ξ and [Λ_{I}]_{¬s} = Δ_{I}, there exists a tagged context Λ_{O} and an RM_{ST} derivation (J :: Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G) such that [Λ_{O}]_{¬s} = Δ_{O}.

Proof The proof is by induction on the derivation (I :: Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G). The two conclusions in each case are marked with asterisks.

Case: I = Γ ; ·; Δ_{I} \ Δ_{I} _{⟹_{0}} a ≐ a ^{rm^{3}-≐}

1. [Λ_{I}]_{s} = ·  assumption
*2. Γ ; Λ_{I} \ Λ_{I} ⟹_{0}^{s} a ≐ a  rm_{st}-≐ on 1
*3. [Λ_{I}]_{¬s} = Δ_{I}  assumption

The rm_{3}-1 and rm_{3}-! cases are similar.

Case: I = Γ ; Ξ ; Δ_{I} \ Δ_{I} _{⟹_{1}} ⊤ rm_{3}-⊤

*1. Γ ; Λ_{I} \ Λ_{I} ⟹_{1}^{s} ⊤  rm_{st}-⊤
*2. [Λ_{I}]_{¬s} = Δ_{I}  assumption

Case: I = {I_{1} \atop Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{0} G_{1}} {I_{2} \atop Γ ; Ξ + (Δ_{I} − Δ_{O}) ; · \ ⟹_{v} G_{2}} Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{0} G_{1} & G_{2} ^{rm^{3}-&^{0v}}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. ∃Λ_{O}. Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1}  inductive hypothesis on I_{1}, 1, 2
*4. [Λ_{O}]_{¬s} = Δ_{O}  “
5. [Λ_{O}]_{s} = ·  theorem 2.2 on 3
6. [s(Λ_{I} − Λ_{O})]_{s} = [Λ_{I} − Λ_{O}] = [Λ_{I} − Λ_{O}]_{s} + [Λ_{I} − Λ_{O}]_{¬s} = Ξ + (Δ_{I} − Δ_{O})  1, 5, 2, 4

7. [s(Λ_{I} − Λ_{O})]_{¬s} = ·
8. ∃Λ_{X}. Γ ; s(Λ_{I} − Λ_{O}) \ Λ_{X} ⟹_{v}^{s} G_{2}  inductive hypothesis on I_{2}, 6, 7
*9. Γ ; Λ_{I} \ Λ_{O} ⟹_{0}^{s} G_{1} & G_{2}  rm_{st}-&_{0v} on 3, 8

Case: I = {I_{1} \atop Γ ; Ξ ; Δ_{I} \ Δ_{M} ⟹_{1} G_{1}} {I_{2} \atop Γ ; Ξ + (Δ_{I} − Δ_{M}) ; Δ_{M} \ Δ_{O} ⟹_{v} G_{2}} Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G_{1} & G_{2} ^{rm^{3}-&^{1v}}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. ∃Λ_{M}. Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{s} G_{1}  inductive hypothesis on I_{1}, 1, 2
4. [Λ_{M}]_{¬s} = Δ_{M}  “
5. Λ_{M} ⊆ Λ_{I}  theorem 2.1 on 3
6. \begin{aligned}[Λ_{M}]_{s} & ⊆ [Λ_{I}]_{s} \\ & = Ξ \end{aligned}  {5 \atop 1}

7. [s(Λ_{I} − Λ_{M}) + Λ_{M}]_{s} = [Λ_{I} − Λ_{M}] + [Λ_{M}]_{s} = [Λ_{I} − Λ_{M}]_{s} + [Λ_{I} − Λ_{M}]_{¬s} + [Λ_{M}]_{s} = (Ξ − [Λ_{M}]_{s} + [Λ_{M}]_{s}) + (Δ_{I} − Δ_{M}) = Ξ + (Δ_{I} − Δ_{M})  {1, 2, 4 \atop 6}

8. \begin{aligned}[s(Λ_{I} − Λ_{M}) + Λ_{M}]_{¬s} & = [Λ_{M}]_{¬s} \\ & = Δ_{M} \end{aligned}  4

9. ∃Λ_{O}. Γ ; s(Λ_{I} − Λ_{M}) + Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}

inductive hypothesis on I_{2}, 7, 8

10. [Λ_{O}]_{¬s} = Δ_{O}  “
*11. Γ ; Λ_{I} \ Λ_{O} − s(Λ_{I} − Λ_{M}) ⟹_{v}^{s} G_{1} & G_{2}  rm_{st}-&_{1v} on 3, 9
*12. \begin{aligned}[Λ_{O} − s(Λ_{I} − Λ_{M})]_{¬s} & = [Λ_{O}]_{¬s} \\ & = Δ_{O} \end{aligned}  10

Case: I = {I_{1} \atop Γ ; ·; Ξ + Δ_{I} \ Δ_{M} ⟹_{0} G_{1}} {I_{2} \atop Γ ; Ξ ∩ Δ_{M} ; Δ_{I} ∩ Δ_{M} \ Δ_{O} ⟹_{v} G_{2}} Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G_{1} ⊗ G_{2} ^{rm^{3}-⊗^{0v}}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. let t be new
4. [Λ_{I}]_{t} = ·  3

5. \begin{aligned}[Λ_{I}]_{¬t} & = [Λ_{I}] \\ & = [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \\ & = Ξ + Δ_{I} \end{aligned}  {3 \atop 1, 2}

6. ∃Λ_{M}. Γ ; Λ_{I} \ Λ_{M} ⟹_{0}^{t} G_{1}  inductive hypothesis on I_{1}, 4, 5
7. [Λ_{M}]_{¬t} = Δ_{M}  “
8. Λ_{M} ⊆ Λ_{I}  theorem 2.1 on 6
9. [Λ_{M}]_{t} = ·  4, 8
10. \begin{aligned}[Λ_{M}] & = [Λ_{M}]_{t} + [Λ_{M}]_{¬t} \\ & = Δ_{M} \end{aligned}  9, 7

11. \begin{aligned}[Λ_{M}]_{s} & = [Λ_{I}]_{s} ∩ [Λ_{M}] \\ & = Ξ ∩ Δ_{M} \end{aligned}  {8 \atop 1, 10}

12. \begin{aligned}[Λ_{M}]_{¬s} & = [Λ_{I}]_{¬s} ∩ [Λ_{M}] \\ & = Δ_{I} ∩ Δ_{M} \end{aligned}  {8 \atop 2, 10}

13. ∃Λ_{O}. Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}  inductive hypothesis on I_{2}, 11, 12
*14. [Λ_{O}]_{¬s} = Δ_{O}  “
*15. Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊗ G_{2}  rm_{st}-⊗_{0v} on 3, 6, 13

Case: I = {I_{1} \atop Γ ; ·; Ξ + Δ_{I} \ Δ_{M} ⟹_{1} G_{1}} {I_{2} \atop Γ ; ·; Δ_{M} \ Δ_{O} ⟹_{v} G_{2}} Γ ; Ξ ; Δ_{I} \ Δ_{I} ∩ Δ_{O} ⟹_{1} G_{1} ⊗ G_{2} ^{rm^{3}-⊗^{1v}}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. let t be new
4. [Λ_{I}]_{t} = ·  3
5. \begin{aligned}[Λ_{I}]_{¬t} & = [Λ_{I}] \\ & = [Λ_{I}]_{s} + [Λ_{I}]_{¬s} \\ & = Ξ + Δ_{I} \end{aligned}  {3 \atop 1, 2}

6. ∃Λ_{M}. Γ ; Λ_{I} \ Λ_{M} ⟹_{1}^{t} G_{1}  inductive hypothesis on I_{1}, 4, 5
7. [Λ_{M}]_{¬t} = Δ_{M}  “
8. Λ_{M} ⊆ Λ_{I}  theorem 2.1 on 6
9. [Λ_{M}]_{t} = ·  4, 8
10. ∃Λ_{O}. Γ ; Λ_{M} \ Λ_{O} ⟹_{v}^{s} G_{2}  inductive hypothesis on I_{2}, 7, 9
11. [Λ_{O}]_{¬t} = Δ_{O}  “
*12. Γ ; Λ_{I} \ Λ_{O} ⟹_{1}^{s} G_{1} ⊗ G_{2}  rm_{st}-⊗_{1v} on 3, 6, 10
13. Λ_{O} ⊆ Λ_{M} ⊆ Λ_{I}  theorem 2.1 on 10, 8

14. [Λ_{O}]_{t} = ·  9, 13
15. \begin{aligned}[Λ_{O}] & = [Λ_{O}]_{t} + [Λ_{O}]_{¬t} \\ & = Δ_{O} \end{aligned}  14, 11

*16. \begin{aligned}[Λ_{O}]_{¬s} & = [Λ_{I}]_{¬s} ∩ [Λ_{O}] \\ & = Δ_{I} ∩ Δ_{O} \end{aligned}  {13 \atop 2, 15}

Case: I = {I_{1} \atop Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G_{1}} Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G_{1} ⊕ G_{2} ^{rm^{3}-⊕^{1}}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. ∃Λ_{O}. Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1}  inductive hypothesis on I_{1}, 1, 2
*4. [Λ_{O}]_{¬s} = Δ_{O}  “
*5. Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} G_{1} ⊕ G_{2}  rm_{st}-⊕_{1} on 3

The rm_{3}-⊕_{2}, rm_{3}-⊃, rm_{3}-∀, rm_{3}-∃, and rm_{3}-atm int cases are similar.

Case: I = {I_{1} \atop Γ ; D, Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G} Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} D ⊸ G ^{rm^{3}-⊸}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. [D^{s}, Λ_{I}]_{s} = D, Ξ  1
4. [D^{s}, Λ_{I}]_{¬s} = Δ_{I}  2
5. ∃Λ_{O}. Γ ; D^{s}, Λ_{I} \ Λ_{O} ⟹_{v}^{s} G  inductive hypothesis on I_{1}, 3, 4
6. [Λ_{O}]_{¬s} = Δ_{O}  “
*7. Γ ; Λ_{I} \ Λ_{O} − D^{s} ⟹_{v}^{s} D ⊸ G  rm_{st}-⊸ on 5
*8. \begin{aligned}[Λ_{O} − D^{s}]_{¬s} & = [Λ_{O}]_{¬s} \\ & = Δ_{O} \end{aligned}  6

Case: I = {I_{1} \atop D ≫ a \ G} {I_{2} \atop Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G} Γ ; Ξ ; D, Δ_{I} \ Δ_{O} ⟹_{v} a ^{rm^{3}-atm lax}

1. [Λ_{I}]_{s} = Ξ  assumption
2. [Λ_{I}]_{¬s} = D, Δ_{I}  assumption

3. \begin{matrix}Λ_{I} = D^{t}, Λ′_{I} \\ where t ≠ s \end{matrix}  2

4. [Λ′_{I}]_{s} = Ξ  3, 1
5. [Λ′_{I}]_{¬s} = Δ_{I}  3, 2
6. ∃Λ_{O}. Γ ; Λ′_{I} \ Λ_{O} ⟹_{v}^{s} G  inductive hypothesis on I_{2}, 4, 5
*7. [Λ_{O}]_{¬s} = Δ_{O}  “
8. ∃ J :: Γ ; D^{t}, Λ′_{I} \ Λ_{O} ⟹_{v}^{s} a  rm_{st}-atm lin on I_{1}, 6
*9. J :: Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} a  8, 3

Case: I = {I_{1} \atop D ≫ a \ G} {I_{2} \atop Γ ; Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} G} Γ ; D, Ξ ; Δ_{I} \ Δ_{O} ⟹_{v} a ^{rm^{3}-atm strict}

1. [Λ_{I}]_{s} = D, Ξ  assumption
2. [Λ_{I}]_{¬s} = Δ_{I}  assumption
3. Λ_{I} = D^{s}, Λ′_{I}  2
4. [Λ′_{I}]_{s} = Ξ  3, 1
5. [Λ′_{I}]_{¬s} = Δ_{I}  3, 2
6. ∃Λ_{O}. Γ ; Λ′_{I} \ Λ_{O} ⟹_{v}^{s} G  inductive hypothesis on I_{2}, 4, 5
*7. [Λ_{O}]_{¬s} = Δ_{O}  “
8. ∃ J :: Γ ; D^{s}, Λ′_{I} \ Λ_{O} ⟹_{v}^{s} a  rm_{st}-atm lin on I_{1}, 6
*9. J :: Γ ; Λ_{I} \ Λ_{O} ⟹_{v}^{s} a  8, 3
□