andrejbauer

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

andrejbauer

andrejbauer

Experiments involving Miquel's theorem. Joint work with Finn Klein.

andrejbauer

# 
METHOD: TABLE
ENCODE: Unicode
PROMPT: LaTeX
VERSION: 1.0
DELIMITER: ,
VALIDINPUTKEY: ^,.?!:;"'/\()[]{}<>$%&@*01234567890123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz
TERMINPUTKEY: 
BEGINCHARACTER
alpha	α

andrejbauer

{- Here is a short demonstration on how to use Agda's solvers that automatically
   prove equations. It seems quite impossible to find complete worked examples
   of how Agda solvers are used.

   Thanks go to @anormalform who helped out with these on Twitter, see
   https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

   I welcome improvements and additions to this file.

   This file works with Agda 2.6.2.2 and standard-library-1.7.1

andrejbauer

#!/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

andrejbauer

(* In Andromeda everything the user writes is "meta-level programming. *)

(* ML-level natural numbers *)
mltype rec mlnat =
  | zero
  | succ of mlnat
  end

(* We can use the meta-level numbers to define a program which computes n-fold iterations
  of f. Here we give an explicit type of iterate because the ML-type inference cannot tell

andrejbauer

open import Data.Nat
open import Data.Fin as Fin

module Primrec where

  -- The datatype of primitive recursive function
  data PR : ∀ (k : ℕ) → Set where
    pr-zero : PR 0 -- zero
    pr-succ : PR 1 -- successor
    pr-proj : ∀ {k} (i : Fin k) → PR k -- projection

andrejbauer

(* Post's theorem in computability theory states that a subset S ⊆ ℕ is
   decidable if both S and its complement ℕ \ S are semidecidable.
   Just how much classical logic is needed to prove the theorem, though?
   In this note we show that Markov's principle suffices.

   Rather than working with subsets of ℕ we work synthetically, with
   semidecidable and decidable truth values. (This is more general than
   the traditional Post's theorem.)
*)

andrejbauer

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)