# Why F-bounded polymorphism and F-bounded quantification are called, well, F-bounded

It's claimed in Wikipedia that:

F-bounded quantification or recursively bounded quantification, introduced in 1989, allows for more precise typing of functions that are applied on recursive types. A recursive type is one that includes a function that uses it as a type for some argument or its return value

Here's the article which Wikipedia refers to, and F-bounded quantification is introduced in that article in following fashion:

F-bounded quantification is a natural extension of bounded quantification that seems particularly useful in connection with recursive types.

My question is - why though it's F-bounded, what does "F" stands for in this particular context?

We say that a universally quantified type is F-bounded if it has the form $$\forall t \subseteq F[t] . \sigma$$ where $$F[t]$$ is an expression, generally containing the type variable $$t$$.
As far as I can tell, the paper contains no other explanation and the most apparent explanation is that the "F" in the terminology is chosen to coincide with the symbol $$F$$ chosen, arbitrarily, for the definition.