Does anybody know of any good resources regarding
δ-reduction (delta-reduction), ie. reducing primitive functions in lambda calculus?
barrywatson.se/lsi/lsi_delta_
Saw it in Section 3 of leodemoura.github.io/files/elaborat, but couldn't find any further references to it in that section. 🤔
Conversation
These seem to talk about slightly different things; there is no such reduction of "primitives" in Lean. The environment is a map from constants (names) to definitions, and delta-reduction is substitution along that map, no further computation involved.
1
2
(Also note that many parts of the paper like unification constraints are outdated regarding Lean 3 and beyond)
1
Ah, interesting. Interested because Pikelet will have primitive types, like integers, characters, etc. with primitive reduction steps for certain operations that can be used during elaboration. That seems to usually be left out of formal specifications, as far as I've seen.
1
How do you ensure that reduction on primitives on open terms is confluent? Do you allow both x + 0 -> x and 0 + y -> y (which IIRC is fine, but usually not supported)? How big’s a kernel supporting this safely?
1
1
I am not sure which of these questions actually matter, but I guess some could be relevant?
1
1
No clue! I'm, still very much a beginner at this stuff, so yeah, these questions are good!