# Re: [isabelle] Where to learn about HOL vs FOL?

On 2/2/2013 4:17 PM, "Mark" wrote:

Yes, I agree it's very difficult.


Mark,


But there's still lots of good news, like "the market" is way past Cambridge LCF, and that low-priced computers now can have 4 cores, 8 GBytes of ram, and run at 2.5GHz or greater, because without fast computers, functional programming would still be the domain of the academics. It was only a few years ago that I would rail about Java, after my computer performance would come to crawl because the browser was starting up Java.


The docs distributed with HOL Zero have some good tutorial information in them, like "3_HOL_Language.txt".


I created the file "HOL_Zero_docs.tex". If a person unzips "holzero-0.6.0.tgz", and puts my .tex file in the folder "./holzero-0.6.0", then they can produce the PDF file "HOL_Zero_docs.pdf".


I had to add the extension ".txt" to the files without an extension, otherwise "\VerbatimInput" gave an error.


I attached "HOL_Zero_docs.tex", and I attached ""HOL_Zero_docs.pdf", where the PDF is for demonstration purposes only. The PDF is to show what a person would have access to if they were to install Latex on their machine and compile the .tex file.


Again, the PDF is for demonstration purposes only. It is required that any student of HOL acquire the sources from the web and compile their own .tex file. The allotted time for viewing the PDF for demonstration purposes is an integer m, where m can be greater than or equal to 1, but less than or equal to 30, where the dimension of m is seconds.

Regards,
GB


When I started in theorem proving I was
also struck by the lack of a clear learning path.  Isabelle is I think one
of the most difficult to *really* understand how everything works.  You have
to understand each of the many layers of Isabelle.  I'm afraid I don't
understand these layers, although I would like to at some stage, but more
seem to be getting added as the years go by!  But the main priorities for
the implementors of Isabelle, as I understand it, have been usability and
power, and having an understandable implementation comes way down the list.
In HOL Zero, trustworthiness and understandable implementation are top of
the list (they go hand-in-hand in my opinion), but of course it is very
basic and no good for creating proofs.  So I think an important part of the

Mark.

on 2/2/13 9:04 PM, Gottfried Barrow<gottfried.barrow at gmx.com>  wrote:


On 2/1/2013 3:41 PM, "Mark" wrote:

Does that clear anything up?

Mark,

I was sort of speaking of maybe where I was a year ago, but "the
problem" is still there to a certain extent.

So I count 30 folders for the "HOL section" of books, then there's the
non-HOL logic folders, where I count 49 folders, along with the ML
folders, 14 of those, and the Isabelle section with about 14 top level
folders, but many subfolders by author or web page.

Before tying into the last paragraph, in the document
kanaskskis-8-logic.pdf, I point out the semi-formal BNF grammar
describing a HOL4 type, page 11, and then the first BNF grammar
describing a term, page 15, followed by the second BNF grammar of a term.

I now ask, "Where is the semi-formal definition of a Isabelle type and
term?"

If you said, "If you understand the HOL4 definitions of a type and term,
then you basically understand Isabelle's".

To that I would reply, "But I'm not interested in studying 2 or 3 or 4
other HOL's to get a general understanding of Isabelle's logic, I'm
interested in studying one logic to get a precise understanding of the
one logic that I'm using."

"The problem" is represented by another question. "What is the clear
learning path for learning about a particular HOL so that a person can
use that HOL in a theorem assistant, and do that within a reasonable
period of time, and not just end up with a foggy notion of ideas?"

The answer is that, for self-education, there is no clear path. It's not
clear what is essential, and what is an unneeded tangent. But that's not
anyone's fault. It just indicates that the market is not mature.

In a mature market, speaking analogously, you don't have to learn C, to
learn C++, to learn Java, when it's Java that you're going to be using.
In a mature market, people have written lots of books to start you
wherever you want to start.

Now to something of a positive nature. The name for your HOL Zero site
on my hard drive is "hoZ", and I downloaded the latest glossary, which
is now named "hoZ__Glossary 130202.pdf".

It occurred to me that I can tweak it to fit my own preferences, so I
saved it to PDF, and with Acrobat, I can add a bookmark entry for each
of the terms, and make them sub-bookmarks of their first character.
Doing that, I'll be able to see the trees, and not just the forest.

There are many mini-lessons in there that don't demand a big investment
of time, so thanks for that.

Regards,
GB


I think it can get quite confusing because different people use the same
names for different things, and different names for the same things, and
sometimes the same people do this too!

"HOL" can mean "higher-order logic" (referring to one or more of various
logics that are higher-order), or it can mean "the HOL logic" (Mike

Gordon's

particular higher-order logic, implemented by HOL4, Isabelle/HOL, HOL

Light,

ProofPower and HOL Zero).  Other theorem provers such as Coq, PVS and

IMPS

implement other higher-order logics.  So the logic described in the HOL4
logic manual really is the same as HOL Light's, etc, the only difference
being that they are built up in different ways (i.e. they start with a
different initial set of axioms and primitive inference rules, but these
axiomatisations are just different ways of defining the same logic).
Does that clear anything up?

Mark.

on 1/2/13 2:23 PM, Gottfried Barrow<gottfried.barrow at gmx.com>   wrote:


On 1/31/2013 1:46 PM, Yannick Duchêne (Hibou57) wrote:

Seems available on‑line; here is a link for the paper you suggest:
http://www.sciencedirect.com/science/article/pii/S157086830700081X#

There's a newer dated version, 20 December 2007, at the author's web
site. The published one says "received in revised form 6 August 2007".

http://imps.mcmaster.ca/doc/seven-virtues.pdf
http://imps.mcmaster.ca/doc/

When the gurus try to succinctly describe Isabelle/HOL, they'll many
times just use the phrase "simply typed lambda calculus".

https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

But if they have time to type a few extra characters, they might add the
phrase "with polymorphism".

If you keep talking long enough, another one might pop in and throw in
the term "type classes".

Because there's no HOL which has yet won the HOL wars, then they use
external, historical vocabulary to begin the description of their HOL,
but then have to start attaching their own internal vocabulary to the
description.

For someone looking for a label to label HOL with, as a starting place
to learn about HOL, it can get confusing.

If you see the phrase "simple type theory" in the title of Farmer's
paper, then you might ask, "Ah, is this what's going to tell me what
Isabelle/HOL is? Because 'simple type theory' sounds suspiciously like
'simply typed lambda calculus'".

https://en.wikipedia.org/wiki/Type_theory#Theory_of_simple_types

Being an authoritative prophet, I can now say that in the future, the
HOL's which win out in the HOL wars will be the standard themselves, and
the references will be to the 700 page textbooks which formalize,
starting with the basics, what the logic of these HOLs are.

For HOL4 they already have that in their logic manual (to what degree I
can't say), which I thought would be the perfect place to learn about
Isabelle/HOL's formal logic, but it's not, it's the perfect place to

http://hol.sourceforge.net/documentation.html

For completeness, I quote from Mark's glossary to show how the gurus
have to do a lot qualifying when they try to explain things:

simply-typed : (adj)  Relating to type systems that are relatively

simple

and
are not, for example, dependently-typed.  There is considerable

variation

in

the
precise intended meaning of "simply-typed" in contemporary usage: in

some

usages
polymorphism is not a disqualifying factor, in other usages polymorphism

is

only
a disqualifying factor if it caters for the quantification of type
variables,
and in other usages still any form of polymorphism is a disqualifying
factor.
To avoid confusion, the usage of this term is avoided in HOL Zero, its
documentation and elsewhere in this glossary.


Still looking at Gottfried's list.

In addition to collecting books, I also rip web pages for past,
educational courses on Isabelle. I haven't had time to study any of this
right now. I'm making enough progress just stumbling along. I'll get
more sophisticated later. Some of these are linked to from the official
Isabelle site, many of them aren't.

Regards, GB

http://cl-informatik.uibk.ac.at/teaching/ss08/atp/schedule.php

http://isabelle.in.tum.de/coursematerial/IJCAR04/

http://archiv.infsec.ethz.ch/education/permanent/csmr.html

http://isabelle.in.tum.de/exercises/

http://www.irisa.fr/celtique/genet/ACF/

http://dream.inf.ed.ac.uk/projects/isabelle/

http://isabelle.in.tum.de/coursematerial/PSV2009-1/

http://www21.in.tum.de/teaching/logik/SS12/

http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/

http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1112/

http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php

http://www.lri.fr/~wenzel/Isar2010-Orsay/

http://www.lri.fr/~wenzel/Isabelle2011-Paris/

http://www.lri.fr/~wenzel/Isabelle_Orsay_2012/

http://www.lri.fr/~wenzel/Isabelle_Orleans_2012/








Attachment: HOL_Zero_docs.pdf

\documentclass[11pt]{article}
\usepackage{color}
\usepackage{fancyvrb}
%==================================================================
%\ooONEoo{[hyperref]}
%==================================================================
]{hyperref}
\urlstyle{rm}
\hypersetup{pdfcenterwindow=false}  % position the document window in the center of the screen
\hypersetup{pdffitwindow=false}     % resize document window to fit document size
\hypersetup{pdfstartview=FitH}      % {XYZ null null 1.1}, FitH
\hypersetup{pdfnewwindow=true}      %
\hypersetup{pdfpagelayout=OneColumn}% OneColumn-continuous
\hypersetup{pdfview=FitH}           % default view for a link
\hypersetup{bookmarks=true}         %
\hypersetup{bookmarksopenlevel=2}   %
\hypersetup{bookmarksnumbered=true} %
\hypersetup{bookmarksopen=true}     %
\hypersetup{pdfpagemode=UseOutlines}% UseOutlines->show bookmarks, None->don't show bookmarks

%==================================================================
%\ooONEoo{Set the frontmatter page numbering style}
%==================================================================
% This will be changed somewhere after the title and TOC are created.
\pagestyle{plain}
\renewcommand{\thepage}{\roman{page}}

%==================================================================
%\ooONEoo{[TOC] tocdepth, secnumdepth}
%==================================================================
\setcounter{tocdepth}{6}
\setcounter{secnumdepth}{6}

%==================================================================
%\ooONEoo{geometry}
%==================================================================
\usepackage[%
paperheight=11in,
paperwidth=7.5in,
asymmetric,      % Without it, the chapter mark is used on every page, due to my fancyhdr setup
hcentering,      % needed if asymmetric is used
width=6.25in,
% PAGE NUMBER AT TOP WITH RULE
top=.2in,
bottom=.1in,
% PAGE NUMBER AT BOTTOM
%includeheadfoot,       % see Figure 2 (b) page 3
%top=.1in,              % Top margin
%foot=.35in,            % Space the footer is in
%bottom=.25in,          % Bottom margin
]{geometry}%

%==================================================================
%\ooONEoo{SECTION COMMAND}
%==================================================================
\newcommand{\SECTION}[1]{%
\newpage%
\renewcommand{\sectionmark}[1]{\markboth{#1}{}}%
\sectionmark{#1}%
\section*{#1}%
}%

%==================================================================
%\ooONEoo{fancyhdr: IS NOW SET TO ARTICLE}
%==================================================================
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
% PAGE NUMBER AT TOP WITH RULE
\fancyhead[LE]{\leftmark}% LE = left even, LO = left odd
\fancyhead[LO]{\leftmark}% LE = left even, LO = left odd
\fancyhead[RE,RO]{\thepage}  % RE,RO = right even, right odd
\renewcommand{\footrulewidth}{0pt}
% PAGE NUMBER AT BOTTOM
%\fancyfoot[CE,CO]{\footnotesize\bf\thepage}
%\renewcommand{\footrulewidth}{0pt}

%==================================================================
%\ooONEoo{raggedbottom, raggedright, parindent, reversemarginpar}
%==================================================================
\flushbottom
%\raggedbottom
%\raggedright                   % must be used with \setlength{\parindent}{0.7cm}
%\setlength{\parindent}{0.0cm}
\parindent 1em                 %"1em", rougly width of uppercase "M" in current font
\parskip 0.5ex                 % 1ex, rougly the height of lower "x" in current font
\reversemarginpar              % Puts margin notes on only 1 side, I think

%==================================================================
%\ooONEoo{fancyvrb commands}
%==================================================================
\definecolor{verbcolor}{rgb}{0,0,0.29}
\definecolor{rulecolor}{rgb}{.7,.7,.7}
\newcommand{\VRBINPUT}{\VerbatimInput[%
gobble=0,firstnumber=1,
formatcom=\color{black},fontsize=\small,fontfamily=tt,%fontshape=em,
frame=leftline,framerule=.2mm,framesep=1.4mm,rulecolor=\color{rulecolor},
xleftmargin=5.5mm,numbers=left,numbersep=1.1mm]}

%==================================================================
%\ooONEoo{BEGIN DOCUMENT}
%==================================================================
\begin{document}

%==================================================================
%\ooONEoo{TITLE}
%==================================================================
\title{\ \\\ \\\ \\\ \\\ HOL Zero Docs}%
\\\ Generated from Documents
\\\ In the HOL Zero Source Tarball
\\\ holzero-0.6.0.tgz
\\\ \\\ at
\\\ www.proof-technologies.com/holzero}%
\date{\today}%
\maketitle
\newpage

%==================================================================
%==================================================================
\tableofcontents
\newpage
\pagestyle{fancy}
\renewcommand{\thepage}{\arabic{page}}
\setcounter{page}{1}

%==================================================================
%\ooONEoo{HOL ZERO DOCS}
%==================================================================

\SECTION{VERSION}
\VRBINPUT{VERSION.txt}

\SECTION{BOUNTY}
\VRBINPUT{BOUNTY.txt}

\SECTION{CHANGES}
\VRBINPUT{CHANGES.txt}

\SECTION{INSTALL}
\VRBINPUT{INSTALL.txt}

\SECTION{doc/COMPARISON}
\VRBINPUT{doc/COMPARISON.txt}

\SECTION{Contents}
\VRBINPUT{doc/User_Manual/Contents.txt}

\SECTION{1\_Introduction}
\VRBINPUT{doc/User_Manual/1_Introduction.txt}

\SECTION{2\_ML\_Library}
\VRBINPUT{doc/User_Manual/2_ML_Library.txt}

\SECTION{3\_HOL\_Language}
\VRBINPUT{doc/User_Manual/3_HOL_Language.txt}

\SECTION{4\_HOL\_Logic}
\VRBINPUT{doc/User_Manual/4_HOL_Logic.txt}

\SECTION{A1\_Library}
\VRBINPUT{doc/User_Manual/A1_Library.txt}

\SECTION{A2\_Input\_and\_Display}
\VRBINPUT{doc/User_Manual/A2_Input_and_Display.txt}

\SECTION{A3\_Language\_Utils}
\VRBINPUT{doc/User_Manual/A3_Language_Utils.txt}

\SECTION{A4\_Theory\_Commands}
\VRBINPUT{doc/User_Manual/A4_Theory_Commands.txt}

\SECTION{A5\_Inference\_Rules}
\VRBINPUT{doc/User_Manual/A5_Inference_Rules.txt}

\SECTION{B1\_Theory}
\VRBINPUT{doc/User_Manual/B1_Theory.txt}

\SECTION{B2\_Theorems}
\VRBINPUT{doc/User_Manual/B2_Theorems.txt}

\SECTION{C\_Grammar}
\VRBINPUT{doc/User_Manual/C_Grammar.txt}

\SECTION{Glossary}
\VRBINPUT{doc/Glossary.txt}

%==================================================================
%\ooONEoo{END DOCUMENT}
%==================================================================
\end{document}


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