Tony's Wiki

Compute the Intermediate Type v.2

8 min read

Based on weakly positive restriction for translated types Based on whether the variable appears on RHS negatively, we can define a relation that captures the way we compute intermediate types in Full Splitting

|-------------|
| A << B |> C |
|-------------|

a does not appear negatively in T?  <-- for the sake of complete case splitting
(or, Bm?)
A << T |> Bm
------------------------------------- rec-wkpos
   zeta a l. A [ a - |->  { l a : A } ] 
<< zeta a l. T [ a - |->  { l a : B } ] 
|> zeta a l. Bm [a - |->  { l a : Bm }]



a appears negatively in T
-------------------------------------
zeta a l. A [ a - |->  { l a : A } ] 
<< zeta a l. T [ a - |->  { l a : B } ] 
|> zeta a l. A [a - |->  { l a : A } ]



A2 << B2 |> Bm2
----------------------------------
A1 -> A2 << B1 -> B2 |> B1 -> Bm2


A1 << B |> C
------------------
A1 & A2 << B |> C


A2 << B |> C
------------------
A1 & A2 << B |> C



+ 1 special rule when B is toplike

Another idea

If all we need to look at is the negative occurrence of a in B, can we define a polarity-aware splitting on recursive types directly?

Note: this idea cannot work, because we may have Top -> ... <: a -> ... but a is still positive

E |- A <| B |> Bs




E, a |- A <| B |> Bs
-------------------------------------
E |- mu a. A <| mu a. B |> [ mu a. T | for T in Bs ]

Example Check:

We have merge then subtyping:

Despite
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. b -> String)
<: merge
    mu a. Top -> (mu b. b -> Int & Bool -> b & b -> String)
<: subtyping
	mu a. a -> (mu b. b -> Int & Bool -> b & b -> String)

It is not true that:
   ...
<:
	mu a. Top -> (mu b. b -> Int & Bool -> b) (----- REFL) 
&   mu a. a -> (mu b. b -> String)            (----- WEAKPOS)
<: [x] because the merge within b is strict not equivalent, it affects a
	mu a. a -> (mu b. b -> Int &  Bool -> b & b -> String)

we must merge then subtyping

Another issue with this example: we cannot find a proper measure?

We might NOT even be able to prove that, it is either wp or {B} <: {A}

by the rules, we find

   mu a. Top -> (mu b. b -> Int & Bool -> b)
<: mu a. Top -> (mu b. b -> Int & Bool -> b)
<: first split of ... 

   mu a. Top -> (mu b. b -> Int & Bool -> b)
<: mu a. Top -> (mu b. Bool -> b)
<: second split of ...

    mu a. Top -> (mu b. b -> String)
<: itself <: third split of ...

We have subtyping then merge

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

but not
  mu a. (Top -> a)
& mu a. (a -> Int & a -> Bool)
<: merge
& mu a. (Top -> a & a -> Int & a -> Bool)
<: subtyping -- no
  mu a. (Int -> a & a -> Int & a -> Bool)

by the rules we find

mu a. (Top -> a) <: mu a. (Int -> a) <: first split of
mu a. (a -> Int & a -> Bool) <: itself <: second/third split of

A Mixed Example

   
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Top -> b)
<: subtype
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Int -> b)
-- even if a <: Top is weakly positive, we cannot replace using
--  mu a. a -> (mu b. Int -> b)
-- also, we can not delay the subtyping 
-- since after the second merge b will be negatively compared
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Int -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b & Int -> b))
<:
	mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b)


though we may
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Top -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Top -> b)
<: subtype	
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Int -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b & Int -> b))
<:
	mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b)

So, the middle type should be:

1) mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b) --- a is pos, b is neg 
.    !!! Problem: this middle type is no longer supertype of mu a. A1 !!
     it has to be the supertype of mu a. A1 & mu a. A2 <: mu a. A1 & A2
2) mu a. a -> (mu b. Bool -> b)  -- a and b are pos
3) mu a. a -> (mu b. Int -> b)  -- a and b are pos

Expected Theorems

Then we are left to prove

Theorem. If A' ~~> A, A << B |> C, then there exists C' s.t. C' ~~> C (Easy)

Theorem. If A' ~~> A, B' ~~> B, Bi in spl(B), A << Bi |> C, then A << C << Bi

  • Proof in case rec-wkpos might be hard,
    • we get A << Bm << T from IH
    • but we need to show A [a- |-> {a : A}] << Bm [a- |-> {a: Bm}] << T [a- |-> {a : B}]
    • given only a ∈+ A << T, but we expect a ∈+ A << Bm
  • Therefore we need to prove another lemma:

Lemma. If A' ~~> A, B' ~~> B, Bi in spl(B), A << Bi |> C, then for any a, a ∈+ A << Bi implies a ∈+ A << C

since we cannot specify a concrete a, we have to state as an implication

  • Proof in case rec-wkpos:
    • a ∈+ A << T
    • IH tells for any a a ∈+ A << T implies a ∈+ A << Bm
    • Goal is to show for any b, if b ∈+ A [a- |-> {a : A}] << T [a- |-> {a: B}] then b ∈+ A [a- |-> {a : A}] << Bm [a- |-> {a : Bm}]

need to rely on substitution lemmas for weak pos

  • Proof in case rec-self: ok

Now prove the theorem again

  • Proof in case rec-wkpos:
    • we get A << Bm << T from IH
    • a ∈+ A << T, and applying the lemma, we get a ∈+ A << Bm
    • By a ∈+ A << T, we derive
    • A [a- |-> {a : A}] << Bm [a- |-> {a: Bm}] << T [a- |-> {a : B}]
      • LHS by a ∈+ A << Bm
      • RHS by Bm << T and B << Bm (? How)
  • Proof in case rec-self?

What is special about Top

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

but not merge then subtype

Idea: define two inductive relations, one for all weak pos , and search from RHS, the other for refl, search from LHS ?

Thm. A ~~> A

Graph View

Backlinks