search

sdiehl / write-you-a-haskell

Building a modern functional compiler from first principles. (http://dev.stephendiehl.com/fun/)
MIT License
3.34k stars 256 forks source link

Paragraph on capture-avoiding substitution (lambda calculus chapter) is confusing #62

Open yanok opened 9 years ago

yanok commented 9 years ago

I guess the text is formally correct (although it can be more precise) but the example is completely misleading: capture might happen if we do substitution under a lambda but in the example substitution comes from the beta-reduction and after the reduction lambda is gone! There is actually nothing bad to have that x in \FV{a}, for example: (\x. x) x -> x. On the other hand, bad things still might happen even if we check x \notin \FV{a}, for example: (\x. \y. xy) y -> \y. yy (capture!). In fact, our substitution is defined to be capture-avoiding in the first place (condition in the last line of the definition ensures that), we probably just need an explanation that if the condition is not met it's always possible to alpha-convert the term such that substitution will be possible.

sdiehl commented 9 years ago

Is this fixed by #61 ?

yanok commented 9 years ago

Not really. I only fixed the typo in the substitution definition.