Hill Bill, > ... > > 0 [`!m. m < p ==> (!q. m * m = 2 * q * q ==> q = 0)`] (A) > 1 [`p * p = 2 * q * q`] (B) > > Now a mathematicians would think this means that we have chosen arbitrary > elements of the set that num denotes, and that the variables p and q will > refer to these fixed, but arbitrary, elements from now on. But I think > that's not what HOL is doing! I think HOL is just saying that the > assumptions and the goals are now written in terms of the free variables p & > q. And I guess HOL and FOL are designed this way because that's the way > math works, but I never saw that before.
Tha'ts right, a variable in HOL is just an arbitrary value of its type. If 'p' and 'q' were free variables in a given theorem, then you could use INST to come up with many different instantiations of this theorem, each giving 'p' and 'q' different values. Constants are different: they are for fixed values. This is no equivalent of INST for constants. However, type variables complicate the matter. These are for parametric polymorphism, and constants as well as variables can have type variables. INST_TYPE instantiates the type variables in constants as well as in variables. > ... > > I bet the information that p, q, and m have type num is stored somewhere. I > know we can infer the type num from the assumptions, but that's not always > true. Can you tell me where this type information is stored? Yes this information is stored somewhere, and it is actually in the term itself. What I mean is in the "internal representation" of the term (of ML datatype 'term', defined in 'fusion.ml'). Each occurrence of a variable has a name and a type. This representation is normally hidden from the user during interaction due to the term parser and pretty printer, but these can be turned off to reveal to true data structures (which are quite unreadable for large terms). Mark. ------------------------------------------------------------------------------ Try New Relic Now & We'll Send You this Cool Shirt New Relic is the only SaaS-based application performance monitoring service that delivers powerful full stack analytics. Optimize and monitor your browser, app, & servers with just a few lines of code. Try New Relic and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
