Update introduction to Relations.lagda.md

[DavidPratten]

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.

[wadler]

Thanks for the suggestion.

I deliberately avoided the approach you take in your introduction: I want to get the reader used to thinking in terms of relations rather than functions that yield a boolean. It is the approach of this chapter that comes first, not the approach of chapter Decidable, so the wording you've given is backwards of what I would say.

Did you find the chapter confusing as written? That would be a good reason to consider some form of change, if not exactly the one you propose. The obvious one would be to give the boolean form of less-than-or-equal first, but I really don't want to do that.

[DavidPratten]

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]

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