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 (2 comments)

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.

→ continue reading (1 comment)

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 (14 comments)

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 (14 comments)

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.

→ continue reading

I have added two new languages to the Programming Languages Zoo which demonstrate polymorphic type inference and type checking with subtypes.

→ continue reading (1 comment)

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.]

→ continue reading

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)
Extended abstract: abstract-cca2098.pdf

→ continue reading

At MSFP 2008 in Iceland I chatted with Dan Piponi about physics and intuitionistic mathematics, and he encouraged me to write down some of the ideas. I have little, if anything, original to say, so this seems like an excellent opportunity for a blog post. So let me explain why I think intuitionistic mathematics is good for physics.

→ continue reading (37 comments)

I have added another language, called Boa, to the Programming Languages Zoo. It is an object-oriented language with the following features:

• integers and booleans as base types,
• first-class functions,
• dynamically typed,
• objects are extensible records with mutable fields,
• there are no classes, instead we can define “prototype” objects and extend them
  to create instances.

→ continue reading (2 comments)

I teach Theory of Programing Languages (page in Slovene). For the course I implemented languages which demonstrate basic concepts such as parsing, type checking, type inference, dynamic types, evaluation strategies, and compilation. My teaching assistant Iztok Kavkler contributed to the source code as well. I decided to publish the source code as a Programming Language Zoo for anyone who wants to know more about design and implementation of programming languages.

→ continue reading (1 comment)

Occasionally I hear claims that uncountable and uncomputable sets cannot be represented on computers. More generally, there are all sorts of misguided opinions about representations of data on computers, especially infinite data of mathematical nature. Here is a quick tutorial on the matter whose main point is:

It is meaningless to discuss representations of a set by a datatype without also considering operations that we want to perform on the set.

→ continue reading (11 comments)

Today I lectured about the Hydra game by Laurence Kirby and Jeff Paris (Accessible Independence Results for Peano Arithmetic, Kirby and Paris, Bull. London Math. Soc. 1982; 14: 285-293). For the occasion I implemented the game in Java. I am publishing the code for anyone who wants to play, or use it for teaching.

→ continue reading (23 comments)

Paul Taylor has published a revised version of his `lambda`-calculus for real analysis. I recommend it to anyone who is interested in real analysis, be it a computer scientist, numerical analyst, or just a “true” analyst.

The first, second, and third time I talked to Paul I could not understand a word of what he was saying, and that's not just because he is a native speaker of English English. I only began to “get it” when he visited me in Ljubljana. So I think it's perhaps worth explaining a bit what this “`lambda`-calculus for real analysis” is about.

→ continue reading (7 comments)

With Iztok Kavkler.

Abstract: We formulate a predicative, constructive theory of continuous domains whose realizability interpretation gives a practical implementation of continuous ω-chain complete posets and continuous maps between them. We apply the theory to implementation of the interval domain and exact real numbers.

Download: constructive-domains.pdf

→ continue reading