systemqfw

commit bf7697253345e223aee8062cdfc976060211070d
parent f682629dcc43bd18f055b659041e5625ddeae326
Author: Robert Russell <robert@rr3.xyz>
Date:   Thu, 29 Aug 2024 04:57:41 -0700

Add TODO notes

Diffstat:
M
README
 | 
10
++++++++++

1 file changed, 10 insertions(+), 0 deletions(-)
diff --git a/README b/README
@@ -11,6 +11,10 @@ quantity (like in normal functional programming), yet without having to deal
 with the "boxing" and "unboxing" of graded modal types.
 
 
+TODO: Explain the economic interpretation of programs, and connect it to the
+sequent calculus.
+
+
 --------------------------------------------------------------------------------
 Quantity algebras
 
@@ -63,6 +67,9 @@ Ledgers  ∋  Σ  ::=  ⋄
                  |  Σ, x~Q
 
 
+TODO: Explain ledgers
+
+
 In the kinding and typing rules, we adopt the convention that type contexts Θ
 and term contexts Γ are unordered and omit mention of the standard side
 conditions regarding variable freshness.
@@ -162,6 +169,9 @@ x:T ∈ Γ
 Θ; Γ ⊢ t [U] ~ Q ↑ T.*[U/X] ⊣ Σ
 
 
+TODO: Discuss rules
+
+
 The auxiliary judgement "⊢ Q >= R" means "the quantity Q (viewed as a supply)
 is greater than the quantity R (viewed as a demand)". We should at least have
 the rule