| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | [email protected] |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Documentation.SBV.Examples.BitPrecise.PrefixSum
Description
The PrefixSum algorithm over power-lists and proof of the Ladner-Fischer implementation. See http://dl.acm.org/citation.cfm?id=197356 and http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.
Synopsis
- type PowerList a = [a]
- tiePL :: PowerList a -> PowerList a -> PowerList a
- zipPL :: PowerList a -> PowerList a -> PowerList a
- unzipPL :: PowerList a -> (PowerList a, PowerList a)
- ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
- lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
- flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
- thm1 :: IO ThmResult
- thm2 :: IO ThmResult
Documentation
>>>-- For doctest purposes only:>>>import Data.SBV
Formalizing power-lists
type PowerList a = [a] Source #
A poor man's representation of powerlists and basic operations on them: http://dl.acm.org/citation.cfm?id=197356 We merely represent power-lists by ordinary lists.
zipPL :: PowerList a -> PowerList a -> PowerList a Source #
The zip operator, zips the power-lists of the same size, returns a powerlist of double the size.
Reference prefix-sum implementation
ps :: (a, a -> a -> a) -> PowerList a -> PowerList a Source #
Reference prefix sum (ps) is simply Haskell's scanl1 function.
The Ladner-Fischer parallel version
lf :: (a, a -> a -> a) -> PowerList a -> PowerList a Source #
The Ladner-Fischer (lf) implementation of prefix-sum. See http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf
or pg. 16 of http://dl.acm.org/citation.cfm?id=197356
Sample proofs for concrete operators
flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool Source #
Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element.
Proves Ladner-Fischer is equivalent to reference specification for addition.
0 is the left-unit element, and we use a power-list of size 8. We have:
>>>thm1Q.E.D.