Jun 26 Meeting

TODO

1. prove transitivity based on translate condition + rewriting
2. try implementing Addeval method

prove transitivity based on translate condition + rewriting

The idea to try:

A' ~~> A
B' ~~> B
C' ~~> C
A << B1
A << B2
B1 <| B |> B2
B << C
then A << C


Proof:
1) rewrite B1, B2 to B1' and B2' (invertible)
2) Lemma: if A << B1 then A << B1'
3) Show A << C by A << B1' & B2' << C

Example and implication

A counterexample to the lemma(2):
(merge then subtyping)

   mu a. Top -> a & mu a . Int -> a
<: mu a. a -> a & mu a . Int -> a
<: mu a. (a -> a) & ( Int -> a)

apply the lemma to

   mu a. Top -> a & mu a . Int -> a
<: mu a. (a -> a) & ( Int -> a)

it does not hold that

   mu a. Top -> a & mu a . Int -> a
<: mu a. (a -> a)