Stream: Coq users

Topic: Non strictly positive occurrence in recursive record?

Julio Di Egidio (Nov 02 2023 at 19:17):

Hi guys, here is a little piece of code inspired by some software development.

While I (more or less) understand the error message, how am I supposed to write this?

(** A generic filesystem item (type). *)
Inductive fsItem : Set := mkFSItem
{
  (** fields *)
  id : nat;
  isDir : bool;
  (** tree *)
  parent : option fsItem;
  children : option (list fsItem);
  (** props *)
  isValid : children = None <-> isDir = false;
}.
(*
  Non strictly positive occurrence of
  "fsItem" in
   "nat ->
    forall isDir : bool,
    option fsItem ->
    forall children : option (list fsItem),
    children = None <-> isDir = false -> fsItem".
*)

Gaëtan Gilbert (Nov 02 2023 at 19:58):

split between data and properties:

Section List.
Context {A:Type} (f:A -> Prop).
Fixpoint LForall (l:list A) :=
  match l with
  | nil => True
  | cons a l => f a /\ LForall l
  end.
End List.

Inductive fsItem0 : Set := mkFSItem
{
  id : nat;
  isDir : bool;
  parent : option fsItem0;
  children : option (list fsItem0);
}.

Fixpoint checkvalid fs :=
  let validparent := match fs.(parent) with None => True | Some parent => checkvalid parent end in
  let validchildren :=
    match fs.(children) with
    | None => fs.(isDir) = false
    | Some children => fs.(isDir) = true /\ LForall checkvalid children
    end
  in
  validparent /\ validchildren.

Definition fsItem := { fs | checkvalid fs }.

Julio Di Egidio (Nov 02 2023 at 20:06):

I see, thank you!

BTW, at a first glance I am puzzled that checking the parent does not lead to Coq complaining: doesn't that amount to an infinite loop? But I am in a rush, I'll have to come back to this later...

Gaëtan Gilbert (Nov 02 2023 at 20:08):

just because you call something "parent" doesn't mean it acts as a parent
in other words you won't be able to create fs1 and fs2 such that fs1.(parent) = Some fs2 and fs2.(children) = Some [fs1] (or any list that contains fs1)

Julio Di Egidio (Nov 02 2023 at 20:11):

No, I meant, if we call checkvalid on a node and that calls checkvalid on the parent, and that in turn calls checkvalid on the parent's children...

Gaëtan Gilbert (Nov 02 2023 at 20:19):

Require Import List.

Inductive fsItem0 : Set := mkFSItem
{
  id : nat;
  isDir : bool;
  parent : option fsItem0;
  children : option (list fsItem0);
}.

Definition self_loop fs :=
  match fs.(parent) with
  | None => False
  | Some parent =>
      match parent.(children) with
      | None => False
      | Some children => In fs children
      end
  end.

Fixpoint no_self_loop fs {struct fs} : self_loop fs -> False.
Proof.
  intros H;generalize H. (* get a copy of the self_loop hyp *)
  unfold self_loop.
  destruct (parent fs) as [parent|]. 2:trivial.
  destruct (children parent) as [children|]. 2:trivial.
  revert children.
  fix aux 1.
  intros [|child children].
  - clear aux. simpl;trivial.
  - simpl. intros [H'|H'].
    + clear aux.
      apply (no_self_loop child).
      rewrite H'. exact H.
    + exact (aux _ H').
Qed.

Gaëtan Gilbert (Nov 02 2023 at 20:20):

Julio Di Egidio said:

No, I meant, if we call checkvalid on a node and that calls checkvalid on the parent, and that in turn calls checkvalid on the parent's children...

the node does not appear in the "parent"'s "children"

Julio Di Egidio (Nov 02 2023 at 22:25):

Of course, given any node, its parent (if any) should have it in its children: indeed, that would be a global (as in a whole tree as opposed to a single item) validation criterion, which I just hadn't even considered above... Indeed, in that sense, I have now realized there is no way to construct a valid tree in the code I have shown: IOW, there is a design bug in that code.

I shall try and rewrite it, of course keeping the separation of data vs properties in mind. Thanks for now.

Gaëtan Gilbert (Nov 02 2023 at 22:33):

btw for this specific property of isDir vs children you could also make isDir a defined value instead of a field, ie

Inductive fsItem : Set := mkFSItem
{
  id : nat;
  parent : option fsItem;
  children : option (list fsItem);
}.
Definition isDir fs := match fs.(children) with None => false | Some _ => true end.

Julio Di Egidio (Nov 02 2023 at 22:41):

That's a tempting simplification but one I would advise against (in any language, this is about design): for one thing, it ties the semantics of that field value to details of the implementation/underlying representation...

Julio Di Egidio (Nov 02 2023 at 22:50):

If/when I get to the bottom of it, I'll show a complete example with a couple of levels in that hierarchy, since the inheritance patterns are also critical here. Then, with more substance, I think it's going to be easier discussing even the details.

Julio Di Egidio (Nov 04 2023 at 13:28):

@Paolo Giarrusso

That's a matter of naming, isn't it?

The short answer is no, but that's a good question and I do not have a definite answer to it: I trust the experts that the two situations do boil down to being equivalent from an operational point of view, OTOH that there is a change in semantics is a fact, as I have shown above.

Here is what I mean by "a change in semantics": imagine you are a programmer and your code relies on some external library to do this or that, and of course you might have a choice among different libraries that offer the same functionality under the same protocol (interface). The behaviour of your code at compilation time, which does affect what and how you write things (think the Fail command for example), now depends on (implementation details of?) the specific library you happen to be importing, and in ways that I doubt can be easily inspected (but on this I might just be wrong)...

Paolo Giarrusso (Nov 04 2023 at 13:38):

That scenario is a problem, but the standard answers are different: a type that allows cyclic data and one that doesn't are semantically very different.

Paolo Giarrusso (Nov 04 2023 at 13:39):

Re "as I have shown above", I don't know what you're hinting at.

Paolo Giarrusso (Nov 04 2023 at 13:42):

And BTW, because Coq doesn't allow cyclic data structures (ignoring coinductives), typical definitions of trees in Coq do not use parent links.

Julio Di Egidio (Nov 04 2023 at 13:42):

Sure, but a cyclic term is not a non-cyclic term is orthogonal, not an answer, to the above, standard or otherwise.

Paolo Giarrusso (Nov 04 2023 at 13:43):

Sorry, I can't parse that

Paolo Giarrusso (Nov 04 2023 at 13:45):

And we might need to agree on the context. Are we discussing a closed program in Coq, or a mixture of Coq and non-Coq code?

Julio Di Egidio (Nov 04 2023 at 13:47):

Paolo Giarrusso said:

And BTW, because Coq doesn't allow cyclic data structures (ignoring coinductives),
typical definitions of trees in Coq do not use parent links.

Maybe this is a matter of terminology, but the tree above is cyclic. Not to mention a tree node with a parent link is the opposite of uncommon...

As for "non-Coq" code I think at this point you should simply reread the thread, you are confusing things...

Paolo Giarrusso (Nov 04 2023 at 13:48):

I agree parent links are common outside Coq. That doesn't carry over to Coq; total programming languages are fundamentally different in some ways, by necessity.

Julio Di Egidio (Nov 04 2023 at 13:49):

There is nothing non-total in what I have written not to mention what I am after: with all due respect, you are simply missing the point.

Paolo Giarrusso (Nov 04 2023 at 13:51):

Maybe this is a matter of terminology, but the tree above is cyclic.

The code above contains no trees, only a type of trees. I can agree that type "is cyclic" :-). I am only saying you will not be able to construct concrete data containing cycles.

Notification Bot (Nov 04 2023 at 13:51):

Paolo Giarrusso has marked this topic as unresolved.

Paolo Giarrusso (Nov 04 2023 at 13:53):

indeed, Gaëtan's no_self_loop proves at least that certain kinds of cycles are impossible — a node fs : fsItem0 cannot appear among the children of its parent.

Paolo Giarrusso (Nov 04 2023 at 14:04):

I've reread the thread — I'm sure there's a miscommunication, but if you want to fix it you might have to be clearer. Or maybe just try fixing the "design bug" you described to clarify what you're after.

There is nothing non-total in what I have written not to mention what I am after

I'm not sure that's adequate. Coq decides to accept what you call "an infinite loop" and reject inputs that would make it loop. So, inside Coq, that function behaves in no way as an infinite loop. If you extracted it outside Coq, things are more complex. That's why I asked if you planned to use extraction.

Gaëtan Gilbert (Nov 04 2023 at 14:06):

Julio Di Egidio said:

There is nothing non-total in what I have written not to mention what I am after: with all due respect, you are simply missing the point.

I don't know what the point is supposed to be either

Julio Di Egidio (Nov 04 2023 at 14:56):

Gaëtan Gilbert said:

Julio Di Egidio said:

There is nothing non-total in what I have written not to mention what I am after: with all due respect, you are simply missing the point.

I don't know what the point is supposed to be either

Which point? You extract a fragment from a conversation that is literally few lines above, I am the one who is at least perplexed.

One thing I have not mentioned about applications: while it is common to have a structure as above in software development, the problem that one cannot validate a tree until after full construction, and node construction itself happening in stages, is rather part of the pattern (notice: we don't need Coq specifically to encounter that). And part of the pattern is also that in that context we would never write a validateTree that walks up the parent chain: validation is only from a node down, i.e. on the tree of which that node is the root.

Anyway, I was more interested into the Section semantics issue. I think we risk to be discussing the sex of angels here.

Dominique Larchey-Wendling (Nov 04 2023 at 15:10):

Julio Di Egidio said:

I am not sure I understand the implications of that, except that using sections changes the semantics of definitions... But I guess that's yet another topic.

Beware that the guard condition, which the guard checker verifies, is a very syntactic notion. You can observe the same issue with nested uses of the map function where the function parameterf is either a parameter of the Fixpoint or part of its environment. If not a parameter, the guard checker can unfold the definition of f, detect and hence accept a nested fixpoint.

Julio Di Egidio (Nov 04 2023 at 15:38):

Dominique Larchey-Wendling said:

Julio Di Egidio said:

I am not sure I understand the implications of that, except that using sections changes the semantics of definitions... But I guess that's yet another topic.

Beware that the guard condition, which the guard checker verifies, is a very syntactic notion. You can observe the same issue with nested uses of the map function where the function parameterf is either a parameter of the Fixpoint or part of its environment. If not a parameter, the guard checker can unfold the definition of f, detect and hence accept a nested fixpoint.

Thank you @Dominique Larchey-Wendling for explaining in detail.

I would maintain we also get a semantic difference there, in the sense (and with the consequences) I have tried to illustrate upthread. I will venture -for the sake of exploring this more, I am far from an expert in formal semantics- a more precise characterization: the operational semantics is the same (they behave equivalently), the denotational semantics is not (at coding/compilation time, which is also the code we read, the two situations are not equivalent).

Paolo Giarrusso (Nov 04 2023 at 15:47):

Which two situations? Dominique was replying about LForall with or without sections — if the definition without section were accepted it'd be equivalent to the other operationally and denotationally (except maybe for some technical details of reduction)

Paolo Giarrusso (Nov 04 2023 at 15:48):

Your point upthread, to the best of my understanding, was about a different comparison?

Julio Di Egidio (Nov 04 2023 at 15:54):

The code I have posted here compiles if LForall is in a section, it doesn't otherwise, and those are the two "situations":
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Non.20strictly.20positive.20occurrence.20in.20recursive.20record.3F/near/400294094

The "illustration" I am talking about is in my very first reply to you: << Here is what I mean by "a change in semantics" [...] >>

Paolo Giarrusso (Nov 04 2023 at 15:56):

ah, I couldn't imagine that's what you meant. I think the ambiguity goes back to "that function" here:
https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Non.20strictly.20positive.20occurrence.20in.20recursive.20record.3F/near/400294744

I thought you meant that we can't call the working version of fsValidTree

Paolo Giarrusso (Nov 04 2023 at 15:58):

so, part of the misunderstanding is simply due to the ambiguity of pronouns.

Julio Di Egidio (Nov 04 2023 at 15:59):

Paolo Giarrusso said:

ah, I couldn't imagine that's what you meant. I think the ambiguity goes back to "that function" here:
I thought you meant that we can't call the working version of fsValidTree

I am not even sure what you mean by that. You keep rephrasing and in ways that keep altogether changing the topic. To the best of my understanding.

Paolo Giarrusso (Nov 04 2023 at 16:00):

well, there are two separate topics — "infinite loops" and the two variants of LForall here. You've suggested sticking to the second, that sounds simpler indeed.

Paolo Giarrusso (Nov 04 2023 at 16:02):

if it seems like I was changing the topic, it's just because of the earlier misunderstanding which you've now clarified.

Julio Di Egidio (Nov 04 2023 at 16:02):

Paolo Giarrusso said:

well, there are two separate topics — "infinite loops" and the two variants of LForall here. You've suggested sticking to the second, that sounds simpler indeed.

I have suggested no such thing.

Paolo Giarrusso (Nov 04 2023 at 16:03):

did I misunderstand this part?

Anyway, I was more interested into the Section semantics issue. I think we risk to be discussing the sex of angels here.

Paolo Giarrusso (Nov 04 2023 at 16:03):

the semantics of Section in this case, and the difference between the two versions of LForall, seem the same topic.

Paolo Giarrusso (Nov 04 2023 at 16:05):

And yes, the two versions of LForall behave indeed differently for clients in this case, since they affect what programs can be written.

Paolo Giarrusso (Nov 04 2023 at 16:24):

And yes it's not ideal but it's hard to avoid.
However, you suggest that the difference between the two versions of LForall might be a difference in implementation details:

The behaviour of your code at compilation time, which does affect what and how you write things (think the Fail command for example), now depends on (implementation details of?) the specific library you happen to be importing

However, in Coq the body of definitions/fixpoints is (unfortunately) always part of the interface, because clients can depend on their bodies in proofs. There are ways to achieve information hiding even in Coq, but (1) those probably warrant a separate thread if you're interested (2) in Coq, one can only implement fsValidTree if the definition of LForall is visible — otherwise, Coq's termination checker has no way to ensure that fsValidTree will terminate on all inputs.

Last updated: Oct 13 2024 at 01:02 UTC