Hi, Ray. Good to hear from you!
I agree with you; Melham's description is to the point. I found the paper
by Tom Melham available in full on his website:
http://www.comlab.ox.ac.uk/tom.melham/pub/Melham-1994-HLE.pdf
I don't want to propose any terminology here, but it seems from what Melham
says that the words "polymorphism" or "polymorphic" would be descriptive of
the version with object language type variables, and not of Church's
original version.
This paper references the book "Edinburgh LCF" by Gordon, Milner, and
Wadsworth, which I do not have yet, but just placed an order on Amazon.
http://www.amazon.com/Edinburgh-LCF-Mechanized-Computation-Computer/dp/3540097244/
Can anyone who has this book available check how it describes the addition
of type variables in the logic?
Peter
On Thu, Sep 25, 2008 at 11:04 PM, Toal, Dr. Raymond J. <[EMAIL PROTECTED]>wrote:
>
> Nice question, Peter, and well-phrased.
>
> I'd also be curious to know if there was a "proper way" to refer to the
> system with type variables in the meta language versus the system with type
> variables in the object language.
>
> I like the way Melham describes the "difference" on
> http://www.springerlink.com/content/v05328771180qj61/ --
>
> "The version of ... logic mechanized in HOL ...
> is essentially Church's ... extended with
> object-language polymorphism of the kind developed
> by Milner...."
>
> I had never thought of it as a "really significant
> innovation" before, but now that you mention it, it really
> is. Good observation!
>
> Ray
>
>
>
> -----Original Message-----
> From: Peter Vincent Homeier [mailto:[EMAIL PROTECTED]
> Sent: Thu 9/25/2008 2:28 PM
> To: [email protected]
> Subject: [Hol-info] How were type variables added to higher order logic?
>
> Since I began using HOL88 many years ago, I have always heard that the
> logic
> of HOL was "higher order logic," sometimes called "Church's simple theory
> of
> types." In the current version of the HOL4 DESCRIPTION manual, it says in
> the Preface on page 3:
>
> The version of higher order logic used in HOL is predicate calculus with
> > terms from the typed lambda calculus (i.e. simple type theory). This was
> > originally developed as a foundation for mathematics [2].
> >
>
> Here "[2]" is a reference to Church's paper "A formulation of the simple
> theory of types", published in The Journal of Symbolic Logic, Vol. 5, No.
> 2.
> (Jun., 1940), pp. 56-68. This paper is available online at
>
>
> http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.jsl/1183387805
>
> I have also heard that the logic of HOL is essentially the same as the
> logic
> Q_0 described in chapter 5 of Andrews's book "An Introduction to
> Mathematical Logic and Type Theory: To Truth Through Proof", Peter B.
> Andrews, Academic Press, 1986, ISBN 0-12-058535-9. A new second edition is
> available at
>
> http://www.amazon.com/Introduction-Mathematical-Logic-Type-Theory/dp/1402007639
>
> However, when reading both of these, I see that in neither case does the
> type system proposed contain type variables within the logic. They both
> use
> type variables as meta-variables, e.g. when describing an infinite class of
> related axioms, but they do not express such a notion as a single axiom
> using a type variable within the logic.
>
> It appears from checking page 11 of the HOL4 LOGIC manual, that the
> inventor
> of this idea was Robin Milner:
>
> 1. *Type variables: *these stand for arbitrary sets in the universe. In
> Church's original
>
> formulation of simple type theory, type variables are part of the
> meta-language
>
> and are used to range over object language types. Proofs containing type
> variables
>
> were understood as proof schemes (i.e. families of proofs). To support such
>
> proof schemes *within *the HOL logic, type variables have been added to the
> object
>
> language type system.2
> ...
> ________________
>
> 2This technique was invented by Robin Milner for the object logic PP of
> his
> LCF system.
>
> I am very curious about this addition. This is actually an idea of great
> and subtle power, and I think it was a really significant innovation. It
> allows for simple but powerful types such as I:'a -> a' and map:('a -> 'b)
> -> ('a list -> 'b list) which I use all the time. In fact, one wonders if
> the popularity of HOL would have been as wide without this key idea.
>
> I have several questions about this. First, what is the proper terminology
> to refer to both systems, with or without type variables? Second, how
> should credit be given for this innovation? Third, is there any more
> information about this invention by Robin Milner, ie. did he ever publish a
> paper about this. Given the surpassing practical benefit of type
> variables,
> this seems a remarkably unremarked jewel of type theory history.
>
> Peter
>
> --
> "In Your majesty ride prosperously
> because of truth, humility, and righteousness;
> and Your right hand shall teach You awesome things." (Psalm 45:4)
>
>
--
"In Your majesty ride prosperously
because of truth, humility, and righteousness;
and Your right hand shall teach You awesome things." (Psalm 45:4)
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
