HOL’s core principle of type definition *is* based on predicates, inasmuch as a
new type is constructed by appealing to a non-empty predicate over an existing
type to represent the new type.
But I guess this doesn’t quite give you the “style” you want.
Are you aware of the predicate sub-typing offered by PVS?
Michael
From: Cris Perdue <c...@perdues.com>
Date: Tuesday, 23 January 2018 at 11:36
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] Inquiry: Introducing new types as predicates
Are any of you readers of this list aware of investigations or implementations
of logics that, like the HOL family of provers, are based on the simple theory
of types, but which support introduction of new types through new predicates
rather than new type constants? Presumably numbers then could be individuals,
like other individuals, with some being integers, some real, and so on.
Any references to results of existing efforts to explore the potential and/or
issues raised by such arrangements would be much appreciated.
A significant part of my own interest in this approach is related to usability
by non-specialists, and in that sense style might be more an issue than
ultimate expressive power. Ideally such a system would also support a
relatively flexible and rich system of "types", without the need to bring in
the conceptual complexity of dependent types, and their accompanying notations.
Best regards and thanks in advance,
Cris
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
