eyedia

Shortest Path

The cheapest way from A to D, and the honest fine print behind “cheapest”.

shortest-path.pl · output · proof · check · try it in the playground

The question

A small road map: four places, five one-way roads, each with a cost (think minutes, or kilometres).

a --4--> b --3--> d
a --2--> c --1--> b
         c --8--> d

What is the cheapest way to get from a to d?

Finding a route is easy. Saying a route is the cheapest means saying that no cheaper route exists — a claim about everything you didn’t pick.

What we tell Eyedia: the map and the routes

edge(a, b, 4).
edge(a, c, 2).
edge(c, b, 1).
edge(b, d, 3).
edge(c, d, 8).
path(X, Y, Cost) :+ edge(X, Y, Cost).
path(X, Z, Cost) :+ path(X, Y, Before), edge(Y, Z, Weight), Cost is Before+Weight.

A road is a path; a path followed by one more road is a longer path, and the costs add up. The :+ means “keep applying this until nothing new follows”.

What we tell Eyedia: “cheapest”

cheaper(X, Y, Cost) :- path(X, Y, Other), Other < Cost.
shortest(X, Y, Cost) :+ path(X, Y, Cost), \+ cheaper(X, Y, Cost).
true :+ shortest(a, d, Cost).

\+ means “not”. A path is the shortest if there is no cheaper path between the same two places. The last line asks the question.

Eyedia first finishes listing all paths, and only then looks for “no cheaper one”, so the search for something cheaper is over a complete list.

What Eyedia concludes

shortest(a, d, 6).

There are three ways from a to d, costing 7 (via b), 10 (via c) and 6 (via c, then b). The cheapest costs 6.

Why: the proof in plain words

  1. Road a → c costs 2 — fact 2, so there is a path of cost 2.
  2. Road c → b costs 1 — fact 3; path a → b now costs 2 + 1 = 3.
  3. Road b → d costs 3 — fact 4; path a → d now costs 3 + 3 = 6.
  4. No path from a to d is cheaper than 6 — searched, none found.
  5. So the shortest a → d costs 6 — the shortest rule.

Steps 1–3 are shown in full. Step 4 is different: it is a claim that something does not exist.

Checked, with one obligation

An absence means Eyedia looked through everything it knows and found no cheaper path. A proof can show a path exists; it cannot show one doesn’t. So the checker records this as an obligation, and checks that nothing in the proof contradicts it — no cheaper path appears there.

Verdict: checked_with_obligations.

Strict mode

If you need a proof with nothing taken on trust, ask for it:

node bin/eyedia.js --proof examples/shortest-path.pl > /tmp/sp-proof.pl
node bin/eyedia.js --strict-proof --check-proof /tmp/sp-proof.pl examples/shortest-path.pl

The strict check refuses this proof — verdict failed(1) — because it leans on the trusted absence. Nothing is wrong with the answer; strict mode just does not accept “searched and found nothing” as evidence.

Try it

node bin/eyedia.js examples/shortest-path.pl            # the answer
node bin/eyedia.js --proof examples/shortest-path.pl    # with its proof

Or open it in the playground. Add a direct road edge(a, d, 5). and run again: the answer becomes shortest(a, d, 5).

Takeaway

“Best” always hides a “nothing better exists”. Eyedia shows the route it found, and tells you plainly which part of the answer is a search that came up empty.

This site is open source. Improve this page.