On 12/12/17 12:08, John Harrison wrote:
> Hi Mario,
>
> | Is there some established standard as to how to represent a function
> | with a domain that may be smaller than the type? More specifically, I
> | need a representation of arbitrary products (i.e.: The "tuples" are
> | functions from an arbitrary set to the elements of the tuple) to
> | formalize theorems about product spaces in topology.
>
> Unless you actually need to encode domain and codomain in the function
> (rather than treating them as other related parameters in your theorem)
> a reasonable "cheap" alternative is to use ordinary functions that map
> to some canonical value (say ARB = @x. F) outside the domain. This at
> least gives a set of functions of the right size so you can do things
> like talk about its cardinality and about the existence of a unique
> function in the usual way. And it is at the same time a normal kind of
> HOL function and can be applied as usual etc. [...]
Thanks for your reply John.
In your experience, what is the advantage of this approach over
introducing a dedicated type for “partial” functions? Currently my
approach is to introduce a new type “('a,'b) pfun”, where the constant
“APPLY:('a,'b) pfun -> 'a -> 'b” is used for function application
(“APPLY Fn x” is displayed and can be entered as “Fn‘x”). One can
recover an ordinary HOL function with partial application. i.e.: “APPLY
Fun”. The constant “apply” is “undefined” outside the domain (the
definition is an implication of the form “x ∈ dom Fn ⇒ Fn‘x = [...]”)
but it could be modified to change it to “ARB”.
Regards.
--
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
------------------------------------------------------------------------------
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
