This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import math | |
from statistics import mean | |
from PIL import Image, ImageColor, ImageDraw | |
import sys | |
import numpy as np | |
import random | |
# Copying/cooking my own version Akiyoshi Kitaoka's amazing art (see https://www.ritsumei.ac.jp/~akitaoka/index-e.html) | |
filename='bird.png' | |
img = Image.open(filename) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import breeze.linalg._ | |
import breeze.linalg.LU.primitive.LU_DM_Impl_Double | |
import doodle.core._ | |
import doodle.java2d._ | |
import doodle.syntax.all._ | |
import cats.effect.unsafe.implicits.global | |
import doodle.image._ | |
import doodle.image.syntax._ | |
import doodle.image.syntax.all.ImageOps | |
import doodle.image.syntax.image.ImageOps |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- this file implements the Grothendieck construction and its inverse for functions i.e.\ the equivalence between functions f : X -> Set and functions \int f -> X. In the language of functional programming, this gives a reversible procedure for turning dependent types into function types. | |
-- finite sets with n elements | |
-- just a dependent type | |
import Data.Vect | |
Deptype :Type -> Type | |
Deptype x = x -> Type |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
data Mu : (pattern : Type -> Type) -> Type where | |
In : {f: Type -> Type} -> f (Mu f) -> Mu f | |
data TwoOps x a = Val x | Addunit | Mulunit | Add a a | Mul a a | |
Functor (TwoOps x) where | |
map f (Val y) = Val y | |
map f (Addunit) = Addunit | |
map f (Mulunit) = Mulunit | |
map f (Add a1 a2) = Add (f a1) (f a2) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import matplotlib.pyplot as plt | |
import numpy as np | |
import math | |
from PIL import Image | |
#this code takes a matrix M, regards it as a weighted graph where the entry M_ij indicates the weight between vertex i and vertex j. The free category on this graph is computed using the geometric series formula F(M) = Sum_{n geq 0} M^n with operations valued in the min plus semiring. The function freemetricspace(M,res) computes this formula to the first res terms. In words, this computes the shortest paths which occur in <= n steps. | |
#this function computes naive matrix multiplication in the min plus semiring | |
def mult(m1,m2): | |
assert (m1.shape[1] == m2.shape[0]), "shape mismatch" |