Skip to content

Instantly share code, notes, and snippets.

View Jademaster's full-sized avatar

Jade Master Jademaster

View GitHub Profile
Jademaster / Gravity.scala
Last active November 22, 2023 18:33
Simulates the three-body problem in Scala using doodle for animation and breeze for numerical integration.
import breeze.linalg._
import breeze.linalg.LU.primitive.LU_DM_Impl_Double
import doodle.core._
import doodle.java2d._
import doodle.syntax.all._
import doodle.image._
import doodle.image.syntax._
import doodle.image.syntax.all.ImageOps
import doodle.image.syntax.image.ImageOps
-- 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
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)
Jademaster /
Created September 28, 2021 16:47
Code that regards a picture as a weighted graph and finds the shortest paths which occur in a fixed number of steps.
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"