Four colours

Colouring the map of the European Union so that no neighbours match.

four-color.js · output · proof · check · try it in the playground

The question

Mapmakers like neighbouring countries to have different colours. A famous result, the four colour theorem, says four colours are always enough for any flat map.

Can eyecode colour the 27 countries of the European Union with red, green, blue and yellow, so that no two neighbours share a colour?

What we tell eyecode

The map, as a list of neighbours for each country:

fact(neighbours('Belgium', ['France', 'Netherlands', 'Luxemburg', 'Germany']))
fact(neighbours('Netherlands', ['Belgium', 'Germany']))
// … 24 more countries
fact(neighbours('Croatia', ['Slovenia', 'Hungary']))

query(colors('mapEU', _))

Islands such as Ireland, Cyprus and Malta have an empty list [].

How it colours

implied_by(
  places([[Place, Color], ...Tail]),
  [
    places(Tail),
    neighbours(Place, Neighbours),
    member(Color, ['red', 'green', 'blue', 'yellow']),
    not(conflict(Color, Tail, Neighbours)),
  ],
)

Countries are coloured one at a time, starting from the end of the list. Each takes the first colour from red, green, blue, yellow that no already-coloured neighbour has. not(...) means “it is not the case that”: here, there is no conflict. If a country is left without a colour, eyecode backtracks and revisits earlier choices.

The query starts from a list of [Country, Colour] pairs that findall builds with the colours still unknown, and once keeps the first complete colouring.

What eyecode concludes

One colouring of all 27 countries (excerpt):

colors('mapEU', [['Belgium', 'yellow'], ['Netherlands', 'green'],
  ['Luxemburg', 'green'], ['France', 'blue'], ['Germany', 'red'],
  ['Italy', 'red'], ['Denmark', 'green'], ['Ireland', 'red'],  // …
  ['Bulgaria', 'green'], ['Romania', 'red'], ['Croatia', 'red']])

Only red, green, blue and yellow are used; yellow is needed just twice, for Austria and Belgium.

Why: the proof in plain words

Gather all countries on the map into a list (27 of them).
Croatia goes first: red, since nothing is coloured yet.
Romania: red is fine, Croatia is not its neighbour.
Bulgaria: its neighbour Romania is red, so it takes green.
…and so on until Belgium, whose neighbours already use red, green and blue, so it gets yellow.

Each “no conflict” is a step in the proof.

Checked, not just claimed

The checker verifies 66 steps against the program, and confirms the one once step from the colouring beneath it. 28 steps are taken on trust and listed as obligations:

1 collected: the list of countries gathered with findall (“find all”) is assumed to be the complete map;
27 absent: one per country, “this colour clashes with no coloured neighbour”. eyecode searched and found no clash; the checker records that rather than proving a negative.

The checker did look for evidence against all 28 and found none.

Verdict: checked_with_obligations. 95 steps, 28 on trust.

Try it

eyecode examples/four-color.js

Swap the colour order to ['yellow', 'blue', 'green', 'red']: you get a different, equally valid map, starting with Belgium red. Or give Ireland a neighbour: change its line to fact(neighbours('Ireland', ['United Kingdom'])) and add fact(neighbours('United Kingdom', ['Ireland'])) — the UK becomes red and Ireland turns green.

Takeaway

A search that says “no clash here” is making a claim about what is not there. eyecode finds the colouring, shows each choice, and lists exactly which of those “nothing found” claims you are trusting.