From 7d233728465038067a71ec46979051747b07d6b0 Mon Sep 17 00:00:00 2001
From: Ellen Arvidsson <ellen@log-e.se>
Date: Tue, 24 Jun 2025 22:44:46 +0200
Subject: [PATCH] added trace pairs

---
 docs/about/formalities.md | 31 +++++++++++++++++++++++++------
 1 file changed, 25 insertions(+), 6 deletions(-)

diff --git a/docs/about/formalities.md b/docs/about/formalities.md
index c2a2472..b2b01f1 100644
--- a/docs/about/formalities.md
+++ b/docs/about/formalities.md
@@ -24,29 +24,36 @@ a ∈ opname
 
 ## sappho subtyping rules
 
-```
+```cmath
+// trace pairs: none
 ---- [identity]
 s, γ ⊢ s, δ
 
+// trace pairs: none
 ---- [true-right]
 γ ⊢ true, δ
 
+// trace pairs: none
 ---- [false-left]
 false, γ ⊢ δ
 
+// trace pairs: none
 s, t, γ ⊢ δ
 ---- [conj-left]
 s & t, γ ⊢ δ
 
+// trace pairs: none
 γ ⊢ s, t, δ
 ---- [disj-right]
 γ ⊢ s | t, δ
 
+// trace pairs: none
 s, γ ⊢ δ
 t, γ ⊢ δ
 ---- [disj-left]
 s | t, γ ⊢ δ
 
+// trace pairs: none
 γ ⊢ s, δ
 γ ⊢ t, δ
 ---- [conj-right]
@@ -54,24 +61,24 @@ s | t, γ ⊢ δ
 
 // XXX
 // remove s => t? always make progress
+// trace pairs: none
 s => t, s, t, γ ⊢ δ
 ---- [impl-left]
 s => t, s, γ ⊢ δ
 
-// discussion about implication below
-// check how "normal sequent calculus handles this"
+// trace pairs: none
 s, γ ⊢ t, δ
 ---- [impl-right]
 γ ⊢ s => t, δ
 
-
-
 // box works as a kind of "forall" for concrete types
+// trace pairs: none
 box t, t, γ ⊢ δ
 ---- [box-left]
 box t, γ ⊢ δ
 
 // (.)-- filters the contexts.
+// trace pairs: premise[0] -- conclusion
 γ-- ⊢ t, δ--
 ---- [box-right]
 γ ⊢ box t, δ
@@ -82,6 +89,7 @@ box t, γ ⊢ δ
 // to exclude typedefs like
 // type A = A
 // Or that our cycle detection excludes paths between "identical" states.
+// trace pairs: none
 γ ⊢ expand(a[t..]), δ
 ----
 γ ⊢ a[t..], δ
@@ -92,6 +100,7 @@ a[t..], γ ⊢ δ
 
 
 // member types are filtered according to member name
+// trace pairs: premise[0] -- conclusion
 γ >> m ⊢ δ >> m
 ---- [member]
 γ ⊢ δ
@@ -99,11 +108,14 @@ a[t..], γ ⊢ δ
 
 // foralls are unwrapped and variable substituted with fresh name
 // i.e. we treat the bound variable nominally
+// trace pairs: premise[1] -- conclusion
 n fresh
 γ [n] ⊢ δ [n]
 ---- [forall]
 γ ⊢ δ
 
+// 1 + n! premises
+// trace pairs: i ∈ [1..(n! + 1)], premise[i] -- conclusion
 c, γ*  ⊢ a_1, ..., a_n
 ∀ I ⊆ {1, ..., n}.
 	c, γ* ⊢ { a_i | i ∈ I }, δ*
@@ -113,7 +125,6 @@ c, γ*  ⊢ a_1, ..., a_n
 a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
 ```
 
-
 ### context operators
 
 * box filtering
@@ -136,6 +147,14 @@ a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ
                  γ [n]              otherwise
 ```
 
+### trace pairs
+Trace pairs are related to cyclic proofs. They identify the pairs of 
+`premise -- conclusion` that are *productive*, i.e. leads to some progress
+making a cycle in the proof tree admissable as a cyclic proof of the nodes in
+the cycle.
+
+The trace pairs are described in the comments for each subtyping rule.
+
 ### Semantic function subtyping
 
 *Here we try to give an intuitive explainer of how to reason about function