### 1. Introduction

The goal of this blog post is to introduce and formalize the rotated versions of Pascal’s triangle and the binomial coefficient, which were the subject of the previous blog post.

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 binomial coefficient in Section 3, where we show how to obtain it in two different ways. The blog is concluded in Section 4.

### 2. Rotating Pascal’s triangle

Rather than motivate the introduction of the rotated version of Pascal’s triangle, we dive right in and perform the rotation and subsequently examine the properties of the new triangle. So, given the traditional version of Pascal’s triangle,

we rotate it counterclockwise in such a way that we can address its entries using rows and columns,

similar to how we address the entries of a matrix.

First, we notice that the base case of Pascal’s triangle, where $\binom{n}{0} = 1$, now corresponds to the first column of the rotated Pascal’s triangle,

Furthermore, the case where $\binom{n}{k} = 0$, when $% $, has now disappeared due to the rotation making us unable to index outside of the triangle, and the case $\binom{n}{n} = 1$ now corresponds to the first row of the rotated Pascal’s triangle,

Lastly, in the inductive case, $\binom{n}{k} = \binom{n-1}{k} + \binom{n-1}{k-1}$, where we added the two entries just above the entry we wanted to calculate, we now add its immediate western and northern neighbors,

giving us three nice and simple cases. Thus, by combining the observations above, we can formalize the rotated version of Pascal’s triangle with the two base cases,

and

along with the inductive case,

where $r$ refers to the row index, $c$ refers to the column index and the subscripted $r$ indicates that these rules refer to the rotated version of Pascal’s triangle.

Not only is the formalization of the rotated Pascal’s triangle more elegant than its counterpart, even some of its properties also benefit from this transformation. In particular, the symmetry property of the traditional version of Pascal’s triangle,

now becomes,

which is void of any subtraction operations in its indices. Instead, we simply swap the value of the row and column indices, respectively, and still obtain the same result.

Having formalized the rotated Pascal’s triangle and discussed some of its properties, our next goal is to define a rotated binomial coefficient function as a dual to the rotated Pascal’s triangle.

### 3. The rotated binomial coefficient

When defining the rotated binomial coefficient, we have the choice between two approaches:

• Lift the function definition from the formalization of the rotated Pascal’s triangle, or
• capture the rotation transformation as a function and apply it to the binomial coefficient.

For the sake of completeness, we introduce both function definitions in the following sections.

#### 3.1 Lifting the rotated binomial coefficient from the rotated Pascal’s triangle

Just as in the previous post, we can reduce the formalization of the rotated Pascal’s triangle into a computable function, rotatedBinomialCoefficient, by mapping the base cases and the inductive case of our formalization to the base cases and inductive cases of our function, i.e. the row and column indices, r and c. Thus, if we take a look at the two base cases, $\binom{0}{c}_r = 1$ and $\binom{r}{0}_r = 1$, we note that these naturally map to the two base cases for our function, (r = 0, c > 0) and (r > 0, c = 0). Likewise, there exists a natural mapping from the inductive case of our formalization, $\binom{r + 1}{c + 1}_r = \binom{r + 1}{c}_r + \binom{r}{c + 1}_r$, to the inductive case of our function, (r > 0, c > 0), which - when combined - gives us the following Haskell definition,

Again, we use guards to express the base cases and the inductive case in a straight forward manner that nicely captures the original formalization.

Having shown that we can derive the rotated binomial coefficient function from the rotated Pascal’s triangle, in exactly the same way as we derived the binomial coefficient function from Pascal’s triangle, we move on to show how we can obtain it the rotated binomial coefficient function by viewing it as a transformation.

#### 3.2 Capturing the rotated binomial coefficient as a rotation transformation

In order to define the rotated binomial coefficient function as a transformation of the traditional binomial coefficient function, we have to the capture counterclockwise rotation happening in-between Figures \ref{fig:pascal-s-triangle} and \ref{fig:rotated-pascal-s-triangle}.

So, as we have already noted, the row index r maps directly to the row index n, since we have the following relation of the base cases $\binom{r}{0}_r = \binom{r}{0} = 1$. Furthermore, if we let r = 0, we notice that the column index c maps to both n and k, specifically the case where $n = k$, giving us the relation $\binom{0}{c}_r = \binom{c}{c}$, as also observed in the previous section. Putting these relations together yields the following definition of the rotated binomial coefficient function, as a transformation applied to the binomial coefficient function,

Lastly, we note that we did not have to take the inductive case into account as the definition only required us to capture how the rotation affected the two indices - which was easiest to see in the base cases.

Now that we have introduced both the rotated Pascal’s triangle and the rotated binomial coefficient function, we can conclude this blog post.

### 4. Conclusion

In this blog post, we have introduced and formalized the rotated Pascal’s triangle and defined the rotated binomial coefficient function.

We obtained the above results by first applying the rotation transformation on the traditional version of Pascal’s triangle and subsequently formalizing the result. Having formalized the rotated Pascal’s triangle, we then lifted the definition of the rotated binomial coefficient function from the formalization. Furthermore, we also defined the rotated binomial coefficient function as the rotation transformation applied to the binomial coefficient function.

This post - and the previous - was a small excerpt from my Master’s thesis, in which I also prove how we can use the rotated Pascal’s triangle and the rotated binomial coefficient to come up with a characteristic function for Moessner’s sieve.1

1. Moessner’s sieve is the procedure described in “Eine Bemerkung über die Potenzen der natürlichen Zahlen” (1951) by Alfred Moessner, and the term Moessner’s sieve was first coined by Olivier Danvy in the paper “A Characterization of Moessner’s sieve” (2014).