Zulip Chat Archive

Stream: new members

Topic: Partial functions


view this post on Zulip zaa (Oct 02 2018 at 00:29):

Are there cases where partial functions are actually necessary? [Should probably make a new topic.]

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 00:43):

Necessary for lean, or for mathematics?

view this post on Zulip zaa (Oct 02 2018 at 00:44):

I can imagine that high school math (or some university math) definitely contains exercises with, for example, functions not defined for all real numbers.
"Find the domain of definition of blah-blah function, and it's range of values, etc."
"Find the solutions and don't forget about domain of definition."

Programming should have use for them too, imo (they could throws exceptions, errors or NaNs)

...

view this post on Zulip zaa (Oct 02 2018 at 00:44):

Necessary for lean, or for mathematics?

For math.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:47):

There are plenty of places where partial functions in all their guises are useful

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:48):

But there are many ways to interpret what "partial function" even means

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 00:48):

There are definitely lots of circumstances when the domain of a function is only a subset of some initial set that we are interested in; I guess you might call that a partial function, though I think most of the time people prefer just to talk about functions with different domains.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:49):

In dependent type theory, you have the ability to specify such precise domains that it is not really necessary to have a partial function in the truest sense

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:50):

Usually when I talk about a partial function in lean I mean a function with an argument that is a proof

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:50):

Every partial function is isomorphic to a total function, over the subtype

view this post on Zulip zaa (Oct 02 2018 at 00:51):

Usually when I talk about a partial function in lean I mean a function with an argument that is a proof

Like F: forall x, P x -> A?

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:51):

Right

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:53):

Actually there are two ways to losslessly totalize the function. One is to "push the argument left" to form the subtype {x // P x} -> A, and the other is to push the argument right, into the output, as X -> \Sigma p, p -> A

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:53):

also known as X -> roption A or X ->. A which is the mathlib type of partial functions

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:55):

When working in a programming context, it is often reasonable to upgrade this to X -> option A. Here the function will "tell you" if you have gone out of domain, and will return a result if not

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:55):

whereas X -> roption A will not "tell you" if you have got the domain right; you have to pass in a proof that you are allowed to call the function before you get a result

view this post on Zulip zaa (Oct 02 2018 at 00:57):

X -> option A is what people have at school. :D

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 00:57):

It looks like roption is only used in the computability stuff in mathlib, whereas option appears much more frequently.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:58):

That's mostly because we don't use partial functions that much

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:58):

Most of the time you can avoid it one way or another

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:59):

Notice that with either approach, you get a plain nondependent function. This is important for stuff like rewriting to work smoothly

view this post on Zulip Mario Carneiro (Oct 02 2018 at 00:59):

with the proof exposed version, you have a dependent function, and then rw will often fail and simp will produce huge goals

view this post on Zulip zaa (Oct 02 2018 at 01:03):

How are square root or logarithms (staying with real numbers) done in lean?

view this post on Zulip zaa (Oct 02 2018 at 01:07):

Coq has that positive := { x | x >= 0 } approach and than square root works on them, if I remember correctly.
No idea about logarithms, should check if they're even in the Standard Library. It seems they're not.

view this post on Zulip Bryan Gin-ge Chen (Oct 02 2018 at 01:08):

Here's sqrt and here's the in-progress fork with ln.

view this post on Zulip Mario Carneiro (Oct 02 2018 at 01:10):

Most mathematical functions in mathlib are totalized, meaning that rather than preserving the proof part we just do something random when it's not true

view this post on Zulip Mario Carneiro (Oct 02 2018 at 01:11):

e.g. a sqrt function might be defined to be the usual thing for nonnegative x and 0 for negative x

view this post on Zulip Kenny Lau (Oct 02 2018 at 04:54):

unfortunately sqrt(-1) is not 37

view this post on Zulip zaa (Oct 02 2018 at 06:29):

And 1/0 isn't too.

view this post on Zulip zaa (Oct 02 2018 at 06:31):

Ok, then partial functions are used only if really necessary. We should do that at school math too :D.

view this post on Zulip Kevin Buzzard (Oct 02 2018 at 07:17):

I am a mathematician and was very uncomfortable initially with the fact that sqrt(-1) was not NaN. But now I interpret it exactly as Mario says -- I have a mental note not to use the square root function on negative numbers in the statements of my theorems because I use it like a partial function even though it's total. Of course in the proofs I can do what I like. The fact that the square root function "should" only be used on non-negative integers is somehow something which a human uses for guidelines, but Lean doesn't need to be told this.


Last updated: May 16 2021 at 21:11 UTC