Stream: Coq users

Topic: I am struggling to understand well_founded


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Nov 24 2022 at 09:10):

So no infinite decreasing sequence becomes all decreasing sequences are finite.

view this post on Zulip walker (Nov 24 2022 at 09:14):

I understand what you said but I still feel lost.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Guillaume Melquiond (Nov 24 2022 at 09:24):

walker said:

nothing here says that the size of y is less than the size of x

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".

view this post on Zulip walker (Nov 24 2022 at 09:34):

alright I kind of understand to some degree. but is there good reading material on this ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Jan 29 2023 at 03:28 UTC