[Haskell-beginners] structural induction, two lists, simultaneous

[Rustom Mody]

On Thu, Dec 18, 2014 at 12:28 PM, Pascal Knodel <pascal.knodel at mail.com>
wrote:
>
>
> > (∀ ys • (∀ f,zs • map f (ys ++ zs)  =  map f ys ++ map f zs))
> >
> > And now you can see that you want a proof of a one-variable theorem
>
> Thank you, Rustom Mody, that's it, reordering of universal quantifiers.
> By the way, I'm searching for a 'good' book about predicate logic for
> quite some time now.
> One with a strong link to mathematics and the quantification style
> that is used there would be nice. By chance, is there a reference
> (script/paper/book )
> you would recommend?
>

Two predicate calculus books that are particularly my favorites:
1. Dijkstra and Scholtens Predicate Calculus and Program semantics (5th
chapter is logic)
2. Logical Approach to Discrete Math by Gries and Schneider

Second is more of a student textbook

My own attempts (20 year old!) at integrating the Haskell philosophy with
the Dijkstra style of logic described in these books is here:

http://blog.languager.org/2014/09/pugofer.html
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20141218/5f2e0cc4/attachment.html>