Notes on Getting Started in OCaml

I know a bit of Haskell. It’s the functional programming language I have the strongest background in. OCaml is very similar to Haskell, which is why I haven’t felt a strong need to learn it. Having had to delve into it for necessity because of work I think that was an oversight. The biggest thing for me is being able to more easily read a new set of literature and see familiar things in a new light, which is very refreshing.

Getting OCaml

opam is the package manager. Follow the instructions to install it and get your environment variables setup. It’ll tell you some extra commands you have to run to do so. You use it to install packages via opam install packagename. You can also use it to switch between different ocaml compiler versions via command like opam switch 4.08.1.

Dune is a build tool. You can place a small config file called dune in your folder and it can figure out how to appropriately call the compiler. Dune is in flux, so check out the documentation. What I write here may be wrong.

Here’s an example execution. Note that even though the file is called in this example, you call build with main.exe. And exec requires the ./ for some reason. Weird.

dune init exe hello
dune exec ./main.exe
dune build main.exe

Here’s a dune file with some junk in it. You make executables with blocks. You include a list of the files without the .ml suffix require by the executable in the modules line. You list libraries needed in the libraries line.

 (name main)
 (modules ("main"))
 (libraries core z3 owl owl-plplot)

  (name lambda)
  (modules ("lambda"))
  (libraries core)

You want to also install merlin. opam install merlin. Merlin is a very slick IDE tool with autocomplete and type information. dune will setup a .merlin file for you

The ReasonML plugin is good for vscode. Search for it on the marketplace. It is the one for OCaml also. ReasonML is a syntactic facelift intended for the web btw. I don’t particularly recommend it to start. There are also emacs and vim modes if that is what you’re into.

The enhanced repl is called utop. Install it with opam install utop. Basic repl usage: Every line has to end with ;;. That’s how you get stuff to be run. Commands start with #. For example #quit;; is how you end the session. #use "";; will load a file you’ve made. Sometimes when you start you need to run #use "topfind";; which loads a package finder. You can load libraries via the require command like #require "Core";;

#help;; for more.

A Quick Look at the Language

With any new language I like to check out Learn X from Y if one is available.

Here are some shortish cheat sheets with a quick overview of syntax

More In Depth Looks

This is a phenomenal book online book built for a Cornell course:

Real World OCaml is also quite good but denser. Very useful as a reference for usage of Core and other important libraries.

The reference manual is also surprisingly readable . The first 100 or so pages are a straightforward introduction to the language. Pretty basic workshop. Could be useful getting you up and running though.

Useful libraries

Core – a standard library replacement. Becoming increasingly common It is quite a bit more confusing for a newcomer than the standard library IMO. And the way they have formatted their docs is awful.

Owl – a numerical library. Similar to Numpy in many ways. These tutorials are clutch

Bap – Binary Analysis Platform. Neato stuff

Lwt – asynchronous programming

Graphics – gives you some toy and not toy stuff. Lets you draw lines and circles and get keyboard events in a simple way.

OCamlGraph – a graph library

Jupyter Notebook – Kind of neat. I’ve got one working on binder. Check it out here.

Menhir and OCamlLex. Useful for lexer and parser generators. Check out the ocaml book for more

fmt – for pretty printing

Interesting Other Stuff (A Descent into Lazy Writing) – The discourse. Friendly people. They don’t bite. Ask questions. Awesome-Ocaml list. A huge dump of interesting libraries and resources.

An excerpt of cool stuff:

  • Coq – Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
  • Why3 – Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions.
  • Alt-Ergo – Alt-Ergo is an open-source SMT solver dedicated to the proof of mathematical formulas generated in the context of program verification. – A pretty good set of beginner advice and articles. Seems like I have a lot of accidental overlap. Would’ve been nice to find earlier – advanced functional programming course. Interesting material.

TAPL – Has implementations in OCaml of different lambda calculi. Good book too.

It is not uncommon to use a preprocessor in OCaml for some useful features. There is monad syntax, list comprehensions, deriving and more available as ppx extensions. ppx perepsorcssor. ocamlp4 5 are both preprocessors too The jane street blog. They are very prominent users of ocaml. Jane Street style guide

Oleg Kiselyov half works in Haskell, half in OCaml, so that’s cool. oleg effects without monads

Oleg metaocaml book. MetaOCaml is super cool. And the switch funtionality of opam makes it easy to install!

Oleg tagless final

Cohttp, LWT and Async ocaml graphs Mirage os. What the hell is this?

ppx_let monaidc let bindings

some of the awesome derivinig capabilites are given by ppx_jane. SExp seems to be a realy good one. It’s where generic printing is?

dune build lambda.bc.js will make a javascript file. That’s pretty cool. Uses js_of_ocaml. The js_of_ocaml docs are intimidating

Note you need to install both the js_of_ocaml-compiler AND the library js_of_ocaml and also the js_of_ocaml-ppx.

 (name jsboy)
 (libraries js_of_ocaml)
 (preprocess (pps js_of_ocaml-ppx))
open Js_of_ocaml
let _ =
  Js.export "myMathLib"
       method add x y = x +. y
       method abs x = abs_float x
       val zero = 0.

Go digging through your _build folder and you can find a completely mangled incomprehensible file jsboy.bc.js. But you can indeed import and use it like so.

var mystuff = require("./jsboy.bc.js").myMathLib;
node test.js

dune build --profile release lambda.bc.js putting it in the release profile makes an insane difference in build size. 10mb -> 100kb

There is also bucklescript for compiling to javascript. Outputs readable javascript. Old compiler fork?

Check out J.T. Paach’s snippets. Helpful


Z3 ocaml

Ocaml new monadic let syntax

#require “ppx_jane”;; in utop in order to import a thing using ppx

And argument could be made for working from a docker

Weird dsls that generate parsers and lexers. Also oddly stateful.

Took a bit of fiddling to figure out how to get dune to do.

 (name lisp)
 (modules ("lisp" "parse_lisp" "lex_lisp" "ast"))
 (preprocess (pps  ppx_jane))
 (libraries core)

  (modules lex_lisp))

 (modules parse_lisp))

Otherwise pretty straight forward encoding

expereince rport: using f omega as a teaching language

Because they aren’t hidden behind a monadic interface (for better or for worse), OCaml has a lot more of imperative feel. You could program in a subset of the language and have it not feel all that different from Java or python or something. There are for loops and while loops, objects and classes, and mutable variables if you so choose. I feel like the community is trying to shy away from these features for most purposes however, sitcking to the functional core.

However, it does let you do for loops and has an interesting community anddifferent areas of strength.

Maybe more importantly it let’s you access a new set of literature and books. Sligthly different but familiar ideas

I think Core is bewildering for a newcomer.

Rando Trash Poor Style OCaml Snippets

lex_lisp.mll : simplistic usage of ocamllex and menhir

type token = RightParen | LeftParen | Id of string

open Lexing
open Parse_lisp

exception SyntaxError of string

let next_line lexbuf =
  let pos = lexbuf.lex_curr_p in
  lexbuf.lex_curr_p <-
    { pos with pos_bol = lexbuf.lex_curr_pos;
               pos_lnum = pos.pos_lnum + 1

let white = [' ' '\t']+
let newline = '\r' | '\n' | "\r\n"
let id = ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']*

rule read =
  | white    { read lexbuf }
  | newline  { next_line lexbuf; read lexbuf }
  | '('      { LEFTPAREN }
  | ')'    { RIGHTPAREN }
  | id     {  ID( Lexing.lexeme lexbuf )  }
  | eof     {  EOF }


%token <string> ID
%token EOF

%start <Ast.tree list> prog

  | s = sexpr; p = prog              { s :: p }
  | EOF                      {[]}

sexpr : 
  | LEFTPAREN;  l = idlist; RIGHTPAREN { Ast.Node( l ) }
  | s = ID                         { Ast.Atom(s) } 

(* inefficient because right recursive 
There are thingy's in menhir to ake this better?
idlist :
  | (* empty *) { [] }
  | x = sexpr; l = idlist { x :: l  } 

(* *)

Doinking around with some graphics

open Core
(* Printf.printf "%b\n" status.keypressed *)
let loop : Graphics.status -> unit = fun _ -> Graphics.draw_circle 200 200 50;
                                              Graphics.fill_rect 400 400 50 50

                                              (* Graphics.synchronize () *)

let main () = Graphics.open_graph ""; 
              Graphics.set_window_title "My Fun Boy";
              (* Graphics.auto_synchronize true; *)
              Graphics.draw_circle 200 200 50;
              List.iter ~f:(fun i -> Graphics.fill_circle (200 + 20 * i) 200 50) [1;2;3;4];
              (* Graphics.sound 500 5000; *)
              let img = Images.load "fish.jpg" [] in 
              (* Images. *)
     "notfish.jpg" (Some Images.Jpeg) [] img;
              Graphic_image.draw_image img 0 0;
              Graphics.loop_at_exit [Graphics.Poll;Graphics.Key_pressed] loop
              let evt = Graphics.wait_next_event [Graphics.Key_pressed] in
              () *)

(* let i = create_image 640 640 *)
(** resize_window  640 640 *)


let () = main ()

A couple Advent of code 2018

open Core_kernel

(** if I want to try pulling input from the web *)
(** *)

let r = In_channel.read_lines "puzz.txt"

let main () = Printf.printf "Hey\n";
              let puzz = In_channel.read_lines "puzz.txt" |> ~f:int_of_string  in
              (* List.iter puzz ~f:(fun x -> Printf.printf "%d " x); *)
              let res = List.fold puzz ~init:0 ~f:(+) in
              Printf.printf "Sum: %d\n" res

let () = main ()
open Core_kernel

Obviously the way I'm doing it is not that efficient, nor all that clean really.

let exists23 str = let charset = String.to_list str |> Set.of_list (module Char) |> Set.to_list in
                  let counts = ~f:(fun c -> String.count str ~f:(fun y -> y = c)) charset in
                  (List.exists counts ~f:(fun i -> i = 3), List.exists counts ~f:(fun i -> i = 2)) 

let exists23 str = let charset = String.to_list str |> Set.of_list (module Char) in
                   let counts = (module Int) ~f:(fun c -> String.count str ~f:((=) c)) charset in
                   (Set.mem counts 2, Set.mem counts 3) 

let main () = Printf.printf "Hey\n";
              let puzz = In_channel.read_lines "puzz2.txt" in
              let res = ~f:exists23 puzz in
              let (c2,c3) = List.fold res ~init:(0,0) ~f:(fun (x,y) (a,b) -> (begin if a then (x + 1) else x end, begin if b then y + 1 else y end)) in
              Printf.printf "Prod: %d\n" (c2 * c3)

let () = main ()

A little Owl usage

open Core_kernel
open Owl

module Plot = Owl_plplot.Plot
let () = print_endline "Hello, World!"
let greeting name = Printf.printf "Hello, %s%i \n%!" name 7
(* let x : int = 7 *)

let () = greeting "fred"
let () = match (In_channel.input_line In_channel.stdin) with
 | None -> ()
 | Some x -> print_endline x

let () = In_channel.with_file "dune" ~f:(fun t -> 
    match In_channel.input_line t with
    | Some x -> print_endline x
    | None -> ()
type 'a mygadt = 
| Myint : int mygadt
| Mybool : bool mygadt
let kmat i j = if i = j then -2.0 
               else if abs (i - j) = 1 then 1.0 
               else 0.0

let main () = 
    Mat.print (Mat.vector 10);
    Mat.print (Mat.uniform 5 5);
    Mat.print (Mat.zeros 5 5);
    let h = Owl_plplot.Plot.create "plot_003.png" in
    Plot.set_foreground_color h 0 0 0;
    Plot.set_background_color h 255 255 255;
    Plot.set_title h "Function: f(x) = sine x / x";
    Plot.set_xlabel h "x-axis";
    Plot.set_ylabel h "y-axis";
    Plot.set_font_size h 8.;
    Plot.set_pen_size h 3.;
    (* Plot.plot_fun ~h f 1. 15.; *)
    let x = Mat.linspace 0.0 1.0 20 in
    (*let f x = Maths.sin x /. x in
    Plot.plot_fun ~h f 1. 15.; *)
    let y = (Mat.ones 1 20) in
    Mat.print (Mat.ones 1 20);
    Mat.print (Mat.ones 10 1);
    Mat.print y;
    Mat.print x;
    (* y.{0,10} <- 0.0; *)
    (* Mat.set y 10 1 0.0; *)
    Plot.plot ~h x (Mat.vector_ones 20);
    (* Owl_plplot.Plot.plot ~h x (Mat.vector_ones 20); *)
    Owl_plplot.Plot.output h;
    (* let q = Arr.create [|2;2;2|] 1.8 in *)
    let k = Mat.init_2d 10 10 kmat in 
    Mat.print k;
    Linalg.D.inv k |> Mat.print;
    Plot.plot ~h x (Mat.row (Linalg.D.inv k) 5);
    Plot.plot ~h x (Mat.row (Linalg.D.inv k) 7);
    let r = Mat.zeros 1 10 in
    Mat.set r 0 0 (-2.0);
    Mat.set r 0 1 (1.0);
    let k2 = Mat.kron k k in
    let g2 = Linalg.D.inv k2 in
    let s = Mat.row g2 10 in
    let phi = Mat.reshape s [|10;10|] in 
    Plot.plot ~h x (Mat.row  phi 7); (** not convinecd this is actually doing what I want *)

    let k' = Mat.toeplitz r in (* also works. more cryptic though *)
    Mat.print k'

let () = main ()

The Classical Coulomb Gas as a Mixed Integer Quadratic Program

The coulomb gas is a model of electrostatics where you take the discreteness of charge into account. That is what makes it hard compared to the continuous charge problem. Previously, I’ve used mixed integer programming to find lowest energy states of the ising model. This is even more obvious application of mixed integer programming to a physics model.

We ordinarily consider electric charge to be a continuum, but it isn’t. It comes in chunks of the electron charge. Historically, people didn’t even know that for quite a while. It is usually a reasonable approximation for most purposes to consider electric charge to be continuous

If you consider a network of capacitors cooled to the the level that there is not enough thermal energy to borrow to get an electron to jump, the charges on the capacitors will be observably discretized. With a sufficiently slow cooling to this state, the charges should arrange themselves into the lowest energy state.

The coulomb gas model also is of interest due to its connections to the XY model, which I’ve taken a stab at with mixed integer programming before. The coulomb gas models the energy of vortices in that model. I think the connection between the models actually requires a statistical or quantum mechanical context though, whereas we’ve been looking at the classical energy minimization.

We can formulate the classical coulomb gas problem very straightforwardly as a mixed integer quadratic program. We can easily include an externally applied field and a charge conservation constraint if we so desire within the framework.

We write this down in python using the cvxpy library, which has a built in free MIQP solver, albeit not a very good one. Commercial solvers are probably quite a bit better.

import cvxpy as cvx
import numpy as np
#grid size
N = 5
# charge variables
q = cvx.Variable( N*N ,integer=True)

# build our grid
x = np.linspace(0,1,N) 
y = np.linspace(0,1,N) 
X, Y = np.meshgrid(x,y, indexing='ij')
x1 = X.reshape(N,N,1,1)
y1 = Y.reshape(N,N,1,1)
x2 = X.reshape(1,1,N,N)
y2 = Y.reshape(1,1,N,N)
eps = 0.1 / N #regularization factor for self energy. convenience mostly
V = 1. / ((x1-x2)**2 + (y1-y2)**2 + eps**2)** ( 1 / 2)
V = V.reshape( (N*N,N*N) )

U_external = 100 * Y.flatten() # a constant electric field in the Y direction 
energy = cvx.quad_form(q,V) + U_external*q

# charge conservation constraint
prob = cvx.Problem(cvx.Minimize(energy),[cvx.sum(q)==0])
res = prob.solve(verbose=True)


#plotting junk

import matplotlib.pyplot as plt
from mpl_toolkits.mplot3d import Axes3D  
fig = plt.figure()
ax = fig.add_subplot(111, projection='3d')

ax.plot_surface(X, Y, q.value.reshape((N,N)))
A plot of charge in a constant external electric field.

The results seems reasonable. It makes sense for charge to go in the direction of the electric field. Going to the corners makes sense because then like charges are far apart. So this might be working. Who knows.

Interesting places to go with this:

Prof Vanderbei shows how you can embed an FFT to enable making statements about both the time and frequency domain while keeping the problem sparse. The low time/memory N log(N) complexity of the FFT is reflected in the spasity of the resulting linear program.

Here’s a sketch about what this might look like. Curiously, looking at the actual number of nonzeros in the problem matrices, there are way too many. I am not sure what is going on. Something is not performing as i expect in the following code

import cvxpy as cvx
import numpy as np
import scipy.fftpack # import fft, ifft
def swizzle(x,y):
    assert(x.size == y.size)
    N = x.size
    s =  np.exp(-2.j * np.pi * np.arange(N) / N)
    #ret = cvx.hstack( [x + s*y, x - s*y]) 
    return cvx.hstack( [x - s*y, x + s*y]) 

def fft(x):
    N = x.size
    #assert(2**int(log2(N)) == N) # power of 2

    if N == 1:
        return x, []
        y = cvx.reshape(x,(N//2,2))
        c = []
        even, ce = fft(y[:,0])
        c += ce
        odd, co = fft(y[:,1])
        c += co
        z = cvx.Variable(N, complex=True)
        c += [z == swizzle(even,odd)]
        return z, c

N = 256
x = cvx.Variable(N, complex=True)
z, c = fft(x)
v = np.zeros(N) #np.ones(N) #np.random.rand(N)
v[0]= 1
c += [x == v]
prob = cvx.Problem( cvx.Minimize(1), c)
res = prob.solve(verbose=True)
print(scipy.fftpack.fft(v) - z.value)

The equivalent dense DFT:

x = cvx.Variable(N, complex=True)
fred = cvx.Variable(N, complex=True)
c = [fred == np.exp(-2.j * np.pi * np.arange(N).reshape((N,1)) * np.arange(N).reshape((1,N)) / N) * x]
prob = cvx.Problem( cvx.Minimize(1), c)

It would be possible to use a frequency domain solution of the interparticle energy rather than the explicit coulomb law form. Hypothetically this might increase the sparsity of the problem.

It seems very possible to me in a similar manner to embed a fast multipole method or barnes-hut approximation within a MIQP. Introducing explicit charge summary variables for blocks would create a sparse version of the interaction matrix. So that’s fun.

Doing Basic Ass Shit in Haskell

Haskell has lots of fancy weird corners, but you want to get rippin’ and runnin’

The Haskell phrase book is a new useful thingy. Nice and terse.

This one is also quite good

I also like what FP complete is up to. Solid set of useful stuff, although a bit more emphasis towards their solutions than is common

I was fiddling with making some examples for my friends a while ago, but I think the above do a similar better job.

Highlights include:

Makin a json request

-# LANGUAGE OverloadedStrings, DeriveGeneric #-}
module JsonRequest where

import Data.Aeson
import Network.Wreq
import GHC.Generics
import Control.Lens

data ToDo  = ToDo {
    userId :: Int,
    id :: Int,
    title :: String,
    completed :: Bool
  } deriving (Generic, Show)
instance ToJSON ToDo

instance FromJSON ToDo

my_url = ""

main = do r <- get my_url
          print $ ((decode $ r ^. responseBody) :: Maybe ToDo) -- ((decode $ r ^. responseBody) :: Maybe ToDo)

Showing a plot of a sine function

module Plot where

import Graphics.Rendering.Chart.Easy
import Graphics.Rendering.Chart.Backend.Cairo -- Chart-cairo
import Graphics.Image as I -- hip

filename = "example1_big.png"

main = do 
        toFile def filename $ plot (line "a sine" [[ (x :: Double, sin x) | x <- [0, 0.1 .. 2 * pi]]])
        plotimg <- readImageRGB VU filename -- yeah,I want the plot to pop up
        displayImage plotimg
        print "Press Enter to Quit"

Doing a least squares fit of some randomly created data

module LeastSquares where

import Numeric.LinearAlgebra

n = 20
x = linspace n (-3,7::Double)
y0 = 3 * x

main = do
        noise <- randn 1 n
        let y = (flatten noise) + y0
        let sampleMatrix = (asColumn x) ||| (konst 1 (n,1))
        let sol = (sampleMatrix <\> y) 
        print $ "Best fit is y = " ++ show (sol ! 0) ++ " * x + " ++ (show (sol ! 1))

Not too complicated stuff to get you excited about Haskell:

I love Power Serious. Infinite power series using the power of laziness in something like 20 lines Using the list monad to solve SEND+MORE=MONEY puzzle. Jerzy Karczmarczuk doing automatic differentiation in Haskell before it was cool. Check out Conal Elliott's stuff after.

Very simple symbolic differentiation example. When I saw this in SICP for the first time, I crapped my pants.

data Expr = X | Plus Expr Expr | Times Expr Expr | Const Double
deriv :: Expr -> Expr
deriv X = Const 1
deriv (Const _) = Const 0
deriv (Plus x y) = Plus (deriv x) (deriv y)
deriv (Times x y) = (Times (deriv x) y) `Plus` (Times x (deriv y)) Why functional Programming Matters by John Hughes John Backus emphasizing escaping the imperative mindset in his 1978 Turing Award speech. A call to arms of functional programming Richard Bird defining sudoku solutions and then using equation reasoning to build a more efficient solver - Functional Pearls

Here's how I find useful Haskell packages:

I google. I go to hackage (if I'm in a subpage, click on "contents" in the upper right hand corner). Click on a category that seems reasonable (like "web" or something) and then sort by Downloads (DL). This at least tells me what is popular-ish. I look for tutorials if I can find them. Sometimes there is a very useful getting started snippet in the main subfile itself. Some packages are overwhelming, others aren't.

The Real World Haskell book is kind of intimidating although a lovely resource.

The wiki has a pretty rockin set of tutorials. Has some kind soul been improving it?

I forgot learn you a Haskell has a chapter on basic io

Learn more

When you're ready to sit down with Haskell more, the best intro is currently the Haskell Book

You may also be interested in this MOOC or this Data61 course

Then there is a fun infinitude of things to learn after that.


More ideas for simple examples?

This post is intentionally terse.

IO is total infective poison.

standard output io

main = do
      x <- getStrLn
      putStrLn "Hello"
      print [1,2,3]
      print (Just 19022.32)
      print x

mutation & loops. You probably don't want these. They are not idiomatic Haskell, and you may be losing out on some of the best lessons Haskell has to offer.

file IO

web requests

web serving - scotty

image processing

basic data structures

command line arguments


Parallelism and Concurrency

CAV 2019 Notes: Probably Nothin Interestin’ for You. A bit of noodling with Liquid Haskell

I went to the opening workshops of CAV 2019 in New York this year (on my own dime mind you!) after getting back from joining Ben on the long trail for a bit. The tutorials on Rosette and Liquid Haskell were really fun. Very interesting technology. Also got some good ramen and mochi pudding, so it’s all good. Big Gay Ice Cream was dece.

Day 1 workshops

Calin Belta a new book. Control of Temporal logic systems. Automata. Optimized. Partition space into abstraction. Bisimulation

Control Lyapunov Function (CLF) – guarantees you are going where you want to go

Control Barrier Function – Somehow controls regions you don’t want to go to.

Lyapunov function based trajectory optimization. You somehow have (Ames 2014) Is this it?

Differential flatness , input output linearization

Sadradiini worked there.

Temproal logic with

Rise of Temporal Logic

Linear Temporal Logic vs CTL

Fixpoint logic,

Buchi automata – visit accepting state infinite times

equivalency to first order logic

monadic logic, propositions only take 1 agrument. Decidable. Lowenheim. Quantifier elimination. Bounded Mondel property

Languages: ForSpec, SVA, LDL, PSL, Sugar

Monadic second order logic (MSO).

method of tableau


Polytopic regions. Can push forward the dynmaics around a trajectory and the polytope that you lie in. RRT/LQR polytopic tree. pick random poitn. Run.

Evauating branching heuristics

branch and prune icp. dreal.

branch and prune. Take set. Propagate constraints until none fire.

branching heuristics on variables

largest first, smearing, lookahead. Try different options see who has the most pruning. Non clear that helped that muhc

QF_NRA. dreal benchmarks. flyspeck, control, robotics, SMT-lib


commands: saolver adied programming

verify – find an input on which the assertions fail. exists x. not safe

debug – Minimal unsat core if you give an unsat query. x=42/\ safe(s,P(x))$ we know thia is unsat because of previous step

solve – exists v si.t safe(v)

synthesis – exists e forall x safe(x,P(x))

define-symbolic, assert, verify, debug, solve, sythesis

Rosette. Alloy is also connected to her. Z Method. Is related to relational logic?

Building solver aided programming tool.

symbolic compiler. reduce program all possible paths to a constraint

Cling – symbolic execution engine for llvm

implement intepreter in rosette

Symbolic virtual machine

layering of languages. DSL. library (shallow) embedding. interpreter (deep) embedding.

deep embedding for sythesis.

I can extract coq to rosette?

how does it work?

reverse and filter keeping only positive queries.

symbolic execution vs bounded model checking

symbolic checks every possible branch of the program. Cost is expoentntial


type driven state merging. Merge instances of primitiv types. (like BMC), value types structurally ()

instance Merge Int, Bool, Real — collect up SMT context

vs. Traversable f => Merge (f c) – do using Traversable

symbolic union a set of guarded values with diskoint guard.

merging union. at most one of any shape. bounded by number of possible shapes.

puts some branching in rosette and some branch (on primitives) in SMT.

symbolic propfiling. Repair the encdoing.

tools people have built.

veify radiation

strategy generation. That’s interesting. builds good rewrite rules.


certikso komodo keystone. fintie programss

IS rosette going to be useful for my work? coooooould be

Liquid Haskell

{-# LANGUAGE GADTs, DataKinds, PolyKinds #-}
{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--ple" @-}

{-@ type TRUE = {v: Bool | v = True }@-}
{-@  type NonEmpty a = {v : [a] | len v > 0}  @-}
{-@ head :: NonEmpty a -> a @-}
head (x : _) = x

{-@ measure f :: Int -> Int @-}
f x = 2 * x

{-@ true :: TRUE @-}
true = True

-- impl x y = x ==> y
-- {-@ congruence :: Int -> Int -> TRUE @-}
-- congruence x y = (x == y) ==> (f x == f y)
-- {-@ (==>) :: {x : Bool |} -> {y : Bool |} -> {z : Bool | z = x ==> y} @-}
-- x ==> y = (not x) || y

-- aws automated reaosning group
nullaway uber. 
sadowski google static anaylis
infer faecobook

give programmer early 

refinement types

why and how to use
how to implement refinement types

mostly like floyd hoare logic

types + predicates = refinement type

t := {x:b | p} erefinemed b
      x : t -> t -- refined function type
linear arithemtic

congruence axioms

emit a bunch of verification conditions (VC)
p1 => p2 => p3 ... 

SMT can tell if VC is alwasy true


{-@ type Zero = {v : Int | v == 0} @-}
{-@ zero :: Zero @-}
zero = (0 :: Int) -- why?

{-@ type NAT = {v: Int | v >= 0} @-}
{-@ nats :: [Nat]  @-}
nats = [0,1,1,1] :: [Int]



in an environemnt Gamma, t1 is a subtype of t2
x are vairables are in scope.
/\x |- {v | q} <= {v | r}

True  => 


{-@ plus :: x : Int -> y : Int -> {v : Int | v = x + y} @-}
plus :: Int -> Int -> Int
plus x y = x + y

-- measure. uninterpeteyd function called measure.
-- {-@ measure vlen :: Vector a -> Int @-}

-- {-@ at :: vec :Vector a -> {i : Nat | i < vlen vec} ->  @-}

-- {-@  size :: vec : Vector a -> {n : Nat | n == vlen vec} @-}

horn contrints infer 

Collections and Higher and order fucntions

reduce :: (a -> b -> a) -> a -> [b] -> a
type a is an invaraint that holds on initial acc and indictively on f
Huh. That is true.

-- Huh. I could prove sum formulas this way.

sum'' = vec = let is = range 0 (size vec)
              add = \tot i -> ot + at vec i

              properties of data structures

size of of a list
allow uninterpetyed functions inside refinements

{ measre length}

LISTNE a = {v : [a] | 0 < length v}

measure yields refined constructions

[] :: {v : [a] | legnth v = 0}


              Q: measure?
              Q : environment?
              Q : where is standard libraru?
              no foralls anywhere? All in decidable fragment

              p : ([a],[a]) | (fst p) + (snd p) == lenght xs
              measures fst and snd


              impossible :: {v : String | false} -> a

imperative language


/inlcude folder has prelude

basic values
{v : Int | lo <= v && v < hi }

invaraint properties of structures

encoe invraints in constructor

data OrdPair = OP {opX :: Int, opY :: Int}

{-@ data OrdPair = OP {opX :: Int, opY :: {v : Int | opX < v}@-}

class Liquid Int
class Liquid Bool
class Liquid ... Real?

{-@   @-}

Liquid Relations?
{  }

data OList 
{-@data OList a LB = Empt | :< {oHd :: {v : a | LB = v}   oTl :: OList a oHd }   @-}

{-@   {oHd :: a, oTl :: OList {v : a | oHd < v}   }@-}
data MyList a where
    Nil :: MyList a
    {-@ Cons :: v : a -> MyList {x : a | x < v} ->  MyList a @-}
    Cons :: a -> MyList a -> MyList a

test :: MyList Int
test = Cons 2 (Cons 1 Nil)


abstracting the invaraint from the data structure
parametrzie by relations

data [a]<rel :: a -> a -> Bool> where
    = []
    | (:) {hd :: }

    rel != is unique list

{\x y -> x >= y}
type level lambdas!? .... uh.... maybe.

reflecting singletons into liquid?

termination metrics

/ [length xs + len ys] -- merge sort

{-@ Half a s = }@-}

Oncey ou have temrination proofs you have proofs of correctness

Propositions as Types

Plus commutes is trivial
{n = n + n}


{-@ easyProof :: {True} @-}
easyProof = ()

-- hot damn. I mean this is in it's legerdomain. But prettttty sweet.
{-@ commute :: x : Int -> y : Int -> {x + y = y + x} @-}
commute :: Int -> Int -> ()
commute x y = ()

{-@ reflect mysum @-}
{-@ mysum :: Nat -> Nat @-}
mysum :: Int -> Int
mysum 0 = 0 -- if n <= 0 then 0 else  2 * n + (mysum (n - 1))
mysum n = 2 * n + (mysum (n - 1))

-- what is going on here? why do I need _?
{-@ mysumpf :: _ -> {mysum 0 = 0 } @-}
-- mysumpf :: Proof
mysumpf _ = let x = mysum 0 in x

{-@ mysumpf' :: {mysum 3 = 12 } @-}
-- mysumpf :: Proof
mysumpf' = ()

{-@ reflect fastsum @-}
{-@ fastsum :: Nat -> Nat @-}
fastsum :: Int -> Int
fastsum n = n * (n + 1)

type Proof = ()
{-@ pfsum :: x : Nat -> {fastsum x = mysum x} @-}
pfsum :: Int -> Proof
pfsum 0 = () -- let _ = fastsum 0 in let _ = mysum 0 in ()
pfsum n = pfsum (n-1)  

{-@ pfsum :: x : Nat -> {fastsum x = mysum x} @-}
pfsum :: Int -> Proof
pfsum 0 = () -- let _ = fastsum 0 in let _ = mysum 0 in ()
pfsum n = pfsum (n-1)  



reflect takes the prcondition of sum and dumps it as the poscondition

sum3 _ = let s0 =sum 0
             s1  = sum 1
             s2  = sum 3 -- all are going to be in scope.
z3 will connect the dots.

using proof combinatos from Proof Combinators
long chains of claculations

reflection of singletons

data SS s where
    {-@ SZero :: {v : Int | v = 0} -> SS 'Zero @-} 
    SZero :: Int -> SS 'Zero 
    {-@ SZero :: {v : Int | v = 0} -> SS 'S a @-} 
    SZero :: Int -> SS 'Zero 

    proof by induction
    sum n = n * (n + 1)/2

    2 * sum n  = n * (n + 1)

point free liquid types

(.) :: (a -> b) -> (a -> )
? Can I abstract over predicates like this?
({v:a | p} -> {s:}) -> 


cauchy schwartz


data V2 a = V2 a a 

{-@ reflect dot @-} 
dot (V2 x y) (V2 x' y') = x * x' + y * y'

{-@ reflect vplus @-}
vplus (V2 x y) (V2 x' y') = V2 (x + x') (y + y')

{-@ reflect smul @-}
smul s (V2 x' y') = V2 (s * x') (s * y')
{-@ cauchy :: x : V2 Int -> y : V2 Int -> {(dot x y) * (dot x y) <= (dot x x) * (dot y y) } @-}
cauchy :: V2 Int -> V2 Int -> Proof
cauchy x y = let q = dotpos (vplus x y) in let r = dotpos (vplus x (smul (-1 :: Int) y)) in (\_ _ -> ()) q r

-- {-@ square :: Int -> Nat @-} -- basiclly the same thing
{-@ reflect square @-}
square :: Int -> Int
square x = x * x

{-@ sqpos :: x: Int -> {square x >= 0} @-}
sqpos :: Int -> ()
sqpos x = ()

{-@ dotpos :: x: V2 Int -> {dot x x >= 0} @-}
dotpos :: V2 Int -> ()
dotpos x = ()

{-@ dotsym :: x: V2 Int -> y : V2 Int -> {dot x y = dot y x} @-}
dotsym :: V2 Int -> V2 Int ->  ()
dotsym x y = ()

{-@ vpluscomm :: x: V2 Int -> y : V2 Int -> {vplus x y = vplus y x} @-}
vpluscomm :: V2 Int -> V2 Int ->  ()
vpluscomm x y = ()

{-@ dotlin :: x: V2 Int -> y : V2 Int -> z : V2 Int -> {dot (vplus x y) z = dot x z + dot y z} @-}
dotlin :: V2 Int -> V2 Int ->  V2 Int ->  ()
dotlin x y z = ()


What else is interesting to prove?

verify stuff about ODEs?

fold [1 .. t] where t = 10

could give little spiel about how dynamical systems are like imperative programming

get some rationals.

p a b
a -> b are refined functions

I should learn how to abstract over typeclasses. Verified typeclasses?

SMT has built in rationals prob?

data Rat = Rat Int Int 

{-@ reflect rplus @-}
rplus :: Rat -> Rat -> Rat
rplus (Rat x y) (Rat x' y') = Rat (x*y' + x'*y) (y * y')

{-@ reflect rmul @-}
rmul :: Rat -> Rat -> Rat
rmul (Rat x y) (Rat x' y') = Rat (x*x') (y * y')

data Nat' = S Nat' | Z

{-@ measure nlen @-}
{-@ nlen :: Nat' -> Nat @-}
nlen :: Nat' -> Int
nlen Z = 0
nlen (S x) = 1 + (nlen x) 
-- failing?
-- crash: SMTLIB2 respSat = Error "line 31 column 169: unknown sort 'Main.SNat'"
data SNat a where
    SZ :: SNat 'Z
    SS :: SNat x -> SNat ('S x)

{-@ reflect conv @-}
{-@ conv :: x : Nat -> {v : Nat' | nlen v = x} @-}
conv :: Int -> Nat'
conv 0 = Z
conv x = S (conv (x-1))

-- It's an isomorphism

{-@ pfconv :: x : Nat -> {nlen (conv x) = x} @-}
pfconv :: Int -> Proof
pfconv 0 = ()
pfconv x = pfconv (x - 1)

{-@ pfconv' :: x : Nat' -> {conv (nlen x) = x} @-}
pfconv' :: Nat' -> Proof
pfconv' Z = ()
pfconv' (S x) = pfconv' x

{-@ reflect plus' @-}
plus' :: Nat' -> Nat' -> Nat'
plus' Z x = x
plus' (S x) y = S (plus' x y)

{-@ plusz' :: x : Nat' -> {plus' x Z = plus' Z x}  @-}
plusz' :: Nat' -> Proof
plusz' Z = ()
plusz' (S x) = plusz' x

{-@ pluscomm' :: x : Nat' -> y : Nat' -> {plus' x y = plus' y x} / [nlen x, nlen y] @-}
pluscomm' :: Nat' -> Nat' -> Proof
pluscomm' Z y = plusz' y
pluscomm' (S x) (S y) = const (pluscomm' (S x) y) $ const (pluscomm' x (S y)) $  pluscomm' x y
    -- const () $ const (plus' (S x) (S y)) $ const (plus' x (S y)) (plus' x y)
    -- const (pluscomm' (S x) y) $ const (pluscomm' x (S y)) $  pluscomm' x y
 -- flip const is proof combinator .==   
    {-let q = pluscomm' x (S y) in
                        let w = pluscomm' (S x) y in 
                        let r = pluscomm' x y in (\b n m -> ()) q w r -- ? Was this necessary? -}
pluscomm' x Z = plusz' x

-- {-@ data Iso = @-}
data Iso a b = Iso { to :: a -> b, from :: b -> a, p1 :: Proof, p2 :: Proof}


We also have type level lambdas.
refinement polymorphism

LH is somewhat like singletons in the sense there is a manual reflection step.
In singletons the manual reflection is in the Sing type
in LH it is kind of all over the place. (+) has a type. Where is it defined?

How does it know that the Haskell function + is the same as the SMT solver function?

Coq and Agda and Idris type checking is powered quite a bit by an internal unification engine
explicit annotation may lessen the burden somewhat

SMT solvers as a unification engine
structure unification vs uninterpeted functions.
f a ~ Int is not a valid Haskell constraint. Maybe with the unmatchable arrow it is?
In a funny sense, there is a difference between  Just and (+ 1). 
One being a constructor means we can match out of it
Just :: a ->> b
(+ 1) :: Int -> Int


-- test' :: (f a ~ Int) => ()
-- test' = ()

Liquid Haskell – What is?

another thing we could do is galois connections between refinements. Pos, Zero, Neg <-> Int

Liquid Haskell uses SMT solvers to resolve it’s type checking requirements.

Agda et al also work very much via unification. Unification is a broad term but it’s true.

It also has a horn clause solver for inference. Every language needs some kind of inference or you’d go insane. Also it is piggybacking on haskell

It’s not as magical as I thought? Like seeing the magicians trick. It really does understand haskell code. Like it isn’t interpretting it. When it knows facts about how (+) works, that is because the refined type was put in by hand in the prelude connecting it to SMT facts. What is imported by liquid haskell?

The typing environment is clutch. You need to realize what variables are in scope and what their types are, because that is all the SMT can use to push through type checking requirements.

Installing the stack build worked for me. It takes a while . I couldn’t get cabal install to work, because I am not l33t.

Uninterpeted functions. Unmatchability?

It wouldn’t be haskell without a bunch of compiler directives. It is somewhat difficult to find in a single cohesive place what all the syntax, and directives are from liquid haskell. Poking around it best.

  • ple
  • reflection
  • no-termination
  • higherorder – what is this? course notes some of software foundations niki vazou’s pubs. Check out refinement reflection draft work? Shows stuff about typeclasses. This is a haskell 2017 paper though intro to liquid haskell. Interesting to a see a different author’s take presentations. They are fairly similar to one another.

Liquid haskell gives us the ability to put types on stuff that wasn’t possible before.

Linearity :: f :: {a -> b | f (s ^* a) == s ^* (f a) }

Pullback. {(a,b) | f a == g b}


Many things in categoruy theory rely on the exists unique. Do we have functiona extensionality in Liquid haskell?

product : {(a,b) | f q = x, g q = y, => }

Pushing the boundaries on what liquid haskell can do sounds fun.

Equalizer. The eqaulizer seems prominents in sheaves. Pre-sheaves are basically functors. Sheaves require extra conditions. Restriction maps have to work? Open covers seem important

type Equalizer f g a b = {(e :: a , eq :: a -> b) | f (eq e) = g (eq e) }

I think both the type a and eq are special. e is like an explcit parametrization.

type Eq f g a = {e :: a | f e = g e} I think this is more in the spirit. Use f and g both as measures.

presheaf is functor. But then sheaf is functor that

(a, Eq (F a) (G a)). typelevel equalizer? All types a that F and G agree on.

Records are sheaves – Jon Sterling. Records have subtyping. This gives you a toplogy feeling thing.

What about purescript records?

{foo | a} {bar | a} -> intersection = {foo bar | b} can inhabit either

union is
or do you want closed records? union is union of fields. intersection is intersection of fields.

In this case a cover would be a set of records with possibly overlapping fields whose combined labels cover the whle space we want to talk about. consistency condition of sheaf/equalizer is that overlapping records fields have to match. I guess { = } ?There is a way to combine all the stuff up. This is exactly what Ghrist was getting at with tables. Tables with shared columns.

data R1 = R1 {foo :: Int, bar :: Int}

{ (r1 :: R1, r2 :: R2) | (foo r1) = (foo r2) } — we manitain duplicates across records.

{. }

if you have a “cover” {foo bar |} {bar fred} {gary larry} whose in

Sheaves. As a model of concurrency? Gaguen paper.

sheaves as constraint satisfcation? sheafifcation. Constraint solving as a way of fusing the local constraints to be globally consistent.

sheaves as records

sheaves as data fusion

Escardo. Compact data types are those finitely searchable

Continuous funcitons are ~computable? Productive?

typed recursion theory toplogy

typed computatabiltity theory

Topological notions in computation. Dictionary of terms realted decidable, searchable, semi decidablee

Through NDArray overloading, a significant fragment of numpy code is probably verifiable.

Start with functional arithmetic programs.

Need to inspect function annotations to know how to build input type.

@verify() tag

Use (Writer a) style monad.

If statements are branching. We are again approaching inspecting functions via probing. But what if we lazily probe. At every __bool__ point, we run a z3 program to determine if there is an avaiable bool left possible (we don’t need to inspect dead code regions. Also would be cool to mention it is a dead region). Curious. We’re reflecting via Z3.

Loops present a problem. Fixed loops are fine. but what about loops that depend on the execution? for i in range(n). I guess again we can hack it…? Maybe. range only takes an integer. we don’t have overload access.

Maybe we need to go into a full eval loop. utterly deconstructing the function and evaluating it statelemnt by statement.

(compare :: a -> a -> Comparison). We could select a choice based on if there is a new one avaialable. Requires access to external store. We lose the thread. How can we know a choice was made? How can we know what the choice was? Did it ask var1 or var2? We can probably do it in python via access to a global store. But in haskell?

while loops take invariant annotations.

It would be cool to have a program that takes

pre conditions. Post ocnditions, but then also a Parameter keyword to declare const variables as deriveable. exists parameter. forall x precondition x => post condition.

Parameter could be of a type to take a dsl of reasonable computations. Perhaps with complexity predicates. and then interpretting the parameter defines the computation.

Or simpler case is parameter is an integer. a magic number.

@pre(lambda x: None)
@post(lambda r: r >= 0)
def square(x):
	return x**2

@verify(pre, post) # Easier. because now we can also verify the individual function. Call Z3 at function definition time.
def pre(f,cond):
   return fnew
   def fnew(x):
	   		if(x == VerificationEnv):
	   			newenv = x.copy
	            newVar = Z3.variable()
	            newenv.add(newVar == f(x.var))

	        	return f(x)

def post(f, cond):
   def fnew(x):
    if x == VerifcationEnv:
        Z3.findmodel(not cond(x.var), x.env)
        if can't find one:
           we're good.
           return x
           assert(False, model, function name, function postcondition code.)

#overloading assignment. isn't a problem.
class VerifyArray():
   #numpy Z3 shim.

#termination requires measure decreasing at every recursive call.
#arbaitrary loops? How to deal with those?
#maybe a hierarchy of envs to make it easier on z3. Like it doesn't need to give the whole program history if the local use is good enough.

class VerificationEnv():
    self.var = []
    self.pre = [] = []

Dump of Nonlinear Algebra / Algebraic geometry Notes. Good Links Though

Old notes on nonlinear algebra. I dunno about the content but some very good links and book suggestions in here, so I’m gonna dump this one out there. Maybe it’ll help someone.

Systems of multivariable polynomial equations are more solvable than people realize. There are algebraic and numeric methods. Look at Macaulay, Singular, Sympy for algebraic methods. phcpack and bertini  and homotopycontinuation.jl for numerical .

Algebraic methods are fixated on Groebner bases, which are a special equvialent form your set of equations can be manipulated to. You can disentangle the variables using repeated polynomial division (buchberger’s algorithm) turning your set of equations into an equivalent set that has one more variable per equation. This is like gaussian elimination which is actually the extremely simple version of buchberger for linear equations.

The numerical methods use perturbation theory to take a system of equations you know how to solve and smoothly perturb them to a new system. Each small perturbation only moves the roots a little bit, which you can track with a differential equation solver. Then you can fix it up with some Newton steps. People who really care about this stuff make sure that there are no pathological cases and worry about roots merging or going off to infinity and other things.

You need to know how many roots to build and track in your solvable system. For that two theorems are important

bezout thereom – for dense systems, number of solutions is bound by product of total degree of equations.

bernstein bound – newton polytope gives bound of number of solutions of polynomial system. useful for sparse

One could make an argument for the homotopy continuation methods being the analog of iterative solutions for linear equations if grobner basis are gaussian elimibnation. Take equation we know how to solve (~preconditioner) and perform some iterative thing on it.

add enough random linear equations to make system full (points).

Then you have a membership algorithm due to sweeping of planes. Once you have points on actual varieites, pairwise compare them.

Cox OShea book is often reccomended. It’s really good.

More advanced Cox et al book

Bernd Sturmfels,  Mateusz Michalek (including video lectures)

(Bernd is da man!)

Maculay 2 book

Singular books

Planning Algorithms, in particular chapter 6

Gröbner bases in Haskell: Part I

Summer school on tensor methods

Extensions of

Numerical Polynomial Algebra by Hans Stetter

Introduction to Non-Linear Algebra V. Dolotin and A. Morozov. A high energy physics perspective

Click to access 0609022.pdf

Nonlinear algebra can also be approach via linear algebra surprisingly. Resultants. As soon as you see any nonlinearity, the linear part of your brain shuts down, but a good question is linear in WHAT? Consider least squares fitting, which works via linear algebra. Even though you’re fitting nonlinear functions, the expressions are linear in the parameters/coefficients so you’re all good.

Similarly you can encode root finding into a linear algebra problem. A matrix has the same eigenvalues as it’s characterstic polynomial det(A - \lambda) has roots, so that already shows that it is plausible to go from linear algebra to a polynomial root finding problem. But also you can encode multiplying a polynomial by x has a linear operation on the coefficients. In this way we can .

[1 x x^2 x^3 …] dot [a0 a1 a2 a3 …] = p(x)

Multiplying by x is the shift matrix. However, we also are assuming p(x)=0 which gives use the ability to truncate the matrix. x * [1 x x^2 x^3 …]  = Shift @ xbar. This is somewhat similar to how it feels to do finite differnce equations. The finite difference matrix is rectangular, but then boundary conditions give you an extra row. Multiplication by x returns the same polynomial back only when p(x)=0 or x = 0. The eigenvalues of this x matrix will be the value of x at these poisitions (the roots). This is the companion matrix

We can truncate the space by using the zero equation.

It’s a pretty funky construction, I’ll admit.

To take it up to multivariable, we bring in a larger space [1 x y x^2 xy y^2 …] = xbar kron ybar

We now need two equations to reduce it to points. The X matrix is lifted to X kron I. and we can pad it with ?

Multiplying by an entire polynomial. Sylvester matrix for shared roots. Double root testing.

Sylvester matrix is based on something similar to bezout’s identity. To find out if some things p q has common factors you can find 2 things r s such that r*p + q*s = 0’s_identity_and_extended_GCD_algorithm

Sum of Squares is somewhat related material on systems of polynomial inequalities which can be translated to semidefinite matrix constraints. If you want to include equalities, you can use groebner bases to presolve them out.

Parrilo course material on Sum of Squares.

Paper on using greobner and CAD (cylindrical algebraic decomposition) for opitmization and control

Using groebner basis for constraint satisfaction problems: x^n=1 gives a root of unity. There are n solutions. This gives a finite set to work with. Then you can add more equations. This is related to the max-cut thing. I saw this on Cox webpage.
You can require neighbors to have different vertices by  0=(xi^k – xj^k)/(xi – xj). You can encode many constraints using clever algebra.
an example using the same technique to solve sudoku
Sympy tutorial solving geoemtric theorems and map coloring
explicitly mentions toric groebner as integer programming.

other interesting exmaples

Noncommutative grobner basis have application to solving differential equations? The differential operators are noncommutative. Not just silly quantum stuff. I mean the simple exmaple of non commutativty are the shcordinger momentum operators.

Automatic loop invariant finding

Geometric theorem rpvong

robotic kinematics

Optics? Envelopes, exchange of coordinates. Legendre transformations. Thermodynamics?

Global optimization? Find all local minima.

Nonlinear finite step.

Dynamic Prgramming. Add implicit V variab le for the vlaue function. Constrain via equations of modtion. Perform extermization keeping x0 v0 fixed. dx0=0 dv0=0 and dV=0. Grobner with ordering that removes x1 v1 V1. Iterate. Can keep dt as variable. Power series in t? Other integration schemes.

Probably need some method to simplify that left over relations so that they don’t get too complex. Smoothing? Dropping terms? Minimization may require factoring to find global minimum.

Differentiation. Add to every variable a dx. Collect up first order as a seperate set of constraints. Add conditions df=0 and dy=0 for fixed variables to perform partial differentiation and extremization. A very similar feel to automatic differentiation. Functions tend to not be functions, just other wriables related by constraints

Variable ordering

lex – good for elimination

deglex – total degree then a lex to tie break

grevlex – total degree + reverse lexicographic. The cheapest variable is so cheap that it goes last

block ordering, seperate variables into blocks and pick orderings inside blocks

general matrix ordering. Apply a matrix to the exponent vectors and lex comparse the results. Others are a subset.

Can’t I have a don’t care/ partial order? would be nice for blockwise elimination I feel like.



CAD book

Rings have addition and multiplication but not division necessarily. Polynomials, integers, aren’t guarenteed to have inverses that remain polynomials or integers.

ideal = a subset of a ring that absorbs multiplication. Also closed under addition

All polynomial conseqeunces of a system of equations

HIlbert Basis theorem – all ideals are egenrated by a finite set

ideal generated from set – any element of ring that can be generated via addition and multiplication by arbitary element. Is ideal because if you multiplied it by another object, it is still and sum of multiples.

Ideals are sometimes kind of a way of talking about factors without touching factors. Once something is a multiple of 5, no matter what you multiply it with, it is still a multiple of 5. If (x – 7) is a factor of a polynomial, then no matter what you multiply it with, (x-7) is still a factor. Zeros are preserved.

Principal ideal domain – every ideal is generated by a single object

Prime ideal. if a*b is in ideal then either a or b is in ideal. Comes from prime numbers ideal (all number divislable by prime number). If ab has a factor of p then either a or b had a factor of p. whereas consider all mutiples of 4. if a = b =2 then ab is a mutiple of 4, but neither a nor b are a multiple of 4.

1d polynomials. Everything is easy.

Polynomial division is doable. You go power by power. Then you may have a remained left over. It’s pretty weird.

You can perform the gcd of two polynomials using euclidean algorithm.

The ideal generated by a couple of them is generated by the multipolynomial gcd?

a = cx + dy + r

multivariate division: we can do the analog of polynomial division in the multivariate case. But we need an ordering of terms. reaminder is not unique.

But for certain sets of polynomials, remainder is unique.

Why the fixation on leading monomials?

The S-polynomial is the analog of one step of the euclidean algorithm. It also has the flavor of a wronskian or an anticommutator.

The bag euclidean algorithm. Grab the two things (biggest?). Take remainder between them, add remainder into bag.

This is the shape of the buchberger algorithm.

Finding homology or cohomology of solutions. Good question. One can see how this could lead to categorical nonsense since Category theory was invented for topological questions.

The variety is where a set of polynomials is 0. Roots and zero surfaces

List gives set of polynomials.

[forall a. Field a => (a,a,a) -> a ]

Or explicit

union and intersection can be achieved via multiplication and combining the sets

Krull dimension – Definition of dimension of algebraic variety. Maximal length of inclusion chain of prime ideals.

Ideals and Varieites have a relation that isn’t quite trivial.

The ideal of a variety

Envelopes – parametrized set of varieties f(x,t)=0 and partial_t f(x,t)=0. Eliminate t basically to draw the thing. Or trace out t?

Wu’s method for geometric theorem proving. You don’t need the full power of a grobner basis.

Polynomial maps. Talk about in similar language to differential geometry.

Boxes are a simple way to talk about subsets. Or lines, planes. Or polytopes.

Also any function that gives a true false value. But this is very limited in what you can actually do.

Varieties give us a concrete way to talk about subsets. Grothendieck schemes give unified languages supposedly using categorical concepts. Sounds like a good fit for Haskell.

class Variety

use powser. Functor composition makes multivariable polynomials. Tuples or V3 with elementwise multiplication

-- give variables names
newtype X a = X [a]

newtype Y a = Y [a]

-- from k^n -> k^m
type family PolyFun n m k where
   PolyFun n (S m) k = (PolyFun n 1, PolyFun n m)
   PolyFun (S n) 1 k = [PolyFun n 1 k] 
   PolyFun 1 1 k = k
-- Gonna need to Make a typeclass to actually do this. Yikes
-- it's just not as simple as Cat a b type. You really need to do computation
-- and input a is not same as 
class PolyF f where
   pcompose :: PolyFun b c k -> PolyFun a b k -> PolyFun a b k
   pid :: Num k => PolyFun b c k

-- related to ideal of n generators on a space k^m
-- this functions will compose some incoming 
-- or is this better thought of as a variety?
type Idealish :: (PolyFun n 1) -> PolyFun m 1
makeidealish :: PolyFun m n -> Ideal
makeidealish f = flip pcompose f

-- apply turns polynomial into haskell function
apply :: (PolyFun n m) -> V n -> V m

-- somehow should be able to replace points with varieties. It's like a whole thing
type VarietyFun = (PolyFun n 1 k) -> (PolyFun m 1 k)
(PolyFun n 1 k -> PolyFun m 1 k) -> (PolyFun m 1 k -> PolyFun l)

The polynomial as a type parameter for agda. Regular Functions are functions from one variety to another. They are the same as the polynomial ring quotiented out by the ideal of the variety.

Ring Space and Geometric Space (affine space)

Maximal ideals can be thought of as points. (ideal of x-a, y-b, …).

Free Polynomials ~ Free Num. Sparse representation. Uses Ordering of a. We should not assume that the are a power like in

Ord is monomial ordering. Think of a as [X,Y,X,X,X]

divmod :: (Integral a, Ord a) => Poly r a -> Poly r a -> Poly r a

newtype Monomial a = Monomial [a]

— different monomial newtype orderings for lex, etc.

Monomial (Either X Y)

divmod as bs = remove bs from as. if can’t remainder = as, div = 0

Intuition pumps : algebraic geometry, differential geoemtry, ctaegory theory, haskell agda.

In differential geometry, embedding sucks. We get around it by defining an atlas and differential maps.

There is a currying notion for polynomials. We can consider a polynomial as having coefficinets which themselves are polynomials in other variables or all at once.

What can be solved linearly? The Nullstullensatz certificate can be solved using linear equations

Resultants. What are they? Linear sums of monomials powers * the orginal polynomials. Det = 0 implies that we can find a polynomial combination

What is the deal with resultants

Toric Varieties. C with hole in it is C*. This is the torus because it is kind of like a circle. (Homologically?). There is some kind of integer lattice lurking and polytopes. Gives discrete combinatorial flavor to questions somehow. Apparently one of the more concrete/constructive arenas to work in.

binomaial ideals. the variety will be given by binomials

maps from one space to another which are monomial. can be implicitized into a variety. map is described by integer matrix. Integer programming?

Similar “cones” have been discussed in teh tropical setting is this related?

Algebraic statistics. Factor graph models. Probablisitc graphical models. Maybe tihs is why a PGM lady co taught that couse with Parillo


Tropical geometry

Loits of really intriguing sounding applications. Real time verification


How does the polynomial based optimization of the EDA course relate to this stuff?

Mixed volume methods? Polytopes.

cdd and other polytopic stuff. Integration of polynomials over polytopes

Software of interest



Singular – Plural non-commutative?

FGb – Faugiere’s implmentation of Grobner basis algorithms



tensorlab –


PolyBori – polynomials over boolean rings




polymake – slick Calabi Yau Palp????


frobby – can get euler charactersitics of monomial ideals?


Homotopy continuation:


phcpy and phcpack





bezout thereom – for dense systems, number of solutions is bound by product of total degree of equations.

bernstein bound – newton polytope gives bound of number of solutions of polynomial system. useful for sparse

One could make an argument for the homotopy continuation methods being the analog of iterative solutions for linear equations if grobner basis are gaussian elimibnation. Take equation we know how to solve (~preconditioner) and perform some iterative thing on it.

add enough random linear equations to make system full (points).

Then you have a membership algorithm due to sweeping of planes. Once you have points on actual varieites, pairwise compare them.

Suggestion that “linear program” form helps auto differentiation?

local rings. thickening? Infinite power series modded out by local relation. One maximal ideal.

differential geometry on algebaric surfaces.

modules are like vector spaces.

Ring linear

Canonical example, a vector of polynomials.

1-d space of polynomials.

Module morphism – respects linearity with sresepct to scalar multiplacation and addition Can be specified compoent wise. But has to be specified in such a way that resepct.

Basis – Linearly Independent set that spans the whole module. May not exist.

So were are kind of stuck always working in overcomplete basis to make thje vector space analogy. The generators have non trivial relations that equal zero. These coefficients form their own vector space. The space whole image is zero because of the relations is called the first syzygy module.

But then do we have a complete basis of all the relations? Or is it over complete?

If you ignore that the entries of a vectors are polynomials it becomes vector space. But but because they are they have secret relations.

even 1 dimensional vector space has some funky structure because of the polynomial nautre of the ring.

Somehow fields save us?

Paramaetrized vector curves, surfaces.

Parametrzied matrices.

Noncommutative polynomials. We could perhaps consider the process of normal ordering something related to a grobner basis calcaultion. Perhaps a multi polynomial division process? Consider the ordering where dagger is greaer than no dagger. Canonical basis also has i<j (more important for fermion).

SOS gives you the exact minimum of 1-d polynomial. You could also imagine encoding this as a semidefintier program. H-lam>=0. Min lam. Where H is the characterstic matrix.

We can diagonalize to the sos form, and then take each individual term = 0 to solve for x*.

While integer programming does that funky toric variety stuff with the objective vector deswcribing the grobner basis, binary programming is simple. x^2=x + linear eequations and constraints

haskell grobener

1. Monomials. Exponent vectors. Logarithmic representation. Mutiplication is addition. Composition is elementwise multiplication. Type level tag for ordering.

newtype Mon3 ord = V3 Int

data Lex

data DegLex

Ordering of monomials is important. Map is perfect

Map (Mon3 ord) ring

Groebner bases can be used to describe many familiar operations. Linear algerba, gaussian elminiation. Using commutators. Building power series assuming terms are relatively irrelevant.

Can I get a power series solution for x^2 + ax + 1=0 by using a negative ordering for a? I need another equation. x = \sum c_n * a^n. (x+dx)? How do I get both solutions?

Dual numbers for differential equations. dx is in a ring such that dx^n = 0.

Subset sum. Find some of subset of numebrs that add up to 0.

s um variables s_i

Solutions obey

s_0 = 0

(s_i – s_{i-1})(s_i – s_{i-1}-a_{i-1})=0

s_N = 0

Factors give OR clauses. Sepearte oplynomials give AND clauses. pseudo CNF form. Can’t always write polys as factors though? This pattern also matches the graph coloring.

More interesting books:

Some fun with algebraic numbers

Polynomial Factorization

Numerical vs Symbolic


Pick a random point. Then apply Newton’s method. Do this over and over. If you find N unique factors, you’ve done it. A little unsatisfying, right? No guarantee you’re going to find the roots.

2. Perturbation theory / Holonomy continuation. Start with a polynomial with the same number of total roots that you know how to factor. x^N – 1 = 0 seems like an easy choice. Given f(x)+\lambda g(x)=0, \partial g dx \lambda + \partial f dx  +g(x){d\lambda}= 0 . \frac{dx}{d\lambda} = \frac{-g(x)}{\lambda \partial g + \partial f}. You can use this ODE to track the roots. At every step use Newton’s method to cleanup the result. Problems can still arise. Do roots collapse? Do they smack into each other? Do they run off to infinity?

3. The Companion matrix. You can convert finding the roots into an eigenvalue problem. The determinant of a (A – \lambda) is a polynomial with roots at the eigenvalues. So we need tyo construct a matrix whose deteerminant equals the one we want.  The companion matrix simulates multiplication by x. That is what the 1 above the diagonal do. Then the final row replaces x^(N+1) with the polynomial. In wikipedia, this matrix is written as the transpose.

4. Stetter Numerical Polynomial Algebra. We can form representations basically of the Quotient Rings of an Ideal.  We can make matrices A(j) that implement multiplication by monomials x^j in F[x]/I. Then we can take joint eigensolutions to diagonalize these multiplications. Something something lagrange polynomials. Then if the solutions respect some kind of symmettry, it makes sense that we can use Representation theory proper to possibly solve everything. This might be the technique of Galois theory metnoined in that Lie Algebra book. This is not unconnected with the companion matrix technique above. These matrices are going to grow very higher dimensional.

Thought. Could you use holonomy continuation to get roots, then interpolate those roots into a numerical grobner basis? Are the Lagrange polynomials of the zero set a grobner basis?


Part of what makes it seem so intimidating is that it isn’t obvious how to brute force the answer. But if we constrain ourselves to certain kinds of factors, they are brute forceable.

Given a suggested factor, we can determine whether it actually is a factor by polynomial division. If the remainder left over from polynomial division is 0, then it is a factor.

If we have an enumerable set of possibilities, even if large, then it doesn’t feel crazy to find them.

Any root of a polynomial with rational coefficients can be converted to integer coefficients by multiplying out all the denominators.

Let’s assume the polynomial has factors of integer coefficients.

Rational Root Test

Kronecker’s method

Finite Fields. It is rather remarkable that there exists finite thingies that have the algerbaic properties of the rationals, reals, and complex numbers. Typically when discretizing continuum stuff, you end up breaking some of the nice properties, like putting a PDE on a grid screws over rotational symmetry. Questions that may be hard to even see how to go about them become easy in finite fields in principle, because finite fields are amenable to brute force search. In addition, solutions in finite fields may simply extend to larger fields, giving you good methods for calculations over integers or rationals or what have you.

SubResultant. A curious property that if two polynomials share roots/common factors, it is pretty easy to seperate that out. The GCD of the polynomials.

Kind of the gold standard of root finding is getting a formula in terms of square roots. This is an old question. Galois Theory is supposedly the answer.

Fool’s Rules Regatta 2019

For four years running now we’ve done the fool’s rules regatta in Jamestown as Team Skydog in the unlimited category.

It’s a short boat race where you make a boat in 2 hours out of crap and then race ’em.

The first year we did trash bags filled with air with a platform. We were told we were very creative. We got incredibly dehydrated and sunburnt that year.

Then next two years we did a catamaran with triangular plywood pontoons held together with zip ties. Here’s some link from last year

This year we did a 2×4 and 2×3 frame with plastic sheeting stapled to the inside. It worked surprisingly well! Nearly unsinkable even when we intentionally punctured huge holes . The wind was blowing out to sea and almost everyone was drifting out to Newport. We got first place this year! We celebrated with bbq and our ice cream bucket prize.

Thoughts for next year: Make a keel / centerboard so we can tack? Maybe that is crazy talk.

Declan’s post on the same event:

So majestic.
Will is the ultimate cutie. Ladies, please apply inside.
Layin’ out the frame
Sky dog ascendent!
Our reward for first place was an unholy bucket of ice cream