<div dir="ltr"><div><div><div>I have proved the following connection between CF's app_basic (as on master) and a revised formulation of the translator's Arrow, modulo 4 cheats. In this email, I will show: the final theorem proved, the cheated lemmas, and the new Arrow definition. I ask for the following feedback:<br>1. Does the final theorem look like a strong enough connection?<br>2. Do any of the cheated lemmas look false?<br>3. Does the Arrow definition look reasonable?.<br>If there aren't any problems, then I can work towards upgrading the translator to use this definition, and proving the cheats.<br><br></div>Final theorem:<br>  |- Arrow a b f v ⇔ ∀x v1. a x v1 ⇒ app_basic p v v1 emp (cond ∘ b (f x))<br><br></div>Cheated lemmas:<br></div>(N.B. I want someone else to prove 2. I can tackle the rest.)<br><br><div>1. evaluate ck env s exp (s',r) ⇒ LENGTH s.refs ≤ LENGTH s'.refs<br><br>2. evaluate F env st exp (st',Rval res) ∧<br>   SPLIT (st2heap p st') (g,st2heap p st) ⇒<br>   st'.ffi = st.ffi<br><br>3. evaluate F env (empty_state with refs := s.refs) exp<br>     (empty_state with refs := s.refs ++ refs',Rval x) ⇒<br>   evaluate F env s exp (s with refs := s.refs ++ refs',Rval x)<br><br></div><div>(s is 'ffi state, whereas empty_state is unit state)<br></div><div><br>4. evaluate F env s es (s',Rval r) ∧ s.refs ≼ s'.refs ∧ s'.ffi = s.ffi ∧<br>   t = empty_state with refs := s.refs ∧<br>   t' = empty_state with refs := s'.refs ⇒<br>   evaluate F env t es (t',Rval r)<br><br></div><div>Arrow definition:<br>Arrow a b = (λf v. ∀x. AppReturns (a x) v (b (f x)))<br>AppReturns P cl Q ⇔<br>     ∀v.<br>       P v ⇒<br>       ∀refs.<br>         ∃env exp refs' u.<br>           do_opapp [cl; v] = SOME (env,exp) ∧<br>           evaluate F env (empty_state with refs := refs) exp<br>             (empty_state with refs := refs ++ refs',Rval u) ∧ Q u<br></div></div>