On 31/08/12 12:39, Bill Richter wrote: > Thanks for the HOL lesson, Michael, and clarifying about theorem-proving! > Can you give me some advice on how to read your 45 page Logic manual? I need > to understand why
>> x : point [means] "x is an element of the set point" (the reading we can >> derive using the semantics) On page 17, the language "...if the term involves $m$ free variables..., then it is interpreted as a function $Y_1 \times \cdots \times Y_m \to Y$ where the sets $Y_1$,\dots,$Y_m$ are the interpretations of the types of the free variables in the term and the set $Y$ is the interpretation of the type of the term." In the case of a single variable, $m=1$ and $Y_1 = Y$ because the type of the variable is the type of the whole term. This language is saying that the interpretation of the bare variable $x$ is a function from Y to Y. The domain of this function is all the possible values that $x$ might take on, and the result is the value of the whole term. Clearly then the function in this case will be the identity. This is the story in the absence of type variables. If you further assume you are working only with closed terms where there are no free variables, the denotation will be a function from an empty vector of sets into the set denoted by the term's type (see midway through p19). In this way we see that a closed term t of type σ denotes precisely one element in the set denoted by σ. If you were dealing with closed terms only and terms with no type variables, then the semantics would be completely obvious: - type constants map to non-empty sets - type-operators like "list" map type-arguments to other types - the function operator maps two sets to the total-function-space set over the two arguments - term constants map to elements of their type (which may be a function space of course) - applications map to the result of applying the corresponding function to the corresponding argument This is the naive way of thinking about HOL that John referred to. When you deal with free variables, as you have to when giving a meaning to abstractions, things start getting more complicated, though very much "in the way you'd expect". Likewise dealing with type variables. >> And really, why do we care? > That's easy! I want a smart HOL guy like you to think about how we > can make miz3 (holby, actually) more powerful. I'm having a bad > interaction, I hazily conjecture, between the FOL that MESON is good > at and the set theory in my paper. For that, you must understand > that intentional weakness isn't a miz3 goal, for then you efforts > would be wasted. My theory would be that the problem is that MESON is bad at equational reasoning. All you need to do (easy for me to say, of course) is to occasionally use rewriting as well as MESON. 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
