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
