On Mon, Jan 22, 2018 at 4:40 PM, <michael.norr...@data61.csiro.au> wrote:
> 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.
>
Yes, and thank you for the response.
I understand that new types are based on predicates over existing types.
Operations on a new type are defined in terms of operations on the existing
type, through bijections. But of course values of the new type are not
instances of the old type. A HOL4 expression confusing them does not even
typecheck.
>
>
But I guess this doesn’t quite give you the “style” you want.
>
True. In this "predicate" style the old and new types might both be
"individual", but only members of the new type would satisfy the new
predicate and provide the defined operations. So an expression might type
check, but not have a defined meaning. As a result, I would imagine that
the type of individuals in such a logic would have some sort of null value
for the result of applying a function to an input that is not in its
domain. I presume other types would also have null values of some kind.
>
> Are you aware of the predicate sub-typing offered by PVS?
>
No, I don't believe I know anything about that. A quick search suggests to
me that it might be useful for working with various kinds of numbers that
can be considered as subsets, as I mention in my email. I am just as
concerned though with types that conceptually do not have overlapping
membership.
For what it's worth, I understand the flexibility of set theory, but for
various reasons would prefer to work in a simple higher-order logic.
-Cris
>
>
> 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
