2
$\begingroup$

My textbook(Pierce's Types and Programming Languages defines $\mathbb{B}$(untyped) our language as consisting of the terms $True$, $False$, and $if\ t_{1}\ then\ t_{2}\ else\ t_{3}$ and the evaluation rules $$(1)\ if\ True\ then\ t_{2}\ else\ t_{3}\ \rightarrow\ t_{2} \\ (2)\ if\ False\ then\ t_{2}\ else\ t_{3}\ \rightarrow\ t_{3} \\ (3) \frac{t\ \rightarrow\ s}{if\ t\ then\ t_{2}\ else\ t_{3}\ \rightarrow\ if\ s\ then\ t_{2}\ else\ t_{3}}$$

It then goes on to define a binary relation "$\rightarrow$" as the "one-step evaluation" which is the smallest binary relationship satisfying the rules above.

Shortly after, he defines "$\rightarrow^{*}$", as the reflexive, transitive closure of "$\rightarrow$". And by the sound of it this is meant as some nice notation and not to add anything new, but I do not see how we can have reflexiveness. For example, consider $t\ =\ if\ True\ then\ False\ else\ True$ then we clearly get by (1) that $t\ \rightarrow\ False$ and this is the only way to evaluate $t$. So, I don't see how we can get back to $t$. Especially since we also proved that if $t\ \rightarrow\ s$ and $t\ \rightarrow\ s'$ then $s = s'$, so any evaluation of $t$ must be $False$ and the evaluations must stop there. Am I missing something or does this reflexiveness break what we want(which I assume is nice notation for iterated evaluations)?

$\endgroup$

1 Answer 1

4
$\begingroup$

The $\rightarrow^*$ is adding something new. Forget the details of the definition of $\rightarrow$ for the moment and just treat it as an arbitrary relation. "Reflexive, transitive closure" means the smallest relation extending $\rightarrow$ such that $\rightarrow^*$ is both reflexive and transitive.

Therefore, by definition, for every $t$, we have $t \rightarrow^* t$, even if (as you seem to be saying) we do not have $t \rightarrow t$ in the original relation.

And if $t \rightarrow u$ and $u \rightarrow v$, then by definition we have $t \rightarrow^* v$, even though we might not have $t \rightarrow v$ originally.

In general, you should think of $t \rightarrow^* u$ as saying: we can get from $t$ to $u$ by applying $\rightarrow$ some finite number of times. This finite number can be zero.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .