Stream: Beginner Questions

Topic: Partial function as parameter

Lessness (May 25 2021 at 10:21):

Hello, i just started learning Isabelle. Is it possible to use partial function as a parameter in theorems in Isabelle?

(I want to formalise calculus book proofs to understand them better, and there functions are partial usually.)

Manuel Eberl (May 25 2021 at 11:04):

In Isabelle/HOL, not really because HOL is a logic of total functions. You can emulate partiality in various ways, e.g. by viewing a partial function from a type 'a to a type 'b as a total function 'a ⇒ 'b option. Then you can just map everything that is supposed to be undefined to None and everything else to Some y (where y is the actual value).

In practice, it is not very nice to work this way. The recommended approach is thus to simply do everything with total functions, track the information about what their domain is separately, and just ignore the behaviour of functions outside their intended domain. There are some constants and some notation to facilitate this, e.g. $f \in A\to B$ means that $f$ is a function that maps any element of $A$ to an element of $B$, and $f\in A\to_E B$ additionally requires $f$ to map anything not in $A$ to the designated undefined value. For more information about the undefined value, see Joachim Breitner's blog article. If you really do want to treat partiality explicitly, I would suggest this approach over the option one.

In our analysis formalisation in the Isabelle/HOL standard library, the problem of partiality never really arises, I think. We always just do everything with total functions, but assumptions in theorems may sometimes assume that the function is only continuous/differentiable/etc. on a certain set, e.g. continuous_on A f means that f is continuous on the set A.

You could in principle also use Isabelle/ZF. ZF (Zermelo–Fraenkel set theory) is often considered the ‘standard’ foundation for mathematics, and it does have partial functions. I cannot really say how pleasant or unpleasant it would be to do analysis with this in Isabelle/ZF, but I can say that HOL is definitely used much more in Isabelle than ZF, and certainly more developed.

Manuel Eberl (May 25 2021 at 11:32):

Personally I think if you're just starting to learn Isabelle, it's probably easier to start with Isabelle/HOL because there's more material. It may also be less frustrating to start with something like the prog-prove tutorial or the ‘Concrete Semantics’/‘Functional Data Structures’ books (which are free!) because you get a sense of achievement more easily than when formalising maths, in my opinion.

Last updated: Dec 21 2024 at 16:20 UTC