Errata to "An Operational Account of Call-By-Value Minimal and
Classical lambda-calculus in 'Natural Deduction' Form", Hugo Herbelin
and Stephane Zimmermann
-----------------------------------------------------------------
(last update: December 2010)
- Confusion on the definition of let_let and let_app
Page 4, Section 1.2: the rules let_let and let_app should be as
shown on Figure 1, page 5.
Page 4, Section 1.3: Footnote 2 is irrelevant and should be removed.
Page 9, Section 1.5, before Proposition 6: The paragraphs "But then
... calculus" and "To solve this, ... proposition:" are irrelevant
and should be removed.
- Standardization
Page 8, Section 1.5, Definition of Plotkin's standard reduction
sequences: two clauses are missing:
- any variable alone is a s.r.s.
- if M1, ..., Mn is a s.r.s. then lambda x.M1, ..., lambda x.Mn is a s.r.s.
Page 8, Section 1.5, Definition of weak-head reduction: In the first
clause defining M -h-> M', the subset of rules to consider is
restricted as follows:
If (letv) is present in the subset, we assume that M in the rules
(let_app), (let_let), (let_var) and (eta_let^E) is restricted to
the form E[yM'] so that head reduction favors (let_v). If
(eta_let^E) is present, we assume that N in the rules (let_app),
(let_let) and (let_var) is not of the form E[x] so that head
reduction favors (eta_let^E).
Page 8, Section 1.5, Definition of standard reduction sequences: The
following clause is missing:
- if M1 -h-> M and M2, ..., Mn is a s.r.s., then M, M, ..., M_n$ is
a s.r.s.
Remark: a posteriori, a better definition of weak-head reduction
would be obtained by considering the (let_app) and (let_let) as
operational rules as follows: G[M] -h-> G[M'] is M -r-> M' for (=>),
(letv), (let_app) or (let_let), and G is defined by
G ::= H | let x = H in M where H ::= [] | H M
- Confluence for the classical calculus
Page 12, proof of Proposition 9: "generalization of (mu_v) and
(mu_base) to contexts of the form E or [q]E" should be "generalization
of the rules involving mu and let".
- Typos
Page 9, Section 1.6: more reducing -> more reductions