Copyright	(C) 2015-2016 University of Twente 2017 QBayLogic B.V.
License	BSD2 (see the file LICENSE)
Maintainer	Christiaan Baaij <christiaan.baaij@gmail.com>
Safe Haskell	None
Language	Haskell2010

GHC.TypeLits.Normalise.SOP

Contents

SOP types
Simplification

Description

SOP: Sum-of-Products, sorta

The arithmetic operation for Nat are, addition (+), subtraction (-), multiplication (*), and exponentiation (^). This means we cannot write expressions in a canonical SOP normal form. We can get rid of subtraction by working with integers, and translating a - b to a + (-1)*b. Exponentation cannot be getten rid of that way. So we define the following grammar for our canonical SOP-like normal form of arithmetic expressions:

SOP      ::= Product '+' SOP | Product
Product  ::= Symbol '*' Product | Symbol
Symbol   ::= Integer
          |  Var
          |  Var '^' Product
          |  SOP '^' ProductE

ProductE ::= SymbolE '*' ProductE | SymbolE
SymbolE  ::= Var
          |  Var '^' Product
          |  SOP '^' ProductE

So a valid SOP terms are:

x*y + y^2
(x+y)^(k*z)

, but,

(x*y)^2

is not, and should be:

x^2 * y^2

Exponents are thus not allowed to have products, so for example, the expression:

(x + 2)^(y + 2)

in valid SOP form is:

4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2

Also, exponents can only be integer values when the base is a variable. Although not enforced by the grammar, the exponentials are flatted as far as possible in SOP form. So:

(x^y)^z

is flattened to:

x^(y*z)

Synopsis

data Symbol v c
- = I Integer
- | C c
- | E (SOP v c) (Product v c)
- | V v
newtype Product v c = P {
- unP :: [Symbol v c]
}
newtype SOP v c = S {
- unS :: [Product v c]
}
reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c
mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c -> Either (Symbol v c) (Symbol v c)
mergeP :: (Eq v, Eq c) => Product v c -> Product v c -> Either (Product v c) (Product v c)
mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c

SOP types

data Symbol v c Source #

Constructors

I Integer	Integer constant
C c	Non-integer constant
E (SOP v c) (Product v c)	Exponentiation
V v	Variable

Instances

(Eq c, Eq v) => Eq (Symbol v c) Source #
Instance details Methods (==) :: Symbol v c -> Symbol v c -> Bool # (/=) :: Symbol v c -> Symbol v c -> Bool #
(Ord c, Ord v) => Ord (Symbol v c) Source #
Instance details Methods compare :: Symbol v c -> Symbol v c -> Ordering # (<) :: Symbol v c -> Symbol v c -> Bool # (<=) :: Symbol v c -> Symbol v c -> Bool # (>) :: Symbol v c -> Symbol v c -> Bool # (>=) :: Symbol v c -> Symbol v c -> Bool # max :: Symbol v c -> Symbol v c -> Symbol v c # min :: Symbol v c -> Symbol v c -> Symbol v c #
(Outputable v, Outputable c) => Outputable (Symbol v c) Source #
Instance details Methods ppr :: Symbol v c -> SDoc # pprPrec :: Rational -> Symbol v c -> SDoc #

newtype Product v c Source #

Constructors

P
Fields unP :: [Symbol v c]

Instances

(Eq c, Eq v) => Eq (Product v c) Source #
Instance details Methods (==) :: Product v c -> Product v c -> Bool # (/=) :: Product v c -> Product v c -> Bool #
(Ord v, Ord c) => Ord (Product v c) Source #
Instance details Methods compare :: Product v c -> Product v c -> Ordering # (<) :: Product v c -> Product v c -> Bool # (<=) :: Product v c -> Product v c -> Bool # (>) :: Product v c -> Product v c -> Bool # (>=) :: Product v c -> Product v c -> Bool # max :: Product v c -> Product v c -> Product v c # min :: Product v c -> Product v c -> Product v c #
(Outputable v, Outputable c) => Outputable (Product v c) Source #
Instance details Methods ppr :: Product v c -> SDoc # pprPrec :: Rational -> Product v c -> SDoc #

newtype SOP v c Source #

Constructors

S
Fields unS :: [Product v c]

Instances

(Eq v, Eq c) => Eq (SOP v c) Source #
Instance details Methods (==) :: SOP v c -> SOP v c -> Bool # (/=) :: SOP v c -> SOP v c -> Bool #
(Ord v, Ord c) => Ord (SOP v c) Source #
Instance details Methods compare :: SOP v c -> SOP v c -> Ordering # (<) :: SOP v c -> SOP v c -> Bool # (<=) :: SOP v c -> SOP v c -> Bool # (>) :: SOP v c -> SOP v c -> Bool # (>=) :: SOP v c -> SOP v c -> Bool # max :: SOP v c -> SOP v c -> SOP v c # min :: SOP v c -> SOP v c -> SOP v c #
(Outputable v, Outputable c) => Outputable (SOP v c) Source #
Instance details Methods ppr :: SOP v c -> SDoc # pprPrec :: Rational -> SOP v c -> SDoc #

Simplification

reduceExp :: (Ord v, Ord c) => Symbol v c -> Symbol v c Source #

reduce exponentials

Performs the following rewrites:

x^0          ==>  1
0^x          ==>  0
2^3          ==>  8
(k ^ i) ^ j  ==>  k ^ (i * j)

mergeS :: (Ord v, Ord c) => Symbol v c -> Symbol v c -> Either (Symbol v c) (Symbol v c) Source #

Merge two symbols of a Product term

Performs the following rewrites:

8 * 7    ==>  56
1 * x    ==>  x
x * 1    ==>  x
0 * x    ==>  0
x * 0    ==>  0
x * x^4  ==>  x^5
x^4 * x  ==>  x^5
y*y      ==>  y^2

mergeP :: (Eq v, Eq c) => Product v c -> Product v c -> Either (Product v c) (Product v c) Source #

Merge two products of a SOP term

Performs the following rewrites:

2xy + 3xy  ==>  5xy
2xy + xy   ==>  3xy
xy + 2xy   ==>  3xy
xy + xy    ==>  2xy

mergeSOPAdd :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c Source #

Merge two SOP terms by additions

mergeSOPMul :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c Source #

Merge two SOP terms by multiplication

normaliseExp :: (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c Source #

Expand or Simplify complex exponentials

Performs the following rewrites:

b^1              ==>  b
2^(y^2)          ==>  4^y
(x + 2)^2        ==>  x^2 + 4xy + 4
(x + 2)^(2x)     ==>  (x^2 + 4xy + 4)^x
(x + 2)^(y + 2)  ==>  4x(2 + x)^y + 4(2 + x)^y + (2 + x)^yx^2