Tony's Wiki

Jun 26 Meeting

4 min read

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)

Another attempt

We should instead try to argue that

If
B' ~~> B
B1 <| B |> B2
C' ~~> C
B << C
cord C
---------------
either B1 << C or B2 << C

Result: we proved transitivity with no extra conditions

Encoding

Extend constructor

Extend Attempt 4 - structural rules + encoding F< with intersection types with Neg constructor:

doubleNum[Exp] (self: NumSig<IDouble & Exp>) 
	: NumSig<IDouble & Exp, IDouble > = {
   Lit (val: Int) = fold [IDouble] { double = self.Lit (val + val) } ;
   Add (e1 : IDouble & Exp ) (e2 : IDouble & Exp ) = fold [IDouble]
      { double = self.Add 
		      (unfold [IDouble & Exp] e1).double  
		      (unfold [IDouble & Exp] e2).double
} 


type NegSig<Exp> = { Neg : Exp -> Exp };


evalNeg (self : Top) : NegSig<IEval> = {
		Neg (e : IEval) = fold [IEval] {
				eval = - (unfold [IEval] e).eval
		}
};

doubleNeg[Exp] (self: NegSig<IDouble & Exp>)
    : NegSig<IDouble & Exp, IDouble> = {
		Neg (e : IDouble & Exp) = fold [IDouble] {
				double = self.Neg (unfold [IDouble & Exp] e).double
		}
};



implLang = evalNum ,, evalNeg ,, doubleNum @ IEval ,, doubleNeg @ IEval
: Top -> NumSig<IEval, IEval>
& Top -> NegSig<IEval, IEval>
& NumSig<IDouble & IEval> -> NumSig<IDouble & IEval, IDouble>
& NegSig<IDouble & IEval> -> NegSig<IDouble & IEval, IDouble>
<: (NumSig & NegSig)<IDouble & IEval>
 -> NumSig<IEval, IEval> & NegSig<IEval, IEval>
  & NumSig<IDouble & IEval, IDouble>
  & NegSig<IDouble & IEval, IDouble>
<: (NumSig & NegSig)<IDouble & IEval>
 -> NumSig<IDouble & IEval, IEval & IDouble>
  & NegSig<IDouble & IEval, IEval & IDouble>
<: (NumSig & NegSig)<IDouble & IEval> -> (NumSig & NegSig)<IDouble & IEval>

evalAdd “binary method”


type IEvalAdd = mu X. { evalAdd : X -> Int };

eaddNum[Exp] (self: Top) 
	: NumSig<IEvalAdd & Exp, IDouble > = {
   Lit (val: Int) = fold [IEvalAdd] 
	   { evalAdd (e: IEvalAdd & IEval) = 
		   (unfold [IEvalAdd] e).evalAdd + val
	   } ;
   Add (e1 : IDouble & Exp ) (e2 : IDouble & Exp ) = fold [IDouble]
      { double = self.Add 
		      (unfold [IDouble & Exp] e1).double  
		      (unfold [IDouble & Exp] e2).double
}

compareDepth

type IDepthCmp = mu X. { depth : Int , isDeeper : X -> Bool }

depthCmpNum (self: Top) : NumSig<IDepthCmp> = {
	Lit (val : Int) = fold [IDepthCmp] {
	   depth = 1;
	   isDeeper (other : IDepthCmp) = 
		   (unfold [IDepthCmp] other).depth < 1)
	};
	Add (e1 e2 : IDepthCmp) = fold [IDepthCmp] {
	   depth = (unfold [IDepthCmp] e1).depth + 
			   (unfold [IDepthCmp] e2).depth;
	   isDeeper (other : IDepthCmp) = 
		   (unfold [IDepthCmp] other).depth <
		    1 + max((unfold [IDepthCmp] e1).depth, (unfold [IDepthCmp] e2).depth))
	};
}

type ICmp = mu X. { isDeeper : X -> Bool }
depthCmpNum (self: Top) : NumSig<IDepthCmp, ICmp> = {
	Lit (val : Int) = fold [ICmp] {
	   isDeeper (other : ICmp) = 
		   (unfold [IDepthCmp] other).depth < 1)
	};
	Add (e1 e2 : IDepthCmp) = fold [ICmp] {
	   isDeeper (other : ICmp) = 
		   (unfold [IDepthCmp] other).depth <
		    1 + max((unfold [IDepthCmp] e1).depth, (unfold [IDepthCmp] e2).depth))
	};
}

Graph View