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