Tony's Wiki

Apr 30 - Meeting

11 min read

  mu a. Top -> mu b. (b -> Int)
& mu a. Top -> mu b. (Int -> b)
& mu a. (Int -> (mu b. a -> Int) & (Int -> (mu b. a -> Bool)

<:

mu a. 
   a -> (mu b. (b -> Int) & (Int -> b))
 & Int -> (mu b. a -> Int) 
 & Int -> (mu b. a -> Bool)

Expected Lemma:

Lemma:
for any A << [Bi [a- |-> {a : B}] ]
there exists (invertible) C,
A << [C [a- |-> {a : C}]] << [Bi [a- |-> {a : B}] ]
and Bi << C << B

Example:

A = (mu a. Top -> a) & (mu a. a -> Int )

B = mu a. (Int -> a) & (a -> Int)

Consider the first Bi: [ Int -> a ]
what is between 
   (Int -> a) & (a -> Int)
and
   Int -> a?

Cannot be [Top -> a]

For weakly positive case we must rewrite the right substitution

Example:

A =  mu a. Top -> mu b. (b -> Int) 
   & mu a. Top -> mu b. (Int -> b)

B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

The translate subtyping will split B, but for reasoning we do not want to split B


With controled subtyping, we need to consider mcod(A)? ---- I think so, see lemma below


-------++++-------
What happen if we get into?
A =  mu a. Top -> mu b. (b -> Int) 
   & mu a. a -> mu b. ..... ?
B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

-------++++-------
Or, we keep the full splitting, but the intermediate type is going to be:

A1 =  mu a. a -> mu b. (b -> Int) & (Int -> b) <--- due to negative b inside

A2 =  mu a. a -> mu b. (Int -> b)

B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

Lemma Proposal

Lemma: for any T which is a precise split of B, if A << T [ a- |-> {a : B} ] and T is ordinary then

  • there exists C as part of A,
  • D as part of B, T as part of D,
  • invertible D such that B << D << precise(T) << T such that: mcod(C) [a- |-> {a: mcod(C)}] << D [ a- |-> {a : D} ] <<

Case Study 1

Case:

A =  mu a. Top -> mu b. (b -> Int) 
   & mu a. Top -> mu b. (Int -> b)

B = mu a. a -> (mu b. (b -> Int) & (Int -> b))


A1 = [Top -> [ {b : b -> Int} -> Int ] ]
For the T1 = [a -> [ {b : (b -> Int) & (Int -> b)} -> Int ]] fragment,
precise(T1) = [a -> [ ({b : (b -> Int) & (Int -> b)} -> Int) & (Int -> b) ] ]
which is invertible to : a -> mu b. (b -> Int) & (Int -> b)


From A1 << T1 [a- |-> {a : B}], we know that a is weakly positive in A1 and T1
so exists C:=A1, D:=precise(T1) << T1

then there exists D := mu a. a -> mu b. (b -> Int) & (Int -> b)

Case Study 1a

By tuning the negative b’s in B, an invertible function comes to be handy

invert([ T [a- |-> {a : B}] ]) = mu a. T if a does not appear negatively in T
invert([ T [a- |-> {a : B}] ]) = mu a. B if a appears negatively in T

What is the property/spec of invert?

The use of invert

B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

The invert of the first fragment of B:
  mu a. a -> (mu b. (b -> Int) & (Int -> b))
The invert of the second fragment of B:
  mu a. a -> (mu b. Int -> b)

B = mu a. a -> (mu b. (Top -> Int) & (Int -> b))
The invert of the first fragment of B:
	mu a. a -> (mu b. (Top -> Int) )
	+++ so that not only 
		A1 = mu a. Top -> mu b. (b -> Int) 
		but also
		A1 = mu a. a -> mu b. (b -> Int) 
		can be the subtype of invert(B1)
The invert of the second fragment of B:
	mu a. a -> (mu b. Int -> b)

Case Study 2 — non-equivalent negative

A = (mu b. Top -> (mu a. a -> (Top -> Bool)))
  & (mu b. Top -> (mu a. (a -> Int) & (a -> (Int -> Bool))))

B = mu b. b -> (mu a. (a -> Int) & (a -> (Top -> Bool)))

invert(B1) = invert(B2) = mu b. b -> (mu a. (a -> Int) & (a -> (Top -> Bool)))

Lemma Proposal - revisited

Lemma: for any T which is a precise split of B, if A << T [ a- |-> {a : B} ] and T is ordinary then

  • there exists C as part of A, such that:
   mcod(C) [a- |-> {a: mcod(C)}] 
<< invert(T) [ a- |-> {a : invert(T)} ] 
<< T [ a- |-> {a : B} ]

“ Case: A [a- |-> { a : A }] << T [ a- |-> {a : B} ]

  1. a is weakly positive in A and T
    • A [a- |-> { a : A }] << T [ a- |-> {a : invert(T)} ]
  2. a is compared negatively, {a : B} << {a : A}
    • B << A << T

Case: A << T1 [a- |-> {a : B} and A << T2 [a- |-> {a : B}], where T1 <| T |> T2

Lemma Proposal 3 - working with fragments

If we go for fully splits → then we should aim for single A such that B << A << T The hurdle is that for nested recursive types:

A =  mu a. Top -> mu b. (b -> Int) 
   & mu a. Top -> mu b. (Int -> b)
<<
B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

We tend to write

mu a. a -> mu b. (b -> Int)

for the intermediate type, instead of

mu a. a -> mu b. (b -> Int) & (Int -> b)



   [ Top -> [ {b : b -> Int} -> Int ] ]

<< (Can we say exists here ??)
   [ {a : ..... } -> [ { b : (b -> Int) & (Int -> b) }  -> Int
                      & Int -> b ] ] <--- We are not really sure "Int -> b" comes from the same source of Ai as the current fragment

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

Lemma Proposal 3 - working with one layer

If we are not working with fragments, but only split up to one layer of recursive type, then we must face the S-and case, where we need to combine IHs from splits

A =  mu a. Top -> mu b. (b -> Int) 
   & mu a. Top -> mu b. (Int -> b)
<<
B = mu a. a -> (mu b. (b -> Int) & (Int -> b))

If we treat B as a whole:

   [ Top -> [ {b : b -> Int} -> Int ] ] <~~~ mu a. Top -> mu b. b -> Int
 & [ Top -> [ Int -> b] ]               <~~~ mu a. Top -> mu b. Int -> b
<< [ {a : ..... } -> [ { b : (b -> Int) & (Int -> b) }  -> Int
                      & Int -> b ] ]

Goal is to show that

mu a. (Top -> mu b. b -> Int) & (Top -> mu b. Int -> b) are also valid subtypes of the RHS

[ Top -> [ { b : (b -> Int) } -> Int ]
& Top -> [ Int -> b]  ]

This is enabled by the fact that there are no negative a's !!

Do we get into cases where we have negative a’s ?

A1 [a- |-> {a : A1}] & A2 [a- |-> {a : A2}]
<< T [a- |-> {a : B}]

If a is negatively compared in A1 and T
then B << A1

If at this point A2 also contributes to the subtyping, which means 
A1 is not subtype of T, but A1 & A2 is subtype of T

do we get into trouble? or do we get into new reasoning?


>>>> A1 and A2 cannot be negative at the same time while also contributing to T, because: we get B << A1, B << A2, A1 & A2 << T, while not A1 << T and not A2 << T ?


If A1 is negative, A2 is positive,

   A1 [a- |-> {a : A1}] & A2 [a- |-> {a : A2}]
== A1 [a- |-> {a : A1}] & A2 [a- |-> {a : A1 & A2}]
<< T [a- |-> {a : B}]

How is this example rejected?
A =  mu a. a -> mu b. (b -> Int) 
   & mu a. Top -> mu b. (Int -> b)
   & mu a. a -> Int
<< (wrong)
B = mu a. (a -> (mu b. (b -> Int) & (Int -> b))) & a -> Int

we get B << A1, B << T (T is precise split of B), 
but A1 & A2 << T and not A1 << T
can we derive a contradiction?




we instantiate it:

B << A1
  (a -> [ ({b : (b -> Int) & (Int -> b)} -> Int) & (Int -> b) ])
& a -> Int
<< (wrong)
  a ->  [ ({b : (b -> Int)} -> Int) ]

A1 & A2 << T
   (a -> mu b. (b -> Int)) & (Top -> mu b. (Int -> b))
<< (a -> (mu b. (b -> Int) & (Int -> b))                 OK



The proof problem becomes:
	can we derive A1 << T somewhere?
	given that 
		A1 & A2 << T
		a is negatively compared in A1 and T (leading to B << A1)
		==> a is negatively compared in A1 and B (since T is precise part of B)

B  = (T & ...) << A1
A1 & A2 << T, where a appears negatively in A1 and T
[A1 [a- |-> {a : A1}]] & [A2 [a- |-> {a : A2}]] << T [a- |-> {a : B}]
T is precise part of B

Lemma: If A << T [a- |-> {a : B}] where T is a precise split of B, then there exists invertible C such that A << C [a- |-> {a : C}] << T [a- |-> {a : B}] Proof draft: Case S-rec: A [a- |-> {a : A}] << T [a- |-> {a : B}]

  • If a is weakly positive, then exists T, and T [a- |-> {a : T}] = T [a- |-> {a : B}]
  • If a is negatively compared, then B <: A <: T, let C:=T, OK Case S-spl: A << T1 [a- |-> {a : B}] and A << T2 [a- |-> {a : B}], where T1 <| T |> T2 By IH, (problem: we cannot apply IH since T1, T2 are no longer precise splits) exists invertible C1 and C2 such that
  • A << C1 [[a- |-> {a : C1}] << T1 [a- |-> {a : B}]
  • A << C2 [[a- |-> {a : C2}] << T2 [a- |-> {a : B}]
  • Cases 1): a is weakly positive in both C1 and C2, then C1 & C2 is invertible and satisfies the new relation: `A << C1 & C2 [a- |→ {a : C1 & C2}] << T1 & T2 [a- |→ {a : B}]“
  • Cases 2): a appears negatively reflexively in one subtyping, w.l.o.g. C1 and T1,
    • then B << C1 << T1

Alternative translate subtyping

Graph View

Backlinks