I was inspired by someone commenting they'd like more conversations about maths in here, so I just want to post about an interesting mathematical result I did not expect.
First, a bit of an introduction. You may know that the Curry-Howard correspondence links computer programs with proofs. If you've heard this and you're not very clear what it means, it means that logic and computation are intimately related. Different types of computation are isomorphic to logics, for example, natural deduction is isomorphic to lambda calculus. If you have a valid program, this program can be understood as proving some sort of theorem. Specifically, a proof is a program, and the formula that is proven is the type for the program. Likewise, if you have the prove of some theorem, this can be understood as a computation, but here comes an important proviso: classical logic uses axioms such as excluded middle that allow certain forms of proof through double negation elimination that are not computable. In these proofs you don't necessarily show how to constract an object O, but negate the negation of O. Intuitionistic logic is different and does not allow the use of excluded middle or other non-computable axioms. When you have the existential of an object, in order to satisfy the proof, you must show how to construct an object that will satisfy it.
This is interesting, but what happens with non-terminating programs? After all, we know from the halting problem that it is impossible in general to mechanically decide if a program will halt. It turns out, non-terminating programs are proofs of false, they can prove anything.
So only terminating programs give us valid proofs. But we already established we cannot tell if a program terminates or not. What a pickle. This is not strictly true though, not if we weaken our programming language so that it is no longer turing-complete. It is possible to make programming languages for which all computations must end in finite time (though not necessarily in reasonable time!). These languages forbid things like infinite loops or infinite recursion. They use techniques such as structural recursion (where a function has to always call a smaller argument, such as a fuel limit) or some kind of proof of productiveness for a computation to be legally valid. These languages are called total languages.
The really weird thing: for the longest time it was believed that total languages are too limited to be useful in terms of universal computation. Certainly, all else equal, writing code in a total language is harder and takes significantly more effort. One specific thing that was thought impossible was for a total language to interpret itself. That is, one cannot write the interpreter for a total language in that total language.
Well, it turns out one can! In a paper titled Breaking through the normalisation barrier, it was shown that this is possible. I think this result is well-known these days, but it still delights me.
https://dl.acm.org/doi/10.1145/2837614.2837623
=> More informations about this toot | View the thread | More toots from modulux@node.isonomia.net
text/geminiThis content has been proxied by September (3851b).