search

hbr / Lambda-Calculus

Some papers on "Lambda Calculus"
25 stars 4 forks source link

typos in CoC paper #10

Open tromp opened 5 months ago

tromp commented 5 months ago

While reading https://hbr.github.io/Lambda-Calculus/cc-tex/cc.pdf I found some typos:

Page 4: Carring out computations Carrying

Page 7: based to some extend extent

Page 6,9,...,105 wellformed welltyped well-formed well-typed

Page 19: Πx^A.B where the variable x is bound, but can appear free in B. Last B should be A.

I may open another issue for the next 20 pages.

hbr commented 5 months ago

Thanks for the comments. Your comment on page 19 does not apply. The bound variable x can occur free in B.

The other typos you have mentioned should be corrected in the online version.

tromp commented 5 months ago

The bound variable x can occur free in B.

Oops. Sorry for not thinking that through:-(

tromp commented 4 months ago

I think

Theorem 5.13. Subject reduction lemma Reduction of a term does change its type.

should say "does not change its type".

hbr commented 4 months ago

I think

Theorem 5.13. Subject reduction lemma Reduction of a term does change its type.

should say "does not change its type".

Your are absolutely right. The subject reduction theorem is a central theorem in any typed calculus. It basically says that a term of the promised type is actually return after computation (which is beta reduction in lambda calculus). Thanks for the hint.

The corrected version shall be available.

Regards Helmut