		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Candidate-with-least-nth-place-votes

Returns a candidate to be eliminated in step (2) of the IRV algorithm

Signature
(candidate-with-least-nth-place-votes n cids xs) → cid
Arguments: n — nth preference under consideration.
Guard (natp n).; cids — Candidates relevant in this round of tie-breaking (in ascending order).
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).
Returns: cid — Type (acl2::maybe-natp cid), given (and (natp n) (nat-listp cids) (irv-ballot-p xs)).

This function encodes step (2) of the IRV algorithm. If it can find exactly one candidate among cids with the fewest nth-place votes, then it returns that candidate. Otherwise, if it finds more than one candidate (i.e., if there is a tie), it goes on with its search among these candidates to pick one with the fewest n+1th-place votes, and so on. If the tie persists till we run out of candidates, then it returns the candidate with the smallest candidate ID.

For example:

(candidate-with-least-nth-place-votes 0 '(1 2 3 4) 
                                      '((1 2 3 4) (2 3 1 4) (3 2 1 4)))

Result: candidate 4
Reason: 4 has zero 0th-place votes.

(candidate-with-least-nth-place-votes 0 '(1 2 3) 
                                      '((1 2 3) (1 3 2) (3 2 1) (3 2 1) (2 3 1)))

Result: candidate 2
Reason: 2 has the fewest number of 0th-place votes.

(candidate-with-least-nth-place-votes 0 '(1 2 3) '((1 2 3) (1 3 2) (3 2 1) (2 3 1)))

Result: candidate 2
Reason: 2 and 3 are tied for fewest number of 0th, 1st, and 2nd place votes. So we pick 2, because it is lesser than 3.

Note that this function will not be called by irv on ballots where step (1) of the IRV algorithm applies, i.e., when there is a majority in the first-place votes.

Definitions and Theorems

Function: candidate-with-least-nth-place-votes

(defun candidate-with-least-nth-place-votes (n cids xs)
  (declare (xargs :guard (and (natp n)
                              (nat-listp cids)
                              (irv-ballot-p xs))))
  (let ((__function__ 'candidate-with-least-nth-place-votes))
    (declare (ignorable __function__))
    (b* (((when (endp cids)) nil)
         (n (lnfix n))
         ((unless (< n (number-of-candidates xs)))
          (pick-candidate cids))
         (count-alst (create-nth-choice-count-alist n cids xs))
         (candidates-with-min-votes
              (candidates-with-min-votes count-alst)))
      (if (equal (len candidates-with-min-votes)
                 1)
          (car candidates-with-min-votes)
        (candidate-with-least-nth-place-votes
             (1+ n)
             candidates-with-min-votes xs)))))

Theorem: maybe-natp-of-candidate-with-least-nth-place-votes

(defthm maybe-natp-of-candidate-with-least-nth-place-votes
  (implies
       (and (natp n)
            (nat-listp cids)
            (irv-ballot-p xs))
       (b* ((cid (candidate-with-least-nth-place-votes n cids xs)))
         (acl2::maybe-natp cid)))
  :rule-classes :rewrite)

Theorem: candidates-with-min-votes-is-a-subset-of-cids

(defthm candidates-with-min-votes-is-a-subset-of-cids
  (subsetp-equal (candidates-with-min-votes
                      (create-nth-choice-count-alist n cids xs))
                 cids))

Theorem: candidate-with-least-nth-place-votes-is-in-cids

(defthm candidate-with-least-nth-place-votes-is-in-cids
  (b* ((cid (candidate-with-least-nth-place-votes n cids xs)))
    (implies cid (member-equal cid cids))))

Theorem: candidate-with-least-nth-place-votes-returns-a-natp

(defthm candidate-with-least-nth-place-votes-returns-a-natp
  (implies (and (nat-listp cids)
                (consp cids)
                (irv-ballot-p xs))
           (natp (candidate-with-least-nth-place-votes n cids xs)))
  :rule-classes (:rewrite :type-prescription))

Subtopics

Candidates-with-min-votes: Returns a list of candidates, if any, which received the minimum number of votes
Pick-candidate-with-smallest-id: Pick candidate with the smallest ID.