explain neutral terms and add a simple exercise #1021
Conversation
There was a problem hiding this comment.
We cannot accept a pull request with a bracketed comment that is to be removed later. Please resolve such comments before putting in pull requests.
The revised text is much longer than the current text, and in my view less helpful.
I take it seriously when a reader doesn't understand a passage. That means something should change! But I'm not keen on a change that is much longer, and replaces my intuition by your intuition---best to have both, but I definitely don't want to lose my point of view.
I don't understand why terms that are not lambdas play a special role in normal forms or how that helps. A better exercise may be to show that terms in normal and neutral form do not reduce.
|
I didn't expect the PR to be accepted as is. But I thought a PR the best way to start the discussion. I don't mind removing the bracketed comment or writing the exercise (and a model solution). But I can't express your intuition. So until I hear from you that updating the PR would be productive, I plan to do nothing. The unanswered questions are:
|
In the Untyped chapter, I did not
understand the motivation for neutral terms. The best I
could find through web search was to notice that a neutral term
can be substituted for a variable without creating a β-redex. But
the Untyped chapter does not mention this property.
To address my own concern, I have written something about
alternative ways to define normal forms. And I have conjectured
that you prefer using neutral terms because it requires fewer Agda
constructors to specify normal forms─thereby reducing the number
of cases in relevant proofs. The PR discusses
alternatives and also includes a couple of exercises.
The pull request includes this unanswered question: Why does
the Untyped chapter use syntactic criteria to define normal form,
when the earlier chapters on typed lambda calculi used a semantic
criterion (the term does not reduce)?