philzook58

module Numeric.ADLens.Interval where
import Numeric.Interval

-- interval combinators

type Lens a b = a -> (b, b -> a) 

class Lattice a where
   (/\) :: a -> a -> a
   (\/) :: a -> a -> a

philzook58

from z3 import *
def numbery_proofs(sort):
    
    x = Const("x", sort)
    y = Const("y", sort)
    z = Const("z", sort)
    print("Commutativity")
    prove(x + y == y + x) #Commutativity
    print("Associativity")
    prove(((x + y) + z) == ((x + (y + z)))) #associativity

philzook58

plus = GraphCat.block("+",   ["a","b"],   ["c"])
I = GraphCat.idd()
p1 = plus
p2 = p1 @ (p1 * p1)
p3 = p1 @ (p2 * p2)
p4 = p1 @ (p3 * p3)

d = p4.run()
d.format = "png"
d.render("adders")

philzook58

{-# LANGUAGE GADTs, NoImplicitPrelude, StandaloneDeriving, RankNTypes #-}

module NBE where

import Data.Monoid
import Control.Category
import Prelude hiding ((.), id, fst, snd)
import Control.Arrow ((&&&))
data FM a = Pure a | Mappend (FM a) (FM a) | Mempty deriving (Eq, Show)

philzook58

T = 10 # total number of time steps as a global parameter
class PetriCat():
    def compose(f,g):
        def res():
            a, b , fcon = f()
            b1, c, gcon = g()
            return a, c, fcon + gcon + [b == b1]
    def idd():
        def res()
           x = cvx.Variable((T-1,1), integer = True)

philzook58

from z3 import *

def compare_and_swap_z3(x,y):
    x1, y1 = FreshInt(), FreshInt()
    c = If(x <= y, And(x1 == x, y1 == y) , And(x1 == y, y1 == x) )
    return x1, y1, c
    
# predicates of interest
def sorted_list(x): # list is sorted
    return And([x <= y for x,y in zip(x , x[1:])])

philzook58

def controller(Cat,pend_step, pos, vel):
   acc = Cat.idd(3)
   for i in range(10):
      acc = acc @ pend_step
   init = Cat.const(pos) * Cat.const(vel) * Cat.idd(1) 
   return acc @ init

philzook58

import numpy as np
import scipy
import scipy.linalg
# https://docs.scipy.org/doc/numpy/user/basics.subclassing.html
class FinVect(np.ndarray):
    def __new__(cls, input_array, info=None):
        # Input array is an already formed ndarray instance
        # We first cast to be our class type
        
        obj = np.asarray(input_array).view(cls)

philzook58

class IntOrderCat():
    def __init__(self, dom, cod):
        assert(dom <= cod)
        self.cod = cod
        self.dom = dom
        self.f = ()
    def idd(n):
        return IntOrderCat(n,n)
    def compose(f,g):
        assert( f.dom == g.cod )

philzook58

from collections import Counter
class FinSet():
    def init(self, dom ,cod , f):
        '''  In order to specify a morphism, we need to give a python set that is the domain, a python set 
        that is the codomain, and a dictionary f that encodes a function between these two sets.
        We could by assumption just use f.keys() implicitly as the domain, however the codomain is not inferable from just f.
        In other categories that domain might not be either, so we chose to require both symmettrically.
        '''
        assert( dom == set(f.keys())) # f has value for everything in domain
        assert( all( [y in cod for y in f.value()] )) # f has only values in codomain