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