Quote: Original post by ToohrVyk

Quote: Original post by Steadtler
there exist at least one node on the open list with g(x) = L(x) and h(x) <= d(x,end)

Why?

• Perhaps the algorithm explores the destination node last (and so the open list is empty) but has failed somewhere during processing, making the path suboptimal.
  

Well any proof for an algorithm will assume that the algorithm is correctly executed. If the open list is empty, then you explored all possible paths and thus the algorithm must have returned the optimal path by brute force.

Quote: Original post by ToohrVyk

Even if the open list does contain nodes, how can you know for sure that the one on the optimal path satisfies g(x) = L(x) ? In fact, most of the nodes in the open list do not satisfy this property, otherwise Dijsktra would be an O(N) algorithm. This property is true, but it's not obvious and needs to be proven.

Such a node exist on the open list because the algorithm returned a non-optimal path. Thus it must exist on the open list a node that you should have choosen to lead to the optimal path but did not. Such a node will have g(x) = L(x) (by definition, else it would be another, "earlier" node) and h(x) < d(x,end) (because the heuristic is admissible).

Quote: Original post by Steadtler
Well any proof for an algorithm will assume that the algorithm is correctly executed. If the open list is empty, then you explored all possible paths and thus the algorithm must have returned the optimal path by brute force.

Your sentence contains two arguments: the fact that the algorithm is correctly executed and the fact that all nodes have been explored. Both these arguments apply to any search algorithm, not only A*. Therefore, if they were sufficient to prove that A* is correct, then they are sufficient to prove that, say, breadth-first search also finds the shortest path in a weighted graph. Consider this graph:

          B - C - D         /         \  start - A           F - G - end         \___ E ___/          

Let's assume that the lengths guarantee AE + EF > AB + BC + CD + DF (as such, the shortest path is ABCDFG). A breadth-first search will explore node F before node D, and thus the path found by it will be AEFG, which is suboptimal. This happens even if breadth-first has explored all nodes, and even if it has executed correctly.

This is akin to saying, "Fish have eyes, therefore they can breathe underwater". Fish can breathe underwater, but this isn't because they have eyes—humans have eyes too, but I don't really enjoy lungfuls of water.

In essence, there is a specific property of the A* algorithm which lets it find the shortest path, and this is what you need to mention in any correctness proof.

Quote: Such a node will have g(x) = L(x) (by definition, else it would be another, "earlier" node)

Nonsense. Also, the presence of quotes around "earlier" hints at overzealous hand-waving. You're trying to shorten the proof as much as you can, but you're dropping out fundamental arguments.

You're trying to show that g(x) = L(x) for a given node in the open list. Given the way g(x) is computed, this implies that you expect the closest explored neighbor of x, which we'll call y, to verify g(y) = L(y), so that g(x) = g(y) + d(x,y) = L(y) + d(x,y), which you hope is equal to L(x) but haven't formally proven either (and you won't be able to prove it, since you haven't really defined 'x' yet beyond its being in the open list, and that you hope g(x) = L(x) is true). And if you wish to prove g(y) = L(y), then you need a lot more words than "by definition", since it has nothing to do about definitions and everything to do about proving an algorithm invariant.

To prove the correctness of A*, you need to argue the fact that at any point during execution, for any explored node y so far, g(y) = L(y). This is your algorithm's invariant, and without it you cannot assume that the value of g(x) makes sense—because if g(y) wasn't the intended value for the explored nodes, then A* will compute an unintended value of g(x) for open list nodes as well, which makes g(x) = L(x) an awfully difficult assumption to make.

To prove that g(x) = L(x) for any explored node, you need to reason on the shortest path from start to x, since this is what L(x) represents. However, since your entire reasoning works around the shortest path from start to destination, you simply cannot prove that g(x) = L(x), which is why I consider your proof insufficient.

For those still wondering what the hell is going on and whether A* returns an optimal path always/sometimes/never...

A* is optimally efficient

That means that it guarantees to return the shortest cost path (if it exists) and in addition, guarantees to search no more nodes than any other algorithm on the same problem space.

In addition, A* guarantees to expand (search) every node within a given cost contour before expanding any node in a higher cost contour.

A* does this only if the following holds. For a cost-to-go function,

f(.) = g(.) + h(.)

being an additive sum of the expended cost, g(.), plus the estimated remaining cost, h(.), then for any two nodes x and y such that y is a child of x, A* is optimally efficient i.f.f.:

f(y) ≥ f(x) (so costs are monotonically increasing with search depth)
h(y) ≤ h(x) (estimated costs are monotonically decreasing with search depth)
h(y) ≤ h*(y) (estimated costs never over-estimate the actual future cost of any path through y)

For those that are interested the A* algorithm follows from Bellman's dynamic programming principle.

If you want a proof of these claims, see above... or I can post a shorter proof if needed.

Cheers,

Timkin

Maybe we can explain the role of the admissible heuristic in a more intuitive way.
A search algorithm can only produce a suboptimal result if after finding some portion of the optimal path, up to node n, decides to expand other nodes rather than continuing with n's neighbours (where the optimal path continues).
A* doesn't risk doing this mistake, because when it "blesses" a result it can guarantee that continuing from every node that is still "open" would be at least as expensive as the heuristic indicates and more expensive than the actual cost of the result; rather than ending with the first complete path, search is supposed to continue with candidates that might turn out better than the first expanded.
With an inadmissible heuristic, discarded paths are merely likely to be worse than the selected result, and/or guaranteed not to be much better; extending them to the destination would be required to be sure of the solution's optimality.

Quote: Original post by ToohrVyk

Quote: Original post by Steadtler
Well any proof for an algorithm will assume that the algorithm is correctly executed. If the open list is empty, then you explored all possible paths and thus the algorithm must have returned the optimal path by brute force.

Your sentence contains two arguments: the fact that the algorithm is correctly executed and the fact that all nodes have been explored. Both these arguments apply to any search algorithm, not only A*. Therefore, if they were sufficient to prove that A* is correct, then they are sufficient to prove that, say, breadth-first search also finds the shortest path in a weighted graph. Consider this graph:

You're loosing yourself, and are taking this way too seriously. First, we were not proving that A* is correct, but proving that A* is admissible. Then no, its not sufficient to prove that A* is either complete nor admissible, but thats not what I was saying either.

Quote: Original post by ToohrVyk
You're trying to show that g(x) = L(x) for a given node in the open list.
.

No, *again*, thats not what I wrote. More reading, less typing.

Quote: Original post by Steadtler
First, we were not proving that A* is correct, but proving that A* is admissible.

The proof I wrote, and from which this discussion stemmed, contained both a correctness proof and an admissibility proof. If all you provide is an admissibility proof, then:

• While literally correct, your statement that a shorter proof exists is not very meaningful (for almost every proof of X + Y, there exists a shorter proof of X alone).
  
  
• I would tend to believe that correctness implies finding any< path, while admissibility implies finding the best path only. As such, I'd be tempted to say that g(x) = L(x) should be proven as part of the admissibility proof, with the correctness proof being the same as that of breadth-first search. I'll assume,for the rest of the discussion, that g(x) = L(x) is proven through correctness, not admissibility.
  
  
• Then, your admissibility proof is too long. A shorter version is simply:
  "If A* is correct, it computes g(x) = L(x) for every explored node including g(end) = L(end), so it has constructed the shortest path from start to end."

The fact that I didn't consider correctness an acceptable assumption made my proof longer, since correctness itself is not as easy to prove. It certainly could be shortened by omitting non-essential details:

Initially, g(start) = L(start) = 0. If g(x) = L(x) for explored nodes, and y is explored, then g(y) = L(y): if it wasn't, the shortest path from start to y contains a non-explored node. If z is the first such node along that path, then g(z) = L(z) < g(y) and h(z) ≤ h(y), so f(z) < f(y) and so z would be chosen first. By contradiction, g(y) = L(y).

However, arguing that an admissibility-and-correctness proof could be made shorter, and then providing an admissibility-only proof to uphold that point, both leads to confusion and thus a length exchange of replies, and is not as constructive as providing a shorter proof which also includes correctness.

No one said A* was uncomplete or uncorrect, but frankly who cares. To quote that dear Eco, remove the plug, sir.

Quote: Original post by ToohrVyk
If z is the first such node along that path, then g(z) = L(z) < g(y) and h(z) ≤ h(y), so f(z) < f(y) ...

If h(z)≤h(y) then you're in serious troubles with regards to admissibility.