Gilles Dowek
email: gilles.dowek@inria.fr

Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory

Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higherorder resolution. In this note, we compare how it behaves on type theory and on set theory.

Higher-order theorem proving (e.g. higher-order resolution [1,[START_REF] Huet | Constrained resolution: a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF]) is different from first-order theorem proving in several respects. First, the first-order unification algorithm has to be replaced by the higher-order one [START_REF] Huet | A unification algorithm for typed lambda calculus[END_REF][START_REF] Huet | Résolution d'équations dans les Langages d[END_REF]. Even then, the resolution rule alone is not complete but another rule called the splitting rule has to be added. At last, the skolemization rule is more complicated [START_REF] Miller | Proofs in higher order logic[END_REF][START_REF] Miller | A compact representation of proofs[END_REF].

On the other hand, higher-order logic, also called simple type theory, can be expressed as a first-order theory [7], and first-order theorem proving methods, such as first-order resolution, can be used for this theory. Of course, first-order resolution with the axioms of this theory is much less efficient than higher-order resolution. However, we can try to understand higher-order resolution as a special automated theorem proving method designed for this theory. A motivation for this project is that it is very unlikely that such a method applies only to this theory, but it should also apply to similar theories such as extensions of type theory with primitive recursion or set theory.

In [START_REF] Dowek | Theorem proving modulo[END_REF], together with Th. Hardin and C. Kirchner, we have proposed a theorem proving method for first-order logic, called resolution modulo, that when applied to a first-order presentation of type theory simulates exactly higher-order resolution. Proving the completeness of this method has required to introduce a new presentation of first-order logic, called deduction modulo that separates clearly computation steps and deduction steps.

Resolution modulo can be applied both to type theory and to set theory. The goal of this note is to compare how resolution modulo works for one theory and the other. In order to remain self contained, we will first present shortly the ideas of deduction modulo and resolution modulo.

1 Resolution modulo

Deduction modulo

In deduction modulo, the notions of language, term and proposition are that of (many sorted) first-order logic. But, a theory is formed with a set of axioms Γ and a congruence ≡ defined on propositions. In this paper, all congruences will be defined by confluent rewrite systems (as these rewrite systems are defined on propositions and propositions contain binders, these rewrite systems are in fact combinatory reduction systems [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF]). Propositions are supposed to be identified modulo the congruence ≡. Hence, the deduction rules must take into account this equivalence. For instance, the modus ponens cannot be stated as usual

A ⇒ B A B
but, as the two occurrences of A need not be identical, but need only to be congruent, it must be stated

A ′ ⇒ B A if A ≡ A ′ B
In fact, as the congruence may identify implications with other propositions, a slightly more general formulation is needed

C A if C ≡ A ⇒ B B
All the rules of natural deduction or sequent calculus may be stated in a similar way, see [START_REF] Dowek | Theorem proving modulo[END_REF][START_REF] Dowek | Proof normalization modulo[END_REF] for more details.

As an example, in arithmetic, in natural deduction modulo, we can prove that 4 is an even number:

axiom ∀x x = x (x, x = x, 4) ∀-elim 2 × 2 = 4 (x, 2 × x = 4, 2) ∃-intro ∃x 2 × x = 4
Substituting the variable x by the term 2 in the proposition 2 × x = 4 yields the proposition 2 × 2 = 4, that is congruent to 4 = 4. The transformation of one proposition into the other, that requires several proof steps in natural deduction, is dropped from the proof in deduction modulo. It is just a computation that need not be written, because everybody can re-do it by him/herself.

In this case, the congruence can be defined by a rewriting system defined on terms 0 + y -→ y S(x) + y -→ S(x + y)

0 × y -→ 0 S(x) × y -→ x × y + y
Notice that, in the proof above, we do not need the axioms of addition and multiplication. Indeed, these axioms are now redundant: since the terms 0 + y and y are congruents, the axiom ∀y 0 + y = y is congruent to the equality axiom ∀y y = y. Hence, it can be dropped. In other words, this axiom has been built-in the congruence [START_REF] Plotkin | Building-in equational theories[END_REF]1,[START_REF] Stickel | Automated deduction by theory resolution[END_REF].

The originality of deduction modulo is that we have introduced the possibility to define the congruence directly on propositions with rules rewriting atomic propositions to arbitrary ones. For instance, in the theory of integral rings, we can take the rule

x × y = 0 -→ x = 0 ∨ y = 0 that rewrites an atomic proposition to a disjunction. Notice, at last, that deduction modulo is not a true extension of first-order logic. Indeed, it is proved in [START_REF] Dowek | Theorem proving modulo[END_REF] that for every congruence ≡, we can find a theory T such that Γ ⊢ P is provable modulo ≡ if and only if T Γ ⊢ P is provable in ordinary first-order logic. Of course, the provable propositions are the same, but the proofs are very different.

Resolution modulo

When the congruence on propositions is induced by a congruence on terms, automated theorem proving can be performed like in first-order logic, for instance with the resolution method, provided the unification algorithm is replaced by an equational unification algorithm modulo this congruence. Equational unification problems can be solved by the narrowing method [START_REF] Fay | First-order unification in an equational theory[END_REF][START_REF] Hullot | Canonical forms and unification[END_REF][START_REF] Jouannaud | Solving equations in abstract algebras: a rulebased survey of unification[END_REF]. The method obtained this way, called equational resolution [START_REF] Plotkin | Building-in equational theories[END_REF][START_REF] Stickel | Automated deduction by theory resolution[END_REF], is complete.

The situation is different when the congruence identifies atomic propositions with non atomic ones. For instance, in the theory of integral rings, the proposition a × a = 0 ⇒ a = 0 is provable because it reduces to

(a = 0 ∨ a = 0) ⇒ a = 0 Hence the proposition ∃y (a × a = y ⇒ a = y)
is also provable. But, with the clausal form of its negation

a × a = Y ¬a = Z
we cannot apply the resolution rule successfully, because the terms a × a and a do not unify. Hence, we need to introduce a new rule that detects that the literal a×a = Y has an instance that is reducible by the rewrite rule

x × y = 0 -→ x = 0 ∨ y = 0 instantiates it, reduces it and puts it in clausal form again. We get this way the clause a = 0 that can be resolved with the clause ¬a = Z. Hence, the rewrite rules have to be divided into two sets: the set E of rules rewriting terms to terms that are used by the equational unification algorithm and the set of rule R rewriting atomic propositions to arbitrary ones and that are used by this new rule called extended narrowing. The system obtained this way is called extended narrowing and resolution or simply resolution modulo. Figure 1 gives a formulation of this method where unification problems are postponed as constraints. A proposition is said to be provable with this method when, from Extended resolution: {A1, . . . , An, B1, . . . , Bm}/E1 {¬C1, . . . , ¬Cp, D1, . . . , Dq}/E2 {B1, . . . , Bm, D1, . . . , Dq}/E1 ∪ E2 ∪ {A1 =E . . . An =E C1 =E . . . Cp}

Extended narrowing:

C Transforming axioms into rewrite rules enhances the efficiency of automated theorem proving as shown by this very simple example.

/E if l -→ r ∈ R cl(C[r]p)/(E ∪ {C |p =E l})
Example. To refute the theory P 1 ⇔ (Q 2 ∨ P 2 ), ..., P i ⇔ (Q i+1 ∨ P i+1 ), ..., While, in resolution modulo, the propositions P i ⇔ (Q i+1 ∨ P i+1 ), Q i ⇔ ⊥ and P n+1 ⇔ ⊥ can be transformed into rewrite rules

P n ⇔ (Q n+1 ∨ P n+1 ), P 1 , Q 2 ⇔ ⊥, ..., Q n+1 ⇔ ⊥, P n+1 ⇔ ⊥,
P i -→ Q i+1 ∨ P i+1 Q i -→ ⊥ P n+1 -→ ⊥
The only proposition left is P 1 . It reduces to ⊥ ∨ ... ∨ ⊥ and its clausal form is hence the empty clause. Of course, reducing the proposition P 1 has a cost, but this cost is much lower than that of the non deterministic search of a refutation resolution with the clauses above. Indeed, the reduction process is deterministic because the rewrite system is confluent.

Cut elimination and completeness

Resolution modulo is not complete for all congruences. For instance, take the congruence induced by the rewrite rule

A -→ A ⇒ B The proposition B has a proof in sequent calculus modulo axiom A ⊢ A axiom B ⊢ B weak.-left A, B ⊢ B ⇒-left A, A ⊢ B contr.-left A ⊢ B ⇒-right ⊢ A axiom A ⊢ A axiom B ⊢ B weak.-left A, B ⊢ B ⇒-left A, A ⊢ B contr.-left A ⊢ B cut ⊢ B
but it is not provable by resolution modulo. Indeed, the clausal form of the negation of the proposition B is the clause ¬B and neither the extended resolution rule nor the extended narrowing rule can be applied successfully.

However, it may be noticed that the proposition B has no cut free proof in sequent calculus modulo. Hence sequent calculus modulo this congruence does not have the cut elimination property. We have proved in [START_REF] Dowek | Theorem proving modulo[END_REF] that resolution modulo is complete for all congruences ≡ such that the sequent calculus modulo ≡ has the cut elimination property. Together with B. Werner, we have proved in [START_REF] Dowek | Proof normalization modulo[END_REF] that cut elimination holds modulo a large class of congruences and conjectured that it holds modulo all congruences that can be defined by a confluent and terminating rewrite system.

When cut elimination does not hold, only propositions that have a cut free proof are proved by resolution modulo.

2 Simple type theory and set theory

Simple type theory

Simple type theory is a many-sorted first-order theory. The sorts of simple type theory, called simple types, are defined inductively as follows.

ι and o are simple types, if T and U are simple types then T → U is a simple type.

As usual, we write

T 1 → ... → T n → U for the type T 1 → ... (T n → U ).
The language of simple type theory contains the individual symbols

-S T,U,V of sort (T → U → V ) → (T → U ) → T → V , -K T,U of sort T → U → T , -∨ of sort o → o → o, -¬ of sort o → o, -∀T of sort (T → o) → o, the function symbols -α T,U of rank (T → U, T, U ),
and the predicate symbol

As usual, we write (t u) for the term α(t, u) and (t u 1 ... u n ) for (...(t u 1 ) ... u n ). Usual presentations of simple-type theory [START_REF] Church | A formulation of the simple theory of types[END_REF][START_REF] Andrews | An introduction to mathematical logic and type theory: to truth through proof[END_REF] define propositions as terms of type o. But, as we want type theory to be a first-order theory, we introduce a predicate symbol ε that transforms a term of type o into a genuine proposition. Then, we need an axiom relating the proposition ε(α(α( ∨, x), y)) and the proposition ε(x) ∨ ε(y). For instance, the axiom

∀x ∀y (ε( ∨ x y) ⇔ (ε(x) ∨ ε(y)))
This axiom can be built in the congruence, if we take the rewrite rule

ε( ∨ x y) -→ ε(x) ∨ ε(y)
This leads to the rewrite system of the figure 2. This rewrite system is confluent because it is orthogonal and we prove in [START_REF] Dowek | Proof normalization for a first-order formulation of higher-order logic[END_REF] that it is strongly normalizing. Hence, the congruence is decidable.

(S x y z) -→ (x z (y z)) (K x y) -→ x ε( ¬ x) -→ ¬ε(x) ε( ∨ x y) -→ ε(x) ∨ ε(y) ε( ∀ x) -→ ∀y ε(x y)
It is proved in [START_REF] Dowek | Proof normalization modulo[END_REF] that deduction modulo this congruence has the cut elimination property, i.e. every proposition provable in sequent calculus modulo this congruence has a cut free proof.

Set theory

The language of Zermelo's set theory is formed with the binary predicate symbols ∈ and =. This theory contains the axioms of equality and the following axioms. pair:

∀x ∀y ∃z ∀w (w ∈ z ⇔ (w = x ∨ w = y)) union: ∀x ∃y ∀w (w ∈ y ⇔ ∃z (w ∈ z ∧ z ∈ x))
power set:

∀x ∃y ∀w (w ∈ y ⇔ ∀z (z ∈ w ⇒ z ∈ x))
subset scheme:

∀x 1 ...∀x n ∀y ∃z ∀w (w ∈ z ⇔ (w ∈ y ∧ P ))
where x 1 , ..., x n are the free variables of P minus w.

To these axioms, we may add the extensionality axiom, the foundation axiom, the axiom of infinity, the replacement scheme and the axiom of choice.

To have a language for the objects of the theory we may skolemize these axioms introducing the function symbols {}, , P and f x1,...,xn,w,P . We then get the axioms

∀x ∀y ∀w (w ∈ {}(x, y) ⇔ (w = x ∨ w = y)) ∀x ∀w (w ∈ (x) ⇔ ∃z (w ∈ z ∧ z ∈ x)) ∀x ∀w (w ∈ P(x) ⇔ ∀z (z ∈ w ⇒ z ∈ x)) ∀x 1 ...∀x n ∀y ∀w (w ∈ f x1,...,xn,w,P (x 1 , ..., x n , y) ⇔ (w ∈ y ∧ P ))
Then, these axioms may be built in the congruence with the rewrite system of figure 3. This rewrite system is confluent because it is orthogonal. But it does Deduction modulo this congruence does not have the cut elimination property. A counter example is again Crabbé's proposition (see [START_REF] Hallnäs | On normalization of proofs in set theory[END_REF][START_REF] Ekman | Normal proofs in set theory[END_REF] for a discussion). As we have seen, this proposition A rewrites to a proposition of the form B ∧ ¬A. Hence, the proposition ¬B has the following proof

w ∈ {}(x, y) -→ w = x ∨ w = y w ∈ (x) -→ ∃z (w ∈ z ∧ z ∈ x) w ∈ P(x) -→ ∀z (z ∈ w ⇒ z ∈ x) v ∈ fx 1 ,...,
axiom B ⊢ B axiom A ⊢ A weakening-left A, B ⊢ A ¬-left A, B, ¬A ⊢ ∧-left A, A ⊢ contraction-left A ⊢ ¬-right ⊢ ¬A weakening-left B ⊢ ¬A ∧-right B ⊢ A axiom A ⊢ A weakening-left A, B ⊢ A ¬-left A, B, ¬A ⊢ ∧-left A, A ⊢ contraction-left A ⊢ cut B ⊢ ¬-right ⊢ ¬B
but it is easy to check that the proposition ¬B, i.e. ¬f w,¬w∈w (a) ∈ a, has no cut free proof.

3 Resolution modulo in type theory and in set theory

ε( ∨ x y) -→ ε(x) ∨ ε(y) ε( ∀ x) -→ ∀y ε(x y)
rewrite propositions to propositions and are used by the extended narrowing rule.

Equational unification modulo the rules S and K is related to higher-order unification. Actually since the reduction of combinators is slightly weaker than the reduction of λ-calculus, unification modulo this reduction is slightly weaker than higher-order unification [START_REF] Dougherty | Higher-order unification via combinators[END_REF]. To have genuine higher-order unification, we have to take another formulation of type theory using explicit substitutions instead of combinators (see section 5).

The extended narrowing modulo the rules ¬, ∨ and ∀ is exactly the splitting rule of higher-order resolution. A normal literal unifies with the left member of such a rule if and only if its head symbol is a variable.

The skolemization rule in this language is related to the skolemization rule of type theory. When we skolemize a proposition of the form ∀x ∃y P we introduce a function symbol f of rank (T, U ) where T is the type of x and U the type of y (not an individual symbol of type T → U ) and the axiom ∀x [f (x)/y]P Hence, the Skolem symbol f alone is not a term, but it permits to build a term of type U when we apply it to a term of type T . This is, in essence, the higherorder skolemization rule, but formulated for the language of combinators and not for λ-calculus. Again, we have the genuine higher-order skolemization rule if we use the formulation of type theory using explicit substitutions instead of combinators (see section 5).

Resolution modulo in set theory

In set theory, there is no rule rewriting terms to terms. Hence, unification in set theory is simply first-order unification. Converselly, all the rules of figure 3 rewrite propositions to propositions and thus the extended narrowing is performed modulo all theses rules.

In set theory, resolution modulo is incomplete. We have seen that the proposition ¬f w,¬w∈w (a) ∈ a has a proof in set theory, but it cannot be proved by the resolution modulo method. Indeed, from the clausal form of its negation f w,¬w∈w (a) ∈ a we can apply neither the resolution rule nor the extended narrowing rule successfully.

4 On the differences between set theory and type theory

Termination

The first difference between resolution modulo in type theory and in set theory is that the rewrite system is terminating in type theory and hence all propositions have a normal form, while some propositions, e.g. Crabbé's proposition, have no normal form in set theory. Hence, during proof search, we can normalize all the clauses while this is impossible in set theory. Formally, the method modified this way requires a completeness proof.

Completeness

Another difference is that, as type theory verifies the cut elimination property, resolution modulo this congruence is complete, while it is incomplete modulo the congruence of set theory.

A solution to recover completeness may be to use an automated theorem proving method that searches for proofs containing cuts. For instance if we add a rule allowing to refute the set of clauses S by refuting both the set S ∪ {¬P } and the set {P } then we can refute the proposition B above.

Another direction is to search for another presentation of set theory or for a restriction of this theory that enjoys termination and cut elimination. We conjecture that if we restrict the subset scheme to stratifiable propositions in the sense of W.V.O. Quine [START_REF] Quine | Set theory and its logic[END_REF], we get a restriction of set theory that is sufficient to express most mathematics, that terminates and that verifies the cut elimination property. The cut elimination and completeness results obtained by S.C. Bailin [START_REF] Bailin | A normalization theorem for set theory[END_REF][START_REF] Bailin | A λ-unifiability test for set theory[END_REF] for his formulation of set theory let this conjecture be plausible.

Typing literals

A minor difference is that when we try to prove a theorem of the form "for all natural numbers x, P (x)", we have to formalize this theorem by the proposition ∀x (x ∈ N ⇒ P (x)) in set theory. In contrast, in type theory, we can choose to take ι for the type of natural numbers and state the theorem

∀x P (x)
During the search, in set theory, extra literals of the form x ∈ N appear and have to be resolved.

The role of unification and extended narrowing

In resolution modulo, like in most other methods, the main difficulty is to construct the terms that have to be substituted to the variables. In resolution modulo, these terms are constructed by two processes: the unification algorithm and the extended narrowing rule.

The main difference between resolution modulo in type theory and in set theory is the division of work between the unification and the extended narrowing. In type theory, unification is quite powerful and the extended narrowing is rarely used. In contrast, in set theory, unification is simply first-order unification and all the work is done by the extended narrowing rule.

This difference reflects a deep difference on how mathematics are formalized in a theory and the other. Indeed, the unification in type theory is rich because there are rules that rewrite terms to terms and these rules are there because the notion of function is primitive in type theory. When we have a function f and an object a we can form the term (f a) and start rewriting this term to a normal form. In set theory, there is no such term and a term alone can never be reduced. Instead of forming the term (f a) we can form a proposition expressing that b is the image of a by the function f , < a, b >∈ f , that then can be rewritten.

For example, in the proof of Cantor's theorem we have a function f from a set B to its power set and we want to form Cantor's set of objects that do not belong to their image.

If x is an element of B, in type theory we can express its image (f x), then the term of type o reflecting the proposition expressing that x belongs to its image (f x x), the term of type o reflecting its negation ¬(f x x) and then Cantor's set λx ¬(f x x) that, with combinators, is expressed by the term

C = (S (K ¬) (S (S (K f ) (S K K)) (S K K)))
In contrast, in set theory, we cannot form a term expressing the image of x by the function f . Instead of saying that x does not belong to its image we have to say that it does not belong to any objet that happens to be its image.

C = {x ∈ B | ∀y (< x, y >∈ f ⇒ ¬x ∈ y)}
This requires to introduce two more logical symbols ⇒ and ∀. These symbols cannot be generated by the unification algorithm and are generated by the extended narrowing rule.

It is not completely clear what is the best division of work between unification and extended narrowing. Experiences with type theory show that the unification algorithm is usually well controlled while the splitting rule is very productive. Loading the unification and unloading the extended narrowing seems to improve efficiency.

However, two remarks moderate this point of view. First, in type theory, the functions that can be expressed by a term are very few. For instance, if we take the type ι for the natural numbers and introduce two symbols O and Succ for zero and the successor function, we can only express by a term the constant functions and the functions adding a constant to their argument. The other functions are usually expressed with the description operator (or the choice operator) and hence as relations. We may enrich the language of combinators and the rewrite system, for instance with primitive recursion, but then it is not obvious that unification is still so well controlled.

Another remark is that having a decidable and unitary unification (such as first-order unification) permits to solve unification problems on the fly instead of keeping them as constraints. This permits to restrict the use of the extended narrowing rule. For instance, in type theory, when we have a literal ε(P x) and we apply the extended narrowing rule yielding two literals ε(A) and ε(B) and a constraint ε(P x) = ε(A ∨B)

we keep this constraint frozen and we may need to apply the extended narrowing rule to other literals starting with the variable P . In contrast, in set theory, if we have a literal x ∈ P and we apply the extended narrowing rule yielding two literals y = a and y = b and a constraint (x ∈ P ) = (y ∈ {a, b}). The substitution {a, b}/P can be immediately propagated to all the occurrences of P initiating reductions that let the extended narrowing steps be useless.

As an illustration of this discussion, we want to compare resolution modulo proofs of Cantor's theorem in type theory and in set theory. However, the presentations of type theory and set theory above are a little too rough to be really practicable. In both cases, we shall use a more sophisticated presentation where the language contains a full binding operator. Indeed, in type theory, we want to express Cantor's set by the term

C = λx ¬(f x x)
and not by the term

C = (S (K ¬) (S (S (K f ) (S K K)) (S K K)))
Similarily, in set theory we want to express this set as

C = {x ∈ B | ∀y (< x, y >∈ R ⇒ ¬x ∈ y)}
where < x, y > is a notation for the set {{x, y}, {x}} i.e. {}({}(x, y), {}(x, x)), and not by the term

C = {x ∈ B | ∀y (∀u ((∀v (v ∈ u ⇔ (∀w (w ∈ v ⇔ (w = x ∨ w = y)) ∨ ∀w (w ∈ v ⇔ w = x)))) ⇒ u ∈ R) ⇒ ¬x ∈ y)} 1
For type theory, such a first-order presentation with a general binding operator has been proposed in [START_REF] Dowek | HOL-λσ: an intentional first-order expression of higher-order logic[END_REF]. It uses an expression of λ-calculus as a first-order language based on de Bruijn indices and explicit substitutions. In this presentation, the sorts are of the form Γ ⊢ T or Γ ⊢ ∆ where T is a simple type and Γ and ∆ are finite sequences of simple types. The language contains the following symbols

-1 Γ A of sort AΓ ⊢ A, -α Γ A,B of rank (Γ ⊢ A → B, Γ ⊢ A, Γ ⊢ B), -λ Γ A,B of rank (AΓ ⊢ B, Γ ⊢ A → B), -[] Γ,Γ ′ A of rank Γ ′ ⊢ A, Γ ⊢ Γ ′ , Γ ⊢ A), -id Γ of sort Γ ⊢ Γ , -↑ Γ A of sort AΓ ⊢ Γ , 1
In the presentation of set theory above, there is no instance of the subset scheme for the proposition ∀y (< x, y >∈ R ⇒ ¬x ∈ y) because it contains Skolem symbols. Hence, we replace the proposition < x, y >∈ R by the equivalent one

∀u ((∀v (v ∈ u ⇔ (∀w (w ∈ v ⇔ (w = x ∨ w = y)) ∨ ∀w (w ∈ v ⇔ w = x)))) ⇒ u ∈ R)
Then we can build the set C with the function symbol introduced by the skolemization of this instance of the scheme. The proposition x ∈ C is then provably equivalent to x ∈ B ∧ ∀y (< x, y >∈ R ⇒ ¬x ∈ y) but it does not reduce to it.

-. Γ,Γ ′ A of rank (Γ ⊢ A, Γ ⊢ Γ ′ , Γ ⊢ AΓ ′ ), -• Γ,Γ ′ ,Γ ′′ of rank (Γ ⊢ Γ ′′ , Γ ′′ ⊢ Γ ′ , Γ ⊢ Γ ′ ), -∨ of sort ⊢ o → o → o, -¬ of sort ⊢ o → o, -∀T of sort ⊢ (T → o) → o, -ε of rank (⊢ o).
And the rewrite system is that of figure 4.

β-reduction and η-reduction:

(λa)b -→ a[b.id] λ(a 1) -→ b if a =σ b[↑] σ-reduction: (a b)[s] -→ (a[s] b[s]) 1[a.s] -→ a a[id] -→ a (λa)[s] -→ λ(a[1.(s • ↑)]) (a[s])[t] -→ a[s • t] id • s -→ s ↑ • (a.s) -→ s (s1 • s2) • s3 -→ s1 • (s2 • s3) (a.s) • t -→ a[t].(s • t) s • id -→ s 1. ↑-→ id 1[s].(↑ • s) -→ s reduction of propositions: ε( ∨ x y) -→ ε(x) ∨ ε(y) ε( ¬ x) -→ ¬ε(x) ε( ∀T x) -→ ∀y ε(x y)
Fig. 4. The rewrite rules of type theory with explicit substitutions

A formulation of set theory with a general binder has been given in [START_REF] Dowek | Lambda-calculus, combinators and the comprehension scheme[END_REF]. But it is not expressed in a first-order setting yet. Waiting for such a theory, for the example of Cantor's theorem, we add a constant C and an ad hoc rewrite rule

x ∈ C -→ x ∈ B ∧ ∀y (< x, y >∈ R ⇒ ¬x ∈ y)
6 Three proofs of Cantor's theorem

We now give three resolution modulo proofs of Cantor's theorem that there is no surjection from a set to its power set. The first is in type theory with a function expressing the potential surjection from a set to its power set. The second is also in type theory, but this potential surjection is expressed by a relation. The last one is in set theory and the surjection is, of course, expressed by a relation.

Automated theorem proving for Cantor's theorem in type theory is discussed in [START_REF] Huet | Constrained resolution: a complete method for higher order logic[END_REF][START_REF] Huet | A mechanization of type theory[END_REF][START_REF] Andrews | Automating higher-order logic[END_REF].

In type theory with a function

In type theory, a set is expressed by a term of type T → o. Here, we choose to consider only the set of all objects of type ι. Its power set is the set of all objects of type ι → o. Hence we want to prove that there is no surjection from the type ι to ι → o. The first solution is to represent this potential surjection by a function f of type ι → ι → o. The surjectivity of this function can be expressed by the existence of a right-inverse g to this function, i.e. a function of type (ι → o) → ι such that for all x, (f (g x)) = x. Using Leibniz' definition of equality this proposition is written

∀x ∀p (ε(p (f (g x))) ⇔ ε(p x))
Putting this proposition in clausal form yields the clauses

¬ε(P (f (g X))), ε(P X) ε(Q (f (g Y ))), ¬ε(Q Y )
The search is described on figure 5. It returns the empty clause constrained by

1 ¬ε(P (f (g X))), ε(P X) 2 ε(Q (f (g Y ))), ¬ε(Q Y ) 3 narr. (1) ¬ε(P (f (g X))), ¬ε(R)/c1 4 narr. (2) ε(Q (f (g Y ))), ε(S)/c2 5 res. (3, 4) 2/c1, c2, c3, c4, c5 with c1 (P X) = ¬R c2 (Q Y ) = ¬S c3 (P (f (g X))) = R c4 (Q (f (g Y ))) = S c5 (P (f (g X))) = (Q (f (g Y )))
P X) = ¬R (Q Y ) = ¬S (P (f (g X))) = R (Q (f (g Y ))) = S (P (f (g X))) = (Q (f (g Y )))
that have the solution and

X = Y = λ ¬[↑](f [↑] 1 1) P = Q = λ(1 (g[↑] λ ¬[↑ 2 ](f [↑ 2 ] 1 1))) R = S = (f (g λ ¬[↑](f [↑] 1 1)) (g λ ¬[↑](f [↑] 1 1))) 6
F : ∀x ∀y ∀z (ε(R x y) ⇒ ε(R x z) ⇒ ∀p (ε(p y) ⇔ ε(p z)))
Putting these propositions in clausal form yields the clauses

ε(R g(U ) U ) ¬ε(R X Y ), ¬ε(R X Z), ¬ε(P Y ), ε(P Z) ¬ε(R X Y ), ¬ε(R X Z), ¬ε(P Z), ε(P Y )
The search is then described on figure 6 where we simplify the constraints and substitute the solved constraints at each step. It returns the empty clause constrained by the equations

(P Y ) = ¬ ∀G 1 (G 1 W 1 ) = ¬(R g(U 1 ) U 1 ) ∨ ¬ ∀G 2 (G 2 y 1 ) = ¬A 2 ∨ ¬B 2 (G 1 W ′ 1 ) = ¬A 2 ∨ ¬B 2 (P Y ) = ¬ ∀G 3 (G 3 y 2 ) = ¬(R g(Y ′ ) Z ′ ) ∨ ¬B 3 (P Z ′ ) = ¬B 3 (P Y ′ ) = ¬ ∀G 4 (G 4 W 2 ) = ¬(R g(U 2 ) U 2 ) ∨ ¬ ∀G 5 (G 5 y 3 ) = ¬A 5 ∨ ¬B 5 (G 4 W ′
2 ) = ¬A 5 ∨ ¬B 5

Remarks

The termination and completeness issues are not addressed by these examples because, even in set theory, Cantor's theorem has a cut free proof and the search involves only terminating propositions. The proof in set theory is longer because several steps are dedicated to the treatment of typing literals that are repeatedly resolved with the clause [START_REF] Dowek | HOL-λσ: an intentional first-order expression of higher-order logic[END_REF].

In type theory with a function, only two extended narrowing steps are needed to generate the symbol ¬ in the term λ ¬[↑](f [↑] 1 1) (i.e. λx ¬(f x x)) that expresses Cantor's set. In type theory with a relation, four extended narrowing steps are needed to generate the term λ ∀

[↑]λ ( ¬[↑ 2 ](R[↑ 2 ] 2 1) ∨[↑ 2 ] ¬[↑ 2 ](1 2
)) (i.e. λx ∀λy ( ¬(R x y) ∨ ¬(y x))) that expresses Cantor's set. The term expressing Cantor set is thus mostly constructed by the unification algorithm in the first case and mostly constructed by the extended narrowing rule in the second. In set theory, like in type theory with a relation, the term expressing Cantor's set is mostly constructed by the extended narrowing rule.

In this case, a single step is needed because we have taken the ad hoc rule

x ∈ C -→ x ∈ B ∧ ∀y (< x, y >∈ R ⇒ ¬x ∈ y)

But in a reasonable formulation of set theory several steps would be needed. Notice, at last, that in the proof in type theory with a relation, the term expressing Cantor's set is constructed several times, because the constraints are frozen while in set theory, because the constraints are solved on the fly, this term is constructed only twice and propagated. To avoid this redundancy in type theory with a relation, it would be a good idea to solve as soon as possible the constraints c 1 and c 2 .

Conclusion

Using a single automated theorem proving method for type theory and for set theory permits a comparison.

Although the use of a typed (many-sorted) language can be criticized, type theory has several advantages for automated theorem proving: typing permits to avoid typing literals, it enjoys termination and cut elimination, and the possibility to form a term (f a) expressing the image of an object by a function avoids indirect definitions.

This motivates the search of a type-free formalization of mathematics, that also enjoys termination and cut elimination and where functions are primitive.

Fig. 1 .

 1 Fig. 1. Resolution modulo

Fig. 2 .

 2 Fig. 2. Rewriting rules for simple type theory

Fig. 3 .

 3 Fig. 3. Rewriting rules for set theory

3. 1

 1 Resolution modulo in type theoryIn the rewrite system of figure2, the first two rules (S x y z) -→ (x z (y z)) (K x y) -→ x rewrite terms to terms and are used by the unification algorithm. The three others ε( ¬ x) -→ ¬ε(x)

Fig. 5 .

 5 Fig. 5. Cantor's theorem in type theory with a function

. 2

 2 In type theory with a relation Instead of using the primitive notion of function of set theory, we can code the functions as functional relations R of type ι → (ι → o) → o. The surjectivity and functionality of this relation are expressed by the propositions E : ∀y ∃x ε(R x y)

¬ε(R X Y ), ¬ε(R X Z), ¬ε(P Y ), ε(P Z) 3 ¬ε(R X Y ), ¬ε(R X Z), ¬ε(P Z), ε(P Y ) 4 res. (1,[START_REF] Andrews | An introduction to mathematical logic and type theory: to truth through proof[END_REF] ¬ε(R g(Y ) Z), ¬ε(P Y ), ε(P Z) 5 res. (1,[START_REF] Bailin | A normalization theorem for set theory[END_REF] ¬ε(P Y ), ε(P Y ) 6 five narr. ( 5) ¬ε(A1), ¬ε(B1), ε(P Y )/c1, c2 7 res. [START_REF] Church | A formulation of the simple theory of types[END_REF]1) ¬ε(B1), ε(P Y )/c1, c ′ 2 8 four narr. (7) 18)

res. [START_REF] Klop | Combinatory reduction systems: introduction and survey[END_REF][START_REF] Hullot | Canonical forms and unification[END_REF] ¬ε

In set theory

We consider a set B and a potential surjection from this set to its power set. We express this potential surjection by a set R. The surjectivity and functionality of this set are expressed by the propositions

We use also the axiom of equality L : ∀z ∀x ∀y (x = y ⇒ ¬z ∈ x ⇒ ¬z ∈ y)

The proposition E reduces to the proposition

Putting this proposition in clausal form yields the clauses

The two other propositions yield the clauses

The search is described on figure 7 where we simplify the constraints and substitute the solved constraints at each step. Propagating the solved constraints may lead to new reductions that require to put the proposition in clausal form again. This explains that some resolution steps yield several clauses. It returns the empty clause.


Peter Clote
email: clote@bc.edu

Evangelos Kranakis
email: evankranakis@gmail.com

Danny Krizanc
email: dkrizanc@wesleyan.edu

Bruno Salvy
email: bruno.salvy@inria.fr

Asymptotics of Canonical and Saturated RNA Secondary Structures

It is a classical result of Stein and Waterman that the asymptotic number of RNA secondary structures is 1.104366 • n -3/2 • 2.618034 n . In this paper, we study combinatorial asymptotics for two special subclasses of RNA secondary structures -canonical and saturated structures. Canonical secondary structures are defined to have no lonely (isolated) base pairs. This class of secondary structures was introduced by Bompfünewerer et al., who noted that the run time of Vienna RNA Package is substantially reduced when restricting computations to canonical structures. Here we provide an explanation for the speed-up, by proving that the asymptotic number of canonical RNA secondary structures is 2.1614 • n -3/2 • 1.96798 n and that the expected number of base pairs in a canonical secondary structure is 0.31724 • n. The asymptotic number of canonical secondary structures was obtained much earlier by Hofacker, Schuster and Stadler using a different method.

 to show that the density of states for [all resp. canonical resp. saturated] secondary structures is asymptotically Gaussian. We introduce a stochastic greedy method to sample random saturated structures, called quasi-random saturated structures, and show that the expected number of base pairs of is 0.340633 • n.

Introduction

Imagine an undirected * graph, described by placing graph vertices 1, . . . , n along the periphery of a circle in a counter-clockwise manner, and placing graph edges as chords within the circle. An outerplanar graph is a graph whose circular representation is planar; i.e. there are no crossings. An RNA secondary structure, formally defined in Section 2, is an outerplanar graph (no pseudoknots) with the property that no vertex is incident to more than one edge (no base triples) and that for every chord between vertices i, j, there exist at least θ = 1 many vertices that are not incident to any edge (hairpin requirement). RNA secondary structure is equivalently defined to be a well-balanced parenthesis expression s 1 , . . . , s n with dots, where if nucleotide i is unpaired then s i = •, while if there is a base pair between nucleotides i < j then s i = ( and s j = ) . This latter representation is known as the Vienna representation or dot bracket notation (dbn).

Formally, a well-balanced parenthesis expression w 1 • • • w n can be defined as follows. If Σ denotes a finite alphabet, and α ∈ Σ, and w = w 1 • • • w n ∈ Σ * is an arbitrary word, or sequence of characters drawn from Σ, then |w| α designates the number of occurrences of α in w. Letting Σ = { ( , ) }, a word w = w

1 • • • w n ∈ Σ * is well-balanced if for all 1 ≤ i < n, |w 1 • • • w i | ( ≥ |w 1 • • • w i | ) and |w 1 • • • w n | ( = |w 1 • • • w n | ) .
Finally, when considering RNA secondary structures, we consider instead the alphabet Σ = { ( , ) , • }, but otherwise the definition of well-balanced expression remains unchanged. The number of well-balanced parenthesis expressions of length n over the alphabet Σ = { ( , ) } is known as the Catalan number C n , while that over the alphabet Σ = { ( , ) , • } is known as the Motzkin number M n [START_REF] Donaghey | Motzkin numbers[END_REF]. Stein and Waterman [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF] computed the number S n of well-balanced parenthesis expressions in the alphabet Σ = { ( , ) , • }, where there exist at least θ = 1 occurrences of • between corresponding left and right parentheses ( respectively ) . It follows that S n is exactly the number of RNA secondary structures on [1, n], where there exist at least θ = 1 unpaired bases in every hairpin loop.

In this paper, we are interested in specific classes of secondary structure: canonical and saturated structures. A secondary structure is canonical [START_REF] Bompfunewerer | Variations on RNA folding and alignment: lessons from Benasque[END_REF] if it has no lonely (isolated) base pairs. A secondary structure is saturated [START_REF] Zuker | RNA folding prediction: The continued need for interaction between biologists and mathematicians[END_REF] if no base pairs can be added without violating the notion of secondary structure, formally defined in Section 2. In order to compute parameters like asymptotic value for number of structures, expected number of base pairs, etc. throughout this paper, we adopt the model of Stein and Waterman [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF]. In this model, any position (nucleotide, also known as base) can pair with any other position, and every hairpin loop must contain at least θ = 1 unpaired bases; i.e. if i, j are paired, then ji > θ. This latter condition is due to steric constraints for RNA. At the risk of additional effort, the combinatorial methods of this paper could be applied to handle the situation of most secondary structure software, which set θ = 3.

Examples of secondary structure representations

.)))))....)))))...))))))))))).
Equivalent representations for the same secondary structure may be produced by software jViz [START_REF] Wiese | Rna-a Java tool for RNA secondary structure visualization[END_REF], as depicted in Figure 1. The left panel of this figure depicts the circular Feynman diagram (i.e. outerplanar graph representation), the middle panel depicts the linear Feynman diagram, and the right panel depicts the classical representation. This latter representation, most familiar to biologists, may also be obtained by RNAplot from the Vienna RNA Package [START_REF] Hofacker | Vienna RNA secondary structure server[END_REF]. [START_REF] Szymanski | 5S ribosomal RNA database Y2K[END_REF], and the graph was created using jViz [START_REF] Wiese | Rna-a Java tool for RNA secondary structure visualization[END_REF].

Outline and results of the paper

In Section 2, we review a combinatorial method, known as the DSV methodology and the important Flajolet-Odlyzko Theorem, which allows one to obtain asymptotic values of Taylor coefficients of analytic generating functions f (z) = ∞ i=1 a i z i by determining the dominant singularity of f . The description of the DSV methodology and Flajolet-Odlyzko theorem is not meant to be self-contained, although we very briefly describe the broad outline. For a very clear review of this method, with a number of example applications, please see [START_REF] Lorenz | Asymptotics of rna shapes[END_REF] or the recent monograph of Flajolet and Sedgewick [START_REF] Flajolet | Analytic Combinatorics[END_REF].

In Section 2.1, we compute the asymptotic number 2.1614 • n -3/2 • 1.96798 n of canonical secondary structures, obtaining the same value obtained by Hofacker, Schuster and Stadler [START_REF] Hofacker | Combinatorics of RNA secondary structures[END_REF] by a different method, known as the Bender-Meir-Moon method. In Section 2.2 we compute the expected number 0.31724•n of base pairs in canonical secondary structures. In Section 2.3, we apply the DSV methodology to compute the asymptotic number 1.07427 • n -3/2 • 2.35467 n of saturated structures, while in Section 2.4, we compute the expected number 0.337361 • n of base pairs of saturated structures. In Section 2.5, we compute the asymptotic number 0.323954 • 1.69562 n of saturated stem-loop structures, which is substantially smaller than the number 2 n-2 -1 of (all) stem-loop structures, as computed by Stein and Waterman [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF].

In Section 3, we consider a natural stochastic process to generate random saturated structures, called in the sequel quasi-random saturated structures. The stochastic process adds base pairs, one at a time, according to the uniform distribution, without violating any of the constraints of a structure. The main result of this section is that asymptotically, the expected number of base pairs in quasi-random saturated structures is 0.340633 • n, rather close to the expected number 0.337361 • n of base pairs of saturated structures. The numerical proximity of these two values suggests that stochastic greedy methods might find application in other areas of random graph theory. In Section 4 we provide some concluding remarks.

At the web site http://bioinformatics.bc.edu/clotelab/SUPPLEMENTS/JBCBasymptotics/, we have placed Python programs and Mathematica code used in computing and checking the asymptotic number of canonical and saturated secondary structures, as well as the Maple code for checking Drmota's [START_REF] Drmota | Systems of functional equations[END_REF] conditions to deduce the asymptotic normality of the density of states of RNA structures.

DSV methodology

In this section, we describe a combinatorial method sometimes called DSV methodology, after Delest, Schützenberger and Viennot, which is a special case of what is called the symbolic method in combinatorics, described at length in [START_REF] Flajolet | Analytic Combinatorics[END_REF]. See also the Appendix of [START_REF] Lorenz | Asymptotics of rna shapes[END_REF] for a detailed presentation of this method. This method enables one to obtain information on the number of combinatorial configurations defined by finite rules, for any size. This is done by translating those rules into equations satisfied by various generating functions. A second step is to extract asymptotic expansions from these equations. This is done by studying the singularities of these generating functions viewed as analytic functions.

Since our goal is to derive asymptotic numbers of structures, following standard convention we define an RNA secondary structure on a length n sequence to be a set of ordered pairs (i, j), such that 1 ≤ i < j ≤ n and the following are satisfied.

1. Nonexistence of pseudoknots: If (i, j) and (k, ℓ) belong to S, then it is not the case that i < k < j < ℓ.

2.

No base triples: If (i, j) and (i, k) belong to S, then j = k; if (i, j) and (k, j) belong to S, then i = k.

3. Threshold requirement: If (i, j) belongs to S, then ji > θ, where θ, generally taken to be equal to 3, is the minimum number of unpaired bases in a hairpin loop; i.e. there must be at least θ unpaired bases in a hairpin loop.

Note that the definition of secondary structure does not mention nucleotide identity -i.e. we do not require base-paired positions (i, j) to be occupied by Watson-Crick or wobble pairs. For this reason, at times we may say that S is a secondary structure on [1, n], rather than saying that S is a structure for RNA sequence of length n. In particular, an expression such as "the asymptotic number of structures is f (n)" means that the asymptotic number of structures on [1, n] is f (n).

Grammars

We now proceed with basic definitions related to context-free grammars. If A is a finite alphabet, then A * denotes the set of all finite sequences (called words) of characters drawn from A. Let Σ be the set consisting of the symbols for left parenthesis ( , right parenthesis

) , and dot •, used to represent a secondary structure in Vienna notation. A context-free grammar (see, e.g., [START_REF] Lewis | Elements of the Theory of Computation[END_REF]) for RNA secondary structures is given by G = (V, Σ, R, S 0 ), where V is a finite set of nonterminal symbols (also called variables), Σ = {•, ( , ) }, S 0 ∈ V is the start nonterminal, and

R ⊆ V × (V ∪ Σ) *
is a finite set of production rules. Elements of R are usually denoted by A → w, rather than (A, w). If rules A → α 1 ,. . . , A → α m all have the same left-hand side, then this is usually abbreviated by

A → α 1 | • • • |α m . If x, y ∈ (V ∪ Σ) *
L(G) = {w ∈ Σ * : S 0 ⇒ * G w}.
For any nonterminal S ∈ V , we also write L(S) to denote the language generated by rules from G when using start symbol S. A derivation of word w from start symbol S 0 using grammar G is a leftmost derivation, if each successive rule application is applied to replace the leftmost nonterminal occurring in the intermediate expression. A context-free grammar G is non-ambiguous, if there is no word w ∈ L(G) which admits two distinct leftmost derivations. This notion is important since it is only when applied to non-ambiguous grammars that the DSV methodology leads to exact counts. For the sake of readers unfamiliar with context-free grammars, we present some examples to illustrate the previous concepts. Consider the following grammar G, which generates the collection of well-balanced parenthesis strings, including the empty string. † Define G = (V, Σ, R, S), where the set V of variables (also known as nonterminals) is {S}, the set Σ of terminals is { ( , ) }, where S is the start symbol, and where the set R of rules is given by

S → ǫ| ( S ) |SS
Here ǫ denotes the empty string. We claim that G is an ambiguous grammar. Indeed, consider the following two leftmost derivations, where we denote the order of rule applications r1 := S → ǫ, r2 := S → SS, r3 := S → ( S ) , by placing the rule designator under the arrow. Clearly the leftmost derivation

S → r2 SS → r2 SSS → r3,r1 ( ) SS → r3,r1 ( ) ( ) S → r3,r1 ( ) ( ) ( ) is distinct from the leftmost derivation S → r2 SS → r3,r1 ( ) S → r2 ( ) ( S ) S → r3,r1 ( ) ( ) S → r2 ( ) ( ) ( S ) → r1 ( ) ( ) ( )
yet both generate the same well-balanced parenthesis string. For the same reason, the grammar with rules

S → • | • S| ( S ) |SS Type of nonterminal Equation for the g.f. S → T | U S(z) = T (z) + U (z) S → T U S(z) = T (z)U (z) S → t S(z) = z S → ε S(z) = 1
Table 1: Translation between context-free grammars and generating functions. Here, G = (V, Σ, R, S 0 ) is a given context-free grammar, S, T and U are any nonterminal symbols in V , and t is a terminal symbol in Σ. The generating functions for the languages L(S), L(T ), L(U ) are respectively denoted by S(z), T (z), U (z).

generates precisely the collection of non-empty RNA secondary structures, yet this grammar is ambiguous, and we would obtain an overcount by applying the DSV methodology. In contrast, the grammar whose rules are

S → • | • S| ( S ) | ( S ) S
is easily seen to be non-ambiguous and to generate all non-empty RNA secondary structures.

Generating Functions

Suppose that G = (V, Σ, R, S) is a non-ambiguous context-free grammar which generates a collection L(S) of objects (e.g. canonical secondary structures). To this grammar is associated a generating function S(z) = ∞ n=0 s n z n , such that the nth Taylor coefficient [z n ]S(z) = s n represents the number of objects we wish to count. In the sequel, s n will represent the number of canonical secondary structures for RNA sequences of length n. The DSV method uses Table 1 in order to translate the grammar rules of R into a system of equations for the generating functions.

Asymptotics

In the sequel, we often compute the asymptotic value of the Taylor coefficients of generating functions by first applying the DSV methodology, then using a simple corollary of a result of Flajolet and Odlyzko [START_REF] Flajolet | Singularity analysis of generating functions[END_REF]. That corollary is restated here as the following theorem.

Theorem 1 (Flajolet and Odlyzko) Assume that S(z) has a singularity at z = ρ > 0, is analytic in the rest of the region △\1, depicted in Figure 2, and that as z → ρ in △,

S(z) ∼ K(1 -z/ρ) α .
(1)

Then, as n → ∞, if α / ∈ 0, 1, 2, ..., s n ∼ K Γ(-α) • n -α-1 ρ -n .
It is a consequence of Table 1 that the generating series of context-free grammars are algebraic (this is the celebrated theorem of Chomsky and Schützenberger [START_REF] Chomsky | The algebraic theory of context-free languages[END_REF]). In particular this implies that they have positive radius of convergence, a finite number of singularities, and their behaviour in the neighborhood of their singularities is of the type (1). (See [START_REF] Flajolet | Analytic Combinatorics[END_REF] for an extensive treatment.) A singularity of minimal modulus as in Theorem 1 is called a dominant singularity. The location of the dominant singularity may be a source of difficulty. The simple case is when an explicit expression is obtained for the generating functions; this happens for canonical secondary structures. The situation when only the system of polynomial equations is available is more involved; we show how to deal with it in the case of saturated structures.

Asymptotic number of canonical secondary structures

In Bompfünewerer et al. [START_REF] Bompfunewerer | Variations on RNA folding and alignment: lessons from Benasque[END_REF], the notion of canonical secondary structure S is defined as a secondary structure having no lonely (isolated) base pairs; i.e. formally, there are no base pairs (i, j) ∈ S for which both (i -1, j + 1) ∈ S and (i + 1, j -1) ∈ S. In this section, we compute the asymptotic number of canonical secondary structures. Throughout this section, secondary structure is interpreted to mean a secondary structure on an RNA sequence of length n, for which each base can pair with any other base (not simply Watson-Crick and wobble pairs), and with minimum number θ of unpaired bases in every hairpin loop set to be 1. At the cost of working with more complex expressions, by the same method, one could analyze the case when θ = 3, which is assumed for the software mfold [START_REF] Zuker | Mfold web server for nucleic acid folding and hybridization prediction[END_REF] and RNAfold [START_REF] Hofacker | Vienna RNA secondary structure server[END_REF].

Grammar

Consider the context-free grammar G = (V, Σ, R, S), where V consists of nonterminals S, R, Σ consists of the terminals • , ( , ) , S is the start symbol and R consists of the following rules:

S → •|S • | ( R ) |S ( R ) (2) R → ( • ) | ( R ) | ( S ( R ) ) | ( S • )
The nonterminal S is intended to generate all nonempty canonical secondary structures. In contrast, the nonterminal R is intended to generate all secondary structures which become canonical when surrounded by a closing set of parentheses. We prove by induction on expression length that the grammar G is non-ambiguous and generates all nonempty canonical secondary structures.

Define context-free grammar G R to consist of the collection R of rules from G, defined above, with starting nonterminal S, respectively. Formally,

G R = (V, Σ, R, R).
Let L(G), L(G R ) denote the languages generated respectively by grammars G, G R . Now define languages L 1 , L 2 of nonempty secondary structures with θ = 1 by

L 1 = {S : S is canonical} L 2 = {S : ( S ) is canonical}. Note that structures like • • ( • ) and ( • ) ( • ) belong to L 1 , but not to L 2 , while structures like ( ( • ) ) belong to both L 1 , L 2 .
Note that any structure S belonging to L 2 must be of the form ( S 0 ) ; indeed, if S were not of this form, but rather of the form either • S 0 or ( S 0 ) S 1 , then by ( S ) would have an outermost lonely pair of parentheses.

Claim. L 1 = L(G), L 2 = L(G R ). Proof of Claim. Clearly L 1 ⊇ L(G), L 2 ⊇ L(G R
), so we show the reverse inclusions by induction; i.e. by induction on n, we prove that

L 1 ∩ Σ n ⊆ L(G) ∩ Σ n , L 2 ∩ Σ n ⊆ L(G R ) ∩ Σ n . Base case: n = 1. Clearly L(G) ∩ Σ = { • } = L 1 ∩ Σ, L(G R ) ∩ Σ = ∅ = L 2 ∩ Σ.
Induction case: Assume that the claim holds for all n < k. Subcase 1. Let S be a canonical secondary structure with length |S| = k > 1. Then either (1) S = • S 0 , where S 0 ∈ L 1 , or (2) S = ( S 0 ) , where S 0 ∈ L 2 , or (3) S = ( S 0 ) S 1 , where S 0 ∈ L 2 and S 1 ∈ L 1 . Each of these cases corresponds to a different rule having left side S, hence by the induction hypothesis, it follows that S ∈ L(G). Subcase 2. Let S ∈ L 2 be a secondary structure with length |S| = k > 1, for which ( S ) is canonical. If S were of the form • S 0 or ( S 0 ) S 1 , then ( S ) would not be canonical, since its outermost parenthesis pair would be a lonely pair. Thus S is of the form ( S 0 ) , where either (1) S 0 begins with • , or (2) S 0 is of the form ( S 1 ) , where S 1 is not canonical, but ( S 1 ) becomes canonical, or (3) S 0 is of the form ( S 1 ) , where S 1 is canonical and ( S 1 ) is canonical as well.

In case (1), S 0 is either • or • S 1 , where S 1 is canonical. In case (2), S 0 is of the form ( S 1 ) , where S 1 must have the property that ( S 1 ) is canonical. In case (3), S 0 is of the form ( S 1 ) S 2 , where it must be that ( S 1 ) is canonical and S 2 is canonical. By applying corresponding rules and the induction hypothesis, it follows that S ∈ L(G R ).

It now follows by induction that

L 1 = L(G), L 2 = L(G R ).
A similar proof by induction shows that the grammar G is non-ambiguous.

Generating Functions

Now, let s n denote the number of canonical secondary structures on a length n RNA sequence. Then s n is the nth Taylor coefficient of the generating function S(z) = n≥0 s n z n , denoted by s n = [z n ]S(z). Similarly, let R(z) = n≥0 R n z n be the generating function for the number of secondary structures on [1, n] with θ = 1, which become canonical when surrounded by a closing set of parentheses.

By Table 1, the non-ambiguous grammar (2) gives the following equations

S(z) = z + S(z)z + R(z)z 2 + S(z)R(z)z 2 (3) R(z) = z 3 + R(z)z 2 + S(z)R(z)z 4 + S(z)z 3 (4)
which can be solved explicitly (solve the second equation for R and inject this in the first equation):

S(z) = 1 -z -z 2 + z 3 -z 5 -F (z) 2z 4 (5)
and

S(z) = 1 -z -z 2 + z 3 -z 5 + F (z) 2z 4 (6)
where

F (z) = 4z 5 -1 + z 2 -z 4 + -1 + z + z 2 -z 3 + z 5 2 . ( 7
)
When evaluated at z = 0, Equation ( 6) gives lim r→0 S(z) = ∞. Since S(z) is known to be analytic at 0, we conclude that S(z) is given by ( 5).

Location of the dominant singularity

The square root function √ z has a singularity at z = 0, so we are led to investigate the roots of F (z). A numerical computation with Mathematicaç gives the 10 roots 0.508136, 4.11674, -0.868214-0.619448i, -0.868214+0.619448i, -0.799805-0.367046i, -0.799805+0.367046i, 0.410134 -0.564104i, 0.410134 + 0.564104i, 0.945448 -0.470929i, 0.945448 + 0.470929i. It follows that ρ = 0.508136 is the root of F (z) having smallest (complex) modulus.

Asymptotics

Let T (z) = 1-z-z 2 +z 3 -z 5 2z 4

and factor 1z/ρ out of F (z) to obtain

Q(z)(1 -z/ρ) = F (z). It follows that S(z) -T (ρ) = Q(ρ) 2ρ 4 • (1 -z/ρ) α + O(1 -z/ρ), z → ρ,
where α = 1/2. This shows that ρ is indeed a dominant singularity for S. Note that for each n ≥ 1, S(z) and S(z) -T (ρ) have the same Taylor coefficient of index n, namely s n . Now, it is a direct consequence of Theorem 1 that

s n ∼ K(ρ) Γ(-α) • n -α-1 • (1/ρ) n , n → ∞ (8)
where α = 1/2 and K(z) = √ Q(z) 2z 4 . Plugging ρ = 0.508136 into equation ( 8), we derive the following theorem, first obtained by Hofacker, Schuster and Stadler [START_REF] Hofacker | Combinatorics of RNA secondary structures[END_REF] by a different method.

Theorem 2 The asymptotic number of canonical secondary structures on

[1, n] is 2.1614 • n -3/2 • 1.96798 n . (9)

Asymptotic expected number of base pairs in canonical structures

In this section, we derive the expected number of base pairs in canonical secondary structures on [1, n].

Generating Functions

The DSV methodology is actually able to produce multivariate generating series. Modifying the equations [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF][START_REF] Donaghey | Motzkin numbers[END_REF] by adding a new variable u, intended to count the number of base pairs, we get

S(z, u) = z + S(z, u)z + R(z, u)uz 2 + S(z, u)R(z, u)uz 2 (10) R(z, u) = uz 3 + R(z, u)uz 2 + S(z, u)R(z, u)u 2 z 4 + S(z, u)uz 3 . ( 11
)
This can be solved as before to yield the solution

‡ S(z, u) = n≥0 k≥0 s n,k z n u k = 2u 2 z 4 1 -z -uz 2 + uz 3 -u 2 z 5 - 4u 2 z 5 (-1 + uz 2 -u 2 z 4 ) + (-1 + z + uz 2 -uz 3 + u 2 z 5 ) 2
Here, the coefficient s n,k is the number of canonical secondary structures of size n with k base pairs. Using a classical observation on multivariate generating functions, we recover the expected number of base pairs in a canonical secondary structure on [1, n] using the partial derivative of S(z, u); indeed,

[z n ] ∂S(z,u) ∂u (z, 1) [z n ]S(z, 1) = [z n ] i≥0 k≥0 s i,k z i ku k-1 (z, 1) s n = k≥0 s n,k k s n = k≥0 k s n,k s n ,
and s n,k /s n is the (uniform) probability that a canonical secondary structure on [1, n] has exactly k base pairs. We compute that G(z) = ∂S(z,u) ∂u (z, 1) satisfies

G(z) = -(z 2 -2)(T (z) -F (z) + z F (z)) 2z 4 F (z)
where T (z) = (1 -2z + 2z 3z 4 -3z 5 + z 6 ) and F (z) is as in [START_REF] Flajolet | Singularity analysis of generating functions[END_REF]. Simplification yields

G(z) = -(z 2 -2)(z -1) 2z 4 - T (z)(z 2 -2) 2z 4 • 1 F (z) .

Asymptotics

From this expression, it is clear that the dominant singularity is again located at the same ρ = 0.508136. A local expansion there gives

G(z) ∼ K(ρ)(1 -z/ρ) -1/2 , z → ρ with K(z) = -Q(z) -1/2 T (z)(z 2 -2) 2z 4
. By Theorem 1, we obtain the asymptotic value

K(ρ) Γ(-α) • n -3/2 • (1/ρ) n . ( 12
)
Plugging ρ = 0.508136 into equation ( 12), we find the asymptotic value of [z n ] ∂S(z,u) ∂u (z, 1) is

0.68568 • n -1/2 • 1.96798 n . ( 13
)
Dividing ( 13) by the asymptotic number [z n ]S(z) of canonical secondary structures, given in ( 9), we have the following theorem.

Theorem 3

The asymptotic expected number of base pairs in canonical secondary structures is 0.31724 • n.

Asymptotic number of saturated structures

An RNA secondary structure is saturated if it is not possible to add any base pair without violating the definition of secondary structures. If one models the folding of an RNA secondary structure as a random walk on a Markov chain (i.e. by the Metropolis-Hastings algorithm), then saturated structures correspond to kinetic traps with respect to the Nussinov energy model [START_REF] Nussinov | Fast algorithm for predicting the secondary structure of single stranded RNA[END_REF]. The asymptotic number of saturated structures was determined in [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF] by using a method known as Bender's Theorem, as rectified by Meir and Moon [START_REF] Meir | On an asymptotic method in enumeration[END_REF]. In this section, we apply the DSV methodology to obtain the same asymptotic limit, and in the next section we obtain the expected number of base pairs of saturated structures.

Grammar

Consider the context-free grammar with nonterminal symbols S, R, terminal symbols •, ( , ) , start symbol S and production rules

S → •| • •|R • |R • •| ( S ) |S ( S ) (14) R → ( S ) |R ( S ) (15)
It can be shown by induction on expression length that L(S) is the set of saturated structures, and L(R) is the set of saturated structures with no visible position; i.e. external to every base pair [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF]. Here, position i is visible in a secondary structure T if it is external to every base pair of T ; i.e. for all (x, y) ∈ T , i < x or i > y.

Generating Functions

Let

S(z) = ∞ i=0 s i • z i , R(z) = ∞ i=0 r i • z i (16)
denote the generating functions S resp. R, corresponding to the problems of counting number of saturated secondary structures resp. number of saturated structures having no visible positions. Applying Table 1,we are led to the equations

S = z + z 2 + zR + z 2 R + z 2 S + z 2 S 2 (17) R = z 2 S + z 2 RS. ( 18
)
Location of the dominant singularity By first solving [START_REF] Flajolet | Analytic Combinatorics[END_REF] for R and injecting in ( 17), we get

S = z + z 2 + z 2 S + z 2 S 2 + (z + z 2 ) z 2 S 1 -z 2 S , (19)
which upon normalizing gives a polynomial equation of the third degree

P (z, S) = -S 3 z 4 + z(1 + z) -S 2 z 2 -2 + z 2 + S -1 + z 2 = 0. (20)
Unlike earlier work in this paper, direct solution of this equation by Cardano's formulas gives expressions that are difficult to handle. Instead, we locate the singularity by appealing to general techniques for implicit generating functions [START_REF] Flajolet | Analytic Combinatorics[END_REF]VII.4]. By the implicit function theorem, singularities of P (z, S) only occur when both P and its partial derivative

∂P ∂S (z, S) = -1 + (1 + 4S)z 2 -S(2 + 3S)z 4 (21)
vanish simultaneously.

The common roots of P and ∂P/∂S can be located by eliminating S between those two equations, for instance using the classical theory of resultants (see, e.g., [START_REF] Lang | Algebra[END_REF]). This gives a polynomial

Q(z) = z 11 (1 + z)(4 + z -7z 2 -28z 3 -32z 4 + 4z 6 ), (22)
that vanishes at all z such that (z, S) is a common root of P and ∂P/∂S. Numerical computation of the roots of Q yields 0, -1, -2.29493, -0.854537, -0.244657 -0.5601i, -0.244657 + 0.5601i, 0.424687, 3.2141.

A subtle difficulty now lies in selecting among those points the dominant singularity of the analytic continuation of the solution S of (19) corresponding to the combinatorial problem. Indeed, it is possible that one solution of ( 19) is singular at a given r without the solution of interest being singular there. Considering such a singularity would result in an asymptotic expansion that is wrong by an exponential factor. One way to select the correct singularity is to apply a result by Meir and Moon [START_REF] Meir | On an asymptotic method in enumeration[END_REF] to Equation [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF]. This results in a variant of the computation in [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF].

Instead, we use Pringsheim's theorem (see, e.g., [START_REF] Flajolet | Analytic Combinatorics[END_REF]).

Theorem 4 (Pringsheim) If S(z) has a series expansion at 0 that has nonnegative coefficients and a radius of convergence R, then the point z = R is a singularity of S(z).

In our example, there are only two possible real positive singularities, 0.424687 and 3.2141. The latter cannot be dominant, since it would lead to asymptotics of the form 3.2141 -n , i.e., an exponentially decreasing number of structures. Thus the dominant singularity is at ρ = 0.424687. Since the moduli of the non-real roots of Q is 0.611203 > ρ, the conditions of Theorem 1 hold, provided the function behaves as required as z → ρ.

Asymptotics

We now compute the local expansion of S(z) at ρ. From equation ( 21), we have that

P (ρ, S) = 0.605047 -0.819641S + 0.328189S 2 -0.0325295S 3 (23)
whose (numerical approximations of) roots are the double root S = 1.6569 and single root S = 6.77518. It is easily checked that 1.6569 is the only root of equation ( 23) in which P (ρ, S) is increasing; thus we let T = 1.6569. Recall Taylor's theorem in two variables

f (x, y) = ∞ n=0 ∞ k=0 ∂ n+k f (x 0 , y 0 ) ∂x n ∂y k • (x -x 0 ) n n! • (y -y 0 ) k k! .
We now expand P (z, S) at z = ρ and S = T and invert this expansion. This yields

P (z, S) = P (ρ, T ) + ∂P ∂S (ρ, T )(S -T ) + ∂P ∂z (ρ, T )(z -ρ) + 1 2
∂ 2 P ∂S 2 (ρ, T )(S -T ) 2 + • • • (24)
where the dots indicate terms of higher order. The first two terms are 0, so by denoting P z = ∂P ∂z (ρ, T ) and P SS = ∂ 2 P ∂S 2 (ρ, T ), we have

0 = P = P z (z -ρ) + 1 2 P zz (S -T ) 2 + O(S -T ) 3 + O((z -ρ)(S -T ) 2 ) + O((z -ρ) 2
). ( 25)

Isolating (S -T ) 2 we get (S -T ) 2 = -2P z (z -ρ) P SS + O((z -ρ) 2 ) + O((S -T ) 3 ) S -T = ± 2ρP z P SS • 1 -z/ρ + O(z -ρ).
Since [z n ]S(z) is the number of saturated secondary structures on [1, n] and the Taylor coefficients in the expansion of 1z/ρ are negative, we discard the positive root and thus obtain

S -T = - 2ρP z P SS • 1 -z/ρ + O(z -ρ). (26)
We now make use of Theorem 1 as before and recover the following result, proved earlier in [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF] by the Bender-Meir-Moon method.

Theorem 5 The asymptotic number of saturated structures is 1.07427 • n -3/2 • 2.35468 n .

Expected number of base pairs of saturated structures

In this section, we compute the expected number of base pairs of saturated structures, proceeding as in Section 2.2 by first modifying the equations to obtain bivariate generating functions and then differentiating with respect to the new variable and evaluating at 1 to obtain the asymptotic expectation.

Generating Functions

We first modify equations [START_REF] Graham | Concrete Mathematics -A Foundation for Computer Science[END_REF][START_REF] Flajolet | Analytic Combinatorics[END_REF] by introducing the auxiliary variable u, responsible for counting the number of base pairs:

S = z + z 2 + zR + z 2 R + uz 2 S + uz 2 S 2 (27) R = uz 2 S + uz 2 RS. ( 28
)
Solving the second equation for R and injecting into the first one gives

P (z, u, S) = Suz 2 (z + z 2 ) -(-1 + Suz 2 )(-S + z + z 2 + Suz 2 + S 2 uz 2 ). ( 29
)

Asymptotics

We are interested in the coefficients of ∂S/∂u at u = 1. Differentiating (29) with respect to u gives ∂P ∂u

+ ∂P ∂S ∂S ∂u = 0.
Using equation (26), we replace S(z, 1) by T + K 1z/ρ + O(1z/ρ) in this equation to obtain

ρ 2 T (1 + 2(1 -ρ 2 )T -2ρ 2 T 2 ) + O( 1 -z/ρ) + (4Kρ 2 -2Kρ 4 -6Kρ 4 T ) 1 -z/ρ + O(1 -z/ρ) ∂S ∂u u=1 = 0 and finally ∂S ∂u (z, 1) ∼ - 0.642305 1 -z/ρ .
Applying Theorem 1 to equation (30) gives

ρ n [z n ] ∂S ∂u (z, 1) ∼ 0.642305 Γ(1/2) • n -1/2 = 0.362417 • n -1/2 .
It follows that the asymptotic expected number of base pairs in saturated structures on [1, n] is

[z n ] ∂S(z,u) ∂u (z, 1) [z n ]S(z, 1) ∼ 0.362417 • n -1/2 • ρ -n 1.07427 • n -3/2 • ρ -n = 0.337361 • n
We have just proved the following.

Theorem 6

The asymptotic expected number of base pairs for saturated structures is 0.337361• n.

Since the Taylor coefficient s n,k of generating function S(z, u) = n,k s n,k z n u k is equal to the number of saturated structures having k base pairs, it is possible that the methods of this section will suffice to solve the following open problem.

Open Problem 1 Clearly, the maximum number of base pairs in a saturated structure on [1, n] where θ = 1 is ⌊ n-1 2 ⌋. For fixed values of k, what is the asymptotic number s n,⌊(n-1)/2⌋-k of saturated secondary structures having exactly k base pairs fewer than the maximum? Note that in [START_REF] Clote | Combinatorics of saturated secondary structures of RNA[END_REF], we solved this problem for k = 0, 1.

A related interesting question concerns whether the number of secondary structures s n,k having k base pairs is approximately Gaussian. As first suggested by Y. Ponty (personal communication), this is indeed the case. More formally, consider for fixed n the the finite distribution P n = p 1 , . . . , p n , where p k = s n,k /s n and s n = k s n,k . In the Nussinov energy model, the energy of a secondary structure with k base pairs is -k, so the distribution P n is what is usually called the density of states in physical chemistry. It follows from Theorem 1 of of Drmota [START_REF] Drmota | Systems of functional equations[END_REF] (see also [START_REF] Drmota | Asymptotic distributions and a multivariate Darboux method in enumeration problems[END_REF]) that P n is Gaussian. Similarly, it follows from Theorem 1 of Drmota that the asymptotic distribution of density of states of both canonical and saturated structures is Gaussian. Details of a Maple session applying Drmota's theorem to saturated structures appears in the web supplement http://bioinformatics.bc.edu/clotelab/SUPPLEMENTS/ JBCBasymptotics/.

Asymptotic number of saturated stem-loops

Define a stem-loop to be a secondary structure S having a unique base pair (i 0 , j 0 ) ∈ S, for which all other base pairs (i, j) ∈ S satisfy the relation i < i 0 < j 0 < j. In this case, (i 0 , j 0 ) defines a hairpin, and the remaining base pairs, as well as possible internal loops and bulges, constitute the stem. We have the following simple result due to Stein and Waterman [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF].

Proposition 1 There are 2 n-2 -1 stem-loop structures § on [1, n].
Proof. Let L(n) denote the number of secondary structures with at most one loop on (1, . . . , n). Then L(1) = 1 = L(2). There are two cases to consider for L(n + 1).

Case 1. If n + 1 does not form a base pair, then we have a contribution of L(n).

Case 2. n + 1 forms a base pair with some 1 ≤ j ≤ n -1. In this case, since only one hairpin loop is allowed, there is no base-pairing for the subsequence s 1 , . . . , s j-1 , and hence if n + 1 base-pairs with j, then we have a contribution of L(n -(j + 1) + 1) = L(nj). Hence

L(n + 1) = L(n) + n-1 j=1 L(n -j) = L(n) + L(n -1) + • • • + L(1)
and hence L(1) = 1, L(2) = 1, L(3) = 2, and from there L(n) = 2 n-2 by induction. § In [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF], stem-loop structures are called hairpins. Since the appearance of [START_REF] Stein | On some new sequences generalizing the Catalan and Motzkin numbers[END_REF], common convention is that a hairpin is a structure consisting of a single base pair enclosing a loop region; i.e. ( • • • • • ) . Here we use the more proper term stem-loop.

Since |a 2 | = |a 3 | = .9207 > |a 1 |, it follows that the asymptotic behaviour is given by the term in a 1 .

We have proved the following theorem.

Theorem 7

The number h(n) of saturated stem-loops on [1, n] satisfies

h(n) ∼ 0.323954 • 1.69562 n . (32)
Convergence of the asymptotic limit in equation ( 32) is exponentially fast, so that when n = 20, 0.323954 • 1.69562 n = 12504.2, while the exact number of saturated stem-loops on [START_REF] Bompfunewerer | Variations on RNA folding and alignment: lessons from Benasque[END_REF][START_REF] Szymanski | 5S ribosomal RNA database Y2K[END_REF] is h(20) = 12503.

3 Quasi-random saturated structures

In this section, we define a stochastic greedy process to generate random saturated structures, technically denoted quasi-random saturated structures. Our main result is that the expected number of base pairs in quasi-random saturated structures is 0.0.340633 • n, just slightly more than the expected number 0.337361 • n of all saturated structures. This suggests that the introduction of stochastic greedy algorithms and their asymptotic analysis may prove useful in other areas of random graph theory.

Consider the following stochastic process to generate a saturated structure. Suppose that n bases are arranged in sequential order on a line. Select the base pair (1, u) by choosing u, where θ + 2 ≤ u ≤ n, at random with probability 1/(nθ -1). The base pair joining 1 and u partitions the line into two parts. The left region has k bases strictly between 1 and u, where k ≥ θ, and the right region contains the remaining nk -2 bases properly contained within endpoints k + 2 and n (see Figure 3). Proceed recursively on each of the two parts. Observe that the secondary structures produced by our stochastic process will always base pair with the leftmost available base, and that the resulting structure is always saturated.

Before proceeding further, we note that the probability that the probability p i,j that (i, j) is a base pair in a saturated structure is not the same as the probability q i,j that (i, j) is a base pair in a quasi-random saturated structure. Indeed, if we consider saturated and quasirandom saturated structures on an RNA sequence of length n = 10, then clearly p 1,5 = 1/29 while clearly q 1,5 = 1/8. ¶ Despite the very different base pairing probabilities when comparing ¶ The web supplement contains a Python program to compute the number of saturated structures on n. Clearly p1,5 = s 3 •s 5 s 10 , where s k denotes the number of saturated structures on an RNA sequence of length k. A computation from a Python program (see web supplement) shows that s3 = 1, s5 = 5 and s10 = 145, hence p1,5 = 5/145 = 1/29.

Taking an average over 100 repetitions, we have computed the average number of base pairs and the standard deviation for n = 10, 100, 1000. Results are µ = 0.323, σ = 0.0604 for n = 10, µ = 0.3526, σ = 0.0386 for n = 100 and µ = 0.35618, σ = 0.0361 for n = 1000. This clearly is a different stochastic process than that used for quasi-random saturated structures.

Conclusion

In this paper we applied the DSV methodology and the Flajolet-Odlyzko theorem to asymptotic enumeration problems concerning canonical and saturated secondary structures. For instance, we showed that the expected number of base pairs in canonical RNA secondary structures is equal to 0.31724 • n, which is far less than the expected number 0.495917 • n of base pairs over all secondary structures, the latter which follows from Theorem 4.19 of [START_REF] Hofacker | Combinatorics of RNA secondary structures[END_REF]. This may provide a theoretical explanation for the speed-up observed for Vienna RNA Package when restricted to canonical structures [START_REF] Bompfunewerer | Variations on RNA folding and alignment: lessons from Benasque[END_REF].

Additionally, we computed the asymptotic number 1.07427 • n -3/2 • 2.35467 n of saturated structures, the expected number 0.337361 • n of base pairs of saturated structures and the asymptotic number 0.323954•1.69562 n of saturated stem-loop structures. We then considered a natural stochastic greedy process to generate quasi-random saturated structures, and showed surprisingly that the expected number of base pairs of is 0.340633 • n, a value very close to the expected number 0.337361 • n of base pairs of all saturated structures. Finally, we apply a theorem of Drmota [START_REF] Drmota | Systems of functional equations[END_REF] to show that the density of states for [all resp. canonical resp. saturated] secondary structures is asymptotically Gaussian.

Figure 1

 1 Figure1gives equivalent views of the secondary structure of 5S ribosomal RNA with GenBank accession number NC 000909 of the methane-generating archaebacterium Methanocaldococcus jannaschii, as determined by comparative sequence analysis and taken from the 5S Ribosomal RNA Database[START_REF] Szymanski | 5S ribosomal RNA database Y2K[END_REF] located at http://rose.man.poznan.pl/5SData/. The sequence and its secondary structure in (Vienna) dot bracket notation are as follows:

Figure 1 :

 1 Figure 1: Depiction of 5S ribosomal RNA from M. Jannaschii with GenBank accession number NC 000909. Equivalent representations as (Left) outerplanar graph (also called Feynman circular diagram), (Middle) Feynman linear diagram, (Right) classical diagram (most familiar to biologists). The sequence and secondary structure were taken from the 5S Ribosomal RNA Database[START_REF] Szymanski | 5S ribosomal RNA database Y2K[END_REF], and the graph was created using jViz[START_REF] Wiese | Rna-a Java tool for RNA secondary structure visualization[END_REF].

  and A → w is a rule, then by replacing the occurrence of A in xAy we obtain xwy. Such a derivation in one step is denoted by xAy ⇒ G xwy, while the reflexive, transitive closure of ⇒ G is denoted ⇒ * G . The language generated by context-free grammar G is denoted by L(G), and defined by

Figure 2 :

 2 Figure 2: The shaded region △ where, except at z = ρ, the generating function S(z) must be analytic.

Figure 3 :

 3 Figure 3: Base 1 is base-paired by selecting a random base u such there are at least θ unpaired bases enclosed between 1 and u.

† A well-balanced parenthesis string is a word over Σ = {(, )} with as many closing parentheses as opening ones and such that when reading the word from left to right, the number of opening parentheses read is always at least as large as the number of closing parentheses. RNA secondary structures can be considered to be well-balanced parenthesis strings that also contain possible occurrences of • , and for which there exist at least θ occurrences of • between corresponding left and right parentheses ( respectively ) .

‡ Since S(z, u) is known to be analytic at 0, we have discarded one of the two solutions as before.

Acknowledgements

We would like to thank Yann Ponty, for suggesting that Drmota's work can be used to prove that the density of states for secondary structures is Gaussian. Thanks as well to two anonymous referees, whose comments led to important improvements in this paper. Figure 2 is due to W.A. Lorenz, and first appeared in the joint article Lorenz et al. [12].

Funding for the research of P. Clote was generously provided by the Foundation Digiteo -Triangle de la Physique and the National Science Foundation DBI-0543506 and DMS-0817971. Additional support is gratefully acknowledged to the Deutscher Akademischer Austauschdienst for a visit to Martin Vingron's group in the Max Planck Institute of Molecular Genetics. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. Funding for the research of E. Kranakis was generously provided by the Natural Sciences and Engineering Research Council of Canada (NSERC) and Mathematics of Information Technology and Complex Systems (MITACS). Funding for the research of B. Salvy was provided by Microsoft Research-Inria Joint Centre.

Research partially supported by National Science Foundation Grants DBI-0543506, DMS-0817971, and the RNA Ontology Consortium. Additional support is gratefully acknowledged to the Foundation Digiteo-Triangle de la Physique and to Deutscher Akademischer Austauschdienst. part by Natural Sciences and Engineering Research Council of Canada (NSERC) and

We now compute the asymptotic number of saturated stem-loop structures. Let h(n) be the number of saturated stem-loops on [1, n], defined by h(n) = 1 for n = 0, 1, 2, 3, h(4) = 3, and

for n ≥ 5. Note that we have defined h(1) = 1 = h(2) for notational ease in the sequel, although there are in fact no stem-loops of size 1 or 2. Indeed in this case, the only structures of size 1 respectively 2 are • and • • .

The first few terms in the sequence h(1), h(2), h(3),

Grammar

It is easily seen that the following rules

provide for a non-ambiguous context-free grammar to generate all non-empty saturated stemloops. It defines actually a special kind of context-free language, called regular, whose generating function is rational.

Generating Function

By the DSV methodology, we obtain the functional relation

whose solution is the rational function

where

Asymptotics

For rational functions, an easy way to compute the asymptotic behaviour of the Taylor coefficients is to compute a partial fraction decomposition and isolate the dominant part. This is equivalent to solving the corresponding linear recurrence. See also [17, p. 325] or [16, Thm. 9.2]. Partial fraction decomposition yields

where the a i s are the roots of Q and

(Note that this is an actual equality valid for all n ≥ 0 and not an asymptotic result). Now, the roots of Q are approximately a 1 = 0.5897545, a 2 = -0.294877 -0.872272i, a 3 = -0.294877 + 0.872272i. saturated with quasi-random saturated structures, it is remarkable that the expected number of base pairs over saturated and quasi-random saturated structures is numerically so close.

Let U θ n be the expected number of base pairs of the saturated secondary structure generated by this recursive procedure. In general, we have the following recursive equation

with initial conditions

If we write equation (33) for U θ n+1 and substitute in it the value for U θ n we derive

If we multiply out by nθ and simplify we obtain

which is valid for n ≥ θ + 1.

Asymptotic behavior

We now look at asymptotics. In particular we prove the following result.

Theorem 8 Let U θ n denote the expected number of base pairs for quasi-random saturated structures of an RNA sequence of length n. Then for fixed θ, and as n → ∞

where

)th harmonic number. The first few values can easily be obtained numerically and we have K 1 = 0.340633, K 2 = 0.285497, K 3 = 0.247908, K 4 = 0.220308, K 5 = 0.199018.

Proof. For fixed integer θ, the recurrence (35) is linear with polynomial coefficients. It is a classical result that the generating functions of solutions of such recurrences satisfy linear differential equations. This is obtained by applying the following rules: if

Starting from (35), we first shift the index by θ + 1 and apply these rules together with the initial conditions (34) to get

Finally, this simplifies to

This is a first order non-homogeneous linear differential equation. The homogeneous part

is solved by integrating a partial fraction decomposition

From there, variation of the constant gives the following expression for the generating function:

Because the exponential is an entire function, we readily find that the only singularity is at z = 1, where y ∼ K/(1z) 2 with K as in the statement of the theorem. The proof is completed by the use of Theorem 1.

Note that the asymptotic expected number of base pairs in quasi-random saturated structures with θ = 1 is 0.340633 • n, while by Theorem 6 the asymptotic expected number of base pairs in saturated structures is 0.337361 • n, just very slightly less. This result points out that the stochastic greedy method performs reasonably well in sampling saturated structures, although the stochastic process tends not to sample certain (rare) saturated structures having a less than average number of base pairs.

The stochastic process used to construct quasi-random saturated structures iteratively base-pairs the leftmost position in each subinterval. One can imaging a more general stochastic method of constructing saturated structures, described as follows. Generate an initial list L of all allowable base pairs (i, j) with 1 ≤ i < j ≤ n and j ≥ i + θ + 1. Create a saturated structure by repeately picking a base pair from L, adding it to an initially empty structure S, then removing from L all base pairs that form a crossing (pseudoknot) with the base pair just selected. This ensures that the next time a base pair from L, it can be added to S without violating the definition of secondary structure. Iterate this procedure until L is empty to form the stochastic saturated structure S.