Reachability

Where can you get to from here — even when the roads go in circles?

reachability.js · output · proof · check · try it in the playground

The question

Picture four places, a, b, c and d, joined by one-way roads:

a ──▶ b ──▶ c ──▶ d
▲           │
└───────────┘

From a you can drive to b, from b to c, and from c either back to a or on to d. Nothing leaves d.

From each place, which places can you reach? The loop a → b → c → a means a careless search could go round forever.

What we tell eyecode

// One-way edges; c -> a closes the cycle a -> b -> c -> a.
fact(edge('a', 'b'))
fact(edge('b', 'c'))
fact(edge('c', 'a'))
fact(edge('c', 'd'))
implies(edge(X, Y), reachable(X, Y))
implies([reachable(X, Y), edge(Y, Z)], reachable(X, Z))

Four roads, and two rules:

• if there is a road from X to Y, you can reach Y from X;
• if you can reach Y from X, and there is a road from Y to Z, you can reach Z from X.

implies means “keep applying these until nothing new follows”. A premise written as an array, [A, B], holds when A and B both hold.

What eyecode concludes

reachable('a', 'b')   reachable('b', 'c')   reachable('c', 'a')
reachable('c', 'd')   reachable('a', 'c')   reachable('b', 'a')
reachable('b', 'd')   reachable('c', 'b')   reachable('a', 'a')
reachable('a', 'd')   reachable('b', 'b')   reachable('c', 'c')

12 conclusions (shown three per line). With no query, eyecode lists every fact it derived. From a, b or c you can reach all four places — including the place you started, by going round the loop. From d you reach nothing. And the run stops: once no new pair appears, eyecode is done.

Why: the proof in plain words

How do we know you can get from a back to a?

1. There is a road a → b — fact 1, so a reaches b — rule 5.
2. a reaches b, and there is a road b → c — so a reaches c — rule 6.
3. a reaches c, and there is a road c → a — so a reaches a — rule 6.

Every one of the 12 conclusions has a short chain like this, built only on the four roads we gave.

Checked, not just claimed

A separate checker read all 16 steps of the proof (the 12 conclusions plus the 4 road facts) against the program and confirmed that:

• every step is an exact instance of the line it cites (16 of 16);
• even though the roads loop, the reasoning never does: no conclusion depends on itself;
• every step serves one of the 12 conclusions.

Verdict: checked. Nothing taken on trust.

Try it

eyecode examples/reachability.js            # the answers
eyecode --proof examples/reachability.js    # with their proof

Or open it in the playground. Add a road fact(edge('d', 'e')) and run again: there are now 16 conclusions, because a, b, c and d can all reach e.

Takeaway

A loop in the data does not have to mean a loop in the reasoning. eyecode collects every reachable pair, stops when nothing is new, and backs each pair with a chain that leads straight back to the roads.