Library celebs
Roughly inspired by the article: Richard S. Bird, Sharon A. Curtis: Functional Pearls: Finding celebrities: A lesson in functional programming. J. Funct. Program. 16(1): 13-20 (2006)
Actually, more inspired by a discussion with Nicolas Oury on finding a formalization of the problem and implementing a solution in Coq. Original challenge idea due to Conor McBride.
The goal is to find the clique of celebrities among the guests of a party, knowing that there exists such a clique. The algorithm can then be done in linear time.
The set of people at the party.
Variable person : Set.
Predicate
celeb asserts celebrity.
Variables celeb : person -> Prop.
The type of persons who are celebrities
Definition celebrity : Set := sig celeb.
Who knows who ?
Variable knows : person -> person -> Prop.
Is decidable
Axiom knows_dec : forall x y, { knows x y } + { ~ knows x y }.
Pretty notations.
Notation " x 'knows' y " := (knows x y) (at level 20).
Notation " x 'knows_dec' y " := (knows_dec x y) (at level 20).
Statement that every celebrity is known by everyone.
Program Axiom guest_knows_celeb :
forall (c : celebrity) (g : person), g knows c.
Statement that every celebrity knows only celebrities (closed circle).
Program Axiom celeb_knows_celeb :
forall (c : celebrity) (g : person), c knows g -> celeb g.
We represent set of people by lists.
Definition persons := list person.
Abbreviation for being part of a clique. The
:> casts
subset objects to their underlying support type.
Notation " x 'In' l " := (In (x :>) l) (at level 20).
Definition in_clique p c :=
forall x, x In c -> (p knows x /\ x knows p).
Hint Unfold in_clique.
The
entry program builds the clique of VIPs from all the people
coming at the party using a (disposable) doorman which discriminate
between celebs and regular people.
The definition is clearly tail recursive hence we get a linear-time algorithm
as advertised in the paper.
Program Fixpoint entry (guests : persons)
(doorman : person | celeb doorman \/ exists x : celebrity, x In guests)
(clique : persons | in_clique doorman clique /\
(forall x : celebrity, x In guests \/ x `= doorman \/ x In clique))
{ struct guests } :
{ celebs : persons | forall x, x In celebs <-> celeb x } :=
match guests with
g :: gs =>
if doorman knows_dec g then
if g knows_dec doorman then
entry gs doorman (g :: clique)
else entry gs g nil
else entry gs doorman clique
| nil => doorman :: clique
end.
Obligations.
Skipping 7 obligations solved using the axioms.
We bootstrap the
entry program, asserting that guests
contains all existing people.
Program Definition find_celebs
(guests : persons | (exists x, x In guests /\ celeb x) /\ forall x, x In guests) :
{ celebs : persons | forall x, x In celebs <-> celeb x } :=
match guests with
| nil => !
| p :: ps => entry ps p nil
end.
Again, 3 obligations are generated that are easily solved