[CakeML-Dev] CF to translator

[Magnus Myreen]

Excellent!

> 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:
> 1. Does the final theorem look like a strong enough connection?

Probably yes. I think Armaël might know better than me.

> 2. Do any of the cheated lemmas look false?

No -- but see my comment below about lemma 2

> 3. Does the Arrow definition look reasonable?.

Yes

> If there aren't any problems, then I can work towards upgrading the translator to use this definition, and proving the cheats.
>
> Final theorem:
>   |- Arrow a b f v ⇔ ∀x v1. a x v1 ⇒ app_basic p v v1 emp (cond ∘ b (f x))
>
> Cheated lemmas:
> (N.B. I want someone else to prove 2. I can tackle the rest.)
>
> 1. evaluate ck env s exp (s',r) ⇒ LENGTH s.refs ≤ LENGTH s'.refs
>
> 2. evaluate F env st exp (st',Rval res) ∧
>    SPLIT (st2heap p st') (g,st2heap p st) ⇒
>    st'.ffi = st.ffi

I'm happy to make a minor tweak to the definition of st2heap and prove
the following. I would appreciate help with proving lemma 2 from the
following.

SPLIT (st2heap p st') (g,st2heap p st) ==>
st'.ffi.io_events = st.ffi.io_events /\
st'.ffi.final_event = st.ffi.final_event

> 3. evaluate F env (empty_state with refs := s.refs) exp
>      (empty_state with refs := s.refs ++ refs',Rval x) ⇒
>    evaluate F env s exp (s with refs := s.refs ++ refs',Rval x)
>
> (s is 'ffi state, whereas empty_state is unit state)
>
> 4. evaluate F env s es (s',Rval r) ∧ s.refs ≼ s'.refs ∧ s'.ffi = s.ffi ∧
>    t = empty_state with refs := s.refs ∧
>    t' = empty_state with refs := s'.refs ⇒
>    evaluate F env t es (t',Rval r)
>
> Arrow definition:
> Arrow a b = (λf v. ∀x. AppReturns (a x) v (b (f x)))
> AppReturns P cl Q ⇔
>      ∀v.
>        P v ⇒
>        ∀refs.
>          ∃env exp refs' u.
>            do_opapp [cl; v] = SOME (env,exp) ∧
>            evaluate F env (empty_state with refs := refs) exp
>              (empty_state with refs := refs ++ refs',Rval u) ∧ Q u
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers