DA.Logic

Daml 模块 DA.Logic 参考文档。

DA.Logic

Logic — 命题演算。

模块概览

稳定（Stable）。状态：`active` 引入版本：`3.4.9` 移除版本：`-` 警告：`0` 弃用：`0` 弃用自：`-`

数据类型

`data Formula t`

Formula t 表示命题类型为 t 的命题演算公式。

构造子：

Proposition t Proposition p 即命题 p

Negation (Formula t) 对公式 f，Negation f 表示 ¬f

Conjunction [Formula t] 对公式 f1, …, fn，Conjunction [f1, ..., fn] 表示 f1 ∧ … ∧ fn

Disjunction [Formula t] 对公式 f1, …, fn，Disjunction [f1, ..., fn] 表示 f1 ∨ … ∨ fn

实例：

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)

函数

`&&&`

&&& : Formula t -> Formula t -> Formula t

&&& 为公式布尔代数中的 ∧ 运算，读作「与」。

`|||`

||| : Formula t -> Formula t -> Formula t

||| 为公式布尔代数中的 ∨ 运算，读作「或」。

`true`

true : Formula t

true 为公式布尔代数的单位元 1，表示为空合取。

`false`

false : Formula t

false 为公式布尔代数的零元 0，表示为空析取。

`neg`

neg : Formula t -> Formula t

neg 为公式布尔代数中的 ¬（否定）运算。

`conj`

conj : [Formula t] -> Formula t

conj 是 &&& 的列表版本，利用 ∧ 的结合律。

`disj`

disj : [Formula t] -> Formula t

disj 是 ||| 的列表版本，利用 ∨ 的结合律。

`fromBool`

fromBool : Bool -> Formula t

fromBool 将 True 转为 true，False 转为 false。

`toNNF`

toNNF : Formula t -> Formula t

toNNF 将公式化为否定范式（参见否定范式）。

`toDNF`

toDNF : Formula t -> Formula t

toDNF 将公式化为析取范式（参见析取范式）。

`traverse`

traverse : Applicative f => (t -> f s) -> Formula t -> f (Formula s)

通常意义上的 traverse 实现。

`zipFormulas`

zipFormulas : Formula t -> Formula s -> Formula (t, s)

zipFormulas 对两个结构相同（仅命题不同）的公式进行 zip。

`substitute`

substitute : (t -> Optional Bool) -> Formula t -> Formula t

substitute 根据真值赋值将 True 或 False 代入公式相应位置。

`reduce`

reduce : Formula t -> Formula t

reduce 尽可能化简公式：

移除所有 true 与 false 出现；
移除直接嵌套的 Conjunction 与 Disjunction；
化为否定范式。

`isBool`

isBool : Formula t -> Optional Bool

isBool 尝试将公式转为 Bool。满足 isBool true == Some True 且 isBool false == Some False，否则返回 None。

`interpret`

interpret : (t -> Optional Bool) -> Formula t -> Either (Formula t) Bool

interpret 是 toBool 的变体：先用真值函数代入，再尽可能化简。

`substituteA`

substituteA : Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Formula t)

substituteA 是 substitute 的变体，允许通过 action 获取真值。

`interpretA`

interpretA : Applicative f => (t -> f (Optional Bool)) -> Formula t -> f (Either (Formula t) Bool)

interpretA 是 interpret 的变体，允许通过 action 获取真值。

孤儿类型类实例

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

本文由 CC Privacy Club 根据 Canton Network 官方文档（CC-BY-4.0）整理翻译，仅供学习；实现细节以官方最新版本为准。