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) ------------------------------------------------------------------------- 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
