I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed.Per Martin-Löf. “Constructive mathematics and computer programming” (Logic, Methodology and Philosophy of Science, 1982)
But things are getting HoTTer, and now it is possible to glimpse a world where all mathematics can be regarded as constructive. Or, at least, amenable to integration with programming.
Some real numbers, such as 3.7 and π, are computable in the sense that you can write a program to get as many decimal places as you want. Computable numbers are part of constructive mathematics in a clear way. But most of the reals aren't computable. In some sense those non-computable reals don't exist. But clearly our understanding of the reals helps us think about the real line, and many other important concepts. And the way the reals are constructed and reasoned about creates a consistent mathematical context. And that combination of usefulness for human thought and logical consistency defines the boundaries of mathematics.
Infinitesimals seem even further from constructive mathematics than non-computable reals, but actually that is not true. They are certainly useful for thought and they can be used consistently (as I remember from Uni in the early 70s). So imagine adding infinitesimals to the numeric types. I'll leave the programming language details rather vague. It isn't Wombat, though it could easily be changed to be:
def differentiate T::RealLike==> (f:T=>T) T=>Option(T):
def dfdx(x:T) Option(T):
val dx = Infinitesimal.new
return Infinitesimal.to[T]((f(x+dx)-f(x))/dx)
return dfdx
We presume that arithmetic operations on our float+infinitesimal are just the symbolic calculation we would do. Sometimes (depending somewhat on the cleverness of our libraries) we will end up with a numerator that can be divided by dx, leaving something which the to[T] function will handle by eliminating the Infinitesimals in a safe way. This works easily for polynomial functions as we remember from school. When it doesn't work we return Option.none.
We can call f with parameter (x+dx) because a RealLike type with added Infinitesimals is also a (different) RealLike type.
Some real numbers, such as 3.7 and π, are computable in the sense that you can write a program to get as many decimal places as you want. Computable numbers are part of constructive mathematics in a clear way. But most of the reals aren't computable. In some sense those non-computable reals don't exist. But clearly our understanding of the reals helps us think about the real line, and many other important concepts. And the way the reals are constructed and reasoned about creates a consistent mathematical context. And that combination of usefulness for human thought and logical consistency defines the boundaries of mathematics.
Infinitesimals seem even further from constructive mathematics than non-computable reals, but actually that is not true. They are certainly useful for thought and they can be used consistently (as I remember from Uni in the early 70s). So imagine adding infinitesimals to the numeric types. I'll leave the programming language details rather vague. It isn't Wombat, though it could easily be changed to be:
def differentiate T::RealLike==> (f:T=>T) T=>Option(T):
def dfdx(x:T) Option(T):
val dx = Infinitesimal.new
return Infinitesimal.to[T]((f(x+dx)-f(x))/dx)
return dfdx
We presume that arithmetic operations on our float+infinitesimal are just the symbolic calculation we would do. Sometimes (depending somewhat on the cleverness of our libraries) we will end up with a numerator that can be divided by dx, leaving something which the to[T] function will handle by eliminating the Infinitesimals in a safe way. This works easily for polynomial functions as we remember from school. When it doesn't work we return Option.none.
We can call f with parameter (x+dx) because a RealLike type with added Infinitesimals is also a (different) RealLike type.
The example program is wrong. The parameter function needs to be defined for all RealLike, not for some RealLike. This seems more immediately important than the actual content of the post!
ReplyDelete