6
$\begingroup$

Lambda calculus is often introduced as a rewriting or substitution system. Where $\beta$ reduction is described as replacing bound variables with the value that variable is bound to. For example $(\lambda x. x) y \rightarrow y$ is described as replacing all the instances of "x" in the expression with y.

Now extensions of lambda calculus (such as Martin-Lof type theory) often allow the creation of definitions, for example: $$\text{id} := \lambda x .x$$

My question is as follows. Does this definition create a new rewrite rule that says whenever we encounter "id" rewrite/substitute "$\lambda x.x$" or does it state "id" and "$\lambda x.x$" represent the same underlying referent?

Is the distinction I'm making even meaningful?

$\endgroup$
2
$\begingroup$

The distinction you are making can be useful and is actually used in some proof assistants.

There are many possible rewriting rules in lambda-calculus, the main ones being $\alpha$-conversion, $\beta$-reduction and $\eta$-conversion. The fundamental equivalence relation between terms is syntactic equality $\equiv$, which is usually defined so that it contains $\alpha$-conversion. But there are also other equivalence relations which identify terms up to repeated application of $\beta$-reduction and/or $\eta$-conversion.

For example, intensional equality $=_\beta$ between terms is defined by the rules: $$\frac {M \to_\beta N} {M =_\beta N} \qquad \frac {M \equiv N} {M =_\beta N} \qquad \frac {M =_\beta N} {N =_\beta M} \qquad \frac {L =_\beta M \quad M =_\beta N} {L =_\beta N}$$ which together express the fact that $=_\beta$ is the reflexive, symmetric and transitive closure of $\to_\beta$.

Extensional equality $=_{\beta\eta}$ is another relation between terms, defined by the rules: $$\frac {M \to_\beta N} {M =_{\beta\eta} N} \qquad \frac {M \to_\eta N} {M =_{\beta\eta} N} \qquad \frac {M \equiv N} {M =_{\beta\eta} N} \qquad \frac {M =_{\beta\eta} N} {N =_{\beta\eta} M} \qquad \frac {L =_{\beta\eta} M \quad M =_{\beta\eta} N} {L =_{\beta\eta} N}$$

So, when we say that two terms are "the same" or "equal", we need to specify whether we are talking about syntactic equality, intensional equality or extensional equality.

In your case, what you call "creation of definitions" might be seen as either an extension of syntactic equality with rules such as $$\mathsf {id} \equiv \lambda x. x$$ or as giving introduction rules for another rewriting rule that is sometimes known as $\delta$-conversion. One of such rules could be $$\mathsf {id}\, M \to_\delta M$$ which morally reflects the fact that $\mathsf {id}$ is the identity. In this case, we would then define new equivalence relations $=_{\beta\delta}$ and $=_{\beta\delta\eta}$, just like before but respectively with the additional rules $$\frac {M \to_\delta N} {M =_{\beta\delta} N} \qquad \frac {M \to_\delta N} {M =_{\beta\delta\eta} N}$$

The choice depends on what we want to do. Most of the times we do treat $\mathsf {id}$ as a shortcut for $\lambda x. x$, so we may choose to consider them syntactically equivalent. But in some contexts it makes sense to consider also $\delta$-conversion: for example, in Coq the so-called "unfolding of transparent constants", which essentially corresponds to $\to_\delta$, allows to rewrite a new constant only when it makes sense to do so.

Remark. There are reasons why it is preferable to have $\mathsf{id} \, M \to_\delta M$ instead of $\mathsf{id} \to_\delta \lambda x. x$, see Taroccoesbrocco's comments below.

$\endgroup$
  • $\begingroup$ In my opinion, you are giving a misrepresented notion of $\delta$-reduction. In $\lambda$-calculus extended with constants, $\delta$-reduction replaces a function applied to the required number of arguments (a redex) by a result. But it does not reduce a constant to it is "equivalent" $\lambda$-term (which is what the OP is asking). So, if we extend the $\lambda$-calculus with a constant $\mathsf{id}$ for the identity function, $\mathsf{id} \not \to_\delta \lambda x.x$ but $\mathsf{id}N \to_\delta N$ for any $\lambda$-term $N$. This difference is subtle but is crucial, as I'll explain below. $\endgroup$ – Taroccoesbrocco Aug 13 '18 at 20:45
  • $\begingroup$ Indeed, consider a (simply) typed extension of $\lambda$-calculus with constants such as PCF (which is closer to real functional programming languages): the fixed point combinator $\mathsf{Y}$ in PCF can be seen as a new constant such that $\mathsf{Y}N \to_\delta N (\mathsf{Y}N)$ for any term $N$, but you cannot define $\mathsf{Y} \to_\delta Y$ where $Y$ is the usual $\lambda$-term representing the fixed point combinator, because this $\lambda$-term $Y$ cannot be simply typed and hence it does not belong to the syntax of PCF. $\endgroup$ – Taroccoesbrocco Aug 13 '18 at 20:50
  • $\begingroup$ You're right – I was thinking of untyped lambda-calculus, but even there the two formulations are only extensionally equivalent. I'll edit my answer to reflect this. $\endgroup$ – Luca Bressan Aug 13 '18 at 21:36
1
$\begingroup$

The standard view is that "id" and "$\lambda x.x$" represent the same underlying referent. More precisely, "id" is just a shorthand (a macro, an alias) for the $\lambda$-term "$\lambda x.x$". And similarly for other definitions of this kind.

Adding new rewriting rules for any new definition not only would uselessly complicate the rewrite system, but would also alter$-$and worsen without apparent reason$-$some kinds of investigations such as complexity analysis (which is based on counting the number of reduction steps to reach the normal form; it is an interesting subject in the theory of programming languages from an implementation point of view).

$\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.