Errata to "The Duality of Computation", P.-L. Curien, H. Herbelin ----------------------------------------------------------------- (version 1: June 2003, thanks to Phil Wadler) (version 2: October 2005) (version 3: January 2007) (version 4: November 2010, thanks to Zena Ariola) (version 5: February 2012, thanks to Zena Ariola & Paul Downen) (version 6: June/July 2012, typos and remarks thanks from Guido Gherardi Section 2: translation N: rule for (MN)^N is missing: replace the whole translation by x^N = x (lambda x.M)^N = lambda x.(M^N) (MN)^N = mu alpha.([alpha](MN))^N for alpha fresh (mu beta.c)^N = mu beta.c^N ([alpha]M)^N = M^N_alpha (MN)^N_E = M^N_(N^N.E) V^N_E = where V = x | lambda x.M | mu alpha.M Section 2: Proposition 2.3 is incorrectly stated: translation > preserves call-by-name reduction only up to (mu) expansion (an expansion " -> |alpha>" is needed to simulate the lambda-mu reduction "(mu beta.c) M -> mu alpha.c[beta<-(alpha,M)]"). The first sentence of the statement must be replaced by: The translation > is a homomorphism from lambda-mu-terms to lambda-bar-mu-terms for (call-by-name) reduction, up to (mu) expansion. The beginning of the proof has to be changed accordingly: Preservation of reduction up to the rule (mu) is trivial. The second part of the statement is an easy consequence of the following: ... Remark: the original statement remains correct for ordinary (non classical) lambda-calculus. Section 2, page 3, Remark 2.4: in the bottom of the rule, "lambda (x,alpha).c" should be "lambda (x,beta).c". Section 3, page 4: The rephrasing of Proposition 2.3 is, similarly, incorrectly stated: translation < preserves call-by-name reduction only up to (mu) and (mu~) expansions (an expansion " -> >|alpha>" is needed to simulate the lambda-mu reduction "(mu beta.c) M -> mu alpha.c[beta<-(alpha,M)]"). A correct formulation for the first sentence of the statement is: The translation < is a homomorphism for call-by-name reduction, up to (mu) and (mu~) expansions. Moreover, for any lambda-mu-term M, M^< reduces by repeated applications of the rule (mu) to M^N. Remark: the original statement remains correct for ordinary (non classical) lambda-calculus. Section 4, page 5, middle of the page: Symbol "<" is erroneously typed twice in sentence starting with "It happens that". The correct sentence is: It happens that < provides us with a right-to-left call-by-value discipline while > yields a left-to-right call-by-value discipline (whence the notations for these translations). Section 4, page 5, middle of the page: The statement "It can be proved that translation > is a homomorphism from call-by-value lambda-mu-calculus [17] to the lambda-bar-mu-mu~-calculus in call-by-value discipline" is wrong. An alternative, evasive, correct formulation is: The translation > relates call-by-value lambda-mu-calculus (see e.g. Ong-Stewart [17]) and lambda-bar-mu-mu~-calculus in call-by-value discipline, if both considered at an extended equational level. Section 5: first paragraph: the simple typing systems of lambda-bar-mu-mu~-T and lambda-bar-mu-mu~-Q respectively are LKt and LKq, where LKt (rest LKq) is LKtq from [5,6] where all formulas are coloured t (resp q). Section 6: "we need mu only under a lambda" should more precisely be "in the translation, we need mu only under a lambda", since, more generally, if we constrain mu to occur only under a lambda, one loses the ability to refer to isolated terms of the form mu alpha.c . Section 6: translation V: 2nd case: alpha is fresh. Section 6: definition of lambda-mu-tilde: inconsistent convention about the range of n: in rules (beta^1_V) et (beta^2_V), replace V_1...V_n by V V_1...V_N and V_2...V_n by V_1...V_n and [x <- V1] by [x <- V] so that the implicit convention is uniformly n>=0 both in the syntax and in the reduction rules. Section 7: duality table: column with and is missing: complete as follows x alpha mu beta mu~ x e.v v.e lambda x beta lambda alpha x mu~ x mu beta v.e e.v beta lambda lambda x Section 7: definition of lambda-bar-mu-mu~_Q: in category V, "lambda x.c" should read "lambda x.v". Section 8: The target of the translation is not pure lambda-calculus but lambda-calculus with pairs. There are different possible ways to have pairs. One can for instance extend lambda-calculus with constructions "(v,v')" and "let (x,y) = v in v'" and set "lambda(x,y).v" to mean "lambda z.let (x,y) = z in v" for z fresh. Section 8: Proposition 8.1: it should be added to the last sentence that it is in the case of lambda-bar-mu-mu~_Q that the CBV discipline is validated. Otherwise said, the last sentence should read Moreover, the translation validates the (CBV) reduction discipline of lambda-bar-mu-mu~_Q. Section 8: Proposition 8.3: similarly, it should be added to the last sentence that it is in the case of lambda-bar-mu-mu~_T that the CBN discipline is validated. Otherwise said, the last sentence should read Moreover, the translation validates the (CBN) reduction discipline of lambda-bar-mu-mu~_T. Appendix B: two occurrences of -> should be -o: (A->B)^T = !? A^T -o ? B^T (A->B)^Q = ! A^Q -o ?! B^Q