What4.SpecialFunctions

Utilties for representing and handling certain "special" functions arising from analysis. Although many of these functions are most properly understood as complex valued functions on complex arguments, here we are primarily interested in their restriction to real-valued functions or their floating-point approximations.

The functions considered here include functions from standard and hyperbolic trigonometry, exponential and logarithmic functions, etc. Some of these functions are defineable in terms of others (e.g. tan(x) = sin(x)/cos(x) or expm1(x) = exp(x) - 1@) but are commonly implemented separately in math libraries for increased precision. Some popular constant values are also included.

Representation of special functions

data R

Phantom data index representing the real number line. Used for specifying the arity of special functions.

data SpecialFunction (args :: Ctx Type) where

Data type for representing "special" functions. These include functions from standard and hyperbolic trigonometry, exponential and logarithmic functions, as well as other well-known mathematical functions.

Generally, little solver support exists for such functions (although systems like dReal and Metatarski can prove some properties). Nonetheless, we may have some information about specific values these functions take, the domains on which they are defined, or the range of values their outputs may take, or specific relationships that may exists between these functions (e.g., trig identities). This information may, in some circumstances, be sufficent to prove properties of interest, even if the functions cannot be represented in their entirety.

Constructors

Pi :: SpecialFunction EmptyCtx

HalfPi :: SpecialFunction EmptyCtx

QuarterPi :: SpecialFunction EmptyCtx

OneOverPi :: SpecialFunction EmptyCtx

TwoOverPi :: SpecialFunction EmptyCtx

TwoOverSqrt_Pi :: SpecialFunction EmptyCtx

Sqrt_2 :: SpecialFunction EmptyCtx

Sqrt_OneHalf :: SpecialFunction EmptyCtx

E :: SpecialFunction EmptyCtx

Log2_E :: SpecialFunction EmptyCtx

Log10_E :: SpecialFunction EmptyCtx

Ln_2 :: SpecialFunction EmptyCtx

Ln_10 :: SpecialFunction EmptyCtx

Sin :: SpecialFunction (EmptyCtx ::> R)

Cos :: SpecialFunction (EmptyCtx ::> R)

Tan :: SpecialFunction (EmptyCtx ::> R)

Arcsin :: SpecialFunction (EmptyCtx ::> R)

Arccos :: SpecialFunction (EmptyCtx ::> R)

Arctan :: SpecialFunction (EmptyCtx ::> R)

Sinh :: SpecialFunction (EmptyCtx ::> R)

Cosh :: SpecialFunction (EmptyCtx ::> R)

Tanh :: SpecialFunction (EmptyCtx ::> R)

Arcsinh :: SpecialFunction (EmptyCtx ::> R)

Arccosh :: SpecialFunction (EmptyCtx ::> R)

Arctanh :: SpecialFunction (EmptyCtx ::> R)

Hypot :: SpecialFunction ((EmptyCtx ::> R) ::> R)

Arctan2 :: SpecialFunction ((EmptyCtx ::> R) ::> R)

Pow :: SpecialFunction ((EmptyCtx ::> R) ::> R)

Exp :: SpecialFunction (EmptyCtx ::> R)

Log :: SpecialFunction (EmptyCtx ::> R)

Expm1 :: SpecialFunction (EmptyCtx ::> R)

Log1p :: SpecialFunction (EmptyCtx ::> R)

Exp2 :: SpecialFunction (EmptyCtx ::> R)

Log2 :: SpecialFunction (EmptyCtx ::> R)

Exp10 :: SpecialFunction (EmptyCtx ::> R)

Log10 :: SpecialFunction (EmptyCtx ::> R)

Instances

Eq (SpecialFunction args)

Defined in What4.SpecialFunctions

Methods

(==) :: SpecialFunction args -> SpecialFunction args -> Bool

(/=) :: SpecialFunction args -> SpecialFunction args -> Bool

Show (SpecialFunction args)

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> SpecialFunction args -> ShowS

show :: SpecialFunction args -> String

showList :: [SpecialFunction args] -> ShowS

Hashable (SpecialFunction args)

Defined in What4.SpecialFunctions

Methods

hashWithSalt :: Int -> SpecialFunction args -> Int

hash :: SpecialFunction args -> Int

TestEquality SpecialFunction

Defined in What4.SpecialFunctions

Methods

testEquality :: forall (a :: k) (b :: k). SpecialFunction a -> SpecialFunction b -> Maybe (a :~: b)

OrdF SpecialFunction

Defined in What4.SpecialFunctions

Methods

compareF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool

ltF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool

geqF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool

gtF :: forall (x :: k) (y :: k). SpecialFunction x -> SpecialFunction y -> Bool

HashableF SpecialFunction

Defined in What4.SpecialFunctions

Methods

hashWithSaltF :: forall (tp :: k). Int -> SpecialFunction tp -> Int

hashF :: forall (tp :: k). SpecialFunction tp -> Int

Symmetry properties of special functions

data FunctionSymmetry r

Some special functions exhibit useful symmetries in their arguments. A function f is an odd function if f(-x) = -f(x), and is even if f(-x) = f(x). We extend this notion to arguments of more than one function by saying that a function is even/odd in its ith argument if it is even/odd when the other arguments are fixed.

Constructors

NoSymmetry

EvenFunction

OddFunction

Instances

Show (FunctionSymmetry r)

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> FunctionSymmetry r -> ShowS

show :: FunctionSymmetry r -> String

showList :: [FunctionSymmetry r] -> ShowS

specialFnSymmetry :: SpecialFunction args -> Assignment FunctionSymmetry args

Compute function symmetry information for the given special function.

Packaging arguments to special functions

data SpecialFnArg (e :: k -> Type) (tp :: k) (r :: Type) where

Data type for wrapping the actual arguments to special functions.

Constructors

SpecialFnArg :: e tp -> SpecialFnArg e tp R

Instances

OrdF e => TestEquality (SpecialFnArg e tp :: Type -> Type)

Defined in What4.SpecialFunctions

Methods

testEquality :: forall (a :: k) (b :: k). SpecialFnArg e tp a -> SpecialFnArg e tp b -> Maybe (a :~: b)

OrdF e => OrdF (SpecialFnArg e tp :: Type -> Type)

Defined in What4.SpecialFunctions

Methods

compareF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> OrderingF x y

leqF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool

ltF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool

geqF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool

gtF :: forall (x :: k) (y :: k). SpecialFnArg e tp x -> SpecialFnArg e tp y -> Bool

HashableF e => HashableF (SpecialFnArg e tp :: Type -> Type)

Defined in What4.SpecialFunctions

Methods

hashWithSaltF :: forall (tp0 :: k). Int -> SpecialFnArg e tp tp0 -> Int

hashF :: forall (tp0 :: k). SpecialFnArg e tp tp0 -> Int

traverseSpecialFnArg :: Applicative m => (e tp -> m (f tp)) -> SpecialFnArg e tp r -> m (SpecialFnArg f tp r)

newtype SpecialFnArgs (e :: k -> Type) (tp :: k) args

Data type for wrapping a collction of actual arguments to special functions.

Constructors

SpecialFnArgs (Assignment (SpecialFnArg e tp) args)

Instances

OrdF e => Eq (SpecialFnArgs e tp r)

Defined in What4.SpecialFunctions

Methods

(==) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

(/=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

OrdF e => Ord (SpecialFnArgs e tp r)

Defined in What4.SpecialFunctions

Methods

compare :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Ordering

(<) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

(<=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

(>) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

(>=) :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> Bool

max :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> SpecialFnArgs e tp r

min :: SpecialFnArgs e tp r -> SpecialFnArgs e tp r -> SpecialFnArgs e tp r

(HashableF e, OrdF e) => Hashable (SpecialFnArgs e tp args)

Defined in What4.SpecialFunctions

Methods

hashWithSalt :: Int -> SpecialFnArgs e tp args -> Int

hash :: SpecialFnArgs e tp args -> Int

traverseSpecialFnArgs :: Applicative m => (e tp -> m (f tp)) -> SpecialFnArgs e tp r -> m (SpecialFnArgs f tp r)

Interval data for domain and range

data RealPoint

Values that can appear in the definition of domain and range intervals for special functions.

Constructors

Zero

NegOne

PosOne

NegInf

PosInf

NegPi

PosPi

NegHalfPi

PosHalfPi

Instances

Show RealPoint

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> RealPoint -> ShowS

show :: RealPoint -> String

showList :: [RealPoint] -> ShowS

data RealBound

The endpoint of an interval, which may be inclusive or exclusive.

Constructors

Incl RealPoint

Excl RealPoint

data RealInterval r where

An interval on real values, or a point.

Constructors

RealPoint :: SpecialFunction EmptyCtx -> RealInterval R

RealInterval :: RealBound -> RealBound -> RealInterval R

Instances

Show (RealInterval r)

Defined in What4.SpecialFunctions

Methods

showsPrec :: Int -> RealInterval r -> ShowS

show :: RealInterval r -> String

showList :: [RealInterval r] -> ShowS

specialFnDomain :: SpecialFunction args -> Assignment RealInterval args

Compute the domain of the given special function. As a mathematical entity, the value of the given function is not well-defined outside its domain. In floating-point terms, a special function will return a NaN when evaluated on arguments outside its domain.

specialFnRange :: SpecialFunction args -> RealInterval R

Compute the range of values that may be returned by the given special function as its arguments take on the possible values of its domain. This may include limiting values if the function's domain includes infinities; for example exp(-inf) = 0.