Let's ditch ordinals!

[volodeyka]

We had such definition of exec_event_structures

Structure exec_event_struct := Pack {
  N     : nat;
  lab   : 'I_N -> label;
  fpred : forall m : 'I_N, 'I_m.+1;
  frf   : forall (r : 'I_N), {w : 'I_r.+1 |
                              (w == r :> nat) (+) write_read_ext lab w r}
}.

And we decided to stop using dependent types and ordinals. And abstract to a random subset of identType (instead of ordinals). So we want to have E : identType and lab, fpred, frf to be functions defined on its finite subset. That's why we need a structure for a subclass of finite functions.

My idea was to make a structure which would be parametrized by
1) Dome Codome : eqType -- domain and codomain Type 2) dom : n.-tuple Dome or dom : {fset Dome}... -- elements on with our finite function will be defined 3) r : Dome -> Codome -> bool -- relation s.t. our function must be a sub relation of r 4) dflt : Dome -> Codome -- default function to coerce our finite function on the whole Dome And our structure of finite function should contain: 1) somehow coded finite function f on elements of dom 2) proof that forall x, r x (f x) (for example for fpred we should take r := <=)

Now I'm thinking to do something like that:

Structure rffun {n : nat} {Dome : choiceType} {Codome : eqType}
  (dflt : Dome -> Codome) (dom : {fset Dome}) (r : Dome -> Codome -> bool) := 
  Rffun {
  f : {ffun dom -> Codome};
  #[canonical(false)] dep : [forall x : dom, r (fsval x) (f x)]
}.

Any suggestions?

[eupp]

I generally agree, but the RFC needs to clearly outline possible solutions with their advantages/disadvantages, potential benefits/problems, etc.

But first, some minor stylistic comments. Instead of Dome/Codome we need to choose between Dom/Codom, just A/B, or aT/rT (ssreflect style). The r here can be seen as overapproximation of the function. We might want to reflect it in its name or in the documentation.

The main question is how to represent a function with finite support.

1. Using fsfun from math-comp-finmap. Advantages: we do not reinvent the wheel. The finmap library already has some theory formalized + some machinery (e.g. coercions, notations, etc). Disadvantages: (?)

2. Using n.-tuple-s. Advantages: (?) Disadvantage: will need to prove theory by ourselves and do a lot of tediuos work (define coercions, notations, etc). I see potentially a lot of overlap with fsfun here.

3. Continue using 'I_n as a domain of the function. Advantages: we can get some stuff for free (e.g. we'll have lab, fpred and frf to be instances of finfun for free, this in turn will give us decidable theory also for free). We then can coerce the event structure defined with 'I_n -> 'I_n functions to event structure with nat -> nat functions and prove that resulting functions have finite support. Disadvantages: 'I_n cannot be made an instance of identType, only coerced to nat which is an instance of identType.We can suffer from some boilerplate code and code duplication because of that.

We also should keep in mind the computational behaviour for all possible solutions. Although it is not critical for the first "proof-of-concept" milestone, we still need to care about the performance impact on the extracted interpreter for future uses.

I would like to see a more detailed analysis on each proposed solution before we decide which one to pick.

[volodeyka]

1. Using fsfun from math-comp-finmap. Advantages: we do not reinvent the wheel. The finmap library already has some theory formalized + some machinery (e.g. coercions, notations, etc). Disadvantages: (?)

There are three disadvantages that make work with fsfun in our situation very uncomfortable: 1) in finmap there are no lemmas about expanding its domain, so to do this we should get out finmap form fsfun, expand finmap's domain, and prove something to make it fsfun again. And we should prove a lot of things about our function that expands its domain 2) When we want to represent lab, fpred, frf in exec_event_structure, we want to state that all of these functions have the same domain. But because of 3) we can't just fix some set A, and ask something like domain fpred == domain frf == domain lab == A. 3) There is coercion from {fsfun K -> V of dflt_fun} to K -> V, that sends out-of-domain element x to dflt_fun x (where dflt_fun : K -> V). But it for fsfun there is one constaint: forall x, if it in f's domain then f x != dflt_fun x (where f : {fsfun K -> V}). But we want have id as dflt_fun (for fpred and frf), and it leads to have different domains for fpred and frf.

So using fsfun leads to having lots of tedious work.

But the new definition from my first post rffun solves all these problems 1) we can expand their domain like expanding the domain of rffun, and we should only proof dep, but we should prove it in all cases: r will be responsible for fpred and frf constraints 2) rffun parametrized by its domain, so we will be able to just fix some set A and look only on rffun with such domain 3) we will define coercion without constraint that was used in fsfun

• I tried to use rffun in eventsrtuctures.v and it worked very well

P.S. maybe we can use S/T (Source/Target) instead of Dome/Codome?

[eupp]

1. in `finmap` there are no lemmas about expanding its domain, so to do this we should get out `finmap` form `fsfun`, expand `finmap`'s domain, and prove something to make it `fsfun` again. And we should prove a lot of things about our function that expands its domain

Well, I think this one does not count as a disadvantage of fsfun, since we neither have update theory for your solution. We will have to develop it by our own in either case.

2. When we want to represent `lab`, `fpred`, `frf` in `exec_event_structure`, we want to state that all of these functions have the same domain. But because of 3) we can't just fix some set `A`, and ask something like `domain fpred == domain frf == domain lab == A`.

Well, this is not entirely true. Let's assume that es : {fset E} is the set of events of the event structure. Take, for example, the frf. We can say that it defined not on the whole set of events, but rather on the read events only, i.e. { e \in es | is_read e}. Then its domain does not match the domain of lab, which is defined for all events. Similarly for fpred --- we can say that it is defined only on events that have some predecessor. This approach also solves (3), as indeed, for all elements x in the domain we will have f x =/= x and for all x outside the domain f x = x (f is either fpred or frf).

P.S. maybe we can use S/T (Source/Target) instead of Dome/Codome?

We can also consider this option among other proposed above.

[volodeyka]

Well, I think this one does not cound as a disadvantage of fsfun, since we neither have update theory for your solution. We will have to develop it by our own in either case

Yes, but to update fsfun we should prove a facts about its constraint, and we don't need this constraint at all. However in rffun, we need only to prove dep containt, that we should prove somehow anyway: it just a general case of formulation fredand frf constant (and it's easy to expand ffun). So using fsfun leads to do lots of unseful job

Well, this is not entirely true. Let's assume that es : {fset E} is the set of events of the event structure. Take, for example, the frf. We can say that it defined not on the whole set of events, but rather on the read events only, i.e. { e \in es | is_read e}. Then its domain does not match the domain of lab, which is defined for all events. Similarly for fpred --- we can say that it is defined only on events that have some predecessor. This approach also solves (3), as indeed, for all elements x in the domain we will have f x =/= x and for all x outside the domain f x = x (f is either fpred or frf).

Such way leads to use sig, and writing something like domain frf ==.... But fist one -- using sig in practice cause a lot of problems: we saw it with ordinals, and last one cause lots of rewriting work, it much more better to have one domain and don't think how to transform it. Also if we put all constrains on relation r in rffun, we can use relation algebra to prove things about it.

[eupp]

Yes, but to update fsfun we should prove a facts about its constraint, and we don't need this constraint at all. However in rffun, we need only to prove dep containt, that we should prove somehow anyway: it just a general case of formulation fredand frf constant (and it's easy to expand ffun). So using fsfun leads to do lots of unseful job

Well, updating with x -> y we will only have to prove y =/= dflt x which looks manageable.

Such way leads to use sig, and writing something like domain frf ==.... But fist one -- using sig in practice cause a lot of problems: we saw it with ordinals, and last one cause lots of rewriting work, it much more better to have one domain and don't think how to transform it. Also if we put all constrains on relation r in rffun, we can use relation algebra to prove things about it.

We will not need to use sig. We also do not have to reason about the domain of the function explicitly. Just change dep : [forall x : dom, r (fsval x) (f x)] to dep : forall x, r x (f x)

[eupp]

I'll explain why I'm insisting on fsfun here. Your solution essentially looks like the re-implementation of fsfun to me, with some minor distinction. Let's have a look at fsfun definition:

Record fsfun := Fsfun {
  fmap_of_fsfun : {fmap K -> V};
  _ : [forall k : domf fmap_of_fsfun,
       fmap_of_fsfun k != default (val k)]
}.

It's defined in terms of fmap. Let's have a look at it too.

Record finMap : Type := FinMap {
  domf : {fset K};
  ffun_of_fmap :> {ffun domf -> V}
}.

It's essentially a domf: { fset K } plus a function of type domf -> V. Does it look familiar ? :)

Structure rffun {n : nat} {Dome : choiceType} {Codome : eqType}
  (dflt : Dome -> Codome) (dom : {fset Dome}) (r : Dome -> Codome -> bool) := 
  Rffun {
  f : {ffun dom -> Codome};
  #[canonical(false)] dep : [forall x : dom, r (fsval x) (f x)]
}.

So your proposal is essentially fsfun + additional constraint.

[eupp]

BTW, another solution for f x != dflt x problem could be to just handle it in upd function. That is, to have something like that:

Definition upd f x y := 
  if y == dflt x then f else ... (* perform actual update here *)

[eupp]

Actually, this looks like the update for fsfun.

https://github.com/math-comp/finmap/blob/7ea4ecca938eaa1f75b6b210dcb1a851083e2b89/finmap.v#L3767 https://github.com/math-comp/finmap/blob/7ea4ecca938eaa1f75b6b210dcb1a851083e2b89/finmap.v#L3792

@anton-trunov could you please verify this ?)

[volodeyka]

Ok, it is very difficult to reach an agreement offline, let's discuss it at meeting

[anton-trunov]

Actually, this looks like the update for fsfun.

@eupp That's correct. It's a pretty recent addition, not released yet. But we can always ask Cyril to make a new release and pin the dev version in our dependencies for the time being.

[anton-trunov]

But it for fsfun there is one constaint: forall x, if it in f's domain then f x != dflt_fun x

Ah, it does not work like this, actually :) Basically, when you pair a finite map with an arbitrary extension (default), the domain of the finite map gets filtered using the above disequality so it automatically holds.

[anton-trunov]

One more point: the finmap library is known to block computation, computing with it inside Coq is not going to work (And what it does to extraction remains to be seen). The way one is supposed to go here is to CoqEAL for computations. Although, one would have to extend CoqEAL to finite sets (it didn't support them the last time I looked at it).

One more way to go would be using the extructures library which uses data structures which compute. Although I'm not sure about the efficiency of reasoning with this library.

[eupp]

One more point: the finmap library is known to block computation, computing with it inside Coq is not going to work (And what it does to extraction remains to be seen). The way one is supposed to go here is to CoqEAL for computations. Although, one would have to extend CoqEAL to finite sets (it didn't support them the last time I looked at it).

One more way to go would be using the extructures library which uses data structures which compute. Although I'm not sure about the efficiency of reasoning with this library.

It is a serious problem.

I've looked at extructures, looks like they use simple sorted lists to model finite maps ... https://github.com/arthuraa/extructures/blob/d5dafd24990deb984ff0e1d4d4b1b2b340005763/theories/fmap.v#L77

But the library has an anologue of fsfun, although it has different name (which is kinda annoying). https://github.com/arthuraa/extructures/blob/master/theories/ffun.v

[anton-trunov]

It is a serious problem.

In my opinion, the other side of the problem, i.e. proving, can be even more serious. It's a bit of cheating but we can coerce extraction into compiling Coq finite maps to a well-established implementation of finite maps in OCaml. Also, extending CoqEAL sounds like a fun subproject to me :) I'll look into this issue a bit later.

[eupp]

It is a serious problem.

In my opinion, the other side of the problem, i.e. proving, can be even more serious. It's a bit of cheating but we can coerce extraction into compiling Coq finite maps to a well-established implementation of finite maps in OCaml. Also, extending CoqEAL sounds like a fun subproject to me :) I'll look into this issue a bit later.

Sounds like a plan to me. Developing certified extractable containers is an orthogonal problem. We can assume that implementation from the OCaml standard library is correct.

[volodeyka]

Should we close it for now? @anton-trunov @eupp

[anton-trunov]

Yeah, looks like we've moved on.