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?
Best Answer
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.