Curry-Fubini Isomorphism | Parallels in Math and CS

Computer science revolves around the study of computation. Mathematics, of which computer science was once entirely a subfield within, is the foundation of computation. More aptly: computation is the application of mathematics. When attempting to explain to outsiders that my studies are not in software engineering, I often relent that it is a glorified math degree.

As computer science has grown into its own well respected field, new calculi, grammars, and axioms have been written in order to better serve our studies. In the process, mathematical discoveries that have been refined for hundreds of years become groundbreaking theory in computer science. Today, I will cover some of these isomorphisms, a structure preserving mapping between two objects, and introduce one of my own, which bridge the fields of mathematics and computer science back together.

Loops and Series

I begin with this elementary isomorphism as an example to further clarify the subject of this post.

A simple series of the form: $$ \sum_{n=0}^{5} n $$ can be expressed as a for loop like:

int acc = 0;
for (int i = 0; i <= 5; i++) {
    acc += i;
}

An infinite series, such as the triangle series of the form: $$ \sum_{n = 1}^{\infty} \frac{2}{n (n+1)} $$ can also be expressed as a loop like:

float acc = 0;
for (int i = 1; ; i++) {
    acc += 2 / (i * (i + 1));
}

In practice, this loop will result in stack overflow long before you arrive at any answer. However, through a series of theorems which are too deep to go into here (though an excellent explanation from ProofWiki exists) we can mathematically determine that the series converges at $2$.

See 'Termial' function $n?$ coined by Don Knuth in The Art of Computer Programming

In the domain of programming languages, we have something similar to loop convergence: Fixed-point semantics. By describing the denotational (what) rather than operational (how) semantics of a program, we can reunite with mathematical operations like equality.

There is a more relevant takeaway from this simple isomorphism. For programmers, thinking about closed form solutions to series may be easier when thought of as an imperative loop. For mathematicians, thinking about their loops in code as a series may give more intuition. This isomorphism allows us to reason about computation in either domain, choosing whichever is more practical to the individual.

Curry-Howard Isomorphism

This next isomorphism is an important one in the field of programming languages. It relates propositional logic to the domain of type theory: Propositions as Types.

Propositional logic has been well studied since the age of the Stoics in the 4th century BCE. Though more recent, 19th century work, formal logic as studied by Boole and De Morgan lays the groundwork for the Church-Howard Isomorphism.

Developed through the 1930s, Alonzo Church's $\lambda$-calculus was established as a way to study functions as rules. By the 1940s, Church had developed a theory of types and created a typed $\lambda$-calculus.

In 1934, Haskell Curry first makes an observation mapping functions and implications. Essentially, the implication $A \implies B$ can be mapped to the type signature of a function $A \to B$.

William Alvin Howard, in the later half of the century, publishes a manuscript outlining what we now call the Curry-Howard Isomorphism.

Where a propositional value requires a proof, the existence of a value of a type can be considered a witness to the proof.

From this, we can make the following mappings:

A conjunction $A \wedge B$ requires the proof of both $A$ and $B$. The product type $\tau_A \times \tau_B$ requires two values of types $\tau_A$ and $\tau_B$.

A disjunction $A \vee B$ requires the proof of one of $A$ or $B$. The sum type $\tau_A + \tau_B$ requires one value of either type $\tau_A$ or type $\tau_B$.

Most importantly, functions of type $\tau_A \to \tau_B$ can be translated to the implication $A \to B$. If given a value of type $\tau_A$ as proof, the function proves the existence of a value of type $\tau_B$ by returning a witness value.

This correspondence seems obvious when outlined like this, though it was considered a major breakthrough when first published. The results of this discovery have been instrumental in formally proven programs, such as the CompCert compiler. It has led to powerful tools such as the Calculus of Construction and the Coq programming language. I really suggest checking these out if you are unfamiliar.

Curry-Fubini Isomorphism

The Fubini Theorem in calculus allows the order nested integrals are computed to be interchanged, under certain circumstances. It allows us to compute integrals over functions of more than one variable by integrating with respect to one variable, and holding the other variables as constants. The proof and explanation of solving iterated integrals can be done much better by someone else.

In functional programming, currying is a process in which a multi-argument function is translated into a sequence of unary functions. In OCaml, consider the trivial sum function:

let sum a b = a + b ;;
- : val sum : int -> int -> int = <fun>

sum 5 7 ;;
- : int = 12

This is syntactic sugar for the following unary function:

let sum' = fun a -> fun b -> a + b ;;
- : val sum' : int -> int -> int = <fun>

sum' 5 7 ;;
- : int = 12

When we pay attention to the types of sum, we see, when given an int, it returns a function from int -> int. When that second function is given an int, it returns an int. It is just unary functions, all the way down.

In sum' we make it more explicit, sum' is a function which takes an int and returns a function from int -> int. When the second function is given an int, it returns an int.

To combine Fubini's Theorem from calculus, and Currying from functional programming, we see that both are taking multivariable functions, computing with respect to one variable, and returning a new function with one fewer argument.

I call this the Curry-Fubini Isomorphism. Though not as revolutionary as the Curry-Howard Isomorphism, nor as simple as the Loops and Series Isomorphism, I believe it is a neat way to think about computation, and bridge the gap between mathematics and computer science.

As a student of computer science, I find that solving iterated integrals is easier when I think about it as a form of currying. I hope for a mathematics student studying functional programming, this correspondence helps clarify the concept of currying.

-Acer