Skip to main content

Documentation Index

Fetch the complete documentation index at: https://docs.canton.network/llms.txt

Use this file to discover all available pages before exploring further.

​
DA.Logic

Logic - Propositional calculus.

​
Module Snapshot

Lifecycle

Stable.

Notices

Status: active Introduced in: 3.4.9 Removed in: - Warnings: 0 Deprecations: 0 Deprecated since: -

​
Data Types

​
data Formula t

A Formula t is a formula in propositional calculus with propositions of type t. Constructors:
  • Proposition t Proposition p is the formula p
  • Negation (Formula t) For a formula f, Negation f is ¬f
  • Conjunction [Formula t] For formulas f1, …, fn, Conjunction [f1, ..., fn] is f1 ∧ … ∧ fn
  • Disjunction [Formula t] For formulas f1, …, fn, Disjunction [f1, ..., fn] is f1 ∨ … ∨ fn
Instances:
  • instance Action Formula
  • instance Applicative Formula
  • instance Functor Formula
  • instance Eq t => Eq (Formula t)
  • instance Ord t => Ord (Formula t)
  • instance Show t => Show (Formula t)

​
Functions

​
&&&

&&& : Formula t -> Formula t -> Formula t
&&& is the ∧ operation of the boolean algebra of formulas, to be read as “and”

​
|||

||| : Formula t -> Formula t -> Formula t
||| is the ∨ operation of the boolean algebra of formulas, to be read as “or”

​
true

true : Formula t
true is the 1 element of the boolean algebra of formulas, represented as an empty conjunction.

​
false

false : Formula t
false is the 0 element of the boolean algebra of formulas, represented as an empty disjunction.

​
neg

neg : Formula t -> Formula t
neg is the ¬ (negation) operation of the boolean algebra of formulas.

​
conj

conj : [Formula t] -> Formula t
conj is a list version of &&&, enabled by the associativity of ∧.

​
disj

disj : [Formula t] -> Formula t
disj is a list version of |||, enabled by the associativity of ∨.

​
fromBool

fromBool : Bool -> Formula t
fromBool converts True to true and False to false.

​
toNNF

toNNF : Formula t -> Formula t
toNNF transforms a formula to negation normal form (see https://en.wikipedia.org/wiki/Negation_normal_form).

​
toDNF

toDNF : Formula t -> Formula t
toDNF turns a formula into disjunctive normal form. (see https://en.wikipedia.org/wiki/Disjunctive_normal_form).

​
traverse

traverse : Applicative f => (t -> f s) -> Formula t -> f (Formula s)
An implementation of traverse in the usual sense.

​
zipFormulas

zipFormulas : Formula t -> Formula s -> Formula (t, s)
zipFormulas takes to formulas of same shape, meaning only propositions are different and zips them up.

​
substitute

substitute : (t -> Optional Bool) -> Formula t -> Formula t
substitute takes a truth assignment and substitutes True or False into the respective places in a formula.

​
reduce

reduce : Formula t -> Formula t
reduce reduces a formula as far as possible by:
  1. Removing any occurrences of true and false;
  2. Removing directly nested Conjunctions and Disjunctions;
  3. Going to negation normal form.

​
isBool

isBool : Formula t -> Optional Bool
isBool attempts to convert a formula to a bool. It satisfies isBool true == Some True and isBool false == Some False. Otherwise, it returns None.

​
interpret

interpret : (t -> Optional Bool) -> Formula t -> Either (Formula t) Bool
interpret is a version of toBool that first substitutes using a truth function and then reduces as far as possible.

​
substituteA

substituteA : Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Formula t)
substituteA is a version of substitute that allows for truth values to be obtained from an action.

​
interpretA

interpretA : Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Either (Formula t) Bool)
interpretA is a version of interpret that allows for truth values to be obtained form an action.

​
Orphan Typeclass Instances

  • instance Eq t => Eq (Formula t)
  • instance Ord t => Ord (Formula t)
  • instance Show t => Show (Formula t)
  • instance Functor Formula
  • instance Applicative Formula
  • instance Action Formula