Lean, 66 bytes
def s:_->nat->nat|(m+1)(n+1):=(n+1)*(s m n+s m(n+1))|0 0:=1|_ _:=0
Try it online!
Proof of correctness
Try it online!
Explanation
Let us ungolf the function:
def s : nat->nat->nat
| (m+1) (n+1) := (n+1)*(s m n + s m (n+1))
| 0 0 := 1
| _ _ := 0
The function is defined by pattern matching and recursion, both of which have built-in support.
We define s(m+1, n+1) = (n+1) * (s(m, n) + s(m, n+1) and s(0, 0) = 1, which leaves open s(m+1, 0) and s(0, n+1), both of which are defined to be 0 by the last case.
Lean uses lamdba calculus syntax, so s m n is s(m, n).
Now, the proof of correctness: I stated it in two ways:
def correctness : ∀ m n, fin (s m n) ≃ { f : fin m → fin n // function.surjective f } :=
λ m, nat.rec_on m (λ n, nat.cases_on n s_zero_zero (λ n, s_zero_succ n)) $
λ m ih n, nat.cases_on n (s_succ_zero m) $ λ n,
calc fin (s (nat.succ m) (nat.succ n))
≃ (fin (n + 1) × (fin (s m n + s m (n + 1)))) :
(fin_prod _ _).symm
... ≃ (fin (n + 1) × (fin (s m n) ⊕ fin (s m (n + 1)))) :
equiv.prod_congr (equiv.refl _) (fin_sum _ _).symm
... ≃ (fin (n + 1) × ({f : fin m → fin n // function.surjective f} ⊕
{f : fin m → fin (n + 1) // function.surjective f})) :
equiv.prod_congr (equiv.refl _) (equiv.sum_congr (ih n) (ih (n + 1)))
... ≃ {f // function.surjective f} : s_aux m n
def correctness_2 (m n : nat) : s m n = fintype.card { f : fin m → fin n // function.surjective f } :=
by rw fintype.of_equiv_card (correctness m n); simp
The first one is what is really going on: a bijection between [0 ... s(m, n)-1] and the surjections from [0 ... m-1] onto [0 ... n-1].
The second one is how it is usually stated, that s(m, n) is the cardinality of the surjections from [0 ... m-1] onto [0 ... n-1].
Lean uses type theory as its foundation (instead of set theory). In type theory, every object has a type that is inherent to it. nat is the type of natural numbers, and the statement that 0 is a natural number is expressed as 0 : nat. We say that 0 is of type nat, and that nat has 0 as an inhabitant.
Propositions (statements / assertions) are also types: their inhabitant is a proof of the proposition.
def: We are going to introduce a definition (because a bijection is really a function, not just a proposition).
correctness: the name of the definition
∀ m n: for every m and n (Lean automatically infers that their type is nat, because of what follows).
fin (s m n) is the type of natural numbers that is smaller than s m n. To make an inhabitant, one provides a natural number and a proof that it is smaller than s m n.
A ≃ B: bijection between the type A and the type B. Saying bijection is misleading, as one actually has to provide the inverse function.
{ f : fin m → fin n // function.surjective f } the type of surjections from fin m to fin n. This syntax builds a subtype from the type fin m → fin n, i.e. the type of functions from fin m to fin n. The syntax is { var : base type // proposition about var }.
λ m : ∀ var, proposition / type involving var is really a function that takes var as an input, so λ m introduces the input. ∀ m n, is short-hand for ∀ m, ∀ n,
nat.rec_on m: do recursion on m. To define something for m, define the thing for 0 and then given the thing for k, build the thing for k+1. One would notice that this is similar to induction, and indeed this is a result of the Church-Howard correspondence. The syntax is nat.rec_on var (thing when var is 0) (for all k, given "thing when k is k", build thing when var is "k+1").
Heh, this is getting long and I'm only on the third line of correctness...
11A definition of surjection would be nice. – Stewie Griffin – 2018-04-20T16:02:02.553
3Is it intentional that n cannot equal k? – Dennis – 2018-04-20T16:08:01.507
1@Dennis I like to exclude every possible edge case from my challenges – Leaky Nun – 2018-04-20T16:15:40.117
3That seems like an important edge case to include. My guess is that most answers that work for n>k will also work for n==k but it might allow for some sneaky golfing somewhere – dylnan – 2018-04-20T16:22:42.357
@ whoever voted to close what is your reason? – dylnan – 2018-04-20T18:49:49.040