In HOL Light vectors, there's something like type quantification, and I thought
that wasn't possible in HOL.
First, I could not find an HOL4 analogue of HOL Light vectors. The basic idea
seems to be that to define the type operator ^ which yields the type real^3
which denotes vectors in R^3, 3 must be a type, and somehow it must be a type
with exactly 3 elements, as on p 182 of the HOL Light tutorial we see
# DIMINDEX_3;
val it : thm = |- dimindex (:3) = 3
This type issue means we need the function $ of type A^B->num->A which involves
a bijection from the set of numbers from 1 to n (written 1...n in HOL Light)
and the type B if dimindex (:B) = n. Here's where I'm seeing something like
type quantification, in cart.ml:
let lambda = new_definition
`(lambda) g =
@f:A^B. !i. 1 <= i /\ i <= dimindex(:B) ==> (f$i = g i)`;;
let vector = new_definition
`(vector l):A^N = lambda i. EL (i - 1) l`;;
So the functions (lambda) and vector have types
(num->A)->A^B and
(A)list->A^B resp. Notice that type B is only on the right-hand side? Doesn't
that mean B is brought in by type quantification? I would think that meant
that vector was really defined by
`!l: (A)list. !B. (vector l):A^B = lambda i. EL (i - 1) l`
Do we get away with this "type quantification" because N is so close to a
finite set of natural numbers, which has type num->bool?
In practice this "type quantification" seems to amount to including type
annotations that I'd think weren't needed, as in the same page of the tutorial.
So type_of tells us that
vector[&1;&2;&3]: real^3
has type real^3, but
vector[&1;&2;&3]
has type real^?185046.
Surely the type should be real^3, even if we don't specifically annotate,
right? Because the list has length 3? But that's not what the definition
vector above says! It says to feed in a list l and apparently a type
annotation as well. I think that's pretty interesting, and I'd like to know
more.
--
Best,
Bill
------------------------------------------------------------------------------
Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS
and more. Get SQL Server skills now (including 2012) with LearnDevNow -
200+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only - learn more at:
http://p.sf.net/sfu/learnmore_122512
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
