On 06/08/12 15:01, Bill Richter wrote: > Your type_of `MAP`;; was > plenty illuminating, that's how I figured out what polymorphism meant, with > the Scheme analogy, but I'm confused. On p 350 of > http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf it explains lower-case
> map: map : ('a -> 'b) -> 'a list -> 'b list > Are you saying this is an Ocaml function, and not something we can use in HOL > Light? You can't use it inside the logic; but you can use it in the HOL interactive loop. Recall that there are two languages here: the language of the logic (where you define cong, for example), and the implementation (or meta) language, ML. When you type type_of `MAP` you are applying an ML function, type_of, to the term `MAP`. At the ML level, type_of has type :term -> type and `MAP` has type :term. Within the logic, `MAP` has type (A -> B) -> A list -> B list. > A few pages later is MAP_EVERY : ('a -> tactic) -> 'a list -> tactic > That certainly sounds like HOL Light. That's certainly HOL Light, but it's not a function in the HOL Logic. > There is no MAP in reference.pdf. Indeed; the reference lists ML functions, not those that are defined within the logic. > This brings up a question Colin Rowat was asking earlier: if you define > various vector-related functions in HOL Light (like the maximum of a vector, > or the dot product of two vectors...), how can you check if your code is > working? Is there some cooperation between ML and HOL that I'm missing? > Obviously HOL is coded up in ML, but are you supposed to mix freely ML and > HOL code somehow? No. You check that your definition is correct by proving appropriate theorems about it. For example, HOL4 provides an EVAL function so that you can do things like > EVAL ``FACT 20``; val it = |- FACT 20 = 2432902008176640000: thm and this is the sort of thing you'd like to see. In HOL Light, you could certainly use rewriting to prove this sort of result. (Think about what EVAL's type is. It's another ML function, and it has type :term -> thm. FACT, on the other hand, is a logic function, with type :num -> num.) Michael ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info