Blog
We can define roundness in many ways. For example, as you may know, the circle is the shape that given a fixed perimeter maximizes the area. This definition has many problems. One of the problems is that countries generally have chaotic perimeters (also known as borders), so they tend to be much longer than they seem to be.
For that reason, we have to define roundness some other way. Given a country, I will represent it as a plane region, more precisely a compact set \(C \subset \mathbb{R}^2\), and I will define its roundness as
\[ roundness(C) = \max_{ x \in \mathbb{R}^2, r \in \mathbb{R}_{>0}
} \frac{ area(C \cap D(x,r)) }{ \max \{ area(D(x,r)), area(C) \} } \]
where \(D(x, r)\) is the disk of center \(x\) and radius \(r\).
A linear recurrence is a linear equation that recursively defines a sequence. An example is the Fibonacci sequence, that is defined as
\[F_0 = 0\] \[F_1 = 1\] \[F_n = F_{n-1} + F_{n-2}\]
In this post we will talk about xor. Xor is a logical operator that outputs true when the two input values are different, and false otherwise. It is usually simbolized with \(\oplus\).
We all know we can write any number in base 2. For example, \(18_{10} = 10010_2\). So we can ask a question, are there other (nontrivial) sequences such that any natural number is the sum of a finite subset of it? The answer is yes.
In Type Theory, propositions as types is the idea that types can be interpreted as propositions and vice versa. It is also known as the Curry-Howard isomorphism and closely related with the concept of proofs as programs, this is the reason we will use 3 languages during this post: the language of logic, of type theory and Haskell.