TAPL：满足的解释和示例

Question

这个问题来自我的阅读 “类型和编程语言” (世界猫）本杰明·C·皮尔斯（Benjamin C. Pierce）。

第36页是定义 使满意

规则是 使满意 通过关系，如果对于规则的每个实例，则结论是在关系中，或者没有一个前提。

第36页是定义 实例

一个 实例 通过在规则的结论及其所有前提（如果有）中始终如一地替换每个Metavariable（如果有），则可以通过相同的术语替换每个Metavar。

例如

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页是定义 关系

一个地方 关系 在集合的集合上，$ s_1，s_2，...，s_n $是set $ r subseteq s_1 times ; s_2 ; times ; times ; ... ; times ; s_n $从$ 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规则的术语的最小二进制关系。当对$（t，t'）$处于评估关系中时，我们说“评估声明（或判断）$ t rightarrow t'$是可衍生的。”

第34页是图3-1的三个规则

e-iftrue

begin {equation} if ; true ; then ; t_2 ; else ; t_3 ; rightArrow ; t_2 end end eend {equation}}

电子iffalse

begin {qore} if ; false ; then ; t_2 ; else ; t_3 ; rightArrow ; t_2 end end eend {equation}}

e-if

begin {equination} frac {t_1 rightarrow ; t_1'} {if ; t_1 ; t_1 ; then ; t_2 ; else ; t_3 ; t_3 ; rightArrow ; if ; if ; t_1'; t_2'; ; else ; t_3} end {equation}

有人可以解释这个定义，并为省点的一部分举例说明。
1.结论是关系。
2.其中之一不是。

注意：我知道有一个论坛致力于本书的问题 这里.

注意：您可以使用 谷歌学术 在上下文中查看此问题的更多细节。

编辑

要连接有关我关于统一和任期重写的评论的一些点。

当我看到

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

它使我想起 号角 从 序言, ，与我的理解有关 术语重写. 。有这本书”术语重写以及所有这些" (世界猫）作者：Franz Baader和Tobias Nipkow，我迅速抬起头来令人满意，并在第58页上感到满意。这实际上是整章关于方程问题的开始；但这也覆盖了 统一. 。那时我意识到该定义正在处理 令人满意 从那里有一个我已经很熟悉的话题了。让我抛弃的是本杰明定义它的方式。他以我没有与我的知识联系在一起的方式使用了一个非常精确的定义。

如果您像我一样使用代码并了解逻辑编程，那么该定义很有意义。

Answer 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 $和$（b，c） in r $，则$（a，c） in r $。

说明这一点的另一种方式是，$ r $已被规则关闭（尽管这可能不会使其更清楚）。

现在让我们回到原始语句。什么

如果对于规则的每个实例，结论是在关系中，或者没有一个前提，则可以通过关系来满足规则。

说的是，没有任何场所的关系中有$（a，c）$，但是如果所有场所都在关系中，则必须$（a，c）$。也就是说，可以在不施加任何其他约束的情况下，没有关系中的所有前提。

就个人而言，我认为从含义上考虑这个定义更为简单，因此我可以帮助这种解释有所帮助。

Answer 2

正如戴夫·克拉克（Dave Clarke）指出的 使满意 实际上是一个含义，请记住命题逻辑：$$（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'$使用$ 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$)$

在这里，我们有两种选择满足规则$ 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$)$.

---

正如戴夫·克拉克（Dave Clarke）指出的那样，它可能包含任何规则不需要的其他对。每个单一规则都必须允许这一点，因为我们希望a评估关系以满足多个规则。通过选择最小关系，我们确保不可能得出任何规则捕获的条款。