Partial functions

Stream: new members

[zaa]

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

[Bryan Gin-ge Chen]

Necessary for lean, or for mathematics?

[zaa]

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]

Necessary for lean, or for mathematics?

For math.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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]

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]

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

[Mario Carneiro]

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

[zaa]

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?

[Mario Carneiro]

Right

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[zaa]

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

[zaa]

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.

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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]

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

[Kenny Lau]

unfortunately sqrt(-1) is not 37

[zaa]

And 1/0 isn't too.

[zaa]

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

[Kevin Buzzard]

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.