search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.37k stars 315 forks source link

Update introduction to Relations.lagda.md #1008

Closed DavidPratten closed 5 months ago

DavidPratten commented 5 months ago

Give readers a bridge from the previous chapter, clarifying the chapter's goal and linking it to the Decidability chapter.

The section below on Decidability has been merged into the introduction giving the overview of the chapter up front.

DavidPratten commented 5 months ago

Thanks Philip, I’m not sure my suggestion is the best improvement either.

Really enjoying the book it’s a great introduction to many important ideas

Yes, I experienced the jump from Induction to Relations as puzzling. I couldn’t see the motivation for the change of frame of reference from “computing” to “evidencing”.

The questions, “surely we just realised the addition relation more directly”, and “why are changing approach here?” bugged me until I jumped ahead and got the explanation in Decidable.

wenkokke commented 5 months ago

I'm closing this, since we're unlikely to merge this particular rewrite. Feel free to continue the discussion.