kdrag.modal

Treating T -> Bool as a kind of truth value

• https://en.wikipedia.org/wiki/Modal_companion

• https://en.wikipedia.org/wiki/Modal_logic

• https://en.wikipedia.org/wiki/Boolean-valued_model

Functions

Box(p)
MImplies(p, q)	https://en.wikipedia.org/wiki/Modal_companion
PEq(x, y)	Pointwise equality rather than on the nose equality.
PIf(c, t, e)	Pointwise if-then-else rather than on the nose if-then-else.
PImplies(p, q)	Pointwise Implies
PointEq(x, y)	Pointwise equality rather than on the nose equality.
PointIf(c, t, e)	Pointwise if-then-else rather than on the nose if-then-else.
Valid(p)	Convert from modal truth to regular Bool
coerce(s, e)

kdrag.modal.Box(p: FuncRef) → QuantifierRef

Parameters:

p (FuncRef)

Return type:

QuantifierRef

kdrag.modal.MImplies(p, q)

https://en.wikipedia.org/wiki/Modal_companion

kdrag.modal.PEq(x: ExprRef, y) → ExprRef

Pointwise equality rather than on the nose equality.

>>> x = smt.Int("x")
>>> PointEq(smt.Lambda([x], x), 1)
Lambda(x0!..., x0!... == 1)

Parameters:

x (ExprRef)

Return type:

ExprRef

kdrag.modal.PIf(c, t: ExprRef, e: ExprRef) → ExprRef

Pointwise if-then-else rather than on the nose if-then-else.

>>> x = smt.Int("x")
>>> PointIf(smt.Lambda([x], x > 0), 1, -1)
Lambda(x0!..., If(x0!... > 0, 1, -1))
>>> PointIf(smt.Lambda([x], x > 0), smt.Lambda([x], x+1), -1)
Lambda(x0!..., If(x0!... > 0, x0!... + 1, -1))

Parameters:

• t (ExprRef)

• e (ExprRef)

Return type:

ExprRef

kdrag.modal.PImplies(p, q)

Pointwise Implies

kdrag.modal.PointEq(x: ExprRef, y) → ExprRef

Pointwise equality rather than on the nose equality.

>>> x = smt.Int("x")
>>> PointEq(smt.Lambda([x], x), 1)
Lambda(x0!..., x0!... == 1)

Parameters:

x (ExprRef)

Return type:

ExprRef

kdrag.modal.PointIf(c, t: ExprRef, e: ExprRef) → ExprRef

Pointwise if-then-else rather than on the nose if-then-else.

>>> x = smt.Int("x")
>>> PointIf(smt.Lambda([x], x > 0), 1, -1)
Lambda(x0!..., If(x0!... > 0, 1, -1))
>>> PointIf(smt.Lambda([x], x > 0), smt.Lambda([x], x+1), -1)
Lambda(x0!..., If(x0!... > 0, x0!... + 1, -1))

Parameters:

• t (ExprRef)

• e (ExprRef)

Return type:

ExprRef

kdrag.modal.Valid(p: FuncRef) → BoolRef

Convert from modal truth to regular Bool

https://en.wikipedia.org/wiki/Validity_(logic)#Valid_formula

Parameters:

p (FuncRef)

Return type:

BoolRef

kdrag.modal.coerce(s: SortRef, e) → ExprRef

Parameters:

s (SortRef)

Return type:

ExprRef