currying-exponent.md

Herein, A, B, and C will always refer to finite sets.

Definition: |A| denotes the cardinality of A.

Definition: A -> B denotes the set of functions from A to B, where a function is a one-to-one mapping from domain A to codomain B.

For example, if A = {1, 2} and B = {4, 5, 6}, then there are exactly nine functions A -> B:

1 -> 4, 2 -> 4        1 -> 5, 2 -> 4        1 -> 6, 2 -> 4
1 -> 4, 2 -> 5        1 -> 5, 2 -> 5        1 -> 6, 2 -> 5
1 -> 4, 2 -> 6        1 -> 5, 2 -> 6        1 -> 6, 2 -> 6

I've laid out this list in square to illustate how this count is 3^2.

Fact: The number of functions A -> B is equal to |B|^|A|.

To recap:

• |A -> B| is the cardinality of A -> B.
• |{1, 2} -> {4, 5, 6}| = 3^2
• |A -> B| = |B|^|A|.

Definition: A × B is the cartesian product of A and B (known more often in programming as the set of tuples (A, B)).

Fact: |A × B| = |A| |B|.

Now we're going to show that |(A × B) -> C| = |A -> (B -> C)|. This ought to be the case, because these two sets are isomorphic (the bijection being currying and uncurrying).

This is a straightforward substitution exercise given what we already know.

|(A × B) -> C| = |C|^|A × B|
               = |C|^(|A| |B|)

|A -> (B -> C)| = |B -> C|^|A|
                = (|C|^|B|)^|A|
                = |C|^(|A| |B|)