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:

\forall y, add(0, y, y) \\ \forall x, y, z, add(x, y, z) \to add(S(x), y, S(z))

Or, the more commonly known variant:

\begin{aligned} 0+y &= y \\ S(x)+y &= S(x+y) \end{aligned}

In this blog post, we will generalize recursive functions.

Continue reading “Recursion from first principles”

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.

Continue reading “Implementing a formal system in Python”

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.

Continue reading “An algorithm for a BNF matcher”

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.

Continue reading “The computation of appending lists at the type and value level”

FRACTRAN

Fractran is an esoteric programming language. The name is a combination of the words FORTRAN and fraction. What makes it interesting is its simplicity and the fact that it’s as powerful as any other programming language.

I wrote an interpreter back in 2013 in Python and C. In 2021, I wrote a program in Python that takes a Fractran program and translates it to Python.

In this post, we’ll explain what Fractran is all about.

Continue reading “FRACTRAN”