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



/From/: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr <mailto:yannick_duchene at DOMAIN.HIDDEN>>

  * /Date/: Wed, 01 Jan 2014 20:28:11 +0100

------------------------------------------------------------------------
Le Fri, 01 Feb 2013 15:22:53 +0100, Gottfried Barrow <gottfried.barrow at gmx.com> a écrit:

    ...but it's not, it's the perfect place tolearn
    about HOL4's formal logic:
    http://hol.sourceforge.net/documentation.html
    [...]


The one titled "Logic" (file name "kananaskis-8-logic.pdf") still says in the preface:

    ...Because this logic is shared
    with other theorem-proving systems (HOL Light, ProofPower),
    and is similar to that implemented in Isabelle, where it is
    called Isabelle/HOL, it is now presented in its own manual.


What is perfect will vary according to need. The HOL4 logic manual is imperfect for a perfect understanding of Isabelle/HOL, and also of Isabelle/Pure, because HOL4 is only similar to what is implemented in Isabelle. Significant differences are that with Isabelle there are two logics, along with type classes.

To set the stage, I repeat a variation of a question I've asked in the past, and I state a law.

QUESTION_1: Where is the BNF grammar, or similar grammar, that precisely states what a typed lambda calculus term is in Isabelle/Pure and Isabelle/HOL?

QUICK_COMMENT: Such a grammar might immediately answer certain questions, such as whether an Isabelle/Pure term is identical to an Isabelle/HOL term. Here, I explicitly differentiate between Pure and HOL because of a paper by Wenzel in which he emphasizes that there are two HOLs in Isabelle. I reference the paper below.

LAW OF RIGOR: If you don't have the time to treat a formal, mathematical topic with proper rigor, then do your best to never mention the topic, lest you be accused of being a non-rigorous arm-waver. If you must discuss the topic, then give the shortest, possible overview of the topic, to make it obvious that the overview is not a formal treatment of the topic.

I assume that the Law of Rigor is one reason why the grammar I mention above doesn't exist for the current state of the Isabelle art, though such a thing may actually exist. Simple questions such as "Where is such and such?", when such and such is somewhere, are many times not answered. Such is life.

I say here that I've found several, older documents in which a type and term was defined for the state of the Isabelle art at that time. I reference those documents below.

*COMPLEX TYPED TERMS, NO MOTIVE TO SORT THROUGH A SIMILAR GRAMMAR*

Back to the HOL4 logic manual, on page 8 there is the phrase "[a] more accurate grammar of terms is", and then he gives a grammar which we must sort through using previously defined grammars, along with more formal discussion.

It would be doable, if I was willing to expend enough brain waves, but it would never get me an exact understanding of what an Isabelle/Pure and Isabelle/HOL term is.

I now use my first-order logic analogy. At the point I understood Bilaniuk's definitions 5.1, 5.2, and 5.3 to define the symbols, terms, and formulas of a first-order language, the definition of a first-order language ceased to be Ph.D. level knowledge for me. If I completely understand those definitions, how can it be Ph.D. level knowledge? I don't have a Ph.D.

I bring the first-order logic analogy to an end prematurely to keep things shorter, lamenting that I must sacrifice what would've been the most intellectually stimulating rhetoric of my whole life (a joke? no, no joke), but I also consider the upside of not having to type 800 more characters. It's six of one, or a half dozen of the other, as they say. Economically speaking, we can equate the most intellectually stimulating rhetoric of my whole life with the time I would have spent typing 800 more characters, minus the number of characters in this sentence.

Anyway, I already know that terms have types, and types have types. I don't see any purpose in straining my brain to study something like the HOL4 grammar to only end up understanding, a bit better, that terms have types and types have types. When an authority on Isabelle publishes the grammar of QUESTION_1 above, then it's worth putting out that kind of effort.

*SOME ISABELLE SOURCE BEFORE SOME ORIGINAL SOURCES*

Frequently, I've seen it stated that Isabelle is simply typed lambda calculus. Here, I'd like to make the point that the definition of a lambda calculus term is fairly simple, which I do to compare its simplicity to a typed lambda calculus term, which is not simple.

Consider the following:

term "x::(('a::{type,equal,ord}) list)"

Understanding the typing of concrete examples like this is straightforward, though partly straightforward because I can use the PIDE to show me what some of the inferred typing is.

What the example shows is that the general case for a typed term is not simple at all. There are four things that can vary there: variable, type variable, type variable type (the type class), and type constructor.

*SOME ORIGINAL SOURCES*

Your recent question about sorts led to me sorting through some bibliographies again:

Re: [isabelle] Are sorts of Isabelle the same as what's described for second order logic? http://fa.isabelle.narkive.com/oYtXhS2I/isabelle-are-sorts-of-isabelle-the-same-as-what-s-described-for-second-order-logic

I've decided the available documentation of Isabelle can be described as "30 documents spread over 20 years". There is the question of which is more difficult:

1) Is it more difficult for me to understand involved explanations about how typing works, where some of the names for the types are outdated, and the definitions are mainly formatted in paragraph form, rather than formatted in a BNF grammar type style?

2) Or, is it more difficult for me to remember where the difficult passages are in the 30 documents spread out over 20 years?

I list in chronological order some documents I've sorted through, and make some comments:


*1987: LOGIC AND COMPUTATION, INTERACTIVE PROOF WITH CAMBRIDGE LCF*
By L. C. Paulson
Published by Cambridge Tracts in hardcopy form.

Section 5.1.3 contains a BNF syntax for types, and 5.1.4 has one for terms. The book is pretty much a textbook style book. The first part of the book teaches some basic logic, such as natural deduction and sequent calculus.

I guess after the first time a person does that, the motivation to repeatedly teach the basics decreases over time.


*1994: ISABELLE, A GENERIC THEOREM PROVER*

by Lawrence Paulson, with Contributions by Tobias Nipkow
Published by Springer-Verlag in hardcopy form.

This book was broken up into 5 documents, and distributed with the Isabelle distribution. I looked at Isabelle1999-2 to Isabelle2008. The PDFs for a long time were intro, logics, logics-HOL, logics-ZF, and ref.

The ref document stayed mostly the same up until 2008, after which it started to be subsumed by other documents. With Isabelle2013-2, it's completely gone.

Of note is that the page count of intro.pdf, the old intro, has stayed at about 77 pages from 1999 to 2013-2:

http://isabelle.in.tum.de/website-Isabelle2013-2/dist/Isabelle2013-2/doc/intro.pdf

Section 1.2 discusses type classes, and even explains the empty sort. This seems to be an important document.

Possibly, some type names have changed. I've been wondering what the type of "int" is, because the PIDE doesn't show it has a type with this:

term "a::int"

Section 1.2 tells me that the type of the "int" constructor is "term". I don't ever see that in the PIDE.


*1995: TYPE RECONSTRUCTION FOR TYPE CLASSES*

by Tobias Nipkow and Christian Prehofer
http://www21.in.tum.de/~nipkow/pubs/jfp95.html

There's a grammar for a Mini-Haskell on page 3.

If someone told me, "The Mini-Haskell syntax basically describes a Isabelle/HOL term", I'd say, "Great, so go ahead and modify it so that I know exactly what a Isabelle/HOL term is, rather than basically know. I wouldn't understand it at first, but an important starting point is having a precise definition."


*1997: TYPE CLASSES AND OVERLOADING IN HIGHER-ORDER LOGIC*

by Makarius Wenzel
http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf

Here Makarius, in several ways, treats Isabelle/Pure as the HOL to be considered, rather than Isabelle/HOL. He says,

   As a quite harmless simplification, HOL can be identified directly
   with Isbelle/Pure.

The consequence for me is that I now want to see a precise definition for a typed term for both Isabelle/Pure and Isabelle/HOL. It might help me see a difference that's important, that I otherwise wouldn't see.

In section 3.1 HOL Syntax, he quickly describes the HOL types and terms.


*OUTRO*

I have a better understanding now that terms have types and types have types. I'm better now at understanding what I see when I have show_sorts on.

Below, I include some of what I was looking at. I was mainly interested in looking at the types "type" and "{}".

Regards,
GB



(******************************************************************************)
theory i140105a
imports Complex_Main
begin
declare[[show_sorts=true]]
declare[[show_brackets=true]]

(*OBJ_EXP_1: lambda calculus terms are simple, but typed Isabelle/HOL terms are complex. Four things are involved here: variable, type variable, type variable
type (the type variable type class), and type constructor. Does the type
constructor 'list' also have a type?
*)
term "x::(('a::{type,equal,ord}) list)"


(*OJB_EXP_2: Do type variable constants such as 'int' have a type? Type
variable constants such as 'int' aren't displayed as having type. But in Coq,
type constants have a type, such as "nat:Set":
  http://www.labri.fr/perso/casteran/CoqArt/Tsinghua/C5.pdf
I think that int is a 0-ary type constructor. If so, the basic question is the
same. Do 0-ary type constructors have a type?
*)
term "x::int" (*Displayed: "(x::int)"::int.*)


(*EXP_3: Inferred: x::('a::{})
*)
term "x"
term "x::('a::{})"

(*META_EXP_4: Inferred: x::('a::{}).
*)
term "x == x"
theorem "x == x"
  by(simp)
theorem "x == (x::('a::{}))"
  by(simp)

(*OBJ_EXP_5: Type: x::('a::ab_semigroup_add).
*)
theorem "(x::('a::{type, plus, semigroup_add, ab_semigroup_add})) = x"
  by(simp)

(*OBJ_EXP_6: Type: x::('a::{plus,equal}).
*)
theorem "(x::('a::{plus,equal})) = x"
  by(simp)

(*META_EXP_7: Inferred: x::prop. There is no type variable.
*)
term "PROP x"
theorem "PROP x == PROP x"
  by(simp)

(*OBJ_EXP_8: Inferred: x::('a::type).
*)
term "x = x"
theorem "x = x"
  by(simp)
theorem "x = (x::('a::type))"
  by(simp)

(*OBJ_EXP_9: Trying to make 'a to be type {} gives an error.
*)
(*
theorem "x = (x::('a::{}))"
  (*ERROR: Type unification failed: Variable 'a::{} not of sort type.*)
*)

(*META_EXP_10: defining 'a to have type "type".
*)
theorem "x == (x::('a::type))"
  by(simp)

(******************************************************************************)
end



















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