Mathematics and Computation

May 7, 2008

An object-oriented language Boa

Filed under: plzoo, software — Andrej Bauer @ 00:32

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.

(more…)

May 6, 2008

The Programming Languages Zoo

Filed under: plzoo, software — Andrej Bauer @ 12:43

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

February 6, 2008

Representations of uncomputable and uncountable sets

Filed under: Computation, Tutorial — Andrej Bauer @ 12:27

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.

(more…)

February 2, 2008

The hydra game

Filed under: General, Logic — Andrej Bauer @ 03:13

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

Lambda calculus for real analysis by Paul Taylor

Filed under: General, News — Andrej Bauer @ 01:28

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.

(more…)

January 31, 2008

A constructive theory of domains suitable for implementation

Filed under: Constructive math, Publications, RZ — Andrej Bauer @ 12:50

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

September 28, 2007

Seemingly impossible functional programs

Filed under: Computation, Tutorial — Martin Escardó @ 17:21

Andrej has invited me to write about certain surprising functional programs. The first program, due to Ulrich Berger (1990), performs exhaustive search over the “Cantor space” of infinite sequences of binary digits. I have included references at the end. A weak form of exhaustive search amounts to checking whether or not a total predicate holds for all elements of the Cantor space. Thus, this amounts to universal quantification over the Cantor space. Can this possibly be done algorithmically, in finite time?

(more…)

September 18, 2007

The Role of the Interval Domain in Modern Exact Real Arithmetic

Filed under: Computation, Constructive math, RZ, Talks — Andrej Bauer @ 07:39

With Iztok Kavkler.

Abstract: The interval domain was proposed by Dana Scott as a domain-theoretic model for real numbers. It is a successful theoretical idea which also inspired a number of computational models for real numbers. However, current state-of-the-art implementations of real numbers, e.g., Mueller’s iRRAM and Lambov’s RealLib, do not seem to be based on the interval domain. In fact, their authors have observed that domain-theoretic concepts such as monotonicity of functions hinder efficiency of computation.

I will review the data structures and algorithms that are used in modern implementations of exact real arithmetic. They provide important insights, but some questions remain about what theoretical models support them, and how we can show them to be correct. It turns out that the correctness is not always clear, and that the good old interval domain still has a few tricks to offer.

Download slides: domains8-slides.pdf

May 24, 2007

Synthetic Computability (MFPS XXIII Tutorial)

Filed under: Constructive math, Synthetic computability, Talks, Tutorial — Andrej Bauer @ 12:19

A tutorial presented at the Mathematical Foundations of Programming Semantics XXIII Tutorial Day.
(more…)

May 22, 2007

Metric Spaces in Synthetic Topology

Filed under: Constructive math, Talks — Andrej Bauer @ 16:09

With Davorin Lešnik.

Abstract:
We investigate the relationship between constructive theory of metric spaces and synthetic topology. Connections between these are established by requiring a relationship to exist between the intrinsic and the metric topology of a space. We propose a non-classical axiom which has several desirable consequences, e.g., that all maps between separable metric spaces are continuous in the sense of metrics, and that, up to topological equivalence, a set can be equipped with at most one metric which makes it complete and separable.

Presented at: 3rd Workshop on Formal Topology

Download slides: 3wft.pdf

Next Page »

Powered by WordPress