From 14613724b56cd144e5ecd7c262ebd2aeedc0b4cc Mon Sep 17 00:00:00 2001 From: Ellen Arvidsson Date: Wed, 18 Jun 2025 15:14:38 +0200 Subject: [PATCH] clarification of covering --- README.md | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index 6ecbbf3..1f99d56 100644 --- a/README.md +++ b/README.md @@ -219,32 +219,48 @@ then any function in `intsec` maps `a_I_intsec` into `d`. If `a_I_intsec` happens to intersect with `c`, it "covers" a part of `c`. I.e. the set `I` can be understood as promising to map a part of `c` into `d`. -Defining this formally, we say that `I_cand ⊆ {1..n}` is a (d-)*candidate* if, +Defining this formally, we say that `I_cand ⊆ {1..n}` is a (`d`-)*candidate* if, ``` ∩[i ∈ I_cand] b_i ⊆ d ``` -Now, letting `IC = {I_cand_1..I_cand_k}` be the set of candidates, it is fairly -simple to see that +We can thus see a candidate `I_cand` as a combination, or more specifically, +intersection of the function types `{a_i -> b_i | i ∈ I_cand}`, that according +to the reasoning above promises to map a part of the domain into `d`, namely ``` -intsec <: c -> d +∩[i ∈ I_cand] a_i ``` -iff +A candidate thus "covers" part of the domain or formally speaking, `I` +(`d`-)covers a domain `s` if `I` is a (`d`-)candidate and +``` +s ⊆ ∩[i ∈ I] a_i +``` +If `IS ⊆ P({1..n})` then we say that `IS` (`d`-)covers `s` if all of `s` is +covered by some `I ∈ IS`, that is +``` +s ⊆ ∪[I ∈ IS | I is d-candidate] ∩[i ∈ I] a_i +``` + +Given the function types `{a_i -> b_i | i ∈ {1..n}}` and its set of candidates +`IC = {I_cand_1..I_cand_k}`, it is fairly easy to see that +``` +&[i ∈ {1..n}] (a_i -> b_i) <: c -> d +``` +iff `IC` `d`-covers `c`: ``` c ⊆ ( ∪[I_cand ∈ IC] ∩[i ∈ I_cand] a_i ) ``` -Using some pro gamer moves, we can see that this is equivalent to +Using some *pro gamer moves*, we can see that this is equivalent to ``` c ⊆ ( ∩[I_cand ∈ IC] ∪[i ∉ I_cand] a_i ) ``` This gives us the final form for our subtyping rule - ``` c, γ* ⊢ a_i | ... | a_n, δ* forall I ⊆ {1..n}. &[i ∈ I] b_i, γ* ⊢ d, δ* or c, γ* ⊢ |[i ∉ I] a_i, δ* ----- +---- [loads-o-fun] a_1 -> b_1, ..., a_n -> b_n, γ ⊢ c -> d, δ ```