3
$\begingroup$

I was reading Programming Languages and Lambda Calculi, which defines the multi-step reduction to be the reflexive-transitive closure of the one-step reduction. (Page 15, $\twoheadrightarrow_r$ is the reflexive-transitive closure of $\rightarrow_r$)

A quick search shows that this idea is widely accepted, for example by courses from Princeton, UPenn, CU, etc. However, I think the transtivity should be enough to capture the intuition of many steps. So why is reflexivity needed?

$\endgroup$
  • 1
    $\begingroup$ Because it's more convenient. This isn't about philosophy, but rather about micro-management of technicalities. $\endgroup$ – Andrej Bauer Mar 14 '17 at 22:18
10
$\begingroup$

The practical reason is that it is very convenient to include also the case "zero steps" in the definition of "many steps" (millennia of mathematical experience have taught us that it is usually a good thing to have a 0 around in our set of natural numbers).

One possible technical exemplification of this (but there are probably dozens more, perhaps more interesting than this one) is that $\to^+$, the transitive closure of reduction, does not satisfy the diamond property (a.k.a. confluence), whereas $\to^\ast$ satisfies it. For example, if $I:=\lambda x.x$, there is no way to close the following critical pair by means of $\to^+$:

$$I \leftarrow (\lambda x.I)(II) \to (\lambda x.I)I$$

To close the span, you need to consider the empty reduction $I\to^\ast I$.

$\endgroup$
6
$\begingroup$

The answer given is adequate but I'd like to mention that once you reduce a term to normal form, without reflexivity you're out of luck, with reflexivity you've hit a fixed point and thus you can use a fixed point under beta reduction to define the total reduction, as long as you have the nice normalization properties.

$\endgroup$

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.