Dear Cris,
Links to two different PVS papers on this topic are provided at:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html
http://lists.seas.upenn.edu/pipermail/types-list/2017/001971.html
The disadvantage of the PVS subtype implementation in my opinion is that it
creates
Type Correctness Conditions (TCCs) that have to be proved later on (if I am not
mistaken).
But expressions with type violations like 1/0 shouldn’t be expressible at all,
and this should be prevented by the syntactic means of the formal language.
Of course, R0 allows mathematical entities to have different types,
such that the number tree could have the types nat, real, and nonzero at the
same time.
(However, within an expression (well-formed formula), one has to choose one
type to be used.)
And R0 allows for the introduction of new types through new predicates.
This is part of the language:
"Whenever a theorem of the form p{oα}e{α} [without type information: pe] is
inferred,
meaning that a mathematical entity (or object, element) e of any type α has
property p
(which in set theory is expressed by e ∈ p), [...] the now provably non-empty
set p is
acknowledged as a type by attaching type τ [tau] to it".
http://www.owlofminerva.net/files/formulae.pdf, p. 11
This method of type introduction has the advantage that (unlike in HOL and Q0)
mathematical entities may have different types, and no (non-logical) axioms
have to be introduced (which in HOL express the bijection for each new type).
Best regards,
Ken
____________________________________________________
Ken Kubota
http://doi.org/10.4444/100
> Am 23.01.2018 um 03:21 schrieb Cris Perdue <c...@perdues.com>:
>
> 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
------------------------------------------------------------------------------
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
