Tapl：満足した説明と例

Question

この質問は私の読書から生じます 「タイプとプログラミング言語」 (ワールドキャット）ベンジャミンC.ピアス。

36ページの定義です 満足

ルールはです 満足 関係によって、ルールの各インスタンスについて、結論が関係にあるか、施設のいずれかがそうではない場合。

36ページの定義です 実例

an 実例 推論ルールのルールの結論とそのすべての前提（もしあれば）の同じ用語に各メタバリアブルを一貫して置き換えることによって得られます。

例えば

if true then true else (if false then false else false) -> true

のインスタンスです e-iftrue, 、両方の$ t_2 $の発生が置き換えられています true $ T_3 $は置き換えられました if false then false else false.

15ページの定義です relataion

n-place 関係 セットのコレクション$ s_1、s_2、...、s_n $はセット$ r subseteq s_1 times ; s_2 ; times ; ... ; times ; s_n $ of Tulple of Elements $ s_1 $から$ s_n $から。要素$ s_1 in> s_1 $ thorugh $ s_n in s_n $は$ r $で関連している場合、$（s_1、...、s_n）$は要素または$ r $です。

36ページの定義です ワンステップ評価関係（$ rightArrow $）

ワンステップ評価関係$ rightArrow $ 図3-1の3つのルールを満たす用語に関する最小のバイナリ関係です。ペア$（t、t '）$が評価関係にある場合、「評価ステートメント（または判断）$ t rightArrow t' $は派生可能であると言います。

34ページには、図3-1の3つのルールがあります

e-iftrue

begin {equation} if ; true

e-iffalse

begin {equation} if ; false

e-if

begin {equation} frac {t_1 rightArrow ; t_1 '} {if ; t_1 ; else ; t_3} end {式}

誰かがこの定義を説明し、定義の一部の例を挙げてもらえますか。
1.結論は関係にあります。
2.施設の1つはそうではありません。

注：本の質問に捧げられたフォーラムがあることを知っています ここ.

注：使用できます Google Scholar コンテキストでこの質問の詳細をもっと見るため。

編集

統一と用語の書き換えに関する私のコメントについてのいくつかの点をつなぐ。

私が見たとき

$$（a rightarrow b） equiv（ neg a vee b）$$

それは私に思い出させました ホーン・クロウズ から プロログ, 、それは例とともに、私の理解に関連しています 期間書き換え. 。本を持っている」用語書き換えなど" (ワールドキャット）Franz BaaderとTobias Nipkowによると、私はすぐに満足度を調べ、58ページで満足できることがわかりました。しかし、それもカバーしています 統一. 。その時点で、私は定義が対処していることに気付きました 満足度 そして、そこから私はすでに馴染みのあるトピックがありました。私が投げたのは、ベンジャミンがそれを定義した方法でした。彼は私が自分の知識に関連付けなかった方法で、すぐに非常に正確な定義を使用しました。

あなたが私と同じようにコードを使用してロジックプログラミングを理解している場合、定義は完全に理にかなっています。

Answer 1

の定義を読む1つの方法 満足 それは役立つかもしれません

ルールの各インスタンスについて、結論が関係にあるか、施設のいずれかがそうでない場合、ルールは関係によって満たされます。

論理的に同等のステートメントに

ルールは、ルールの各インスタンスについて、すべての施設が関係している場合、結論が関係している場合、関係によって満たされます。

したがって、例えばルールが言っている場合、

$$ dfrac {a to b quad b to c} {a to c} $$

次に、バイナリ関係$ r $は、ルールの各インスタンスについて、このルールを満たします。

$$ dfrac {a to b quad b to c} {a to c} $$

$（a、b） in r $ and $（b、c） in r $、$（a、c） in r $。

これを述べる別の方法は、$ r $がルールによって閉じられていることです（これはおそらくそれを明確にしないでしょう）。

それでは、元の声明に戻りましょう。何

ルールの各インスタンスについて、結論が関係にあるか、施設のいずれかがそうでない場合、ルールは関係によって満たされます。

施設のない関係に$（a、c）$を持っていることは大丈夫ですが、すべての施設が関係している場合は、$（a、c）$が必要です。つまり、追加の制約を課すことなく、関係のすべての施設を持つことはできません。

個人的には、この定義について考えることは、含意の観点から考えることはより簡単だと思うので、この説明が役立つのを助けます。

Answer 2

デイブ・クラークがの定義を指摘したように 満足 実際に意味は、命題論理で覚えておいてください：$$（a rightArrow b） equiv（ neg a vee b）$$

これは偶然ではありません。推論ルールは、正式なロジックの提供性を定義するためにも使用されます。

---

の例 e-iftrue:

敷地内）：

• 前提はありません。このルールは公理です（または、すべての用語$ t_2 $、$ t_3 $の公理のセット）です。

結論：

• ペア$（$ if true then true else (if false then false else false)$,$ true$)$

ルール以来 e-iftrue 前提がありません、 すべて 敷地内にあります どれか の関係 毎日 実例。したがって、このルールを満たす関係$ r $は、すべてのインスタンスの結論、つまり$ t '$を使用して$ t $から導出できるように、すべての項$（t、t'）$のすべてのペアを含める必要があります。 e-iftrue. 。それで

$\{($ if true then true else false $,$ true $), ($ if true then false else false $,$ false $), ($ if true then false else true $,$ false $）、 dots } subseteq r $。

---

インスタンスの例 e-if:

敷地内）：

• ペア$（$ if true then false else true$,$ false$)$

結論：

• ペア$（$ if (if true then false else true) then true else false $,$ if true then true else false$)$

ここに、ルールを満たすための2つの選択肢があります$ r $： if true then false else true$,$ false$）$または$（$も含める必要があります if (if true then false else true) then true else false $,$ if true then true else false$）$。しかし、実際には、評価関係が満たさなければならないので、前提を除外することは選択肢ではありません e-iftrue また、このルールでは$を含める必要があります（$ if true then false else true$,$ false$)$.

---

デイブ・クラークが指摘したように、それはどの規則のいずれでも要求されていない他のペアを含むかもしれません。これは、複数のルールを満たすための評価関係を必要とするため、各ルールに対して許可する必要があります。最小限の関係を選択することにより、ルールによってキャプチャされない用語を導き出すことができないことを確認します。