Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
Documentation.SBV.Examples.TP.Majority
Contents
Description
Proving Boyer-Moore's majority algorithm correct. We follow the ACL2 proof closely, which you can find at https://github.com/acl2/acl2/blob/master/books/demos/majority-vote.lisp.
Synopsis
- majority :: SymVal a => SBV a -> SInteger -> SList a -> SBV a
- mjrty :: SymVal a => SList a -> SBV a
- howMany :: SymVal a => SBV a -> SList a -> SInteger
- correctness :: SymVal a => IO (Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool))
Calculating majority
majority :: SymVal a => SBV a -> SInteger -> SList a -> SBV a Source #
Given a list, calculate the majority element using Boyer-Moore's algorithm. Note that the algorithm returns the majority if it exists. If there is no majority element, then the result is irrelevant.
mjrty :: SymVal a => SList a -> SBV a Source #
We can now define mjrty, which simply feeds the majority function with an arbitrary element of the domain.
By the definition of majority
above, this arbitrary element will be returned if the given list is empty.
Otherwise, majority will be returned if it exists, and an element of the list otherwise.
howMany :: SymVal a => SBV a -> SList a -> SInteger Source #
The function how-many
in the paper is already defined in SBV as count
. Let's give it a name:
Correctness
correctness :: SymVal a => IO (Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "c" a -> Forall "xs" [a] -> SBool), Proof (Forall "m1" a -> Forall "m2" a -> Forall "xs" [a] -> SBool)) Source #
The generalized majority theorem. This comment is taken more or less directly from J's proof, cast in SBV terms:
This is the generalized theorem that explains how majority works on any c
and
i
instead of just on the initial c
and i=0
.
The way to imagine majority c i xs
is that we started with
a bigger xs'
that contains i
occurrences of c followed by xs
. That is,
xs' = replicate i c ++ xs
. We know that majority c 0 xs'
finds
the majority in xs'
if there is one.
So the generalized theorem supposes that e
occurs a majority of times in xs'
.
We can say that in terms of c
, i
, and xs
: the number of times e
occurs in xs
plus i
(if e
is c
) is greater than half of the length of xs
plus i
.
The conclusion states that majority c i x
is e
. We have:
>>>
correctness @Integer
Inductive lemma: majorityGeneral Step: Base Q.E.D. Step: 1 (2 way case split) Step: 1.1.1 Q.E.D. Step: 1.1.2 Q.E.D. Step: 1.2.1 Q.E.D. Step: 1.2.2 (2 way case split) Step: 1.2.2.1.1 Q.E.D. Step: 1.2.2.1.2 Q.E.D. Step: 1.2.2.2.1 Q.E.D. Step: 1.2.2.2.2 Q.E.D. Step: 1.2.2.Completeness Q.E.D. Step: 1.Completeness Q.E.D. Result: Q.E.D. Lemma: majority Q.E.D. Lemma: ifExistsFound Q.E.D. Lemma: ifNoMajority Q.E.D. Lemma: uniqueness Step: 1 Q.E.D. Result: Q.E.D. ([Proven] majority :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] ifExistsFound :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] ifNoMajority :: Ɐc ∷ Integer → Ɐxs ∷ [Integer] → Bool,[Proven] uniqueness :: Ɐm1 ∷ Integer → Ɐm2 ∷ Integer → Ɐxs ∷ [Integer] → Bool)