Instant-runoff-voting
An ACL2 Formalization of an Instant-Runoff Voting Scheme
The function irv formalizes the following instant-runoff
voting scheme.
The winner of an IRV election will be chosen as follows:
- If a candidate is the first choice of more than half of the voters, then
he/she wins. Otherwise:
- Adjust each ballot by eliminating the candidate with the fewest
first-place votes. If there is a tie for the fewest first-place votes,
then delete the candidate with the least second-place votes, and so on.
If the tie persists all through to the last-place level, then resolve it
using a tie-breaker function that picks exactly one candidate out of
those involved in the tie.
- Go to the first step.
See fairness-criteria for some fairness theorems about this
voting scheme. We also define a simpler version of IRV --- irv-alt --- that may be suitable for proofs of certain kinds of
properties.
Notes
- This IRV formalization accepts partial as well as total rankings; i.e., a
voter can choose to rank a subset of the candidates in the election.
- The tie-breaker function pick-candidate is constrained, so you can
define your own tie-breaker method for execution. By default, we attach the
function pick-candidate-with-smallest-id to pick-candidate to
pick the candidate with the smallest identifier.
Subtopics
- Fairness-criteria
- Some fairness theorems about irv
- Candidate-with-least-nth-place-votes
- Returns a candidate to be eliminated in step (2) of the IRV
algorithm
- Eliminate-candidate
- Eliminate candidate id from every voter's preference
list in xs
- First-choice-of-majority-p
- Returns the candidate, if any, who is the first choice of
more than half of the voters
- Candidate-ids
- Get a sorted list of candidate IDs currently in the election
- Irv
- Compute the winner of an IRV election
- Create-nth-choice-count-alist
- Create a count-alistp for nth-preference candidates
- Irv-alt
- An alternative (but equivalent) definition of irv,
with the majority step removed
- Irv-ballot-p
- Recognizer for a well-formed IRV ballot
- Majority
- Number-of-candidates
- List-elements-equal
- Returns t if all elements of x are equal to e
- Number-of-voters
