|
|||||
|
Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarski’s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs. Download: fixed-points.pdf I have aded to the PL Zoo a mini prolog interpreter. It really is minimalistic, as it only handles pure Horn clauses. There is no arithmetic, lists, cuts, or disjunctions. Nevertheless, it ought to be possible to write a miniml interpreter in it… If anyone does it, please send me the code! This is a short note pointing out that the recent paper on “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al. is no black magic, and that the authors are well aware of it. Unfortunately the paper appeared on Slashdot and has since generated an infinite amount of quasi-mathematical discussions. Continue reading A comment about “Mathematical undecidability and quantum randomness” by Tomasz Paterek et al. I have added two new languages to the PL Zoo. The minor addition is miniml+error, which is just MiniML with an error exception (raised by division by 0) that cannot be caught. The purpose is to demonstrate handling of fatal errors during runtime. The more interesting new animal is levy (written by Matija Pretnar and myself), an implementation of Paul Levy’s call-by-push-value language. If you only know about Haskell’s call-by-name and ML’s call-by-value, I invite you to learn about call-by-push-value. Start by reading Paul’s FAQ. I show how monads in Haskell can be used to structure infinite search algorithms, and indeed get them for free. This is a follow-up to my blog post Seemingly impossible functional programs. In the two papers Infinite sets that admit fast exhaustive search (LICS07) and Exhaustible sets in higher-type computation (LMCS08), I discussed what kinds of infinite sets admit exhaustive search in finite time, and how to systematically build such sets. Here I build them using monads, which makes the algorithms more transparent (and economic). Continue reading A Haskell monad for infinite search in finite time Lately I’ve been thinking about computational effects in general, i.e., what is the structure of the “space of all computational effects”. We know very little about this topic. I am not even sure we know what “the space of all computational effects” is. Because Haskell is very popular and in Haskell computational effects are expressed as monads, many people might think that I am talking about the space of all monads. But I am not, and in this post I show two computational effects which are not of the usual Haskell monad kind. They should present a nice programming challenge to Haskell fans. Continue reading Not all computational effects are monads Back in 2000 John Langford of the Machine Learning (Theory) blog and I wrote a backup script which I am still using today. A number of other people have found it useful so I decided to release it under an open source license. The script is easy to use under Linux. I am told it also backs up Windows with a bit of tweaking. I have added two new languages to the Programming Languages Zoo which demonstrate polymorphic type inference and type checking with subtypes. HERA is an implementation of exact real arithmetic in Haskell using the approach by Andrej Bauer and Iztok Kavkler, see these and these slides. It uses the fast multiple precision floating point library MPFR. Download source, and see documentation and examples of usage at my home page. [Note by Andrej: this is a guest post by AleÅ¡ Bizjak, a first-year student of mathematics at my department. I am very proud of the excellent work he did on his summer project.] Two versions of this talk were given at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008. Joint work with Paul Taylor. Abstract: Cauchy’s construction of reals as sequences of rational approximations is the theoretical basis for a number of implementations of exact real numbers, while Dedekind’s construction of reals as cuts has inspired fewer useful computational ideas. Nevertheless, we can see the computational content of Dedekind reals by constructing them within Abstract Stone Duality (ASD), a computationally meaningful calculus for topology. This provides the theoretical background for a novel way of computing with real numbers in the style of logic programming. Real numbers are defined in terms of (lower and upper) Dedekind cuts, while programs are expressed as statements about real numbers in the language of ASD. By adapting Newton’s method to interval arithmetic we can make the computations as efficient as those based on Cauchy reals. Slides: slides-map2008.pdf (obsolete version: slides-cca2008.pdf) |
|||||
|
|
|||||
