From: Tom M. <Tom...@co...> - 2008-11-18 17:34:32
|
Bart Jacobs and I had a paper a long time ago about faking dependent types in simple type theory. Tom On Tuesday 18 November 2008 01:38:40 John Harrison wrote: > | Infinite product would be dependent type, wouldn't it? HOL doesn't come > | with dependent types out of the box, and I haven't seen an add-on > | library for it. > > Indeed, it's not easy to outfit HOL with dependent types. But you can > at least have infinite product types that are not dependent, i.e. are > parametrized by a type not a term. For example, you can regard the > function space A->B as an A-ary product of B's; indeed set theorists > often write B^A instead of A->B. Using a variant of this idea, I > showed in a TPHOLs 2005 paper how to fake n-ary Cartesian product > types so you almost get a kind of dependent type. > > I interpreted the original question as being about sums and products > of numbers, not of types, though maybe I'm completely wrong. In that > case I don't know the best HOL4 answer, which is why I didn't reply > earlier. But I can give a HOL Light answer if desired. > > John. > > ------------------------------------------------------------------------- > This SF.Net email is sponsored by the Moblin Your Move Developer's > challenge Build the coolest Linux based applications with Moblin SDK & win > great prizes Grand prize is a trip for two to an Open Source event anywhere > in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ > _______________________________________________ > hol-info mailing list > hol...@li... > https://lists.sourceforge.net/lists/listinfo/hol-info |