Category Archives: Tutorial

Topics that are targeted at a wider audience.

Definability and extensionality of the modulus of continuity functional

In an earlier post I talked about the modulus of continuity functional, where I stated that it cannot be defined without using some form of computational effects. It is a bit hard to find the proof of this fact so I am posting it on my blog in two parts, for Google and everyone else to find more easily. In the first part I show that there is no extensional modulus of continuity. In the second part I will show that every functional that is defined in PCF (simply-typed $\lambda$-calculus with natural numbers and recursion) is extensional.  Continue reading Definability and extensionality of the modulus of continuity functional

Running a classical proof with choice in Agda

As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together.


for giving a proof term for classical countable choice, we prove the classical infinite pigeonhole principle in Agda: every infinite boolean sequence has a constant infinite subsequence, where the existential quantification is classical (double negated).

As a corollary, we get the finite pigeonhole principle, using Friedman’s trick to make the existential quantifiers intuitionistic.

This we can run, and it runs fast enough. The point is to illustrate in Agda how we can get witnesses from classical proofs that use countable choice. The finite pigeonhole principle has a simple constructive proof, of course, and hence this is really for illustration only.

The main Agda files are

These are Agda files converted to html so that you can navigate them by clicking at words to go to their definitions. A zip file with all Agda files is available. Not much more information is available here.

The three little modules that implement the Berardi-Bezem-Coquand, Berger-Oliva and Escardo-Oliva functionals disable the termination checker, but no other module does. The type of these functionals in Agda is the J-shift principle, which generalizes the double-negation shift.

Programming with effects II: Introducing eff

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

This is a second post about the programming language eff. We covered the theory behind it in a previous post. Now we turn to the programming language itself.

Please bear in mind that eff is an academic experiment. It is not meant to take over the world. Yet. We just wanted to show that the theoretical ideas about the algebraic nature of computational effects can be put into practice. Eff has many superficial similarities with Haskell. This is no surprise because there is a precise connection between algebras and monads. The main advantage of eff over Haskell is supposed to be the ease with which computational effects can be combined.

Continue reading Programming with effects II: Introducing eff

Programming with effects I: Theory

[UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.]

I just returned from Paris where I was visiting the INRIA ?r² team. It was a great visit, everyone was very hospitable, the food was great, and the weather was nice. I spoke at their seminar where I presented a new programming language eff which is based on the idea that computational effects are algebras. The language has been designed and implemented jointly by Matija Pretnar and myself. Eff is far from being finished, but I think it is ready to be shown to the world. What follows is an extended transcript of the talk I gave in Paris. It is divided into two posts. The present one reviews the basic theory of algebras for a signature and how they are related to computational effects. The impatient readers can skip ahead to the second part, which is about the programming language.

A side remark: I have updated the blog to WordPress to 3.0 and switched to MathJax for displaying mathematics. Now I need to go through 70 old posts and convert the old ASCIIMathML notation to MathJax, as well as fix characters which got garbled during the update. Oh well, it is an investment for the future.

Continue reading Programming with effects I: Theory

Proof of negation and proof by contradiction

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

Tutorial on exact real numbers in Coq

Already a while ago 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.

Intuitionistic mathematics for physics

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 Intuitionistic mathematics for physics

Representations of uncomputable and uncountable sets

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 Representations of uncomputable and uncountable sets