Errata to the ESSLLI 2000 notes
The list of known typos in "Lambda Calculus: a Case for Inductive
Definitions" of July 8, 2000.
- p.2: superdelopments -> superdevelopments
- p.3+35: Curch -> Church
- p.17: footnote 4 is repeated 3 lines below
- p.18: Exercise 3: 0 should be underlined
- p.24: Lemma 8: beta-reduction instead of abstract ->
- p.27: Exercise 7: sr=s -> sr=r
- p.33: wrong quote signs in the parts of the proof of the theorem
- p.36: Exercise 15 (a) shall have parts (i) and (ii) and not twice
(i).
- p.38: Lemma 23, second line of proof: t:tau -> t:rho
- p.39: measure h is defined as a natural number or 0 and in part II, p.15,
defined differently as a natural number (which is assumed to include
0).
- p.40: last case has t and t vector instead of s and s vector
- p.41 (the second most serious typo): The first application of Lemma 21(b)
gives rho such that y vector s has type tau in the context Delta, y:rho
(instead of Delta only).
- p.43: The definition of type substitution shall in the case for
all require beta not in alpha or free in sigma (alpha and beta
swapped), and this is achieved by renaming the bound variable beta!
- p.43:[Bar 93] is not part of the name "system F in Curry-style"
but only a reference where this naming can be found
- p.43: with rho replaced by any type sigma -> with alpha replaced
by any type sigma
- p.55: second diagram needs s -> sigma
- p.56: final paragraph needs an r' instead of r in the first case
for t
- p.60 (the most serious typo): In the conclusion of Lemma 49 one
has to use the transitive
reflexive closure of the relation and not the relation alone.
Comments welcome.
Ralph Matthes
Last modified: Thu Nov 2 16:23:19 CET 2000
http://www.tcs.informatik.uni-muenchen.de/~matthes/papers/essllierrata.html