Instantly share code, notes, and snippets.

# Andrej Bauerandrejbauer

• Sort options
Last active Sep 18, 2019
View beamer-slides-with-notes.pdf Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Created Aug 14, 2019
Pictures of algebraic numbers
View algebraic.py
 #!/usr/local/bin/python3 # Compute algebraic numbers in the complex plane and draw a nice picture import numpy import sys import argparse import math import cairo import pickle
Created Dec 11, 2013
A simple program for computing the Mandelbrot set.
View mandelbrot.c
 /* This program is an adaptation of the Mandelbrot program from the Programming Rosetta Stone, see http://rosettacode.org/wiki/Mandelbrot_set Compile the program with: gcc -o mandelbrot -O4 mandelbrot.c Usage:
Last active Mar 14, 2019
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
View topology.v
 (* How do to topology in Coq if you are secretly an HOL fan. We will not use type classes or canonical structures because they count as "advanced" technology. But we will use notations. *) (* We think of subsets as propositional functions. Thus, if [A] is a type [x : A] and [U] is a subset of [A], [U x] means "[x] is an element of [U]". *) Definition P (A : Type) := A -> Prop.
Last active Jan 28, 2019
Graph theory in Coq
View Graph.v
 (** An attempt to formalize graphs. *) Require Import Arith. (** In order to avoid the intricacies of constructive mathematics, we consider finite simple graphs whose sets of vertices are natural numbers 0, 1, , ..., n-1 and the edges form a decidable relation. *) (** We shall work a lot with statements of the form
Last active Nov 26, 2018
A bijection between numbers and pairs of numbers.
View Bijection.md

## A bijection between numbers and pairs of numbers

Every once in a while I am faced with someone who denies that the rational numbers (or fractions, or pairs of integers) can be put into a bijective correspondence with natural numbers. To deal with the situation, I coded up the bijection. So now I can just say: "Really? Interesting. Please provide a pair of numbers `(i,j)` which is not enumerated by `f`, as defined in my gist." I am still waiting for a valid counter-example.

Anyhow, here is a demo of `f` and `g` at work. I am using the Python version, but a Haskell variant is included as well.

The 100-th pair is:

``````>>> f(100)
(10, 4)
``````
Last active Nov 21, 2018
Uinversal algebra in Coq
View algebra.v
 (* An initial attempt at universal algebra in Coq. Author: Andrej Bauer If someone knows of a less painful way of doing this, please let me know. We would like to define the notion of an algebra with given operations satisfying given equations. For example, a group has of three operations (unit, multiplication, inverse) and five equations (associativity, unit left, unit right, inverse left, inverse right). *)
Last active Sep 26, 2018
How to formulate and prove the statement "all functions are continuous" in an effectful functional language?

# Are all functions continuous?

## Mathematical background

Brouwer's statement "all functions are continuous" can be formulated without reference to topology as follows.

Definition: A functional `f : (N → N) → N` is continuous at `a : N → N` when there exists `m : N` such that, for all `b : N → N`, if `∀ k < m, a k = b k` then `f a = f b`.

Last active May 2, 2018
Experiments in using multicore OCaml effects to simulate dynamically created local effects.
View localization.ml
 (** * General support for creation of dynamic effects *) (** We show how to use the multicore Ocaml effects to dynamically generate local effects. Such effects are akin to the Eff resources, and they can be used to implement ML references. The code is based on "Eff directly in OCaml" by Oleg Kiselyov and KC Sivaramakrishnan (http://kcsrk.info/papers/caml-eff17.pdf). It was written by Andrej Bauer, Oleg Kiselyov, and Stephen Dolan at the Dagstuhl seminar "Algebraic Effect Handlers go Mainstream". *)
Created Apr 19, 2018
Use of effects and handlers to compute the tree representation of a functional.
View functional2tree.eff
 (** This code is compatible with Eff 5.0, see http://www.eff-lang.org *) (** We show that with algebraic effects and handlers a total functional [(int -> bool) -> bool] has a tree representation. *) (* A tree representation of a functional. *) type tree = | Answer of bool | Question of int * tree * tree
You can’t perform that action at this time.