Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.BitPrecise.PrefixSum

Contents

Formalizing power-lists
Reference prefix-sum implementation
The Ladner-Fischer parallel version
Sample proofs for concrete operators

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

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.

tiePL :: PowerList a -> PowerList a -> PowerList a Source #

The tie operator, concatenation.

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.

unzipPL :: PowerList a -> (PowerList a, PowerList a) Source #

Inverse of zipping.

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.

thm1 :: IO ThmResult Source #

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:

>>> thm1
Q.E.D.

thm2 :: IO ThmResult Source #

Proves Ladner-Fischer is equivalent to reference specification for the function max. 0 is the left-unit element, and we use a power-list of size 16. We have:

>>> thm2
Q.E.D.