[isabelle] Question Posed: Where is a good place to learn about HOL?



From: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle

On 5/30/2012 11:12 PM, Bill Richter wrote:
...Let me make a rudimentary FOL point:

I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom.

(Preliminary Comment): In my mind, I'm doubting that the so-called first-order language of Zermelo-Frankael set theory does in fact give one the ability to completely state and prove set theory as a first-order language, primarily because of the absence in the symbols of FOL to name constants in relation to FOL formulas. This sentence, however, should be ignored, since I'm sitting on a question about that.

Listing the books below is the purpose of this reply.

Also, as you may have observed on hol info, I know next to nothing
about HOL... Where is a good place to learn about HOL?

I am a "book collecting" step ahead of you when it comes to learning Isabelle/HOL, which I consider necessary to use Isabelle. My primary interest is not in HOL but in the first-order language of ZF sets. However, it's occurred to me that Isabelle/HOL can probably be used as a meta-language to implement any object-language that I'll be interested in. Additionally, and maybe of more importance, is the need in mathematics for a solid implementation of a number system. I gather that implementing a number system that's useful in a theorem prover is a very difficult thing to do, and it appears that the Isabelle group has put put a whole lot of work in doing that in Isabelle/HOL. It also appears that most of the tool support and code development is going into Isabelle/HOL.

Anyway, no one has told me this, but it appears that to understand Isabelle/HOL in depth, you need to understand a combination of subjects:

1) Natural deduction logic
2) Lambda calculus
3) Typed lambda calculus, some of it coming from a non-constructivist viewpoint
4) The ML programming language
5) The meta-logic of Isabelle/Pure

As to the minimum a person needs to know to be successful with Isabelle, I don't know what that is. Whatever the minimum is, I'm not there yet.

Below are a list of books and documents that I've found. I don't provide links to Amazon because the Amazon URLs get long, and the list server converts all HTML links to the actual URL.

-----NATURAL DEDUCTION LOGIC---

NOTE: You won't find much natural deduction in logic books written by mathematicians. They primarily use truth-table based logic.

"Proof and Disproof in Formal Logic", by Richard Bornat (Amazon)
        This books is what I'm working through. Some of it's written like
"An Idiot's Guide to Natural Deduction", but it's still good, and there's
        the Jape prover for doing some natural deduction exercises.
        http://www.cs.ox.ac.uk/people/bernard.sufrin/personal/jape.org/

"Mathematical Logic", by Ian Chiswell & Wilfrid Hodges (Amazon)
Covers natural deduction, but it also hits on a related logic, sequent calculus, that gets
        referred to in the Isabelle literature.

"Logic for Computer Science", by Jean H. Gallier (Amazon)
        More advanced. I use it to try and find unfamiliar terminology.

"Natural Deduction", by Dag Prawitz (Amazon)
One of the first books (or the first) on natural deduction. I use it to try and find unfamiliar terminology.

"Logic for Computer Science", by Steve Reeves and Mike Clarke (Amazon)
Covers natural deduction, but also hits on "semantic tableaux", which gets referred to in the Isabelle literature.
        http://en.wikipedia.org/wiki/Method_of_analytic_tableaux


---LAMBDA CALCULUS & TYPED LAMBDA CALCULUS---

NOTE: I separated lambda calculus from typed lambda calculus because there are books for typed lambda calculus that take a strong, constructivist approach, and some of these books don't apply as much. What you're looking for is simply typed lambda calculus.

"An Introduction to Functional Programming through Lambda Calculus", by Greg Michaelson (Amazon) Written to be "super friendly", it uses a combination of pseudo-programming syntax and lambda calculus syntax. It works through examples with an obnoxious level of detail which
      serve their purpose to drive the points in.

"Type Theory & Functional Programming", by Simon Thompson (Amazon)
Has intro chapters on propositional logic, first-order logic, and lambda-calculus. It ties together logic, lambda-calculus, and functional programming, and it emphasizes
      types as proofs, and proofs as types.

"Basic Simple Type Theory", by J. Roger Hindley (Amazon)
A more formal, mathematical treatment. Gets to typed lambda calculus fairly fast.

"Lambda-Calculus and Combinators - an Introduction", by Hindley & Seldin (Amazon) Has some of the same material as Hindley's books above, but has too much on
     combinatory logic.

"Foundations of Functional Programming", by Lawrence Paulson
     A quick summary of lambda calculus.
     http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf

"Introduction to Lambda Calculus", by Henk Barendregt & Erik Barendsen (Amazon)

"Lambda Calculi with Types", by Henk Barendregt (Amazon)

"Types and Programming Language", by Benjamin C. Pierce (Amazon)

"Lecture Notes on Lambda Calculus", by Peter Selinger
      http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf


---ML PROGRAMING LANGUAGE---

NOTE: The great thing about learning ML is that you can do your little code snippets in Isabelle. Just use the command "ML{* ...code... *}".

"ML for the Working Programmer", 2nd, by Larry Paulson (Amazon)

"Programming in Standard ML '97", by Stephen Gilmore
       http://homepages.inf.ed.ac.uk/stg/NOTES/

"Introduction to Functional Programming", by Mike Gordon
      http://www.cl.cam.ac.uk/~mjcg/Teaching/FuncProg/Notes/

"Programming in Standard ML", by Robert Harper
      http://www.cs.cmu.edu/~rwh/smlbook/

"Notes on Programming Standard ML of New Jersey", by Riccardo Pucella
      http://www.ccs.neu.edu/home/riccardo/research.html

"Elements of ML Programming", by Jeffrey D. Ullman (Amazon)


---META-LOGIC OF ISABELLE/PURE---

NOTE: I'll ask the list someday what documents explain the meta-logic, but here's some docs that appear to explain the meta-logic to varying degrees.

Paulson: http://www.cl.cam.ac.uk/~lp15/papers/refereed.html
       Isabelle - The Next 700 Theorem Provers
      The Foundation of a Generic Theorem Prover

Urban: http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/
      The Isabelle Cookbook

Wenzel: http://www4.in.tum.de/~wenzelm/papers/
Isabelle/Isar - A Generic Framework for Human-Readable Proof Documents Isabelle/Isar - A versatile environment for human-readable formal proof documents

From the Isabelle2012 release:
     Old Introduction to Isabelle
     The Isabelle/Isar Reference Manual
     A Proof Assistant for Higher-Order Logic


---BEST BOOK I'VE FOUND SO FAR---

"Principles of Mathematical Analysis, with a Friendly Introduction to Natural Deduction & Typed Lambda Calculus, and How to Implement Mathematical Proof in Isabelle2012, for the Working Mathematician, 4th Edition", by Walter Rudin (Amazon)


--GB







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.