说我有 2 个 CNF 逻辑短语 a,b 并且我的 distrib 函数应该返回 a|b (a OR b) 的 CNF 形式。
替换我的规则是:
1) Replace p|(q&r) by (p|q)&(p|r)
2) Replace (q&r)|p by (q|p)&(r|p)
以这种方式定义的道具:
datatype prop = Atom of string | Not of prop | And of prop*prop | Or of prop*prop;
功能:
local
fun doOr(prop1,prop2) = (Or(prop1,prop2))
fun distrib1 (Or(Atom(sName1),Atom(sName2) ) ) = Or(Atom(sName1), Atom(sName2) )
|distrib1 (Or(Not(Atom(sName1) ),Atom(sName2) ) ) = Or(Not(Atom(sName1) ), Atom(sName2) )
| distrib1 (Or(Atom(sName1),Not(Atom(sName2) ) ) ) = Or(Atom(sName1), Not(Atom(sName2) ) )
| distrib1 (Or(Not(Atom(sName1)),Not(Atom(sName2) ) ) ) = Or(Not(Atom(sName1)), Not(Atom(sName2) ) )
| distrib1 (Or(prop1,And(prop2,prop3) ) ) = And( distrib1(Or(prop1,prop2) ), distrib1(Or(prop1,prop3) ) )
| distrib1 (Or(And(prop1, prop2), prop3) ) ) = And( distrib1(Or(prop1,prop3) ), distrib1(Or(prop2,prop3) ) )
in
fun distrib (prop1,prop2) = distrib1(doOr(prop1,prop2) );
end;
好吧,我不知道函数本身是否正确,虽然我刚刚完成了所有基本选项和替换规则,但是现在当 EQALOP 出现在 distrib1 函数之后并且构造函数错误出现 distrib 函数时,我得到了上述错误.
为什么我会收到这些错误?我不确定,但也许我应该使用 let 而不是本地的,但是我怎样才能将它转换为 let 结构?
谢谢。