[formal-methods] Conceptual Mathematics, I.1.6

[Josh Myer]

(Warning, contains spoilers!  I've talked about this with nigh on half
the list, so it was time to just continue the discussion there.)

On Sat, Jun 13, 2009 at 07:11:51PM -0700, Jason Dusek wrote:

>     sum with `c` ranging from 0 to `|A|` of:
> 
>       (|A| choose c) * (c ^ (|A| - c))
> 

That's exactly where I got, and where I realized "Hot damn, that's a
lot of entries, and it's one ugly-assed formula."

Another way to explain how to get there (more intuitive, less
rigorous and iron-clad):

Identity is clearly one f : A -> A s.t. f.f=f, but what about f(a)=1,
1 some element of A?  In this case, f(a) = 1, and f(1) = 1, so
  f(f(a)) = f(1) = 1 = f(a)

Can we generalize it?  Yes we can!
  f(c) = c, for all c in the codomain of f

So, then, for some f(a) = c_a, and since c_a is in the codomain, 
  f(f(a)) = f(c_a) = c_a

Therefore, we ensure that f(c) = c forall c in the codomain.  For
codomains of size k (where k is in {1,...,|A|}), there are |A| choose
k ways to pick a codomain.  Once we've chosen the codomain, the map
for them is frozen: f(c) = c for all of them.  But, for the rest of
the domain, we have free choice of a map, so long as it goes to the
codomain.  There are (|A|-k) elements left in the domain, each of
which can go to one of k entries in the codomain.  That is,
k*k*k*k..., or k^(|A|-k) Thus, we get

  For all k in {1...|A|}, 
     choose a codomain
       then choose the fixed codomain mapping
         then choose the rest of the map
      
Mathematically, we then get

  \sum k 1 to |A| nCr(|A|,k)*1*(k^(|A|-k))

as our final tally of maps.

mik sent me a good reply pointing at the right questions, instead of
directly answering.  He made explicit that I could share with the list
if it was helpful, and I believe it is; I'll go ahead and forward it
as well.
-- 
Josh Myer   650.248.3796
  josh at joshisanerd.com