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

Question

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?

Answer 1

It appears that "F" does not stand for anything in particular: rather, it is the metavariable symbol that is used in the definition of F-bounded quantification. In the paper in which F-bounded quantification was introduced, F-Bounded Polymorphism for Object-Oriented Programming, the authors write:

To solve this problem and related difficulties with other forms of recursive types we introduce a generalization of bounded quantification which we call F-bounded quantification, for want of better terminology.

suggesting that they do not view the name as particularly descriptive. Later, when they define F-bounded quantification explicitly, they write:

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.