Portability | portable |
---|---|
Stability | experimental |
Maintainer | erkokl@gmail.com |
The PrefixSum algorithm over power-lists and proof of the Ladner-Fischer implementation. See http://www.cs.utexas.edu/users/psp/powerlist.pdf and http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.
- 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, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
- thm1 :: IO ThmResult
- thm2 :: IO ThmResult
Documentation
A poor man's representation of powerlists and basic operations on them: http://www.cs.utexas.edu/users/psp/powerlist.pdf. We merely represent power-lists by ordinary lists.
zipPL :: PowerList a -> PowerList a -> PowerList aSource
The zip operator, zips the power-lists of the same size, returns a powerlist of double the size.
ps :: (a, a -> a -> a) -> PowerList a -> PowerList aSource
Reference prefix sum (ps
) is simply Haskell's scanl1
function
lf :: (a, a -> a -> a) -> PowerList a -> PowerList aSource
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://www.cs.utexas.edu/users/psp/powerlist.pdf.
flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBoolSource
Correctness theorem, for a powerlist of given size, an associative operator, and its unit element
Proves Ladner-Fischer is equivalent to reference specification for addition.
0
is the unit element, and we use a power-list of size 8
.