## Stream: new members

### Topic: Partial functions

#### zaa (Oct 02 2018 at 00:29):

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

#### Bryan Gin-ge Chen (Oct 02 2018 at 00:43):

Necessary for lean, or for mathematics?

#### 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)

...

#### zaa (Oct 02 2018 at 00:44):

Necessary for lean, or for mathematics?

For math.

#### Mario Carneiro (Oct 02 2018 at 00:47):

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

#### Mario Carneiro (Oct 02 2018 at 00:48):

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

#### 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.

#### 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

#### 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

#### Mario Carneiro (Oct 02 2018 at 00:50):

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

#### 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?

Right

#### 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

#### 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

#### 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

#### 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

#### zaa (Oct 02 2018 at 00:57):

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

#### 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.

#### Mario Carneiro (Oct 02 2018 at 00:58):

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

#### Mario Carneiro (Oct 02 2018 at 00:58):

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

#### 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

#### 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

#### zaa (Oct 02 2018 at 01:03):

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

#### 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.

#### 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

#### 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

#### Kenny Lau (Oct 02 2018 at 04:54):

unfortunately sqrt(-1) is not 37

#### zaa (Oct 02 2018 at 06:29):

And 1/0 isn't too.

#### 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.

#### 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