折叠设置，使新的设置

说我对命题类型Prop：折叠设置，使新的设置

type Prop = 
    | P of string 
    | Disjunction of Prop * Prop 
    | Conjunction of Prop * Prop 
    | Negation of Prop

其中：

• A "p" representing the atom P, 
• Disjunction(A "P", A "q") representing the proposition P ∨ q. 
• Conjunction(A "P", A "q") representing the proposition P ∧ q. 
• Negation(A "P") representing the proposition ¬P.

我应该使用公式的基于集合的表示中析取正常形式。由于结合是可交换的，缔合和（a∧a）是相当于一个方便的是表示由它的一组文字litOf（BC）碱性的混合BC。

BC被定义为：A literal是原子或原子的否定和碱性的混合是文字

这使我的功能litOf的结合：

let litOf bc = 
    Set.fold (fun acc (Con(x, y)) -> Set.add (x, y) acc) Set.empty bc

我我很确定我的litOf是错误的，并且我在(Con(x,y))部分得到一个错误：“在这个表达式上的不完整模式，例如，'Dis（_，_）'的值可能表示cas不为0，不是被模式覆盖。“，这我也不知道是什么实际上是指在这种情况下。

任何提示我怎么能PROCEDE？

来源

2016-11-22 Khaine775

不知道我理解这里的一切，但有趣的ACC（CON（X，Y ））可能是我阅读它的一个匹配表达式，因此您错过了“匹配”（来自工会）的其余部分。当然，这将帮助很大OM代码在这里，在“跑”的状态：[MCVE] http://stackoverflow.com/help/mcve –

工作的一个例子和测试代码在F＃创建DNF可发现[这里]（https://github.com/jack-pappas/fsharp-logic-examples/blob/master/FSharpx.Books.AutomatedReasoning/prop.fs#L407）。这比你提出的要详细得多，需要几天的时间来理解它，因为它还包括解析和漂亮打印。你也应该让这本书真正理解它。因此它是一个评论。有[实施例]（https://github.com/jack-pappas/fsharp-logic-examples/blob/master/Examples/prop.fsx），用于与一个REPL –

我假设你的榜样型Prop的方式改变从键盘到这里，并orginally是这样的：

type Prop = 
    | P of string 
    | Dis of Prop * Prop 
    | Con of Prop * Prop 
    | Neg of Prop

有几件事情绊倒您：

集。折叠对作为集合的输入进行操作，并对集合中的每个元素执行一些操作。在你的情况下，输入是一个布尔子句，输出是一个集合。
你没有完全界定什么是文字。对于一个连接，文字集是左侧和右侧文字的联合。但是如何分离？编译器错误消息意味着这一点。

这就是我认为你是后：

let rec literals = function 
    | P s -> Set.singleton s 
    | Dis (x, y) -> Set.union (literals x) (literals y) 
    | Con (x, y) -> Set.union (literals x) (literals y) 
    | Neg x -> literals x

就这样，你会得到

> literals (Dis (P "A", Neg (Con (P "B", Con (P "A", P "C"))))) 
val it : Set<string> = set ["A"; "B"; "C"]

来源

2016-11-22 22:11:56

使用在[DNF]（HTTP：// mathworld .wolfram.com/DisjunctiveNormalForm。HTML），除了[变量]（https://en.wikipedia.org/wiki/Disjunctive_normal_form）之外，你不能否定任何其他内容 – kaefer

@kaefer：这是真的，但超出了问题的范围。 –

折叠设置，使新的设置

回答

相关问题