Correct functional implementation on Binomial Heap

Question

I am reading Binomial Heap in Purely Functional Data Structures.

The implementation of insTree function confused me quite much. Here are the set of codes

datatype Tree = Node of int * Elem.T * Tree list

fun link (t1 as Node (r, x1, c1), t2 as Node (_, x2, c2)) = 
  if Elem.leq (x1, x2) then Node (r+1, x1, t2::c1)
  else Node (r+1, x2, t1::c2)

fun rank (Node (r, x, c)) = r

fun insTree (t, []) = [t]
  | insTree (t, ts as t' :: ts') =
      if rank t < rank t' then t::ts else insTree (link (t, t'), ts')

My confusion lies on the bit in insTree that why it does not consider the situation of rank t > rank t'?

In if rank t < rank t' then t::ts else insTree (link (t, t'), ts'),

1. if t's rank is less than t''s rank, then put the t into the heap, no question asked
2. the else has two cases: equal and bigger.
3. For equal, yes, we can link two trees (we link only two trees with the same rank), and then try to insert the new linked tree into the heap, no question asked.
4. but even the bigger case would have the same as equal, why? Even if rank t > rank t', we still link them?

---

Edit

I thought the process of inserting a binomial tree into a binomial heap should be like this:

1. We get the tree t and the heap
2. In the heap (actually a list), we compare rank of the tree t with every tree in the heap
3. We find a missing rank (increasing order in the heap) which matches the rank of t, we put t at that slot
4. We find a tree in the heap with same rank as t, then we link two trees and process a rank+1 new tree and try again insert the new tree to the heap.

So, I think the correct fun insTree could be like this:

fun insTree (t, []) = [t]
      | insTree (t, ts as t' :: ts') =
          if rank t < rank t' then t::ts 
          else if rank t = rank t' then insTree (link (t, t'), ts')
          else t'::(insTree (t, ts'))

Answer 1

insTree is a helper function that is not visible to the user. The user calls insert, which in turn calls insTree with a tree of rank 0, and a list of trees of increasing rank. insTree has an invariant that the rank of t is <= the rank of the first tree in the list. So if it's not <, then it must be =.

You're right that if insTree was a general-purpose public function, rather than a special-purpose private function, then it would have to deal with the missing case.

Answer 2

An important detail behind this is that a binomial heap is not any tree that happens to have k children. It's a tree that's rigorously defined as

The binomial tree of order 0 is a single node, and The binomial tree of order n is a single node with binomial trees of order 0, 1, 2, ..., n - 1 as children.

This answer, explain why the insert function, which is the one required to construct a binomial heap, do not manage these cases (In theory they cannot happen). Maybe the cases you are proposing make sense for a merging operation (but the underlying implementation should differ).