# Posts in the year 2009

### Constructive gem: irrational to the power of irrational that is rational

- 28 December 2009
- Gems and stones, Constructive math

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 (18 comments)### Constructive gem: double exponentials

- 12 October 2009
- Gems and stones, Programming

In the last constructive gem we studied the exponential $2^\mathbb{N}$ and its isomorphic copies. This time we shall compute the *double* exponential $2^{2^\mathbb{N}}$ and even write some Haskell code.

### Constructive gem: juggling exponentials

- 09 September 2009
- Gems and stones

Constructive gems are usually not about particular results, because all constructive results can be proved classically as well, but rather about the *method* and the way of thinking. I demonstrate a constructive proof which can be reused in three different settings (set theory, topology, computability) because constructive mathematics has many different interpretations.

### Constructive stone: minima of sets of natural numbers

- 08 September 2009
- Gems and stones

I promise I will post a constructive gem soon. This constructive stone came up as a reaction to the cardinality of finite sets stone. I show that inhabited sets of natural numbers need not have minima, constructively.

→ continue reading### Constructive stone: cardinality of sets

- 08 September 2009
- Gems and stones

Cardinality of sets in constructive mathematics is not as well behaved as in classical mathematics. Cardinalities of finite sets are *not* natural numbers, and cardinalities are *not* linearly ordered.

### Constructive stone: finite sets

- 07 September 2009
- Gems and stones

Just like in real life, constructive stones are easier to find than constructive gems, so let me start the series with a stone about constructive finite sets.

Two girl one cup

→ continue reading (3 comments)

### Constructive gems and stones

- 07 September 2009
- Gems and stones

In various mathematical forums, mostly those of a logical flavor, I regularly see people asking basic questions about constructive mathematics. I also see misconceptions about constructive mathematics. I shall make a series of posts, _Constructive Gems and Stone_s, which will answer basic questions about constructive mathematics, and will hopefully help fix wrong ideas about constructive mathematics.

A constructive *gem* is something nice about constructive mathematics that makes you want to know more about it. In contrast, a constructive *stone* is a complication in constructive mathematics which does not exist in the classical counterpart.

Here we go! The first one is about finite sets.

→ continue reading### Mathematically Structured but not Necessarily Functional Programming

- 29 May 2009
- Computation, Constructive math, Programming, RZ, Talks

These are the slides and the extended abstract from my MSFP 2008 talk. Apparently, I forgot to publish them online. There is a discussion on the Agda mailing list to which the talk is somewhat relevant, so I am publishing now.

**Abstract:** Realizability is an interpretation of intuitionistic logic which subsumes the Curry-Howard interpretation of propositions as types, because it allows the realizers to use computational effects such as non-termination, store and exceptions. Therefore, we can use realizability as a framework for program development and extraction which allows any style of programming, not just the purely functional one that is supported by the Curry-Howard correspondence. In joint work with Christopher A. Stone we developed RZ, a tool which uses realizability to translate specifications written in constructive logic into interface code annotated with logical assertions. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools. In our experience, RZ is useful for specification of non-trivial theories. While the use of computational effects does improve efficiency it also makes it difficult to reason about programs and prove their correctness. We demonstrate this fact by considering non-purely functional realizers for a Brouwerian continuity principle.

**Download:** msfp2008-slides.pdf, msfp2008-abstract.pdf

### On programming language design

- 11 April 2009
- General, Programming, Tutorial

In a recent post I claimed that Python's lambda construct is broken. This attracted some angry responses by people who thought I was confused about how Python works. Luckily there were also many useful responses from which I learnt. This post is a response to comment 27, which asks me to say more about my calling certain design decisions in Python crazy.

→ continue reading (62 comments)### Python's lambda is broken!

- 09 April 2009
- General

I quite like Python for teaching. And people praise it for the `lambda`

construct which is a bit like $\lambda$-abstraction in functional languages. However, it is **broken**!

I have been writing lecture notes on computable mathematics. One of the questions that came up was whether it is possible to simulate the booleans in the simply-typed $\lambda$-calculus. This is a nice puzzle in functional programming. If you solve it, definitely let me know, although I suspect logicians did it a long time ago.

→ continue reading (8 comments)### On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos

- 23 January 2009
- Constructive math, Publications

**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

### Miniprolog

- 16 January 2009
- Programming languages

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!

→ continue reading (1 comment)