Inside 206-105

Existential Pontification and Generalized Abstract Digressions

Math

A monad is a monoid in the category of endofuctors. What’s the problem dude?

The Difference between Recursion & Induction

Recursion and induction are closely related. When you were first taught recursion in an introductory computer science class, you were probably told to use induction to prove that your recursive algorithm was correct. (For the purposes of this post, let us exclude hairy recursive functions like the one in the Collatz conjecture which do not [...]

A Zerocoin puzzle

I very rarely post linkspam, but given that I’ve written on the subject of anonymizing Bitcoins in the past, this link seems relevant: Zerocoin: making Bitcoin anonymous. Their essential innovation is to have a continuously operating mixing pool built into the block chain itself; they pull this off using zero-knowledge proofs. Nifty! Here is a [...]

A classical logic fairy tale

(Selinger) Here is a fairy tale: The evil king calls the poor shepherd and gives him these orders. “You must bring me the philosophers stone, or you have to find a way to turn the philosopher’s stone to gold. If you don’t, your head will be taken off tomorrow!” What can the poor shepherd do [...]

An Interactive Tutorial of the Sequent Calculus

You can view it here: An Interactive Tutorial of the Sequent Calculus. This is the "system in three languages" that I was referring to in this blog post. You can also use the system in a more open ended fashion from this page. Here's the blurb: This interactive tutorial will teach you how to use [...]

Chain Rule + Dynamic Programming
= Neural Networks

(Guess what Edward has in a week: Exams! The theming of these posts might have something to do with that...) At this point in my life, I’ve taken a course on introductory artificial intelligence twice. (Not my fault: I happened to have taken MIT’s version before going to Cambridge, which also administers this material as [...]

The return of Hellenistic reasoning

I recently attended a talk which discussed extending proof assistants with diagrammatic reasoning support , helping to break the hegemony of symbolic systems that is predominant in this field. While the work is certainly novel in some respects, I can't also but help think that we've come back full circle to the Ancient Greeks, who [...]

Many-valued logics and bottom

I was flipping through An Introduction to Non-Classical Logic by Graham Priest and the section on many-valued logics caught my eye. Many-valued logics are logics with more than the usual two truth values true and false. The (strong) Kleene 3-valued logic, sets up the following truth table with 0, 1 and x (which is thought [...]

Picturing binomial coefficient identities

Guys, I have a secret to admit: I’m terrified of binomials. When I was in high school, I had a traumatic experience with Donald Knuth’s The Art of Computer Programming: yeah, that book that everyone recommends but no one has actually read. (That’s not actually true, but that subject is the topic for another blog [...]

My first proof in Isabelle

One of the distinctive differences between academic institutions in the United States and in Great Britain is the supplementary learning outside of lectures. We have recitations in the US, which are something like extra lectures, while in the UK they have tutorials, or supervisions as they are called in Cambridge parlance. As always, they are [...]

Purpose of proof: semi-formal methods

In which the author muses that “semi-formal methods” (that is, non computer-assisted proof writing) should take a more active role in allowing software engineers to communicate with one another. C++0x has a lot of new, whiz-bang features in it, one of which is the atomic operations library. This library has advanced features that enable compiler [...]