Tropical Semirings and Time Complexity

I've have been thinking about how a compiler might track the cost of a computation, and assuming that it is known to terminate, compute it at compile time. I have no idea if this or something like this is usually done, but its basically constant folding.

What I was thinking is that many operations, arithmetic operations being the best example, can be tagged with a cost (say, 1 for all of the languages primitive operations). Any operation that takes an unbounded amount of time would be tagged with an "infinite" cost. The interesting thing here is that this amounts to a morphism from programs in some language to the tropical semiring (in this case, of natural numbers extended with infinity, with the additive operator the max function, and the multiplicative operator as addition), as I show below. Note that this assumes that they available control structures are sequencing and conditionals.

First off, primitive operations are assigned a fixed cost- perhaps just 1 for each operation. This could be more fine grained if desired, especially if the languages primitive operations are not simple.

Sequencing two operations translates to the addition of them. This seems appropriate as sequencing is like the product of programs. This is because the cost of doing two operations in sequence is the cost of doing the first operation plus the cost of doing the second.

Conditionals have at least two branches, as a one branch conditional statement is like a two branch condition with the empty operation as the second branch. Only one of the conditions will be executed, but we have to assume pessimistically that the more expensive one will be followed. This means that the cost of a conditional is the maximum of cost of the two branches.

Other control structures could perhaps be accommodated. Well founded recursion, or loops of certain forms, could be added, though in general they would have infinite cost. It seems like one would end up evaluating the largest expressions possible that is not tagged with an unknown (infinite) time cost.

So thats all. A trivial observation, and one that I'm sure is well known. To finish this off, note that something like this is also true for determining the size of algebraic data structures. Infinity comes up for structures that may have unbounded size (lists or trees), but otherwise the equations that define the structures (in the algebra of data types), when interpreted as a number is essentially its size, with variables acting as expected.