Explanation of Accessibility?

Stream: new members

[aron]

The docs say:

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x,
Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

I'm not a mathematician, I don't understand a) what this means, and b) how this relates to well-foundedness. Could someone please explain what "accessible through r" means and how this relates to well-foundedness?

[aron]

Ah does it mean that: in order to prove that a recursive function terminates you need to prove that there is a "lowest state" that it gets into, i.e. the base case of the function after which there will be no further recursive calls? and providing an accessibility predicate for your parameter (or combination of parameters) is how you can prove that your function does indeed terminate?

[Robin Arnez]

Yeah right, the simplest example is on natural numbers, e.g.:

def test (x : Nat) : Nat := if x = 0 then 0 else test (x - 1) + 2

By making sure that the parameters is always smaller on recursive calls, we can never get into infinite recursion / an infinite loop.
This can then also be abstracted to other types where there is a similar "less than" relation that ensures we always get to a "base case" (in the case of natural numbers 0).

[Philippe Duchon]

aron said:

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x,
Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

I'm not a mathematician, I don't understand a) what this means, and b) how this relates to well-foundedness. Could someone please explain what "accessible through r" means and how this relates to well-foundedness?

Consider the relation r fixed; also, it's what is written <. Think of r x y as x<y.

Some x is accessible (for r) if (and only if) all y such that y<x are accessible (for r). It's not 100% clear that this is well defined; also, it somehow captures the idea that r is a well-founded order (even though there is no condition that r be an order relation).

If an element x has no smaller y, then it is accessible (because all the non-existent smaller y's are accessible); say, it is "level-1 accessible". Then, if all the y's that are smaller than x have no smaller elements, then they are all accessible, and so x is accessible, say "level-2 accessible".

Continue this pattern, defining all "levels" of accessibility; an element will be "level-k accessible" if all lower elements are accessible at levels $<k$.

Then, define an accessible element as one that is accessible at some level, and r to be well-founded if all elements are accessible.

It should be clear that if your order has an infinite decreasing sequence, then no element in the sequence is accessible (because "accessibility level" decreases when going to a smaller element) and so r is not well-founded. I think you need some form of the axiom of choice to prove the reverse, that if not all elements are accessible then you get an infinite decreasing sequence.

What this boils down to is that if you try to build a recursive function that only makes recursive calls on r-smaller elements, the function will always terminate if called on an accessible element.