Since the death of my old web server my Random Art has not worked. Bringing it up to date and installing it on the new server was a nightmare in software management. But it was worth it. The new Random Art runs the random art program inside your browser!
|
|||||
|
Martín Escardó and Paulo Oliva have been working on the selection monad and related functionals. The selection monad `S(X) = (X -> R) -> X` is a cousin of the continuation monad `C(X) = (X -> R) -> R` and it has a lot of useful and surprising applications. I recommend their recent paper “What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common” which they wrote for MSFP 2010 (if you visit the workshop you get to hear Martín live). They explain things via examples written in Haskell, starting off with the innocently looking functional `ox` (which i I am writting as ox :: [(x -> r) -> x] -> ([x] -> r) -> [x] ox [] p = [] ox (e : es) p = a : ox es (p . (a:)) where a = e (\x -> p (x : ox es (p . (x:)))) It is just four lines of code, so how complicated could it be? Well, read the paper to find out. If you are ready for serious math, have a look at this paper instead. After more than 1300 days of uninterrupted service, the good old PC that served the blog started to spontaneously reboot every 4 minutes or so. It looks like a hardware failure. I moved the site to a temporary machine. I am seriously considering renting a private virtual server and just forget about buying my own hardware in the future. On top of that I discovered that evil forces planted a phishing attack on the blog about two weeks ago. The strategy was this:
So, keep your Wordpress as closed as possible. I get asked every so often to release the source code for my random art project. The original source is written in Ocaml and is not publicly available, but here is a simple example of how you can get random art going in python in 250 lines of code. Download source: randomart.py I am discovering that mathematicians cannot tell the difference between “proof by contradiction” and “proof of negation”. This is so for good reasons, but conflation of different kinds of proofs is bad mental hygiene which leads to bad teaching practice and confusion. For reference, here is a short explanation of the difference between proof of negation and proof by contradiction. Continue reading Proof of negation and proof by contradiction It was time I changed the old blog style to something a bit more modern. I hope you like it. Now I just have to figure out how to port 60 blog posts from ASCIIMathML notation to something a bit friendlier that can use MathML but does not require it. What is out there? I know about jsMath. I am open to suggestions. Already a while ago videolectures.net published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also gave a quick tutorial on Coq. With Davorin Lešnik. Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric spaces coincide if they do so for Baire space. In Russian Constructivism the match between synthetic and metric topology breaks down, as even a very simple complete totally bounded space fails to be compact, and its topology is strictly finer than the metric topology. In contrast, in Brouwer’s intuitionism synthetic and metric notions of topology and compactness agree. Download paper: csms_in_synthtop.pdf The following argument is often cited as an example of the necessity of the law of excluded middle and classical logic. We are supposed to demonstrate the existence of two irrational numbers `a` and `b` such that their power `a^b` is rational. By the law of excluded middle, `sqrt(2)^(sqrt(2))` is rational or not. If it is rational, take `a = b = sqrt(2)`, otherwise take `a = sqrt(2)^(sqrt(2))` and `b = sqrt(2)`. In either case `a^b` is rational. Let us think about this for a moment, from constructive point of view. Continue reading Constructive gem: irrational to the power of irrational that is rational In the last constructive gem we studied the exponential `2^NN` and its isomorphic copies. This time we shall compute the double exponential `2^(2^NN)` and even write some Haskell code. Continue reading Constructive gem: double exponentials |
|||||
|
|
|||||