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

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

• Steve Vickers (University of Birmingham)
• Friday 24 February 2023, 14:00-14:50
• LG23, Computer Science // Zoom.

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”, www.cs.bham.ac.uk/~sjv/expDiff.pdf

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

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• LG23, Computer Science // Zoom
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.