Rotating Pascal's triangle
and the binomial coefficient
prerequisites: The post An introduction to Pascal’s triangle and the binomial coefficient
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 , now corresponds to the first column of the rotated Pascal’s triangle,
Furthermore, the case where , when , has now disappeared due to the rotation making us unable to index outside of the triangle, and the case now corresponds to the first row of the rotated Pascal’s triangle,
Lastly, in the inductive case, , 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 refers to the row index, refers to the column index and the subscripted 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,
and , 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,
, to the inductive
case of our function, (r > 0, c > 0)
, which  when combined  gives us the
following Haskell definition,
1
2
3
4
5
6
rotatedBinomialCoefficient :: Int > Int > Int
rotatedBinomialCoefficient r c
 r == 0 = 1
 c == 0 = 1
 r > 0 && c > 0 = rotatedBinomialCoefficient (r  1) c +
rotatedBinomialCoefficient r (c  1)
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 inbetween Figures \ref{fig:pascalstriangle} and \ref{fig:rotatedpascalstriangle}.
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 . Furthermore, if we let r = 0
, we notice that the column
index c
maps to both n
and k
, specifically the case where ,
giving us the relation , 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,
1
2
rotatedBinomialCoefficient :: Int > Int > Int
rotatedBinomialCoefficient r c = binomialCoefficient (r + c) c
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}.

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). ↩