A website about functional programming, computer sciencey side-projects, with a sprinkling of mathematics for added authority.
"[…] the tools we are trying to use and the language or notation we are using to express or record our thoughts, are the major factors determining what we can think or express at all!" – Edsger W. Dijkstra, EWD340 (1972) Over a decade ago, when I was writing my master’s thesis in computer science, on the topic of interactive theorem proving, my adviser shared the following…
“If you detect a needlessly complex style when you read, look for characters and actions so that you can unravel for yourself the complexity the writer needlessly inflicted on you.” – Joseph M. Williams , Style: Toward Clarity and Grace The goal of this post is to show in Elm how to go from a case of having nested pattern matching and refining it into a point free style using the idioms of…
“We are our choices.” – Jean-Paul Sartre 1. Introduction This is a follow-up post to Product types in Kotlin, Elixir, and Elm . The goal of this blog post is to define the concept of sum types and compare the implementation of sum types in three different functional programming languages: Kotlin , Elixir , and Elm . The post is structured as follows. In Section 2 , we define the concept of…
“All for one and one for all, united we stand divided we fall.” – Alexandre Dumas , The Three Musketeers 1. Introduction This is a follow-up post to Enum types in Kotlin, Elixir, and Elm . The goal of this blog post is to define the concept of product types and compare the implementation of product types in three different functional programming languages: Kotlin , Elixir , and Elm . The…
“‘Begin at the beginning’, the King said, very gravely, ‘and go on till you come to the end: then stop.’” – Lewis Carroll , Alice in Wonderland 1. Introduction The goal of this blog post is to define the concept of enum types and compare the implementation of enum types in three different functional programming languages: Kotlin , Elixir , and Elm . The post is structured as follows. In…
“One chord is fine. Two chords are pushing it. Three chords and you’re into jazz.” – Lou Reed 1. Introduction This is a follow-up post to A grid of Moessner triangles . The goal of this blog post is to state Moessner’s idealized theorem, Long’s idealized theorem, and conjecture a further generalization. The chapter is structured as follows. In Section 2 we start…
“The trick, William Potter, is not minding that it hurts.” – Robert Bolt , Lawrence of Arabia (1962) 1. Introduction This is a follow-up post to A characteristic function of Moessner’s Sieve . The goal of this blog post is to introduce a new combinatorial property which connects Moessner triangles of different rank but with the same triangle index, thus acting as a dual to…
1. Introduction This is a follow-up post to Obtaining Taylor polynomials with Horner’s method and A Dual to Moessner’s Sieve . The goal of this post is to derive Moessner’s sieve from Horner’s method for polynomial division, thus concluding this three part series on Horner’s method. The post is structured as follows. In Section 2 , we introduce and formalize Horner…
1. Introduction This is a follow-up post to An introduction to Horner’s method . The goal of this post is to derive Taylor polynomials using Horner’s method for polynomial division. The post is structured as follows. In Section 2 , we introduce the concept of Taylor polynomials and Taylor’s theorem. In Section 3 , we derive a procedure for obtaining Taylor polynomials using…
“It might be worth-while to point out that the purpose of abstracting is not to be vague, but to create a new semantic level in which one can be absolutely precise” – Edsger W. Dijkstra , 1972 (EWD340) 1. Introduction This is a follow-up post to A dual to Moessner’s Sieve and Rotating Pascal’s triangle and the binomial coefficient . The goal of this post is to…
“The poet doesn’t invent. He listens.” – Jean Cocteau 1. Introduction This is a follow-up post to An introduction to Moessner’s Theorem and Moessner’s Sieve . The goal of this post is to introduce a dual to Moessner’s sieve that simplifies the initial configuration of Moessner’s sieve, by starting from two seed tuples instead of an initial sequence,…
1. Introduction This is a follow-up post to Rotating Pascal’s triangle and the binomial coefficient . The goal of this post is to introduce and formalize Moessner’s theorem and Moessner’s sieve. The post is structured as follows. In Section 2 , we introduce the basics of Moessner’s theorem and Moessner’s sieve. Afterwards, we discuss some of the generalizations of…
1. Introduction This is a follow-up post to An introduction to Pascal’s triangle , which we will build on top off by introducing and formalizing the rotated versions of Pascal’s triangle and the binomial coefficient . The blog post has the following structure. In Section 2 we rotate Pascal’s triangle and formalize its rotated counterpart. Afterwards, we introduce the rotated…
1. Introduction The goal of this blog post is to introduce Pascal’s triangle and the binomial coefficient . The blog post is structured in the following way. In Section 2 , we introduce Pascal’s triangle and formalize its construction. Before we define the binomial coefficient in Section 4 , we first motivate its introduction by stating the Binomial Theorem in Section 3 . The blog is…
1. Introduction This post is a follow-up to An interpreter, a compiler, and a virtual machine , in which we defined the fixpoints we will now use to prove an equivalence relation between interpretation of an arithmetic expression and compilation of an arithmetic expression followed by execution of the bytecode program resulting from compilation . First, we derive the equivalence relation in…
1. Introduction In this post, we show how to implement an interpreter and a compiler for a small arithmetic language, in the Coq Proof Assistant , along with a virtual machine for running the output of the compiler. We implement the language in Coq such that we can later prove an equivalence relation between evaluation with an interpreter and a compiler, in a follow-up blog post. We start by…
“What makes the desert beautiful,” said the little prince, “is that somewhere it hides a well…" – Antoine de Saint-Expuéry , The Little Prince 1. Introduction The goal of this blog post is to introduce Horner’s method for polynomial evaluation and polynomial division, and subsequently prove an equivalence relation between these two types of application. The blog post…
“Beware of bugs in the above code; I have only proved it correct, not tried it.” – Donald Knuth Introduction In this post, we give a short primer on interactive theorem proving in the [ Coq Proof Assistant (or simply, Coq) with the guiding example of natural numbers and their basic arithmetic operators. Rather than give a theoretical introduction to the The Curry-Howard…