2

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;

基本オプションと置換ルールをすべて調べただけなのに、関数自体が正しいかどうかはわかりませんが、今のところ、distrib1関数の後にEQALOPが表示され、コンストラクターエラーがdistrib関数に表示されると、上記のエラーが発生します。 。

なぜこれらのエラーが発生するのですか？よくわかりませんが、ローカルではなくletを使用することになっているかもしれませんが、どうすればlet構造に変換できますか？

ありがとう。

4

1 に答える 1

2

最後のケースでdistrib1は、合計3つの開き括弧がありますが、4つの閉じ括弧があります。

| distrib1 (Or(And(prop1, prop2), prop3) ) ) =

これが、RPARENに関する構文エラーが発生する理由です。

distrib構文エラーのために定義されていないため、エラーが発生しdistrib1ます。したがって、これは不明な変数です。の構文エラーdistrib1を修正すると、これも修正されます。

于 2010-12-24T10:45:46.287 に答える