Image of a computation

[YaZko]

Hey everyone,

This bit of theory comes from our Vellvm project, and has hence been co-authored with @Chobbes, @euisuny and @Zdancewic . It's been long due cleaning up things and porting it to the itree library.

We define in the PR a binary predicate Image (renamed from Returns in Vellvm) such that Image a t captures values a that can be reached in leaves of t. This notion is defined here concretely, but is being explored, among other things, more abstractly by @euisuny as part of another project.

The notion can be useful for various reasons, such as defining restricted notions of refinement over only terminating computations for instance. But the main general motivation is an enriched up-to bind context valid reasoning principle, reducing the domain over which continuations need to be proven related. This is in particular captured by the corollaries eutt_clo_bind_gen and eutt_eq_bind_gen.

Notably, we do not provide any theory related to [iter] in this PR, although I believe @euisuny has this in store.

I stored this file in Core, let me know if anyone thinks there's a better place. More generally, any complaints or requests before merge are welcome!

Best, Yannick

[Lysxia]

eutt_clo_bind_gen seems equivalent to using the original eutt_clo_bind with a sufficiently strong UU. If so, would that avoid the need for the Image relation?

[Lysxia]

I see Image is useful for reasoning about DiamondFinite, since in fact DiamondFinite t <-> exists x, Image x t so facts about DiamondFinite are direct consequences of facts about Image .

Facts of the form Image x t -> Q x are equivalent to has_post t Q, I wonder whether that could be used to reduce the number of lemmas by privileging one or the other formulation.

[YaZko]

Thanks for the comments!

eutt_clo_bind_gen seems equivalent to using the original eutt_clo_bind with a sufficiently strong UU. If so, would that avoid the need for the Image relation?

Well, yes and no. That is true that fun a => Image a t is the strongest post-condition and hence that you can prove that you can always enrich R in an eutt R t u with the images of t and u, and therefore then recover eutt_clo_bind_gen with eutt_clo_bind over this enriched R. But the pattern is sufficiently universal and useful to explicit it I believe, which is precisely what eutt_clo_bind_gen proves in a sense: you don't have to worry about this intersection, you can just get it for free.

Similarly, you are right that you can recover Image as the strongest post, or as the intersection of all PERs in the diagonal (@euisuny is looking at a bunch of related stuff). However the Image is useful in itself notably to inverse eutt equations between binds, defining binds over itree E R -> Prop, ... While has_post is a convenient abstraction to do good old Hoare-style proofs.

So I would tend to argue that having all concepts is useful, even if they are indeed related.

Unless you just mean that the concrete definition of Image is spurious and it could just be defined as the strongest postcondition. That I could agree with, although I don't dislike having a syntactic caracterization of it.

[Lysxia]

Can I rename Image to Leaf?

[YaZko]

I kinda liked image because it is really the good old image of a function but for an impure in the itree sense one, but Leaf is cute, so sure!

[Zdancewic]

I would point out that the definition of image works for any monad that has a suitable definition of EqMR, and "Leaf" is maybe not appropriate for all monads...

[Lysxia]

By EqMR do you mean something of type (a -> b -> Prop) -> (m a -> m b -> Prop)? I see how you can define has_post from that, but can you define Image with it also?

[YaZko]

Yes that's essentially what Steve means. You abstract the structure of (itree E, fun R => eutt R) to an arbitrary monad (M, eqmR) with a proper axiomatization of this eqmR. Then you can define the "Image m" for a computation m : M X as the intersection of all the PER R such that eqmR R m m. @euisuny has defined all of this in a repo of her own, she can point you to it if you're interested.

I still do not mind the name Leaf since here precisely it's the concrete definition as an inductive crawling explicitly the tree down to the leaves. It coincides with the "semantic" caracterization of the Image for itrees, but it's not too shocking to me to have a different name. I don't have a strong opinion either way.

[Lysxia]

I see! We can use the name later for a class/general definition. (Though while we're bikeshedding names, Image is missing a notion of antecedent to be the image of, so I would prefer something like Returns.)

[YaZko]

Yes Image would be a better parallel with Sets on ktrees / Kleisli in general, I agree.

[Zdancewic]

Returns would also be good! (One could also imagine using Returns for a typeclass and Leaf for the more specifically named itree instance of it.