4
$\begingroup$

This question arises from my reading of "Types and Programming Languages" (WorldCat) by Benjamin C. Pierce.

On page 36 is the definition for satisfied

A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

On page 36 is the definition for instance

An instance of an inference rule is obtained by consistently replacing each metavariable by the same term in the rule's conclusion and all its premises (if any).

For example

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

is an instance of E-IFTRUE, where both occurrences of $t_2$ have been replaced by true and $t_3$ has been replaced by if false then false else false.

On page 15 is the definition for relataion

An n-place relation on a collection of sets $S_1, S_2,..., S_n$ is a set $R\subseteq S_1\times\;S_2\;\times\;...\;\times\;S_n$ of tuples of elements from $S_1$ through $S_n$. We say that the elements $s_1\in > S_1$ thorugh $s_n\in S_n$ are related by $R$ if $(s_1,...,s_n)$ is an element or $R$.

On page 36 is the definition for one-step evaluation relation ($\rightarrow $)

The one-step evaluation relation $\rightarrow $ is the smallest binary relation on terms satisfying the three rules of Figure 3-1. When the pair $(t,t')$ is in the evaluation relation, we say that "the evaluation statement (or judgment) $t \rightarrow t'$ is derivable."

On page 34 are the three rules from Figure 3-1

E-IFTRUE

\begin{equation}if\;true\;then\;t_2\;else\;t_3\;\rightarrow\;t_2\end{equation}

E-IFFALSE

\begin{equation}if\;false\;then\;t_2\;else\;t_3\;\rightarrow\;t_2\end{equation}

E-IF

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

Can someone explain this definition and give an example for parts of the defintion.
1. The conclusion is in the relation.
2. One of the premises is not.

Note: I am aware that there is a forum dedicated to questions for the book here.

Note: You can use Google Scholar to see more of the details to this question in context.

EDIT

To connect some of the dots about my comment regarding unification and term rewriting.

When I saw

$$(A\rightarrow B)\equiv (\neg A \vee B)$$

it reminded me of Horn claues from Prolog, that along with the example then connected with my understanding of term rewriting. Having the book "Term Rewriting and All That" (WorldCat) by Franz Baader and Tobias Nipkow, I quickly looked up satisfiability and found satisfiable on page 58. This is actually the start of whole chapter on Equational Problems; but it also covers unification. At that point I realized that the definition was dealing with Satisfiability and from there is was a topic I was already familiar. What threw me was the way Benjamin defined it. He used a very precise definition right up front in a manner I didn't associate with my knowledge.

If you work through the code as I am and understand logic programming, then the definition makes perfect sense.

$\endgroup$
4
$\begingroup$

One way of reading the definition of satisfied that might help is to change

A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

to the logically equivalent statement

A rule is satisfied by a relation if, for each instance of the rule, if all the premises are in the relation, then the conclusion is in the relation.

Thus if the rule says, for instance,

$$ \dfrac{A \to B \quad B\to C} {A\to C} $$

Then binary relation $R$ satisfies this rule whenever for each instance of the rule, such as

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

if $(a,b)\in R$ and $(b,c)\in R$, then $(a,c)\in R$.

Another way of stating this is that $R$ is closed by the rule (though this probably doesn't make it clearer).

Now let's return to the original statement. What

A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.

is saying is that is it okay to have $(a,c)$ in the relation without the premises, but if all of the premises are in the relation, then $(a,c)$ must be. That is, it is okay to have not all of the premises in the relation, without imposing any additional constraint.

Personally, I think that thinking about this definition in terms of an implication is simpler, so I help this explanation helps.

$\endgroup$
  • $\begingroup$ While it is still a bit vague, it is now clear enough that I can move on and hopefully with further reading understand it enough to talk about it in the future. Would you know if the defintion from pg. 58 of "Term Rewriting and All That" is the same? I cam make that a sepearte question if you prefer. $\endgroup$ – Guy Coder Mar 9 '13 at 12:43
  • $\begingroup$ Where is it vague? I can try to fix that. (I don't know the definition from page 58.) $\endgroup$ – Dave Clarke Mar 9 '13 at 13:03
  • $\begingroup$ After seeing $$(A\rightarrow B)\equiv (\neg A \vee B)$$ in frafl's answer, knowing about satisfiable from "Term Rewriting and All That" and unification, it is no longer vague. Thanks for offering to fix it. :) $\endgroup$ – Guy Coder Mar 9 '13 at 13:10
  • $\begingroup$ This is what the first part of my text says. $\endgroup$ – Dave Clarke Mar 9 '13 at 13:15
  • $\begingroup$ It's not your wording, it's my lack of understanding of the relations between the meanings. frafl's way just connected with my knowledge; over all I learned more from your answer. $\endgroup$ – Guy Coder Mar 9 '13 at 13:25
2
$\begingroup$

As Dave Clarke pointed out the Definition of satisfied is actually an implication, remember in propositional logic: $$(A\rightarrow B)\equiv (\neg A \vee B)$$

This is no coincidence, inference rules are also used to define provability in formal logic.


Example for E-IFTRUE:

premise(s):

  • There is no premise, this rule is an axiom (or rather a set of axioms for all terms $t_2$,$t_3$).

conclusion:

  • the pair $($ if true then true else (if false then false else false)$,$ true$)$

Since the rule E-IFTRUE has no premises, all of the premises are in any relation for every instance. So a relation $R$ satisfying this rule has to contain all instance's conclusions, i.e. all pairs of terms $(t,t')$ such that $t'$ can be derived from $t$ using E-IFTRUE. So

$\{($ if true then true else false $,$ true $), ($ if true then false else false $,$ false $), ($ if true then false else true $,$ false $),\dots \} \subseteq R$.


Example for an instance E-IF:

premise(s):

  • the pair $($ if true then false else true$,$ false$)$

conclusion:

  • the pair $($ if (if true then false else true) then true else false $,$ if true then true else false$)$

Here we have two choices to satisfy a rule $R$: Either we leave out $($ if true then false else true$,$ false$)$ or we also have to include $($ if (if true then false else true) then true else false $,$ if true then true else false$)$. But actually, leaving out the premise is not an option, since the evaluation relation has to satisfy E-IFTRUE too and this rule requires the inclusion of $($ if true then false else true$,$ false$)$.


As Dave Clarke pointed out it may contain other pairs not required by any of the rules. This has to be allowed for each single rule because we want a the evaluation relation to satisfy multiple rules. By choosing the minimal relation we ensure that it's not possible to derive terms not captured by any rule.

$\endgroup$
  • $\begingroup$ I used Google Scholar to search for satisfied and found nothing that made sense to me with regards to the definition of satisfied. I will add the definition of one-step evaluation relation from the book and maybe that will help. $\endgroup$ – Guy Coder Mar 9 '13 at 1:17
  • $\begingroup$ Yes, that helped. I found the book using google books, but the definition of E-IF wasn't readable there. That helped even more to understand, how he uses pairs of terms for the evaluation relation. $\endgroup$ – frafl Mar 9 '13 at 12:33
  • $\begingroup$ $$(A\rightarrow B)\equiv (\neg A \vee B)$$ really drove home why the definition is worded as it is. $\endgroup$ – Guy Coder Mar 9 '13 at 12:47
  • 2
    $\begingroup$ How hard is it to spell my name correctly? $\endgroup$ – Dave Clarke Mar 9 '13 at 13:08
  • 1
    $\begingroup$ I'll remove my comments now. $\endgroup$ – Dave Clarke Mar 10 '13 at 7:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.