Skip to content

Instantly share code, notes, and snippets.


Philip Zucker philzook58

View GitHub Profile
Classic cart-pole system implemented by Rich Sutton et al.
Copied from
Edit reset in order to change initial stae to down low
philzook58 /
Last active Aug 18, 2019
import pickle
favorite_color = { "lion": "yellow", "kitty": "red" }
import os
pickle.dump( favorite_color, open( "./logs/save.p", "wb" ) )
print("it good b")
philzook58 / optimal_relation.hs
Created Nov 26, 2019
a sketch of using linear relations for LQR control
View optimal_relation.hs
-- state of an oscillator
data SHOState = X | P deriving (Show, Enum, Bounded, Eq, Ord)
data Control = F deriving (Show, Enum, Bounded, Eq, Ord)
-- Costate newtype wrapper
newtype Co a = Co a deriving (Show, Enum, Bounded, Eq, Ord)
type M = Matrix Double
dynamics :: forall x u. (BEnum x, BEnum u) => Matrix Double -> Matrix Double ->
HLinRel (Either x u) x
philzook58 / SOS Diff Eq.ipynb
Created Dec 12, 2019
Sum of squares for differential equations
View SOS Diff Eq.ipynb
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
philzook58 / laplace.hs
Created Dec 22, 2019
Laplace equation using linear relations in hmatrix
View laplace.hs
type HLinRel2D u d l r = HLinRel (Either u l) (Either d r)
A stencil of 2d resistors for tiling
philzook58 /
Last active Dec 24, 2019
z3 verify sorting network
#direct from
def oddeven_merge(lo: int, hi: int, r: int):
step = r * 2
if step < hi - lo:
yield from oddeven_merge(lo, hi, step)
yield from oddeven_merge(lo + r, hi, step)
yield from [(i, i + r) for i in range(lo + r, hi - r, step)]
yield (lo, lo + r)
philzook58 /
Created Dec 29, 2019
simple z3py proofs
def babylonian(x):
res = 1
for i in range(7):
res = (x / res + res) / 2
return res
x, y = Reals("x y")
prove(Implies(And(y**2 == x, y >= 0, 0 <= x, x <= 10), babylonian(x) - y <= 0.01))
philzook58 /
Last active Jan 7, 2020
positive polynomial optimization + taylor model sketch idea
import cvxpy as cvx
import numpy as np
import sos
import sympy as sy
import matplotlib.pyplot as plt
#raised chebyehve
t = sy.symbols("t")
N = 5
# seems like even N becomes infeasible.
philzook58 /
Last active Jan 25, 2020
z3py relation algebra sketch
trivial = BoolVal(True)
def top1(x,y): # top is the full relation,
return trivial
def bottom1(x,y):
return BoolVal(False)
def top2(sorty):
def res(x):
y = FreshConst(sorty)
philzook58 / linrel.jl
Last active Jan 26, 2020
Sketch of linear relations in julia
View linrel.jl
#A*x = 0
using LinearAlgebra
struct HRep{T}
n :: Int64 #input size
A :: AbstractArray{T}
struct VRep{T}
n :: Int64 #input size
A :: AbstractArray{T}