Category Mathematics

What is defunctionalization?

What is defunctionalization? I recently gave a little demonstration entitled "What is Defunctionalization?" for UCSC TWIGS (the acronym, stolen from a similar seminar in the the U. Mass. math department, stands for The "What Is … ?" Graduate Seminar). The inspiration for this talk was just to present what I’d learned after Conor McBride’s brilliant […]

Debugging with Open Recursion Mixins

The call is out for submissions to the next issue of The Monad.Reader! To get an idea of the content (and because D Stewart told us all to read every past issue) I cracked open Issue 10, which has a nice tutorial by B Pope on the GHCi debugger. But having just finished a post […]

CTL Model Checking in Haskell: A Classic Algorithm Explained as Memoization

As an exercise, since my reading group was discussing model checking this week, I implemented the classic model checker for CTL specifications from the 1986 paper Automatic Verification of Concurrent Systems Using Temporal Logic Specifications by EM Clarke, EM Emerson, AP Sistla. The “efficient algorithm” presented in the paper is, upon reflection, merely […]

Drawing fractals in Haskell with a cursor graphics DSEL and a cute list representation

I’m reading the very fun Measure, Topology, and Fractal Geometry by GA Edgar, and thought I’d hack up some of the examples in Haskell. So this post implements cursor graphics in OpenGL in (I think) DSEL style, demonstrating the StateT and Writer monad gadgets from the standard library and a cool "novel representation of lists" […]

Using OpenGL’s blending to visualize congestion in convex routing (in Haskell)

This is a question posed in my randomized algorithms class. If you are routing in a network whose connectivity looks "more or less" like a convex figure, what does the congestion look like? A quick way to make an educated guess is to draw a bunch of random line segments in such a convex shape […]

Infinite lazy Knuth-Bendix completion for monoids in Haskell

The Knuth-Bendix completion procedure (when it succeeds) transforms a collection of equations into a confluent, terminating rewrite system. Sometimes the procedure fails, and sometimes does not terminate, but The Handbook of Computational Group Theory by D Holt remarked that even in this case it generates an infinite set of rewrite rules that are complete, and […]

Calculating the reflect-rotate-translate normal form for an isometry of the plane in Haskell, and verifying it with QuickCheck.

Any isometry of the plane has a unique normal form as the composition of a translation, rotation and reflection. This note computes this normal form and tests the implementation using the QuickCheck automated testing tool for Haskell. To generate random test data, I use another characterization of isometries as products of up to three reflections. […]