University of Birmingham > Talks@bham > Theoretical computer science seminar > Fundamental Theorem of Calculus, point-free -- applications to exp and log

Fundamental Theorem of Calculus, point-free -- applications to exp and log

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George Kaye.

This is an exercise in the geometric methodology for developing point-free analysis (for a recent outline see [1]). The approach has various advantages, notably that maps are automatically continuous and that it gives an elegant treatment of the fibrewise topology of bundles; but the downside is that its lack of Π-types makes it a non-trivial effort to extract geometric content from established treatments, even constructive ones.

In Ming Ng’s thesis he gave a geometric account of real exponentiation and logarithms and their algebraic properties – see [2].

I shall prove their differentiability, via the Fundamental Theorem of Calculus. The proof illustrates a point that, once one has the right fundamental results, the further development can use methods that wouldn’t look too out of place in a classical treatment. Here the basic result, most characteristically geometric, is that certain 2-sided integrals can be constructed.

Further details in [3].

[1] Vickers “Generalized point-free spaces, pointwise”, arXiv:2206.01113

[2] Ng, Vickers “Point-free construction of real exponentiation”, Logical Methods in Computer Science, 2022.

[3] Vickers “The Fundamental Theorem of Calculus, point-free, with applications to exponentiation and logarithms”,

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.