Recursion from first principles

Recursion is one of the things that makes computation happen – whether you’re doing something on your computer, smart TV, or smartphone.

For example, here’s a definition of the addition function represented in first-order logic:

Or, the more commonly known variant:

In this blog post, we will generalize recursive functions.

Implementing a formal system in Python

Some of the contents of this post are contained in my third book.

In this post, we’ll go deeper into the syntactical part of a formal system, along with the semantical. We’ve discussed formal systems in the past, and in this post, we’ll get more practical by providing an implementation of an example formal system.

An algorithm for a BNF matcher

BNF (short for Backus-Naur Form) is a notation for specifying syntaxes. It allows specifying syntax with sums (|) and products (). For example, foo ::= 1 | 2 specifies that foo can be either 1 or 2, and baz = <foo>2 specifies that baz can be either 12 or 22.

A BNF matcher is a program that takes as input a grammar and a string and tells us whether the string is captured by the grammar or not. A BNF parser works similarly, but instead, it generates a syntax tree out of it rather than telling if a particular string matches the structure.

BNF is important because it’s used as the syntax of languages in computing, mainly in programming languages. That is, any time you get a “Syntax error! Missing ;” or a similar error, you can freely blame BNF 🙂

We will start with a concrete example, then give a general algorithm and finally write a BNF matcher in PHP and Lisp.

High Five

On the 9th of January this year, I turned 5 years at Automattic. This is the longest time I’ve ever been working for the same company, the previous one standing at 4.5 years.

I remember talking to my friend who referred me to work at Automattic (further in the text A8c). At one point he said, “This company will spoil you (in a good way)! You will see!”. I was skeptical, naturally, “Sure, sure, it’s just another company, I work only to get paid and that’s it”, but turned out I was wrong.

The computation of appending lists at the type and value level

Recently, I spent some time experimenting with Haskell’s type families – a concept that allows one to perform computation at the type level in Haskell.

In one example, I wrote an append implementation at the value and the type level, and also other stuff such as Merge Sort implementation at the type level.

In this post, I will show different implementations of appending two lists together, written both in Haskell and in Idris, as well as some observations around the differences.