Toward Normalization of STLC

WHAT: What is my understanding?

We can construct a redex tree for any STLC formula. We know that the degree increases at the abstraction, and the redex tree is finite (since the formula is finite with finite parsing), so we are able to find the abstraction (like the figure below, $\lambda{x}$) with MAXIMUM degree where degrees of all substructures (nodes) of $\phi$ and $\psi$ have to less than the degree of current abstraction (we are allowed to find one because the tree is finite, if in $\phi$, $\psi$ there is a degree greater or equal then we could switch to that abstraction; if $\psi$ is an not reducible abstraction, then the degree for current abstraction is still greater than $\psi$).

A part of redex tree

Then the application for the abstraction will result in the reduction for the number of indexes for the maximum degree. Since application can only result in a finite number of nodes that degree is less than the abstraction, so reduction for each degree is finitary, and since the maximum is finitary, so the whole reduction is finitary.

HOW: How is this understanding useful?

Here are some interesting things from this method. The typical reason the fixed point ($\Omega = (\lambda{x}.xx)(\lambda{x}.xx)$) in ULC is not normalizable is because the type of abstraction is not well-defined in finitary sense so we are not able to determine the degree for current abstraction, but I have a more interesting interpretation:

The fixed point in ULC

Since it is a fixed point, we can interpret it as the degree of an ordinal $\omega$ (first infinite ordinal), then the tree and degree are well-defined (now our definition does not evolve types but only induced from terms). The core of the method failed is that the abstraction has the degree same as the substructure $\psi$, the same degree is yielded by the infinitary function induction from the fixed point. (Just an interpretation, I have not analyzed whether $\Omega$ is the least fixed point).

This method explicits structural induction to the graph theory sense, so I think it might be easier for students to understand, and it is also useful to introduce how structural induction works.