# Posts in the year 2005

### Design of Computer Algebra Systems

- 02 December 2005
- General

Computer algebra systems (CAS), such as Mathematica, are complex systems that have been evolving for a couple of decades. They are advertised as advanced mathematical tools, and users expect them to be such. They are the next-generation calculators. But they also suffer from serious design flaws.

→ continue reading (5 comments)### First Steps in Synthetic Computability Theory (Fischbachau)

- 18 September 2005
- Synthetic computability, Talks

At the EST training workshop in Fischbachau, Germany, I gave two lectures on syntehtic computability theory. This version of the talk contains material on recursive analysis which is not found in the MFPS XXI version of a similar talk.

**Abstract:**

Computability theory, which investigates computable functions and computable sets, lies at the foundation of logic and computer science. Its classical presentations usually involve a fair amount of Goedel encodings. Consequently, there have been a number of presentations of computability theory that aimed to present the subject in an abstract and conceptually pleasing way. We build on two such approaches, Hyland’s effective topos and Richman’s formulation in Bishop-style constructive mathematics, and develop basic computability theory, starting from a few simple axioms. Because we want a theory that resembles ordinary mathematics as much as possible, we never speak of Turing machines and Goedel encodings, but rather use familiar concepts from set theory and

topology.

**Download slides:** est.pdf

### Proof hacking

- 16 September 2005
- Computation, Logic, Tutorial

### Realizability as the Connection between Computable and Constructive Mathematics

- 23 August 2005
- Publications, Talks

### The Dedekind Reals in Abstract Stone Duality

- 27 July 2005
- Publications

With Paul Taylor.

**Abstract:** Abstract Stone Duality (ASD) is an approach to topology that provides an abstract and conceptually satisfying account of topological spaces. The calculus of ASD reveals the computational content of various topological notions and suggests how to compute with them. The distinguishing feature of ASD is a direct axiomatisation in terms of spaces and maps, which does not rely on an underlying set-theoretic or topos-theoretic foundation.

This paper makes the first step in real analysis within ASD, namely the construction of the real line using two-sided Dedekind cuts. Compactness and overtness of the closed interval are proved, and the arithmetic operations are defined. The ASD calculus gives programs for computing the arithmetic operations and the quantifiers that express compactness and overtness.

As the paper aims to be a self-contained introduction to ASD for those interested in constructive and computable topology and analysis, it includes a rapid survey of the ASD calculus. The foundational background to the calculus was covered in detail in earlier work.

Further topics in real analysis within ASD, such as the Intermediate Value Theorem, are presented in a separate paper by Paul Taylor which builds on this one.

To be presented at Computability and Complexity in Analysis 2005, Kyoto, Japan.

**Download:** an up-to-date version from Paul Taylor’s Abstract Stone Duality page.

### Blog as a repository for research papers

- 26 July 2005
- General, Publications

### The blog has moved to math.andrej.com

- 26 July 2005
- General

### How many is two?

- 16 May 2005
- Constructive math, Logic, Tutorial

In constructive mathematics even very small sets can be quite a bit more interesting than in classical mathematics. Since you will not believe me that sets with at most one element are very interesting, let us look at the set of truth values, which has “two” elements.

→ continue reading (18 comments)### The Law of Excluded Middle

- 13 May 2005
- Constructive math, Tutorial

### ASCIIMathML

- 12 May 2005
- General

I have found a good way to write math in web pages. ASCIIMathML is a piece of javascript that translates simple-minded Latex-like ASCII math to MathML, but only if the browser supports MathML. Since the input syntax is very simple, the expressions are quite readable in the raw form, as well.

For example, if I type

`forall x in RR exists y in CC. (1-x^2 )/sqrt(1+y^4)=1`

it is seen as `forall x in RR exists y in CC. (1-x^2 )/sqrt(1+y^4)=1`. If you are going to post to the blog, you may be interested in the ASCIIMathML syntax reference page.

To enable MathML on your computer, install mathplayer plugin

if you are using Internet Explorer. For Firefox and Mozilla, you have to install math fonts.

### First Steps in Synthetic Computability Theory (MFPS XXI)

- 08 May 2005
- Publications, Synthetic computability, Talks

**Abstract:** Computability theory, which investigates computable functions and computable sets, lies at the foundation of computer science. Its classical presentations usually involve a fair amount of Gödel encodings which sometime obscure ingenious arguments. Consequently, there have been a number of presentations of computability theory that aimed to present the subject in an abstract and conceptually pleasing way. We build on two such approaches, Hyland’s effective topos and Richman’s formulation in Bishop-style constructive mathematics, and develop basic computability theory, starting from a few simple axioms. Because we want a theory that resembles ordinary mathematics as much as possible, we never speak of Turing machines and Gödel encodings, but rather use familiar concepts from set theory and topology.

**Presented at:** Mathematical Foundations of Programming Semantics XXI, Birmingham, 2004 (invited talk).

**Download paper:** synthetic.pdf, synthetic.ps.gz

**Download slides:** synthetic-slides.pdf

### What this blog is about

- 24 April 2005
- General

I recently stumbled upon a blog on machine learning by a good friend of mine, John Langford. The blog has gathered together a community of people who discuss various topics (not limited strictly to machine learning). Naturally I wanted to have a blog, too.

I devote a lot of my time to thinking about the relationship between mathematics and computation. There are two sides of this, which can be expressed by a the slogan *“Computable mathematics and mathematics of computation”.* Computable mathematics is about how to do mathematics with computers, while mathematics of computation is about mathematics that describes properties of computation in a mathematical, abstract way.

If this is a subject that interests you, I invite you to join me.

→ continue reading (2 comments)### Specifications via Realizability (CLASE 2005)

- 09 April 2005
- Publications, RZ, Talks