代数的値集合の狭まり

論理プログラミングと同様に、代数的値集合の絞り込み^{[1] [2]は、未解決または部分的に解決された方程式の値を推論する方法を提供します。論理プログラミングが} 解決に依存するのに対し、値集合の代数は絞り込み規則に依存します。絞り込み規則により、解くべき方程式と矛盾する値を解集合から除去できます。

論理プログラミングとは異なり、代数値セットの絞り込みではバックトラックは使用されません。代わりに、すべての値が値セットに含まれ、並列に考慮されます。

このアプローチは制約論理プログラミングにおける制約^[3]の使用にも似ていますが、論理処理の基礎がありません。

確率的値セットは、演繹的確率への値セットの自然な拡張です。値セット構造は、初期値の確率に基づいて計算値の確率を計算するために必要な情報を保持します。

初期のプログラミング言語は命令型でした。これらは変更を表現できるようにすることで機能を実装します。代入ステートメントにより、変数の値を変更できます。

数学では、変数の値は変化しないことがあります。これは数学的アプローチの基本です。ラムダ計算に基づく関数型言語では、プログラミングにこの数学的アプローチを使用できます。関数型言語は、遅延評価を実装し、関数をパラメータとして渡すことができるようにすることで開発されました。

遅延評価は、 Haskellなどの現代の関数型プログラミング言語の重要な機能です。Haskell は、ラムダ計算とlet 式に基づく一連の言語の最新版です。これらの言語は、遅延評価と型推論を使用した多態的な型システムを通じて豊富な機能を提供します。関数型プログラミング言語は当然、高階関数もサポートします。

関数型プログラミングと並行して開発されたResolutionに基づく論理プログラミング。論理プログラミングは、値について推論を行う リレーショナル プログラミングの一種です。制約論理プログラミングは、制約をサポートすることで論理プログラミングを拡張します。ECLiPSe などの制約論理プログラミング言語は、複雑な論理問題を解決する機能を提供します。ただし、ECLiPSe は遅延しません。

論理プログラミング言語は、より優れた演繹能力を備えているにもかかわらず、関数型言語ほどのパワーと柔軟性を獲得することはできませんでした。

ナローイングは、関数型言語の柔軟性を備えた論理的推論を可能にする手法です。

数学では、式は単一の値を表します。関数は、 1 つ以上の値を 1 つの一意の値にマッピングします。

関数の逆関数は、必ずしも関数として適切に定義されるわけではありません。関数の逆関数を関数の定義に適合させるために、追加の条件が必要になる場合があります。

特に、一部のブール演算には、関数として定義できる逆関数がありません。特に、論理和「または」には、2 つの値を許可する逆関数があります。自然言語では、「または」は代替の可能性を表します。

絞り込みは、複数の値をパッケージ化して単一の値として扱うことができる値セットに基づいています。これにより、関数の逆関数は常に関数として扱うことができます。

これを実現するには、値セットが値が属するコンテキストを記録する必要があります。変数は、各可能な世界で 1 つの値のみを取ることができます。値セットは、値セット内の各値に、それが属する世界をタグ付けします。

可能世界は世界集合に属します。世界集合は、相互に排他的なすべての世界の集合です。異なる可能世界からの値を組み合わせることは不可能です。それは、相互に排他的な可能世界を組み合わせることを意味するからです。

関数を値セットに適用すると、異なる世界からの値セットの組み合わせが作成されます。絞り込みでは、同じ世界セットからの異なる世界の組み合わせを排除することで、それらの世界が削減されます。絞り込みルールでは、世界の組み合わせが不可能であることが示される状況も検出されます。

絞り込みの使用では、バックトラッキングは必要ありません。可能な値を値セットにパッケージ化することで、すべての値の組み合わせを同時に考慮できます。評価は関数型言語と同様に、値セット内の値の組み合わせを組み合わせ、絞り込みルールによってセットから不可能な値を排除しながら行われます。

値セットは、変数が持つ可能性のある値のセットを表すオブジェクトです。値セットは数学的には単一の値として動作しますが、内部的には複数の値を表します。これを実現するために、値セットは、値が発生したコンテキストまたは世界とともに値を追跡します。

数学では、式は単一の値を表さなければなりません。例えば、次の方程式を考えてみましょう。

${\displaystyle x^{2}=4}$

つまり、

${\displaystyle x=2\or x=-2}$

しかし、これは少し長すぎるし、複数の値を同時に扱うことはできません。x にさらに条件や制約が追加された場合、それぞれの値が制約に合致するかどうかを検討する必要があります。したがって、単純に次のように記述します。

${\displaystyle x=\pm 2}$

素朴に言えば、

${\displaystyle x+x\in \lbrace 4,0,-4\rbrace }$

しかし、これは間違いです。各 x は、式の中で 1 つの値を表す必要があります。つまり、x は 2 か、x = −2 のいずれかです。この問題を解決するには、2 つの値を追跡して、値が一貫して使用されるようにします。これが値セットの機能です。

'x'に設定される値は次のように記述されます。

${\displaystyle V(\{2::x_{1},-2::x_{2}\})}$

これは、タグ、値のペアのセットを持つ コンテナVです。

• ${\displaystyle 2::x_{1}}$
• ${\displaystyle -2::x_{2}}$

値 2 は可能世界 に関連付けられています。値 -2 は可能世界に関連付けられています。つまり、値が同時に 2 と -2 になることはできません。世界では、値セットの値は 2 でなければなりません。世界では、値セットの値は -2 でなければなりません。 ${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$

方程式の解は、

${\displaystyle x^{2}=4}$

は、

${\displaystyle x=V(\{2::x_{1},-2::x_{2}\})}$

ここで、可能世界は非公式な用語として使用されています。正式には、可能世界はブール条件によって定義されます。可能世界は、条件に一致する世界の可能性の集合と考えることができます。

「可能世界」という用語は、値セットの説明をわかりやすくするために使用されます。

世界集合は、すべての可能性を表す可能世界の集合です。したがって、世界集合は x = 2 (世界) または x= −2 (世界) のいずれかになります。他の可能性はありません。 ${\displaystyle \{x_{1},x_{2}\}}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$

同じ世界集合の世界は相互に排他的であるため、両方の世界の命題が同時に真であるということはあり得ません。 ${\displaystyle x_{1}}$${\displaystyle x_{2}}$

${\displaystyle (x=2\land x=-2)={\text{false}}}$

関数を値セットに適用するための規則は、

${\displaystyle V(M)\ V(N)=V(\{(m_{v}\ n_{v},m_{l}\cap n_{l}):m_{v}::m_{l}\in M\land n_{v}::n_{l}\in N\})}$

例えば、

${\displaystyle x+x=V(\{2::x_{1},-2::x_{2}\})+V(\{2::x_{1},-2::x_{2}\})}$

は、

${\displaystyle =V(\{-2+-2::x_{1}\cap x_{1},-2+2::x_{1}\cap x_{2},2+-2::x_{1}\cap x_{2},2+2::x_{2}\})}$

${\displaystyle =V(\{-4::x_{1}\cap x_{1},0::x_{1}\cap x_{2},0::x_{2}\land x_{1},2+2::x_{2}\cap x_{1}\})}$

可能世界とそれ自身の交差が可能世界である。

${\displaystyle x_{1}\cap x_{1}=x_{1}}$

${\displaystyle x_{2}\cap x_{2}=x_{2}}$

可能世界と、同じ世界集合に属する別の可能世界との交差は空である。

${\displaystyle x_{1}\cap x_{2}=\{\}}$

${\displaystyle x_{2}\cap x_{1}=\{\}}$

それで、

${\displaystyle =V(\{-4::x_{1},0::\{\},0::\{\},4::x_{2}\})}$

空の世界のルールでは、空の世界のタグ付き値をドロップできます。

${\displaystyle V(K)=V(\{(v,l):(v,l)\in K\land l\neq \{\}\}}$

与える、

${\displaystyle =V(\{-4::x_{1},4::x_{2}\})}$

予想どおり、結果は-4 または 4 になります。 ${\displaystyle x+x}$

${\displaystyle a\land b}$

aとb が両方とも true でなければならないことを意味する、a、b 、およびtrueの関係です。

${\displaystyle a\lor b}$

aとbに は複数の値を指定できます。aが

${\displaystyle a=V(\{\operatorname {false} ::a_{1},\operatorname {true} ::a_{2}\})}$

次にbについて

${\displaystyle b=V(\{\operatorname {true} ::a_{1},\operatorname {false} ::a_{2},\operatorname {true} ::a_{2}\})}$

これは、aが偽の場合、b が真でなければならないことを意味します。

さて、考えてみましょう。

${\displaystyle x=2\lor x=-2}$

与える、

${\displaystyle x=V(\{\_::a_{1},2::a_{2}\})}$

そして

${\displaystyle x=V(\{-2::a_{1},\_::a_{2},-2::a_{2}\})}$

これら2つの価値セットを統合すると、

${\displaystyle x=V(\{-2::a_{1},2::a_{2}\})}$

「等しいと主張」ルールにより ペアは削除される。${\displaystyle -2::a_{2}}$

${\displaystyle \forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to m_{l}\cap n_{l}=\{\})}$

その値はと一致しませんでした。 ${\displaystyle -2::a_{2}}$${\displaystyle 2::a_{2}}$

問題を考えてみましょう。

${\displaystyle X=V(\{1::x_{1},3::x_{2},4::x_{3}\})}$

${\displaystyle Y=V(\{8::y_{1},9::y_{2}\})}$

${\displaystyle X*Y<25}$

${\displaystyle X+Y>10}$

まず、 の値セットを計算します。 ${\displaystyle X*Y<25}$

${\displaystyle V(\{8::x_{1}\cap y_{1},24::x_{2}\cap y_{1},32::x_{3}\cap y_{1},9::x_{1}\cap y_{2},27::x_{2}\cap y_{2},36::x_{3}\cap y_{2}\})<25}$

${\displaystyle V(\{8<25::x_{1}\cap y_{1},24<25::x_{2}\cap y_{1},32<25::x_{3}\cap y_{1},9<25::x_{1}\cap y_{2},27<25::x_{2}\cap y_{2},36<25::x_{3}\cap y_{2}\})<25}$

${\displaystyle V(\{{\text{true}}::x_{1}\cap y_{1},{\text{true}}::x_{2}\cap y_{1},{\text{false}}::x_{3}\cap y_{1},{\text{true}}::x_{1}\cap y_{2},{\text{false}}::x_{2}\cap y_{2},{\text{false}}::x_{3}\cap y_{2}\})}$

この文が真であると断言されると、偽の値はすべて削除され、

${\displaystyle V(\{{\text{true}}::x_{1}\cap y_{1},{\text{true}}::x_{2}\cap y_{2},{\text{true}}::x_{1}\cap y_{2}\})}$

世界は、

${\displaystyle x_{3}\cap y_{1}}$

${\displaystyle x_{2}\cap y_{2}}$

${\displaystyle x_{3}\cap y_{2}}$

不可能だ。世界は空っぽだ。

ワールドセットが計算に含まれる場合、ワールドセットのすべてのワールドが結果に含まれなければなりません。ワールドが見つからない場合、それは従属ワールドと呼ばれ、空でなければなりません。ワールドはこの値に表されていないため、空でなければなりません。に設定された値は小さくなり、 ${\displaystyle X_{3}}$${\displaystyle X}$

${\displaystyle X=V(\{1::x_{1},3::x_{2}\})}$

値セットが小さくなったため、2 番目の条件はよりシンプルになりました。

${\displaystyle X+Y>10}$

すると、値セットは次のようになります。

${\displaystyle X=V(\{1::x_{1},3::x_{2}\})}$

${\displaystyle Y=V(\{8::y_{1},9::y_{2}\})}$

そして計算は、

${\displaystyle V(\{1+8::x_{1}\cap y_{1},3+8::x_{2}\cap y_{1},2+9::x_{1}\cap y_{2},1+9::x_{2}\cap y_{2}\})>10}$

しかし、空です。だから、 ${\displaystyle x_{2}\cap y_{2}}$

${\displaystyle V(\{9>10::x_{1}\cap y_{1},11>10::x_{2}\cap y_{1},10>10::x_{1}\cap y_{2}\})}$

と は空なので、 ${\displaystyle x_{1}\cap y_{1}}$${\displaystyle x_{1}\cap y_{2}}$

${\displaystyle V(\{11>10::x_{2}\cap y_{1}\})}$

今では、とが表現されておらず、従属世界として削除されています。つまり、 ${\displaystyle X_{1}}$${\displaystyle Y_{2}}$

${\displaystyle X=V(\{3::x_{2}\})=3}$

${\displaystyle Y=V(\{8::y_{1}\})=8}$

実行されるすべての計算では、従属ワールドを削除することで値セットのサイズが縮小される可能性がありますが、入力値セットのサイズの積であるサイズを持つ新しい値セットが追加されます。次に、入力値セットのサイズの積が最小になるところから計算を進めます。

地獄のようなプロジェクトでクレイジーな締め切りに間に合わせようと懸命に働いた一日の後、午後10時にピザ、ビール、ウイスキーが欲しくなる絶望的な時間がやってきます。ピザショップの営業時間は、

${\displaystyle {\text{PizzaShop}}(V(\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\}))}$

ビールは、

${\displaystyle {\text{BottleshopWithBeer}}(V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\}))}$

ウィスキー、

${\displaystyle {\text{BottleshopWithWhiskey}}(V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\}))}$

警官が近くにいるし、私たちは年を取っている。どこに行けばいいの？

${\displaystyle {\text{WhereToGo}}(x)={\text{PizzaShop}}(x)\land {\text{BottleshopWithBeer}}(x)\land {\text{BottleshopWithWhiskey}}(x)}$

制約が左から右の順序で適用される場合、

${\displaystyle x=V(\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\})}$

次にこれを統合する必要があります。

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})}$

これにより、24 個の組み合わせが作成され、その中から一致するものは次のとおりです。

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap p_{3},{\text{St Kilda}}::b_{2}\cap p_{5},{\text{Carlton}}::b_{3}\cap p_{1}\})}$

最終的にはウイスキーと統一する必要があります。

${\displaystyle x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})}$

6通りの組み合わせがあります。一致するのは、

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap p_{3}\cap w_{2}\})}$

合計30の組み合わせが生成されました。

制約が右から左の順序で適用される場合、

${\displaystyle x=V(\{{\text{Essendon}}::w_{1},{\text{South Melbourne}}::w_{2}\})}$

次にこれを統合する必要があります。

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1},{\text{St Kilda}}::b_{2},{\text{Carlton}}::b_{3},{\text{Docklands}}::b_{4}\})}$

これにより、8つの組み合わせが作成され、その中から一致するものは次のとおりです。

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\})}$

最後にピザと統一する必要があります。

${\displaystyle x=\{{\text{Carlton}}::p_{1},{\text{Richmond}}::p_{2},{\text{South Melbourne}}::p_{3},{\text{Footscray}}::p_{4},{\text{St Kilda}}::p_{5},{\text{Toorak}}::p_{6}\}}$

6通りの組み合わせがあります。一致するのは、

${\displaystyle x=V(\{{\text{South Melbourne}}::b_{1}\cap w_{2}\ \cap p_{3}\})}$

結果は同じですが、結論に到達するまでに生成された組み合わせは 14 個だけです。

すべての計算では、値セットを組み合わせて、入力値セットのサイズの積である値セットを作成します。その後、値セットは削減されます。また、すべての計算には、計算を絞り込むチャンスが均等にあります。したがって、順序を制御し、サイズの積が最小の計算を進めることで、計算が減り、組み合わせ爆発も減ります。

関数ではない関数の逆関数の問題に対する一般的な解決法が必要です。必要なのは、値の集合のメンバーになるように制約された値の表現です。let式は、集合のメンバーである値を表すために使用できます。

${\displaystyle \operatorname {let} x\in X\operatorname {in} x}$

この式には制約があります。制約とは、変数が満たさなければならないブール式です。let式を使用すると、制約を式で表すことができます。制約式の関数適用に一般的なルールがあれば、制約を値のように扱うことができます。 ${\displaystyle x\in X}$

関数適用では、あるlet式を別のlet式に適用すると、

${\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} y\in Y\operatorname {in} y)}$

${\displaystyle =\operatorname {let} x\in X\land y\in Y\operatorname {in} x\ y}$

${\displaystyle =\operatorname {let} (x,y)\in X\times Y\operatorname {in} x\ y}$

ただし、let 式をそれ自体に適用する場合は別のルールが適用されます。let 式は変数 x のスコープを制限しないため、2 つの let 式では x は同じ変数になります。

${\displaystyle (\operatorname {let} x\in X\operatorname {in} x)\ (\operatorname {let} x\in X\operatorname {in} x)}$

${\displaystyle =\operatorname {let} x\in X\operatorname {in} x\ x}$

let 式を組み合わせるための簡単なルールはないようです。必要なのは、値が値セットのメンバーである変数を表す一般的な形式の式です。式は、変数とセットに基づく必要があります。

この形式に関数を適用すると、同じ形式の別の式が生成されます。このように、複数の値を持つ関数の式は、1 つの値を持つものとして扱われます。

フォームが値のセットを表すだけでは不十分です。各値には、式が値を取るタイミングを決定する条件が必要です。結果として得られる構造は、条件と値のペアのセットであり、「値セット」と呼ばれます。

「値セット」Kは、各ペアが値と従属条件のセットで構成されるペアのセットとして定義されます。従属条件のセットは、「条件関数」によって使用され、値セットがその値を取るかどうかが決定されます。

条件関数は3つの公理によって定義される。

1. 各ペアは、リストに適用された条件関数が true の場合、値セットの値がvであることを意味します。${\displaystyle (v,l)}$${\displaystyle V(K)}$${\displaystyle C(l)}$
2. 条件の 1 つが当てはまります。
3. 条件のうち 1 つだけが当てはまります。

条件は、条件の構造を制御できるように、従属条件のセットに適用される関数として表されます。また、条件のセットは、従属値を除外して絞り込む場合にも使用されます。ただし、ほとんどの場合、値セットは値と条件のペアのセットと考えることができます。条件関数は、セットを条件に変換します。

正式には、

値条件と完全集合公理を用いて、

${\displaystyle \exists v\exists l(v,l)\in K\land C(l)\land v=V(K)}$

let式では次のようになります。

${\displaystyle V(K)=\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v}$

単一の値を表す値セットは、

${\displaystyle k=V(\{(k,\{\})\})}$

導出は、

${\displaystyle V(\{(k,\{\})\})}$

${\displaystyle =\operatorname {let} (v,l)\in \{(k,\{\})\}\land C(l)\operatorname {in} v}$

${\displaystyle =\operatorname {let} v=k\land C(\{\})\operatorname {in} v}$

${\displaystyle =\operatorname {let} v=k\operatorname {in} v}$

${\displaystyle =k}$

集合の要素を表す値セットは、

${\displaystyle \forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=\operatorname {let} R=V(\{(w,\{(R,x,w)\}):w\in X\})\operatorname {in} R}$

このかなり奇妙な定義は、従属条件の一部として設定された値を追加します。これは、従属値を除外して絞り込む場合に使用されます。

式の値は

${\displaystyle x=V(R)}$。

R は従属条件が属する値セットを識別し、x はlet 式で値を運ぶために使用される変数を提供するため、 Rとx の両方が従属条件に含まれている必要があります。

従属条件へ のRの追加を無視すると、式はより単純で理解しやすい形になります。

${\displaystyle \forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=V(\{(w,\{(\_,x,w)\}):w\in X\})}$

導出は、

${\displaystyle V(\{(w,\{(r,x,w):w\in X\})}$

${\displaystyle =\operatorname {let} (v,l)\in \{(w,\{(r,x,w)\}):w\in X\}\land C(l)\operatorname {in} v}$

${\displaystyle =\operatorname {let} v\in X\land ({\bigwedge _{(r,z,u)\in \{(\_,x,v)\}}z=u})\operatorname {in} v}$

${\displaystyle =\operatorname {let} v\in X\land (\forall r\forall z\forall u(r,z,u)\in \{(\_,x,v)\}\to z=u)\operatorname {in} v}$

${\displaystyle =\operatorname {let} v\in X\land x=v\operatorname {in} v}$

${\displaystyle =\operatorname {let} x\in X\operatorname {in} x}$

値集合の関数適用は次のように表される。

${\displaystyle V(M)\ V(N)=V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})}$

導出、

${\displaystyle V(M)\ V(N)}$

${\displaystyle =\operatorname {let} (m_{v},m_{l})\in M\land C(m_{l})\operatorname {in} m_{v})\ (\operatorname {let} (n_{v},n_{l})\in N\land C(n_{l})\operatorname {in} n_{v})}$

${\displaystyle =\operatorname {let} (m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\land C(n_{l})\land C(n_{l})\operatorname {in} m_{v}\ n_{v})}$

次に、

${\displaystyle C(m_{l})\land C(n_{l})}$

${\displaystyle =({\bigwedge _{(z,u)\in m_{l}}z=u})\land ({\bigwedge _{(z,u)\in n_{l}}z=u})}$

${\displaystyle =({\bigwedge _{(z,u)\in m_{l}\cup n_{l}}z=u})}$

${\displaystyle =C(m_{l}\cup n_{l})}$

得る、

${\displaystyle =\operatorname {let} (m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\land C(n_{l}\cup n_{l})\operatorname {in} m_{v}\ n_{v})}$

${\displaystyle =\operatorname {let} (v,l)\in \{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\}\land C(l)\operatorname {in} v}$

${\displaystyle =V(\{(m_{v}\ n_{v},m_{l}\cup n_{l}):(m_{v},m_{l})\in M\land (n_{v},n_{l})\in N\})}$

除外は、条件が偽でなければならない場合を決定するルールです。

${\displaystyle V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))}$

これは、

${\displaystyle V(M)\in s}$

${\displaystyle \to \forall v\forall l((v,l)\in M\land C(l))\to (v=V[M]\land V(M)\in s)}$

${\displaystyle \to \forall v\forall l((v,l)\in M\land C(l))\to v\in S}$

${\displaystyle \to \forall v\forall l((v,l)\in M\land v\not \in S)\to \neg C(l)}$

簡略化ルールにより、条件が false である値を削除できます。

${\displaystyle V(K)=V(\{(v,l):(v,l)\in K\land C(l)\}}$

導出

${\displaystyle V(\{(v,l):(v,l)\in K\land C(l)\})}$

${\displaystyle =\operatorname {let} (v,l)\in \{(v,l):(v,l)\in K\land C(l)\}\land C(l)\operatorname {in} v}$

${\displaystyle =\operatorname {let} (v,l)\in K\land C(l)\land C(l)\operatorname {in} v}$

${\displaystyle =\operatorname {let} (v,l)\in K\land C(l)\operatorname {in} v}$

${\displaystyle =V(K)}$

関数を値セットに適用することを定義することで、値セットの等価性の定義も再定義されました。値セットはペアのセットとして構築されるため、等価性の古い定義は依然として存在します。2 つのセットが同じ要素を含む場合、それらは等価です。値セットの等価性のこの定義は、せいぜい誤解を招くものです。

必要なのは、値セットの構造の一部として、値セットが構築される変数の名前または ID を使用することです。これにより、値セットが同じ変数に基づいていない限り、値セットが区別されるようになります。

数学では、量化は値に対して行うものであり、式に対して行うものではありません。値セットの正確な定義をさらに進めるには、式の同一性を比較できるような方法で、式に対して量化を行う必要があります。値を表す式と式の同一性の違いは、使用と言及の区別です。表記法、

${\displaystyle \forall x\#u}$

式xの量化を意味するために導入されます。ここで、x は使用としての値を指し、u は表現または言及された式の同一性を指します。

この表記法を用いると、集合定義の要素は次のようになる。

${\displaystyle \forall x\#u\forall X(\operatorname {let} x\in X\operatorname {in} x)=\operatorname {let} R=V((u,\{(w,\{(R,x,w)\}):w\in X\}))\operatorname {in} R}$

値セットへのすべての参照は、値セット内の追加の構造レベルを考慮して変更する必要があり、説明が読みにくくなります。読みやすさを考慮して、この追加の構造レベルは値セットの定義から省略されています。

「絞り込み」とは、値の条件がfalseになる必要がある場合を決定することです。絞り込みは、2 つの値セットの値が等しいとアサートされたときに開始されます。

2つの値セットが等しいという主張は、狭めのルールを与える。

${\displaystyle \forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))}$

導出は、まず、

${\displaystyle V(M)=V(N)}$

価値条件は、

${\displaystyle (\forall m_{v}\forall m_{l}((m_{v},m_{l})\in M\land C(m_{l})\to v=V(M))\land (\forall n_{v}\forall n_{l}((n_{v},k)\in N\land C(n_{l}))\to n_{v}=V(N))\land V(M)=V(N)}$

${\displaystyle \forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}(((m_{v},m_{l})\in M\land C(m_{l}))\to m_{v}=V(M))\land (((n_{v},n_{l})\in N\land C(n_{l}))\to n_{v}=V(N))\land V(M)=V(N)}$

${\displaystyle \forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (C(j)\land C(k)\to v=u)}$

${\displaystyle \forall m_{v}\forall m_{l}\forall n_{v}\forall n_{l}((m_{v},m_{l})\in M\land (n_{v},n_{l})\in N)\to (m_{v}\neq n_{v}\to \neg (C(m_{l})\land C(n_{l})))}$

いずれかの基本条件が偽の場合、そこから得られるすべての条件は偽になります。

これは条件関数の定義から来ています。

${\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}$

(r, z, u)の基本条件は、

${\displaystyle C(\{(r,z,u)\}=(z=u)}$

したがって、これが偽であれば偽です。 ${\displaystyle C(l)}$

従属条件リストに同じ値セットからの 2 つの異なる基本条件がある場合、それは false である必要があります。

これを導くには、まず排除ルールから始めます。

${\displaystyle \forall v_{1}\forall l_{1}\forall v_{2}\forall l_{2}((v_{1},l_{1})\in K\land (v_{2},l_{2})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))\implies \neg (C(l_{1})\land C(l_{2}))}$

すると、任意の従属条件集合lに対して、

${\displaystyle ((K,x,v_{1})\in l\ \land (K,x,v_{2})\in l\land v_{1}\neq v_{2}}$

${\displaystyle \implies (v_{1},\{(K,x,v_{1})\})\in K\land (v_{2},\{(K,x,v_{2})\})\in K\land (v_{1},l_{1})\neq (v_{2},l_{2}))}$

${\displaystyle \implies \neg (C(\{(K,x,v_{1})\})\land C(\{(K,x,v_{2})\}))}$

${\displaystyle \implies \neg C(l)}$

したがって、従属条件リストが同じ値セットの 2 つの条件に基づいている場合、その従属条件リストの条件値は false になります。

各値セットは、その値セットが構築される基本値セットに制約を課します。基本値セットに、値セットに従属値として存在しない値が含まれている場合、これらの値の条件は false である必要があります。

これを導くには、完全な集合の規則から始める。

${\displaystyle \exists v\exists \ l(v,l)\in K\to C(l)}$

条件関数は、

${\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}$

特定の従属条件は、全体の条件によって暗示されるものとして選択される場合がある。

${\displaystyle \forall L\ C(l)\to (L,z,u)\in l\to z=u}$

それで

${\displaystyle \forall L\exists v\exists l\ (v,l)\in K\to C(l)\to (L,z,u)\in l\to z=u}$

ここで、式は、取り得る値の集合を定義するために並べ替えられる。 ${\displaystyle z=V(L)}$${\displaystyle V(L)}$

${\displaystyle E(K,L)=\{w:(v,l)\in K\land C(l)\land (L,z,w)\in l\}}$

など、

${\displaystyle V(L)\in E(K,L)}$

次に除外ルールを使用して、

${\displaystyle V(M)\in s\iff (\forall v\forall l((v,l)\in M\land v\not \in s)\to \neg C(l))}$

与える、

${\displaystyle (\forall K\forall L\forall v\forall l((v,l)\in L\land v\not \in E(K,L))\to \neg C(l))}$

これは、絞り込み除外ルールです。 は、 値セットKで表される基本値Lセット内の値のセットです。 他の値の条件は false である必要があります。 ${\displaystyle E(K,L)}$

値セットは、値セットが特定の値を持つという命題の真偽を推論するために条件関数が適用される可能性のある従属条件を記録します。同じ構造を使用して、値セットが特定の値に等しい確率を与えることができます。条件関数は、

${\displaystyle C(l)=({\bigwedge _{(r,z,u)\in l}z=u}))}$

確率関数は、

${\displaystyle P(l)=({\prod _{(r,z,u)\in l}P(z=u)}))}$

これは、イベントが独立している場合に、各基本ケースが特定の値を保持する確率です。

確率関数は3つの公理によって定義される。

1. 各ペアは、値セットの確率がvであり、リストに適用される確率関数であることを意味します。${\displaystyle (v,l)}$${\displaystyle V(K)}$${\displaystyle P(l)}$
2. 値セット全体の確率の合計は 1 です。
3. 値セット内の任意の 2 つのペアの確率はゼロです。

確率関数は、ブール帰納的推論によって与えられた初期確率に基づいて結果の確率を与えます。

正式には、

値セット内の各値の確率は、確率関数と値条件を使用して、基本値セット内の確率から計算できます。基本値セットは、単一の値または複数の値のセットのいずれかです。

単一の値を表す値セットは、

${\displaystyle k=V(\{(k,\{\})\})}$

完全なセットルールは、

${\displaystyle \sum _{(v,l)\in K}P(l)}$

${\displaystyle =\sum _{(v,l)\in \{(k,\{\})\}}P(l)}$

${\displaystyle =P(\{\})}$

${\displaystyle =1}$

それは公理と一致しています。

複数の値を表す値セットは、

${\displaystyle \forall x\forall X(\operatorname {let} x\in X\operatorname {in} x)=V(\{(w,\{(\_,x,w)\}):w\in X\})}$

確率は許容値ルールによって与えられ、

${\displaystyle \sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}P(l)=1}$

これを単純化すると、

${\displaystyle \sum _{v\in \operatorname {gset} (V(K))}P(x=v)=1}$

値の確率の事前推定値が与えられている場合、その値が値セット内にあると、事前推定値は事後確率に比例します。

${\displaystyle \forall v\in \operatorname {gset} (V(K)),P(x=v)=w*P_{i}(x=v)}$

値が値セットに含まれていない場合、確率はゼロになります。

${\displaystyle \forall v\not \in \operatorname {gset} (V(K)),P(x=v)=0}$

それで、

${\displaystyle \sum _{v\in \operatorname {gset} (V(K))}w*P_{i}(x=v)=1}$

${\displaystyle w={\frac {1}{\sum _{v\in \operatorname {gset} (V(K))}P_{i}(x=v)}}}$

${\displaystyle \forall v\in \operatorname {gset} (V(K)),P(x=v)={\frac {P_{i}(x=v)}{\sum _{v\in \operatorname {gset} (V(K))}P_{i}(x=v)}}}$

${\displaystyle \forall v\not \in \operatorname {gset} (V(K)),P(x=v)=0}$

事前確率がすべて同じであれば、確率は

${\displaystyle \forall v\in \operatorname {gset} (V(K)),P(x=v)={\frac {1}{|\operatorname {gset} (V(K))|}}}$

一般的な値セットは、基本値セットの適用から作成されます。値条件ルールと確率関数を組み合わせると、

${\displaystyle \forall vP(v=V(K))=\sum _{(v,l)\in K\land v\in \operatorname {gset} (V(K))}({\prod _{(r,z,u)\in l}P(z=u)}))}$

絞り込みにより、変数の制約を満たさない値を排除できます。方程式を解くアルゴリズムの基礎として考えれば、この絞り込みにより、変数の制約と一致する値のセットが得られます。ただし、数学では、この値のセットにアクセスする方法はありません。

が変数xを制約する式である場合、変数が取り得る値の集合は、 ${\displaystyle E(x)}$

${\displaystyle \{z:E(z)\}}$

xのgset をxの制約を満たす値の集合として定義します。gsetを次のように定義することを検討してください。

${\displaystyle \operatorname {gset} (x)=\{z:E(z)\}}$

この定義は、 xのすべての制約を与える条件である式E を知っていることに依存します。数学では、E はxから取得できない場合があります。したがって、値のセットを要求するために変数に適用できる数学関数はありません。では、gset関数を数学に追加できるでしょうか?

gsetのメタ数学的定義は可能かもしれません。私たちが数学として知っているものが、実際にはmathと呼ばれるメタ関数によって実装されていると想像してください。 math は抽象構文木を受け取り、変数と数学的構造に意味を与え、明示的に量化されていない変数に存在量指定子を追加します。

math は、独自の変数を持つメタ数学環境内の式になります。これらのメタ変数を数学変数と区別するには、メタ変数を大文字で表し、数学変数を小文字で表します。

ここで、 xmath関数によって実装された数学の拡張実装があると仮定します。これは次のように定義されます。

${\displaystyle \operatorname {xmath} [E]=\forall M,\operatorname {let} T[M]=\operatorname {math} [E]\operatorname {in} T[\_]}$

xmath を使用すると、gset は次のように定義されます。

${\displaystyle \forall x\#u,\exists N,\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\}}$

ここでも表記は、

${\displaystyle \forall x\#u}$

変数xの量化を意味するために使用されます。ここで、x は値を指し、u は変数の一意の ID を指します。

たとえば、制約式 を例に挙げます。 ${\displaystyle x^{2}=4}$

${\displaystyle x^{2}=4}$

${\displaystyle \land s=\operatorname {gset} (x)}$

${\displaystyle \land (\forall x\#u,\exists N\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\})}$

xmath式は次のようになります。

${\displaystyle \forall M,\operatorname {let} T[M]=}$

${\displaystyle \exists x,\exists s,(x^{2}=4}$

${\displaystyle \land s=\operatorname {gset} (x)}$

${\displaystyle \land (\forall x\#u,\exists N,\operatorname {gset} (x)=\operatorname {let} M[u]=x\operatorname {in} \{z:z=N[u]\land T[N]\})}$

${\displaystyle \operatorname {in} T[\_]}$

ここで、uは変数xの一意の識別子であり、ここでは数値1（gsetの呼び出しで使用される最初の変数）として表されます。

${\displaystyle M[1]=x\land s=\{z:z=N[1]\land T[N]\}}$

ここでは、M を N として T を呼び出します。${\displaystyle T[N]}$

${\displaystyle s=\{z:z=N[1]\land x^{2}=4\land x=N[1]\}}$

${\displaystyle s=\{z:z^{2}=4\}}$

• 関数型プログラミング
  • 遅延評価
  • 多態型システム
  • 型推論
  • 高階関数
  • ハスケル
• ラムダ計算
  • 演繹的ラムダ計算
  • 表現
• 論理プログラミング
  • 解決（ロジック）
  • 制約論理プログラミング
  • 制約
  • 日食
• 数学
  • 関数（数学）
  • 代数
  • 分離
• リレーショナルプログラミング