Meeting Notes - Oct 2

Hi, for our meeting this week I am unable to make it at our scheduled time, as I need to attend Inria’s onboard training. Instead, I can write the problem I get stuck now. Perhaps we can think about it and discuss it next week?

The problem is, I cannot find a proper way to prove the corner case in transitivity to show A <: B, B <: C => A <: C when C is ordinary (but body splittable) and B is splittable. As we discussed last week, transitivity does not necessarily hold with arbitrary translated types:

             [b. (Top -> [a. Top -> Int])] & [b. b -> [a. a -> Bool]]
<:[might ok] [b. (b -> [a. a -> Int]) & (b -> [a. a -> Bool])]     
	         --- splittable
<:[might ok] [b. b -> [a. (a -> Int) & (a -> Bool)]]    
             --- ordinary, but body splittable
    
Might hold with a proper substitution on b 
(e.g. {b : Top} for all negative b's)

However, the conclusion

      [b. (Top -> [a. Top -> Int])] & [b. b -> [a. a -> Bool]]
<:[x] [b. b -> [a. (a -> Int) & (a -> Bool)]]  

is in no way derivable with any substitution, because the right type is not splittable, and merging positive + negative parts on the left is forbidden by the rules

The guess was, with a proper well-formed condition on the types, we can avoid the above counterexamples, as the translated types (with the correct substitutions) are not subtypes:

By translation, 

mu b. (b -> (mu a. a -> Int)) & (b -> (mu a. a -> Bool))
is not a subtype of
mu b. b -> (mu a. (a -> Int) & (a -> Bool))

because:


[b. 
	({b : (b -> [a. {a : a -> Int} -> Int]) & (b -> [a. **{a : a -> Bool}** -> Bool])}
	  -> [a. {a : a -> Int} -> Int])
  & ({b : (b -> [a. {a : a -> Int} -> Int]) & (b -> [a. **{a : a -> Bool}** -> Bool])}
	  -> [a. {a : a -> Bool} -> Bool])
]
<: [no]
[b. 
  {b: b ->
	[a. {a : (a -> Int) & (a -> Bool) } -> Int
	  & {a : **(a -> Int) & (a -> Bool)** } -> Bool ]
  } -> 
  [a. {a : (a -> Int) & (a -> Bool) } -> Int
	& {a : (a -> Int) & (a -> Bool) } -> Bool ]
]


** marks where the check fails

The problem is to find a proper well-formed condition that suits the proof. See the details of proof idea below:

The case in question is:

Given:
A <: B1, A <: B2
where B1 <| B |> B2
B <: [a. C] 
where [a. C] is ordinary (but body splittable) 

Show:
A <: [a. C]

Proof idea:
1) Since [a. C] is ordinary, we can prove that there exists body B'
   which is either the merges of positive mu-parts of B
	        or one of the negative mu-parts of B
   such that [a. B] <: [a. B'] <: [a. C]
   (this step is done as a lemma, as [a. C] is ordinary)

2) with B' being mu-part of B, we know A <: [a. B'] 
   (done as a lemma)
   
3) we need to invert on A <: [a. B'], to get a useful recursive body `A'` from the parts of A, so that we can apply the IH to `A' <: B' <: C` and then conclude the proof
    (this is the tricky part)
    
Note: a lemma we can show for the last step is
A <: [a. B'] => [all the mu-bodies of A] <: B'

However, the (extended) rule we have for subtyping is:

A' is merge of the positive mu-bodies of A
A' <: B
-------------
A <: [a. B]


A' is one of the negative mu-bodies of A
A' <: B
-------------
A <: [a. B]


so [all the mu-bodies of A], which can be a mix of pos/neg parts, is not useful here.


3)[approached again] 
We must find some useful recursive body `A'` which is either all positive or negative.

Note that, the lemma we did in Step 1), relies on the condition that the right type is ordinary. But for inverting `A <: [a. B']`, we do not have such a condition on the right type, so it cannot be applied here.

Instead, what we know is that [a. B'] is either the positive merges of B or one of the negative parts of B. So the hope here is to use the **well-formed** condition to prove that `A'` is also either all positive or negative.

Proof goal I am currently not sure how to solve:

- if B' is the merge of positive parts, A <: [a. B']
  then [all the mu-bodies of A] must be positive as well?

- if B' is a single negative part, then we should have a similar lemma like we have in step 1) but not just for ordinary right types:
  Lemma: If A <: [a. B] where a is negative in B, 
            A and B are well-formed 
         then there either exists a negative mu-body A' of A
         or A' as the merge of all positive mu-bodies of A 
         we have A' <: B

Currently I am not sure how to prove the above last two goals, as it is hard for me to find a well-formed condition that can help here. Maybe the proof idea is not entirely correct? Please let me know your thought

Thoughts for Oct 9

if B’ is the merge of positive parts, A <: [a. B'] then [all the mu-bodies of A] must be positive as well?

due to the chance of dropping negative fields on A. We should instead say:

if B’ is the merge of positive parts, A <: [a. B'] then [all the positive mu-bodies of A] must be subtype of [a. B'] as well?

This is still no true, consider: mu a. (a -> Int) & (Bool -> a) <: mu a. Bool -> a

---

which gives an idea of a counterexample :

• not done yet

   mu a. (a -> Int) & (Bool -> a)
&  mu a. (a -> String) & (Real -> a)
<:
   mu a. (Bool -> a) & (Real -> a)

but this counterexample does not extend to the case in transitivity proof, as we also have B <: C where C is ordinary (but body splittable), suggesting at least, nested recursive types. So there are some other conditions that we can exploit, which might still make proving A <: C possible.

We should say, those `b` in A must be positive?
A = 
   mu b. Top -> (mu a. (a -> Int) & (Bool -> a))
&  mu b. (Top -> (mu a. (a -> String) & (Real -> a)))
        & (b -> (mu a. a -> Float) ) <---- unused part, but affects the left-merges
<:
B = mu b. Top -> mu a. (Bool -> a) & (a -> String) & (Real -> a)
<:
C = mu b. b -> mu a. (Bool -> a) & (a -> String) & (Real -> a)


But B <: C can also be due to dropping fields in `B`

....
<:
B = (mu b. b -> mu a. (Bool -> a) & (a -> String) & (Real -> a)) & ....
<:
C = mu b. b -> mu a. (Bool -> a) & (a -> String) &  (Real -> a)
 

The fix to the rules? make the cont_pos stronger, to also compute those positive components of negative types with their negative parts removed?

~~Maybe the idea is that B <: C, with C ordinary but B splittable suggests that

• for B1 <| B |> B2
  • either B <: C achieved by merging two positive parts B1, B2
  • or B <: C achieved by taking one of the negative part B1 or B2
  • no merge on a negative can happen!~~

---

We are proving the negative lemma as csub_styp_mu_r_inv3 in Controlled Subtyping Coq:

if B' is a single negative part, then we should have a similar lemma like we have in step 1) but not just for ordinary right types:

Lemma: If A <: [a. B] where a is negative in B, A and B are well-formed then there either exists a negative mu-body A’ of A or A’ as the merge of all positive mu-bodies of A we have A’ <: B

• Relax the cont_pos constraint to see what changes