# What exactly is delta reduction?

I have found two definitions of delta reduction:

1. Barry Watson defines it as the result of applying a primitive computation to terms in normal forms
2. But in Coq they define it as the substitution of a variable in a local context for its definition.

Although I wouldn't be entirely surprised if one turns out to be a special case of the other, at first impression they look like different reductions. So which one is correct?

Bonus points: in Coq they define even more reductions. Are these "recognised" in literature or are they specifically defined in Coq only? If they are generally accepted definitions, is there a comprehensive list of all known reductions beyond the standard alpha, beta, eta?

• $\delta$-reduction: the only hard problem in logic! :-)
– cody
Commented Aug 22, 2023 at 19:40
• #irony? Didn't quite understand the joke Commented Aug 22, 2023 at 21:09
• No, just a "pseudo-profound" statement: in general, performing every reduction except $\delta$ is very fast, and conversion checks become slow only when $\delta$ is taken into account (some caveat about record projection applies). Therefore the "hard" problem of conversion checking (which happens all the time during Coq execution) is only hard because of $\delta$!
– cody
Commented Aug 22, 2023 at 22:40
• Thanks. It seems like you have enough insight into this to actually answer the question then? Which definition of delta reduction are you referring to in your reasoning and is it the "one"? Commented Aug 23, 2023 at 15:43

Sadly, there is no clear consensus on what $$\delta$$-reduction is, other than the Greek letter $$\delta$$ being similar to the Latin "d" which also happens to be the first letter of "definition".

Indeed, the two definitions you give are both intuitively "replace a symbol $$f$$ by its definition $$F$$", where $$F$$ is uncurried in the first case, and curried in the second one.

This is related to $$\mathsf{let}$$-reduction as well, since a let is just introducing a symbol representing another term, though as the second link notes the semantics are slightly different (the $$\mathsf{let}$$ is deleted from the context in this case). This variant is called $$\zeta$$ in Coq parlance, also a very non-standard term, sadly.

Note that in non-dependent settings, these can all be replaced by $$\beta$$-reduction, changing a definition $$\mathsf{let}\ f := F\ \mathsf{in}\ t$$ by $$(\lambda f. t)\ F$$

but this does not work in dependently typed languages since the term $$\lambda f. t$$ may now be ill-typed!

Finally: in theorem proving settings, unfolding all the definitions to prove an equality isn't remotely practical, the sizes of terms become huge even with sharing. This means $$\delta$$-conversion needs to be done somewhat cleverly when performing conversion, and is a subject of study in its own right.

• Thanks! It's much clearer now! A follow up question I have is how to deal with delta reduction for recursive functions. I imagine the definition of a delta-redex somehow takes that into account and presumably doesn't even forbid it for infinite recursion since it's not computable anyway? I'll try find some introduction literature to delta reduction but if you have some, I'll be grateful if you share some. Thanks again. Commented Aug 24, 2023 at 8:10
• @RaffaeleRossi Probably worth asking that as a separate question.
– cody
Commented Aug 24, 2023 at 18:44

Even though @cody already gave a great answer, I would maybe simplify it a bit, as the comparison with let might be confusing for beginners.

With one sentence:

The substitution of a defined symbol with its definition is often referred to in the literature as ‘δ reduction’1

Example:
Replacing square with the definition of square

1 Alfred V. Aho. Computer science theory, section 1, lecture 24: The lambda calculus II, 2017. lecture notes, https://www.cs.columbia.edu/~aho/cs3261/Lectures/L24-Lambda_Calculus_II.html