On 15/01/13 20:13, Bill Richter wrote: > 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, ... This is possible in HOL4, using the same “finite cartesian products” approach as in HOL Light. See p84 of the HOL4 Description manual (available at http://sourceforge.net/projects/hol/files/hol/kananaskis-8/kananaskis-8-description.pdf/download); our approach is ported from HOL Light’s. There was a paper by John Harrison at TPHOLs 2005 describing how it all works. > 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. Type inference can’t tell that the argument [1;2;3] has length 3; all it can deduce is that this is indeed a list of numbers. Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery and much more. Keep your Java skills current with LearnJavaNow - 200+ hours of step-by-step video tutorials by Java experts. SALE $49.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122612
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
