Skip to content

Instantly share code, notes, and snippets.

Avatar

Philip Zucker philzook58

View GitHub Profile
View custom_cart.py
"""
Classic cart-pole system implemented by Rich Sutton et al.
Copied from http://incompleteideas.net/sutton/book/code/pole.c
permalink: https://perma.cc/C9ZM-652R
Edit reset in order to change initial stae to down low
"""
@philzook58
philzook58 / app.py
Last active Aug 18, 2019
test_gist
View app.py
print("Success!")
import pickle
favorite_color = { "lion": "yellow", "kitty": "red" }
import os
os.mkdir("logs")
pickle.dump( favorite_color, open( "./logs/save.p", "wb" ) )
print("it good b")
@philzook58
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
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
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
u
/
\
@philzook58
philzook58 / batcher.py
Last active Dec 24, 2019
z3 verify sorting network
View batcher.py
#direct from https://en.wikipedia.org/wiki/Batcher_odd%E2%80%93even_mergesort
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)]
else:
yield (lo, lo + r)
@philzook58
philzook58 / bab.py
Created Dec 29, 2019
simple z3py proofs
View bab.py
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
philzook58 / euler.py
Last active Jan 7, 2020
positive polynomial optimization + taylor model sketch idea
View euler.py
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
philzook58 / combinators.py
Last active Jan 25, 2020
z3py relation algebra sketch
View combinators.py
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
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}
end
struct VRep{T}
n :: Int64 #input size
A :: AbstractArray{T}
end