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 > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info ------------------------------------------------------------------------- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
