walker (Nov 24 2022 at 09:05): walker (Nov 24 2022 at 09:05):Acc, well_founded, and well_founded_induction makes zero sense to me, I understand the very high level idea that well founded recursion induction is one that is structurally decreasing, but I cannot link that high level idea to those three definitions.
Théo Winterhalter (Nov 24 2022 at 09:09):Well it is the constructive counterpart of no infinite decreasing sequence: an element is accessible if all the smaller elements are accessible. The base elements are accessible because there are no smaller ones, and then basically you say that for an accessible element, all decreasing paths reach one of the base elements eventually.
Théo Winterhalter (Nov 24 2022 at 09:10):So no infinite decreasing sequence becomes all decreasing sequences are finite.
walker (Nov 24 2022 at 09:14):I understand what you said but I still feel lost.
walker (Nov 24 2022 at 09:18): Inductive Acc (x: A) : Prop :=
Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
nothing here says that the size of y is less than the size of x
Guillaume Melquiond (Nov 24 2022 at 09:20):First, do you agree that Théo's definition "an element is accessible if all the smaller elements are accessible" is exactly what the type of the Acc_intro constructor means? Second, by definition of inductive types in Coq, any object of type Acc R x looks like a finitely deep tree (though possibly infinitely branching). If you combine both parts, then you get the usual meaning of a well-founded order.
Gaëtan Gilbert (Nov 24 2022 at 09:20):consider something like
Fixpoint foorec {A} (l:list A) n (H:length l = n) {struct n} := ... (* eg recurse on "remove x l" knowing that x was in l *)
Definition foo {A} l := @foorec A l (length l) eq_refl.
ie recursion based on the size of the list
the relation given to Acc (ie R) is a generalized version of "the first one is smaller than the second one"
Guillaume Melquiond (Nov 24 2022 at 09:24):walker said:
nothing here says that the size of
yis less than the size ofx
It is not the size; it is y itself that is smaller than x. And "smaller" is just a word used to shorten "in relation with respect to R".
walker (Nov 24 2022 at 09:34):alright I kind of understand to some degree. but is there good reading material on this ?
Théo Winterhalter (Nov 24 2022 at 10:01):I tried to explain it in Chapter 21 of my PhD thesis. I'll let you judge whether it's a good reading material or not.
Dominique Larchey-Wendling (Nov 24 2022 at 14:42):One important thing to understand is that the finiteness @Théo Winterhalter is talking about is build in the Inductive keyword. There is no notion of size in well foundedness in the sense of something that (computably) mesures values in A. The mesure lies instead in the tree that is the proof of the Acc R x predicate which live in Prop.
You should read the code of both Acc_rect and Fix_F in the Wf module of the standard library. Notice that Acc_rect is auto-generated so you can just Print Acc_rect. They both proceed by structural induction on the proof of the Acc R _ predicate.
Dominique Larchey-Wendling (Nov 24 2022 at 14:57):Also notice that the Acc predicate captures more than just the impossibility of infinite decreasing R-sequences. It captures the finite termination of any process that unfolds along R, not just those given by a law (eg decreasing sequences in nat -> A). I am quoting Th. Coquand here.
Last updated: Sep 26 2023 at 13:01 UTC