Mathematics and Computation

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

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.

(more…)

I quite like Python for teaching. And people praise it for the lambda construct which is a bit like λ-abstraction in functional languages. However, it is broken!

(more…)

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

The simply-typed λ-calculus is a purely functional language in which we have a single base type, functions, and pairs. In this language every term normalizes, so we cannot write a non-terminating program, and it does not matter whether we evaluate eagerly or lazily. To make things more concrete, let me rephrase this as a fragment of Haskell (Ocaml or ML would do just as well). We may use only the following constructs:

1. An abstract “base” type, which is traditionally denoted by O (the letter). In Ocaml this would be a type whose implementation is hidden by a signature. I am not quite sure what it is in Haskell, but it could be a type parameter about which nothing is known. For practical purposes we may take O to be Int and make sure we do not use anything specific about Int.
2. Functions: we may form functions by λ-abstraction and apply them. Very importantly, all variables must be explicitly typed (polymorphism is forbidden). For example, it is ok to write \(x :: O) -> x but not \x -> x because that would be polymorphic. (We must include the pragma {-# LANGUAGE PatternSignatures #-} in Haskell code to allow explicitly typed variables.)
3. Pairs: we may form pairs and use the projections fst and snd. This is really just a convenience, because we can always elimitate pairs by currying.

The question is this: is there a type Boolean (constructed from the base type O using function types and product types) with values

true   :: Boolean
false  :: Boolean

and for each type t a constant

cond_t :: Boolean -> t -> t -> t

such that, for all x and y of type t:

cond_t true  x y = x
cond_t false x y = y

Notice that since polymorphism is forbidden, we have a family of constants cond_t, one for each type t, that simulate the conditional statement.

Booleans via polymorphism

If we allow polymorphic functions, the booleans may be defined thus:

type Boolean t = t -> t -> t

true, false :: Boolean t
true  x y = x
false x y = y

cond :: Boolean t -> t -> t -> t
cond  b x y = b x y

Of course, since we have polymorphism a single cond does the job.

I suspect the answer is negative and the booleans cannot be simulated.

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. (more…)

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 (LICS’07) and Exhaustible sets in higher-type computation (LMCS’08), 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). (more…)

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. (more…)