Deriving Abstract Semantics for Forward Analysis of Normal Logic Programs

The problem of forward abstract interpretation of {\em normal} logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics $F^b and $F^\diamond for forward abstract interpretation of {\em normal} logic programs. $F^b$ is intended for inferring data descriptions for edges in the program graph where an edge denotes the possibility that the control of execution transfers from its source program point to its destination program point. $F^\diamond$ is derived from $F^b$ and is intended for inferring data descriptions for textual program points.

Introduction
Abstract interpretation [7] is a program analysis methodology for statically deriving run-time properties of programs. The derived program properties are then used by other program processors such as compilers, partial evaluators, etc. Program analyses are viewed as program executions over non-standard data domains. Cousot and Cousot first laid solid mathematical foundations for abstract interpretation [7,8]. The idea is to define a collecting semantics for a program which associates with each program point the set of the storage states that are obtained whenever the execution reaches the point. Then an approximation of the collecting semantics is calculated by simulating over a non-standard data domain the computation of the collecting semantics over the standard data domain. The standard data domain is called the concrete domain and the non-standard domain is called the abstract domain.
There has been recently much research into abstract interpretation of logic programs [9]. Abstract interpretation has been used in both forward and backward analyses of logic programs. A forward analysis [3] approximates the set of substitutions that might occur at a program point given a program and a set of goal descriptions. A backward analysis [2,6,28,29] approximates the set of the atoms that are logical consequences of a program [42]. A number of generic abstract semantics, often called frameworks, schemes [3,18,30], have been proposed for forward abstract interpretation of logic programs. These generic abstract semantics have been specialised for the detection of determinacy [10], data dependency analyses [5,11,14,15,32,33], mode inference [4,5,11,26,32,41], program transformation [37], type inference [4,13,16,26], termination proof [43], etc. However, these generic abstract semantics have been developed for forward abstract interpretation of definite logic programs. The problem of forward abstract interpretation of normal logic programs has not been formally addressed in the literature although negation as failure is dealt with in practice through the built-in predicate ! in the way it is implemented in Prolog. This paper proposes a solution to this problem by deriving two generic fixed-point abstract semantics F ♭ P and F ⋄ P for forward abstract interpretation of normal logic programs without relying on any capability of dealing with the built-in predicate !.
Existing generic abstract semantics in the literature are optimisation-oriented and they are used to infer data descriptions for textual program points. However, there are some applications such as debugging where it is helpful to infer data descriptions for edges p← •q in the program graph where p← •q denotes that the control of execution may transfers from program point q to program point p. F ♭ P is intended for these applications. F ⋄ P is derived from F ♭ P and is intended for inferring data descriptions for textual program points.
The way in which F ♭ P and F ⋄ P are derived is conventional. F ♭ P is based on a fixed-point collecting semantics that associates a set of substitutions with each edge p← •q in the program graph. The set of substitutions associated with p← •q includes all the substitutions at program point p whenever the control of execution transfers from program point q to program point p. The collecting semantics is obtained through two approximations. The operational semantics SLDNF-resolution via the left-to-right computation rule is first approximated by a transition system. The transition system is then approximated by the collecting semantics. Obtained from the collecting semantics by a further approximation is F ♭ P that can then be specialised to perform various analyses under certain sufficient conditions. F ⋄ P is derived from F ♭ P through one more approximation and it can be specialised to perform various analyses under the same sufficient conditions as F ♭ P . This paper makes two contributions. Firstly, F ♭ P and F ⋄ P can be used to perform forward abstract interpretation of normal logic programs while the existing generic abstract semantics in the literature can only be used to perform forward abstract interpretation of definite logic programs. A common practice in analysing logic programs with negation as failure is to extend an existing generic abstract semantics with capability of dealing with the built-in predicate ! and then analyse negation as failure in the way it is implemented in Prolog. However, the built-in predicate ! is not a part of the language of normal logic programs. The derivation of F ♭ P and F ⋄ P does not resort to any capability of dealing with any built-in predicate. Secondly, F ♭ P is easier to specialise for inferring data descriptions for edges in the program graph than the existing generic abstract semantics in the literature.
The remainder of this paper is organised as follows. Section 2 briefly recalls on mathematical foundations for abstract interpretation and some terminology in logic program, and introduces some notations used later in this paper. Section 3 reformulates SLDNF in order to facilitate the derivation of the collecting semantics. Section 4 derives the collecting semantics from the operational semantics. Section 5 derives F ♭ P from the collecting semantics through a further approximation, and gives the sufficient conditions for F ♭ P to safely approximate the collecting semantics, and analyses its worst case complexity. Section 6 derives F ⋄ P from F ♭ P through one more approximation, and analyses its worst case complexity. In section 7, we show how F ♭ Let < D, ⊑> be a complete lattice and f ∈ D → D. x ∈ D is a fixed-point of f if x = f (x).
x is the least fixed-point, denoted by lfpf , of f if x ⊑ y for each fixed-point y of f . lfpf = f ↑ β for some ordinal β [40] where if β is a successor ordinal

Abstract Interpretation
We now formalise the notion of abstract interpretation according to the ideas given by [7]. The idea of having an element in an abstract domain <D,⊑ > as description of a element in a concrete domain < D, ⊑> is formalised by a monotonic function fromD to D, called a concretisation function.
We say that an element d in D is approximated by an elementd inD if d⊑ γ(d). There might well be a number of elements that approximate d. If γ ∈D → D and γ ′ ∈D →D are concretisation functions then γ · γ ′ ∈D → D is a concretisation function.
The notion of approximation can also be formalised by means of an abstraction function from the concrete domain to the abstract domain, or a Galois connection between the abstract domain and the concrete domain or a relation between the concrete and the abstract domains [27].
A fixed-point interpretation of a program is the least fixed-point of a function associated with the program on a semantic domain, often a complete lattice. The following theorem shows how the least fixed-point of a monotonic function on one complete lattice can be approximated by the least fixed-point of another monotonic function on another complete lattice.

Logic programming
We assume that the reader is familiar with the terminology in logic programming [24]. Let L be a first order language with function symbol set Σ and predicate symbol set Π which is disjoint from Σ. Let VAR be a denumerable set of variables and V ⊆ VAR. TERM(Σ, V) denotes the set of terms that can be built from Σ and V. ATOM(Π, Σ, V) denotes the set of atoms constructible from Π, Σ and V. The negation of an atom A is denoted as ¬A. A literal is either an atom or the negation of an atom. Let θ and σ be substitutions. σ • θ denotes the composition of σ and θ. dom(θ) denotes the domain of θ. Define Sub def = {θ | θ is a substitution}. An expression is a term, an atom, a literal, a clause, a goal etc. The set of variables in an expression E is denoted as vars(E). For an expression E and a substitution θ, Eθ denotes the instance of E under θ. An expression E ′ is an instance of another expression E if E ′ ≡ Eθ for some substitution θ where A ≡ B denotes that A is syntactically identical to B. Let θ be a substitution and V ⊆ VAR.
Two substitutions σ and θ are equivalent modulo renaming if there are two renamings δ and ρ such that σ = θ•δ and θ = σ •ρ. We write σ ∼ = θ to denote that σ and θ are equivalent modulo renaming. We will not distinguish those substitutions that are equivalent modulo renaming. ∼ = is naturally extended to expressions. Let E 1 and E 2 be two expressions. E 1 ∼ = E 2 if there are two renamings δ and ρ such that E 1 = E 2 δ and E 2 = E 1 ρ.
An equation is a formula of the form l = r where l and r are terms or atoms. The set of equations is denoted as Eq. Let E ∈ ℘(Eq). E is in solved form if, for each equation l = r in E, l is a variable and l does not occur in the right hand side of any equation in E. There is a natural bijection between substitutions and the sets of equations in solved form. Therefore, we sometimes write a substitution as a set of equations in solved form. The unification of a set of equations is decidable and the most general unifiers for a set of equations are equivalent modulo renaming. Let mgu be the function from ℘(Eq) to {fail} ∪ (VAR → TERM(Σ, VAR)) that, given a set of equations E, either returns a most general unifier for E if E is unifiable or returns fail otherwise. mgu({l = r}) is sometimes written as mgu(l, r).
A normal clause is a formula of the form H ← L 1 , L 2 , · · · , L n where H is an atom, L i for each 1 ≤ i ≤ n is a literal. H is called the head of the clause and L 1 , L 2 , · · · , L n the body of the clause. A normal goal is a formula of the form ← L 1 , L 2 , · · · , L n with L i for each 1 ≤ i ≤ n being a literal. A normal program is a set {C ı | ı ∈ ℵ C } of normal clauses where ℵ C is a finite set of distinct natural numbers. Let m[ı] denote the number of the literals in the body of clause C ı . We write C ı as H ı ← L (ı,1) , L (ı,2) , · · · , L (ı,m[ı]) .
A query to a program is a goal that initiates the execution of that program. There might be infinite number of possible queries that a program is intended to respond to. For the time being, we denote the set of all possible queries as {G k Θ k | k ∈ ℵ G } where ℵ G is a finite set of distinct natural numbers such that ℵ G ∩ ℵ C = ∅. G k for each k ∈ ℵ G is a normal goal and Θ k is a set of substitutions θ k . Each G k θ k with θ k ∈ Θ k is a query. Let m[k] be the number of literals in G k . We write G k as ← L (k,1) , L (k,2) , · · · , L (k,m[k]) .
Let ℵ def = ℵ C ∪ ℵ G . Let P i refer to C i for i ∈ ℵ C and to refer to G i for i ∈ ℵ G and define V i def = vars(P i ). Let i ∈ ℵ. We designate P i with m[i] + 1 program points, point (i, j) immediately before We denote by N P the set of all program points designated with P i for all i ∈ ℵ. Let p = (i, j) be a program point. p [1] = i denotes the index to the clause or the query to which p belongs. p [2] = j denotes the position of p in the clause or the query. So, p = (p [1], p [2]). We define two partial functions λp.p + and λp.p over the set of all the program points. p + = (p [1], p[2] + 1) is defined for each p such that p [2] ≤ m[p [1]] and p = (p [1], p[2] − 1) is defined for each p satisfying 2 ≤ p [2] ≤ m[p [1]] + 1. p + is the program point to the right of p if p + exists and p is the program point to the left of p if p exists.
Let p ∈ N P . B p denotes the atom in literal L p . If L p is positive then L p ≡ B p . If L p is negative then L p ≡ ¬B p .
Example 2.2 The following normal logic program will be used in several examples in this paper. The meaning of member(X, L) is that X is a member of list L. The meaning of dif f (X, L, K) is that either X is a member of list L or X is a member of list K but X is not both a member of L and a member of K.
Suppose that the set of queries is described by

Operational semantics
The operational semantics we consider is the SLDNF-resolution via the left to right computation rule. We shall not mention the computation rule explicitly. When the set of all the descendant goals of a set of queries is to be computed, it is necessary to resolve the current goal with every clause whose head unifies with the selected atom in the current goal. Therefore, the selection rule for choosing a particular clause to resolve with the current goal is not of interest. [9] uses general SLD-resolution as operational semantics of definite logic programs and does not take the computation rule into account. This usually leads to less precise analyses [16].

SLDNF
We now briefly recall on SLDNF-resolution (SLDNF in short). The renamed literals will be written in the form Lρ where L is a literal in a clause or a query and ρ a renaming used in standardisation apart [1]. First consider SLD-resolution (SLD in short) for definite logic programs where every literal is positive. For a query and a definite program, SLD works by repeatedly resolving the current goal, initially the query, with a clause in the program. In one resolution step, SLD nondeterministically selects a clause in the program, renames the clause so that it does not have any common variable with the current goal, and derives a new goal by replacing the leftmost literal in the current goal with the body of the renamed clause and applying to the resultant the most general unifier of the head of the renamed clause and the leftmost literal.
If SLD has derived an empty goal, it has successfully computed a computed answer substitution to the query. The computed answer substitution is the restriction, to the variables in the query, of the composition of the most general unifiers in the derivation from the query to the empty goal.
With SLD, only positive information can be derived from a program. SLDNF uses the negation as failure rule to derive negative information. SLDNF deals with positive literals in the same way as SLD. Suppose that the leftmost literal in the current goal is negative. SLDNF first recursively invokes itself with the leftmost literal as the query of the recursive invocation. If the recursive invocation fails then SLDNF removes the leftmost literal from the current goal and continues with the resultant as the new current goal. Otherwise, according to the rule for the weak safe uses of negation as failure [24], SLDNF either backtracks if the computed answer substitution returned by the recursive invocation is a renaming or otherwise flounders.
Let the current goal be where ρ j is the renaming used to rename clause C ij . If L (ij ,k) ≡ ¬B (ij ,k) then SLDNF recursively invokes itself with ← B (ij ,k) τ (j,k) as the query of the recursive invocation.
in the program and a renaming ρ j+1 such that and B (ij ,k) ρ j τ (j,k) and H ij+1 ρ j+1 unify, then the new current goal becomes and Suppose that there is a sub-refutation of 1) with the composition of the most general unifiers used in the sub-refutation being θ. Then the next current goal immediately after the sub-refutation is

VSLDNF
We now propose a variant of SLDNF (VSLDNF in abbreviation) as the operational semantics. VSLDNF is equivalent to SLDNF in the sense that, given the same goal and the same program, VSLDNF reaches a program point iff SLDNF reaches the same program point, and the instantiation of the variables in the clause of the program point by VSLDNF is equivalent (modulo renaming) to that by SLDNF. We now formulate VSLDNF and then establish the equivalence between SLDNF and VSLDNF. Let the current goal be If L (ij ,k) ≡ ¬B (ij ,k) then VSLDNF recursively invokes itself with ← B (ij ,k) σ (j,k) being the query of the recursive invocation. Let L (ij ,k) ≡ B (ij ,k) . The derivation is suspended and a sub-derivation is started as follows. If there is a clause C ij+1 ≡ H ij+1 ← L (ij+1,1) , L (ij+1,2) , · · · , L (ij+1,m[ij+1]) in the program and a renaming ψ j+1 such that and B (ij ,k) σ (j,k) ψ j+1 and H ij+1 unify then the next current goal becomes We call the step to derive a new goal from the current goal and a clause in the program procedure-entry.
Lemma 3.1 VSLDNF is equivalent to SLDNF in the sense that, given the same goal and the same program, VSLDNF reaches a program point iff SLDNF reaches the same program point, and the instantiation of the variables in the clause of the program point by VSLDNF is equivalent (modulo renaming) to that by SLDNF.
VSLDNF performs a procedure-exit step and derives the following from (G1).
This finishes a sub-refutation of (G1). VSLDNF performs a procedure-exit step and derives the following from (G0).
where, letting φ 1 = ∅, This finishes a refutation of (G0). So, σ (0,2) = {X/2} is a computed answer substitution of ← dif f (X, [2,1], [3,1]). 2 VSLDNF differs from SLDNF in several ways. Firstly, a goal in VSLDNF is a part of a clause or a query, in particular, it is a tail of a clause or a query. This helps to approximate VSLDNF as a transition system later. Secondly, when VSLDNF derives a new goal from the current goal and a clause, it renames the leftmost literal in the goal instead of the clause. This is to ensure that the domain of the substitution that will be applied to the body of the clause contains variables in the clause instead of their renamed counterparts. Thirdly, when a sub-refutation is finished, an extra renaming and an extra unification are needed for VSLDNF to calculate the substitution immediately after the sub-refutation whilst these extra operations are not needed in SLDNF. Note that VSLDNF is only used in formulating the collecting semantics.

Program graph
Let p, q ∈ N P , and q be the most recent program point that VSLDNF has reached. There are several possibilities that VSLDNF will reach p next. If q is the exit point of a clause then the only way that VSLDNF can reach p immediately is to perform a procedure-exit. This can happen only if L p is positive and that program clause has been used to resolve with L p . If q is not the exit point of a clause then VSLDNF may reach p immediately either by performing a procedure-entry or by applying the negation as failure rule. VSLDNF may reach p immediately by applying negation as failure rule if L q ≡ ¬B q ∧ q = p . VSLDNF may reach p immediately by performing a procedure-entry either directly when L q is positive or indirectly when L q is negative. Note that if q is the exit point of a query then VSLDNF has succeeded and will not visit any more program points. In order to facilitate further presentation, we assume that VSLDNF starts at a dummy program point (0, 0) ∈ N P from where it can reach entry points of goal clauses by doing nothing. Therefore, there are four ways that VSLDNF will reach p immediately after it has reached q. We use a graph < N + P , E P >, called program graph, to represent the relation among program points p, q that "VSLDNF will possibly visit p immediately after it has visited q. The set N + P of nodes in the program graph is N P ∪ {(0, 0)} and each edge p← •q in E P in the program graph denotes that VSLDNF will possibly visit p immediately after it has visited q. Formally, E P is inductively defined as follows.
P is the collection of edges from dummy program point (0, 0) to the entry points of queries. Edges in E 1 P correspond to procedure-entries, edges in E 2 P to procedure-exits, and edges in E 3 P to the negation as failure rule.
There are 23 edges in the program graph for the program. 2

Collecting semantics
In this section, we present the fixed-point collecting semantics for normal programs. The collecting semantics of normal program P is lfpF ♯ P where F ♯ P is defined below. lfpF ♯ P associates a set of substitutions with each edge p← •q ∈ E P . Sub-section 4.1 uses a transition system to approximate VSLDNF. A state in this transition system corresponds to a goal in VSLDNF. The set of states derivable from a set of initial states by the transition system is then characterised as the least fixed-point lfpF P of a function F P mapping a set of states into another set of states. Therefore, the set of goals derivable from a set of initial goals by VSLDNF is approximated by lfpF P . Sub-section 4.2 derives the fixed-point collecting semantic function F ♯ P from F P and proves that lfpF ♯ P is a safe approximation of lfpF P . Let A, B be atoms, and θ, ω ∈ Sub. Define Although there are infinite number of renamings ρ satisfying vars(Aθρ) ∩ vars(Bω) = ∅ in equation 9, only one renaming must be considered when computing unif y(A, θ, B, ω) because unif y(A, θ, B, ω) for one renaming is equivalent (modulo renaming) to unif y(A, θ, B, ω) for another renaming accoding to lemma 10.2.

Approximating VSLDNF by a transition system
We now devise a transition system to approximate VSLDNF. A state in the transition system corresponds to a goal in VSLDNF. The transition system approximates VSLDNF in the sense that, if a goal is derivable from an initial goal by VSLDNF then the state corresponding to the goal is derivable from the state corresponding to the initial goal by the transition system while the reverse is not necessarily true.
A state in the transition system is a stack that is a sequence of stack items. The empty stack is denoted as $. A stack item is of the form p← •q, θ where p← •q ∈ E P and θ ∈ Sub. The meaning of p← •q, θ is that the control of execution transfers from q to p with θ being the substitution at p. The set S ♯ of all possible stack items is therefore The set S of all possible stacks is the set of all possible sequences of stack items from S ♯ . S can be inductively defined as follows.
• $ ∈ S; and The set S 0 ⊆ S of initial states is determined by the set of queries in VSLDNF.
The set of final states is The set of descendant states of the set S 0 of initial states is obtained by applying the transition rules in figure 1. Rule (0) says that every final state is stable. Rule (1a) corresponds to direct procedure-entry and rule (1b) to indirect procedure-entry. Rule (2) corresponds to procedure-exit and rule (3) deals with negative literals.
Rule (3) causes the inaccuracy of the transition system. When the transition system reaches a state corresponding to a goal with its leftmost literal being negative, the transition system may apply either rule (1b) or rule (3). Applying rule (1b), it will go to a state corresponding to a goal after performing a procedure-entry indirectly. The application of rule (1b) is to enable information to propagate forward so as to ensure that the transition system safely approximates VSLDNF. Applying rule (3), it will go to a state corresponding to the goal as if the recursive The set of descendant states of a set S 0 of initial states is therefore the least fixed-point of function F P that is defined as follows.
The domain D of F P is ℘(S). < D, ⊆> is a complete lattice and F P is monotonic on < D, ⊆>.
Rule (0) of the transition system is not embodied in F P . Since F P is a monotonic function on < D, ⊆>, we have F P ↑ k ⊆ F P ↑ (k + 1) for any k ≥ 0. Therefore, any final state will be in lfpF P if it is derivable from an initial state by the transition system.

Collecting semantics
lfpF P is a set of states. A state is a stack that corresponds to a goal. The collecting semantics lfpF ♯ P first abstracts away the sequential relation between stack items of a stack and then classifies the stack items according to edges p← •q. lfpF ♯ P associates each p← •q in E P with the set of substitutions θ such that p← •q, θ is a stack item in S ♯ . Each edge p← •q ∈ E P will be assocaited with a member from ℘(Sub). < ℘(Sub), ⊆, ∅, Sub, ∩, ∪ > is a complete lattics. Therefore, the domain D ♯ of the collecting semantics is the Cartesian product of the same component domain ℘(Sub) for as many times as the number of edges p← The approximation of a set of stacks by a vector of sets of substitutions is modeled by the following monotonic function γ ♯ ∈ D ♯ → D.
Let A, B be atoms, and Θ, Ω be sets of substitutions. Define The fixed-point collecting semantics is defined in the following.
The collecting semantics lfpF ♯ P is a safe approximation of the operational semantics and can be used as a basis for program analysis because any safe approximation of this collecting semantics is a safe approximation of the operational semantics. [lfpF ♯ P ] p← •q contains all the substitutions whenever the control of execution transfers from program point q to program point p. [lfpF ♯ P ] p← •q is usually an infinite set of substitutions and is therefore not computable in finite time. In order to obtain useful information about the possible substitutions when the control of execution transfers from program point q to program point p, further approximations are needed. This section derives the generic abstract semantics F ♭ P from F ♯ P .

Abstract domains
The collecting semantics lfpF ♯ P associates with each edge p← •q a set of substitutions which is a superset of the set of the substitutions whenever the control of execution transfers from q to p. When program is analysed by means of abstract interpretation, the set of substitutions associated with p← •q is approximated by an abstract substitution associated with p← •q. For edge p← •q, only values of the variables in V p [1] are of interest and, for edge p ′ ← •q ′ , only values of the variables in V p ′ [1] are of interest. The abstract substitions for p← •q and p ′ ← •q ′ are from different domains when p ′ [1] = p [1]. We will simply call a domain for abstract substitutions an abstract domain. We find it convenient to parameterise abstract domains with finite sets of variables instead of having a single abstract domain for all abstract substitutions associated with different edges or constructing abstract domains for different edges in different ways. Let ASub V denote the domain for abstract substitutions for describing values of variables in V. Then [lfpF ♯ P ] p← •q is represented by a member of ASub V p [1] . We require that, for any finite V ⊆ VAR, The domain D ♭ of F ♭ P is constructed in the same manner as the domain D ♯ of F ♯ P was constructed. Each member X ♭ in D ♭ is a vector that is indexed by edges p← •q in E P . X ♭ p← •q is an element from ASub V p [1] . Let X ♭ ∈ D ♭ and Y ♭ ∈ D ♭ . Define The concretisation function γ ♭ is defined in terms of γ Vi . For every p← •q ∈ E P and X ♭ ∈ D ♭ , The monotonicity of γ ♭ ∈ D ♭ → D ♯ follows immediately from equation 21 and C2.

5.2
The Generic Abstract Semantics F ♭ P F ♭ P is derived from F ♯ P as follows. A set Θ ∈ ℘(Sub) of substitutions is replaced by an abstract substitution θ ♭ in ASub V where V is a set of variables whose values are of interest. unif y ♯ applied to two sets of substitutions described by θ ♭ ∈ ASub U and σ ♭ ∈ ASub V respectively is replaced by an operator unif y U ,V applied to θ ♭ and σ ♭ . ∪ in the definition of [F ♯ P ] p← •q is replaced by ⊔ V p [1] . Let θ ♭ k ∈ ASub V k be the least abstract substitution such that Θ k ⊆ γ V k (θ ♭ k ) for each k ∈ ℵ G . Note that θ ♭ k instead of Θ k is given before the program is analysed. Let ǫ Vi ∈ ASub Vi , called an abstract identity substitution in [3], be the least abstract substitution such that ǫ ∈ γ Vi (ǫ Vi ) for each i ∈ ℵ C . F ♭ P is defined as follows.
for any finite U, V ⊆ VAR, any θ ♭ ∈ ASub U , any σ ♭ ∈ ASub V , and any atoms A and B such that vars(A) ⊆ U and vars(B) ⊆ V.

Complexity of F ♭ P
The cost of computing lfpF ♭ P is affected by the characteristics of P , the abstract domain, abstract substitutions θ ♭ k where k ∈ ℵ G , and the algorithm for least fixed-point computation. Using O'Keefe's algorithm for least fixed-point computation [36], the worst case cost of computing lfpF ♭ P is proportional to the product of the number of operations in F ♭ P and the maximum height dmax of ASub Vi for i ∈ ℵ. Since ⊔ is much less costly than unif y in most cases, we measure the worst case number of occurrences of unif y in F ♭ P . Let S be a set and define #S be the number of members in S. Let P is the set of edges whose ending points lie in N  P . Let pmax be the maximum number of predecessors that a program point has. By equations 22 and 25, unif y does not occur in equations for edges in E 0 P ∪ E 3 P . By equation 23, unif y occurs at most pmax times in the equation for an edge in E 1 P . So, unif y occurs at most #E 1 P * pmax times in the equations for edges in E 1 P . By equation 24, unif y occurs at most pmax 2 times in the equation for an edge in E 2 P . So, unif y occurs at most #E 2 P * pmax 2 times in the equations for edges in E 2 P . Since #E 2 P ≤ #E 1 P and #E 1 P ≤ #ℵ C * pmax, the worst case number of occurrences of unif y in F ♭ P is O(#ℵ C * pmax 3 ). Therefore, the worst case cost of computing lfpF ♭ P is The Generic Abstract Semantics F ⋄ P A further approximation may be made of F ♭ P so as to reduce the complexity of program analyses. lfpF ♭ P is a vector indexed by edges in the program graph for P . lfpF ♭ P associates with each program point with several abstract substitutions, each for one edge ending at the program point. This results in fine analyses for applications such as program debugging. However, there are some applications where such fine analyses are not beneficial with respect to their costs and one abstract substitution for each program point is a better choice. F ⋄ P fulfills such purposes and is derived from F ♭ P by one more approximation. The domain of F ⋄ P is D ⋄ and each X ⋄ ∈ D ⋄ is a vector indexed by program points. D ⋄ is constructed from ASub V in a similar manner as is and define The approximation through collapsing the abstract substitutions associated with all the edges ending at a common program point is characterised by the following concretization function.
It follows immediately from equation 31 that γ ⋄ ∈ D ⋄ → D ♭ is monotonic. We now construct a monotonic function Lemma 6.1 lfpF ♭ P ⊑ ♭ γ ⋄ (lfpF ⋄ P ). Proof: See p.35 lfpF ⋄ P associates each program point with an abstract substitution. The simultaneous recurrence equations for F ⋄ P are simpler than those for F ♭ P and hence the computation of lfpF ⋄ P is less costly than that of lfpF ♭ P . F ⋄ P is a generalisation of Nilsson's generic abstract semantics for definite logic programs [34]. Specifically, if P does not have negative literals then lfpF ⋄ P is equal to that in [34]. Nilsson later [35] presented a generic abstract semantics that is based on a collecting semantics that associates with each program point a set of pairs of goal structures. A goal structure is very similar to a stack in our term.
Each program point in P corresponds to an equation of F ⋄ P . By equations 32 and 35, unif y does not occur in equations for points in N 0 P ∪ N 3 P . unif y occurs at most pmax times in an equation for a point in N 1 P ∪ N 2 P according to equations 33 and 34. The worst case number of occurrences of unif y in F ⋄ P is O(#N P * pmax) since #N 1 P + #N 2 P ≤ #N P . Therefore, the worst case cost of computing lfpF ⋄ P is O(dmax * #N P * pmax) F ⋄ P ( a generalisation of the generic abstract semantic in [34] ) may also be used to obtain abstract substitutions for edges. We prefer F ♭ P to F ⋄ P for such analyses since F ♭ P is easier to specialise than F ⋄ P . In order to specialise F ⋄ P (or the generic abstract semantics in [35]) for such an analysis, in addition to the work required to specialise F ♭ P for the same analysis, one needs to do • keeping information about program points in abstract substitutions, an abstract substitution for F ⋄ P is a set of pairs of a program point and an abstract substitution for F ♭ P ; • replacing unif y by unif y which, for each member of θ ⋄ × σ ⋄ , discards point information and calls unif y.
This amounts to requiring the analysis design who specialises F ⋄ P to undo approximation γ ⋄ . A call to unif y may cause unif y to be called as many times as pmax 2 . So, the worst case complexity of F ⋄ P is no less than that of F ♭ P for the same analysis.
We have so far developed the generic abstract semantics lfpF ♭ P and lfpF ⋄ P for forward abstract interpretation of normal logic programs. lfpF ♭ P obtains an abstract substitution for each edge in E P while lfpF ⋄ P obtains an abstract substitution for each program point in N P . In order to specialise either of these generic abstract semantics to perform a particular analysis, it is sufficient to design ASub, γ, ǫ,unif y and ⊔ such that they satisfy C1-C4.

Example
We now illustrate how F ♭ P and F ⋄ P can be specialised to perform a particular analysis through groundness analysis -a simplified version of mode analysis.
In groundness analysis, we are interested in knowing which variables will be definitely instantatiated to ground terms. Therefore, a set of substitutions is approximated naturally by a set of variables. ASub V = ℘(V). The partial order on ASub V induced by ⊆ on ℘(Sub) is ⊇. < ℘(V), ⊇, V, ∅, ∪, ∩ > is a complete lattice.
The approximation of a set of substitutions by a set of variables is modeled by the following concretisation function γ V ∈ ℘(V) → ℘(Sub).
Note that E 0 is written as a set of equations in solved form.

Related work and Discussion
There has been much research into abstract interpretation of logic programs. For a comprehensive survey, see [9]. A number of generic abstract semantics have been brought about for abstract interpretation of logic programs [3,18,29,30]. Abstract interpretation has been used in both forward and backward analyses of logic programs. A forward analysis [3] approximates the set of substitutions that might occur at each program points given a program and a set of goal descriptions. A backward analysis [2,6,28,29] approximates the set of the atoms that are logical consequences of a program [42]. However, the problem of forward abstract interpretation of normal logic programs has not been formally addressed in the literature although negation as failure is dealt with through the built-in predicate ! in the way it is implemented in Prolog. We have proposed a simple solution to the problem. We now review previous work and discuss about the solution.

Approaches to forward abstract interpretation of logic programs
There are three approaches to forward abstract interpretation of logic programs. A bottomup forward abstract interpreter mimics a bottom-up evaluation strategy. A top-down forward abstract interpreter mimics a top-down evaluation strategy. Top-down forward abstract interpreters can be further divided into two sub-classes according to whether or not the underlying top-down evaluation strategy uses memoisation. A fixed-point forward abstract interpreter computes the least fixed-point of a system of simultaneous recurrence equations.

Bottom-up forward abstract interpretation
The abstract interpreter based on Alexander Templates (AT) [18] simulates the bottom-up evaluation based on AT [38]. Given a program and a goal, AT first transforms the program and the goal and then evaluates the transformed program and the transformed goal in a bottomup manner. Given a program and a goal description, the AT-based abstract interpreter first transforms the program and the query description in the same way as AT does and then mimics the evaluation phase of AT by replacing standard unification with an abstract one.

Top-down forward abstract interpretation without memoisation
A top-down forward abstract interpreter without memoisation [3,31,44,46] approximately executes a goal description by mimicing the underlying the top-down evaluation strategy. As an example, we take the top-down forward abstract interpreter in [3].
Given a goal description that is a pair of an atom and an abstract substitution, the topdown forward abstract interpreter in [3] constructs an abstract AND-OR graph to approximate the set of all the intermediate proof trees that may be constructed by SLDNF under the leftto-right computation rule for all the goals satisfying the goal description. In other words, any intermediate proof tree for any goal satisfying the goal description can be obtained by unraveling the abstract AND-OR graph. An AND-node is a clause head and its child OR-nodes are the atoms in the body of the clause. Every OR-node is adorned with one abstract substitution to the left, called abstract call substitution, and with another to the right, called abstract success substitution. The abstract success substitution of an OR-node is the abstract call substitution of its right sibling.
The initial abstract AND-OR graph has one OR-node that is the atom in the goal description and is adorned to the left with the abstract substitution in the goal description. Suppose that the abstract AND-OR graph has been partly constructed. Consider an ORnode A with abstract call substitution β. The abstract interpreter computes the abstract success substitution of OR-node A as follows. For each clause C i ≡ H i ← B (i,1) , · · · , B (i,m[i]) such that H i may match with Aθ for some θ satisfying β, the abstract interpreter adds to OR-node A a child AND-node H i that has m[i] child OR-nodes B (i,1) , · · · , B (i,m[i]) and computes the abstract call substitution β i in of OR-node B (i,1) -the first child OR-node of AND-node H i . β i in approximates the set of the most general unifiers of H i and Aθ for all θ satisfying β. The abstract interpreter extends OR-node B (i,1) by recursively applying the same process and extends OR-node B (i,j+1) in the same way after it has computed the abstract success substitution of OR-node B (i,j) . Eventually, it will have computed the abstract success substitution β i out of OR-node B (i,m[i]) . After computing β i out for each clause such that H i may match with Aθ for some θ satisfying β, the abstract interpreter computes the abstract success substitution β ′ of OR-node A and β ′ approximates from above the set of the most general unifiers of Aθ and H i η for all the θ satisfying β and all the η satisfying β i out . Since there are recursive calls, [3] introduces a fixed-point component to the abstract interpretation process. Suppose that an OR-node A with abstract call substitution β were to be extended. If A has an ancestor OR-node A ′ with abstract call substitution β ′ such that A is a variant of A and β is a variant of β ′ , the abstract interpreter adorns OR-node A to the right with the infimum abstract substitution and proceeds until the abstract success substitution of OR-node A ′ is computed. The abstract interpreter then repeatedly recomputes the part of the AND-OR graph starting from the abstract success substitution of OR-node A to the abstract success substitution of OR-node A ′ by using the abstract success substitution for OR-node A ′ as the abstract success substitution for OR-node A. This fixed-point process finishes when there is no more increase in the abstract success substitution of OR-node A ′ . The same fixed-point component is also used to limit the sizes of abstract AND-OR graphs. [31,44,46] differ from [3] only in dealing with recursive calls. [31] and [46] make use of a memo table and [44] uses stream predicates.

Top-down forward abstract interpretation with memoisation
An abstract interpreter based on an evaluation strategy with memoisation mimics the underlying evaluation strategy with memoisation by replacing concrete substitutions with abstract substitutions and the concrete unification with an abstract unification. For an introduction to evaluation strategies with memoisation, see [45].
The abstract interpreter based on OLDT resolution [19,20,21] mimics the OLDT resolution [39]. The left-to-right computation rule is used in OLDT resolution. Given a goal that is a pair of a sequence of atoms and a substitution, OLDT resolution [39] constructs an OLDT structure for the goal. An OLDT structure consists of a search tree, a solution table and an association. An entry of the solution table has a key and a solution list. The key is an atom and the solution list is a list of atoms that are instances of the key. Each node of the search tree is a pair of a goal and a substitution and each edge of the search tree is labeled with a substitution. The association is a group of pointers between the nodes of the search tree and the entries of the solution table.
Initially, the search tree has one node that is the pair of the sequence of atoms and the substitution, and both the solution table and the association are empty. OLDT resolution extends the OLDT structure as follows until it cannot be further extended. Suppose that the OLDT structure has been partly constructed. Consider a node < (A, R), σ > in the search tree where A is an atom, R a sequence of atoms and σ a substitution. If there is an entry in the solution table with a key that is a variant of Aσ then < (A, R), σ > is called a lookup node. Otherwise, it is called a solution node. OLDT resolution extends the OLDT structure by extending its lookup nodes and its leaf solution nodes. If < (A, R), σ > is a leaf solution node then OLDT resolution first adds into the solution table an entry whose key is Aσ and whose solution list is an empty list that will be filled in later. OLDT resolution then, for each clause such that H i and Aσ unify with θ being the most general unifier, adds < (B (i,1) , · · · , B (i,m[i]) , R), σ • θ > as a child node to node < (A, R), σ > and labels the edge from node < (A, R), σ > to node < (B (i,1) , · · · , B (i,m[i]) , R), σ • θ > with θ. These child nodes will then be extended by the same process. If < (A, R), σ > is a lookup node then, OLDT resolution first adds < R, σ • θ > as a child node to < (A, R), σ > and labels the edge from < (A, R), σ > to < R, σ • θ > with θ for each solution Aσθ in the solution list for key Aσ, and then adds to the association a pointer from lookup node < (A, R), σ > to the tail of the solution list for key Aσ. This pointer will be used to add more child nodes to lookup node < (A, R), σ > because at the moment lookup node < (A, R), σ > is first extended, some solutions for Aσ might be unavailable from the solution list and will show up later. When a unit clause is resolved with a leaf solution node < (A, R), σ >, the unit clause completes a sub-refutation for Aσ and may also completes sub-refutations for the leftmost atoms of other nodes along the path from < (A, R), σ > up to the root of the search tree. Whenever a unit clause is resolved with a leaf solution node, OLDT resolution updates the solution lists for those keys that corresponds to completed sub-resolutions. After the solution list for a key is updated, OLDT resolution expands those lookup nodes that have pointers pointing to the solution list accordingly.
The abstract interpreter mimics OLDT resolution closely by constructing an abstract OLDT structure for a goal description that is a pair of a sequence of atoms and an abstract substitution. The nodes of the abstract OLDT structure are pairs of a sequence of atoms and an abstract substitution instead of a concrete substitution and the edges of the abstract OLDT structure are now labeled with abstract substitutions instead of concrete substitutions. The key of a solution table entry is now a pair of an atom and an abstract substitution and so is each solution in the solution list for the key. The abstract interpreter mimics OLDT by replacing the concrete unification function with an abstract unification function and the concrete composition function for concrete substitutions with an abstract composition function for abstract substitutions.

Fixed-point forward abstract interpretation
Given a program and a set of goal descriptions that are abstract atoms, [30] derives a system of concrete simultaneous recurrence equations whose least solution approximates the set of all the input atoms and the set of all the output atoms that occur in an intermediate proof tree derivable from the program and any goal satisfying one of the goal descriptions. The system of concrete simultaneous recurrence equations is approximated from above by a system of abstract simultaneous recurrence equations with each concrete operation being replaced by an abstract operation. Abstract interpretation is done by computing the least fixed-point of the system of abstract simultaneous equations.
Given a program and a set of goal descriptions each of which is a pair of a goal and an abstract substitution, [34] derives a system of concrete simultaneous recurrence equations whose least solution gives each program point a superset of the set of all the possible substitutions at the program point during the satisfaction of any goal satisfying one of these goal descriptions. A system of abstract simultaneous recurrence equations is derived to approximate from above the system of concrete simultaneous recurrence equations in the same manner as in [30]. Abstract interpretation is accomplished by computing in an abstract domain the least fixed-point of the system of abstract simultaneous recurrence equations.
[34] collects a set of substitutions for every program point. [30] collects the set of input atoms and the set of output atoms. Collecting the set of input atoms corresponds to collecting a set of substitutions for the entry point of each clause, applying each substitution in the set to the head of the clause to obtain a set of atoms for the clause and then lumping together the sets of atoms for all the clauses as well as the given set of input atoms. Similarly, collecting the set of output atoms corresponds to collecting a set of substitutions for the exit point of each clause, applying each substitution in the set to the head of the clause to get a set of output atoms for the clause and lumping together the sets of output atoms for all the clauses. [30] uses the idea of a trace to summarise the execution of a query. When making abstraction, the sets of call substitutions of different calls to the same predicate are lumped together in a single set input. Similarly, the set of success substitutions are lumped together in the set output.
In [17], contexts are recorded only at the entry of each program clause. [17] is also a generic procedure, their core semantics is augmented with application dependent auxiliary functions that are similar to abstract operations in [3]. These auxiliary functions operate on abstract domains consisting of appropriate approximations of the collecting semantics. They distinguish between different call instances. However, there is only one instance of every clause, so substitutions originating from different call instances are lumped together.

The Negation as Failure
The treatment of negation as failure in F ♭ P and F ⋄ P is simple. The transition system F P approximates VSLDNF (an equivalent of SLDNF) by assuming that a negative literal always succeeds while it may fail. This approximation introduces noises into F ♭ P and F ⋄ P . However, it is difficult within the provisions of abstract interpretation to improve on this simple solution.
Let (¬A)σ be selected by SLDNF where ¬A is a negative literal in the body of a clause in the program and σ be a substitution. During abstract interpretation, σ is not known and possible values for σ are described by an abstract substitution σ ♭ ∈ ASub V , often called the abstract call substitution for (¬A). Since σ ♭ usually describes an infinite set of substitutions, it may well be the case that Aσ succeeds for some σ ∈ γ V (σ ♭ ) and fails for other σ ∈ γ V (σ ♭ ). We take σ ♭ as the abstract success substitution for ¬A by simply assuming that Aσ fails for all σ ∈ γ V (σ ♭ ) (¬Aσ succeeds). An improvement needs making the abstract success substitution for ¬A stronger, that is, replacing σ ♭ with another abstract substitution η ♭ ∈ ASub V such that η ♭ ⊑ V σ ♭ . Let us assume that γ V (σ ♭ )\γ V (η) = ∅ for otherwise η ♭ is no stronger than σ ♭ . By safeness requirement for negation as failure and safeness requirement for abstract interpretation, it is necessary to be able to infer ∀θ ∈ γ V (σ ♭ )\γ V (η). ǫ is a computed answer f or P ∪ {← Aθ} To infer 36, we need to under-estimate success and over-estimate failure in order to make the analysis safe. However, abstract interpreters over-estimate success and under-estimate failure.
Note that the word approximation in abstract interpretation means approximation from above. An abstract interpreter over-estimates success by means of an abstract unification function which approximates the normal unification function from above, that is, over-estimates the success of the normal unification function. To infer 36, we must use a unification function which approximates the normal unification function from below. Such a unification function should succeed only if the normal unification function succeeds. Of course, we could use a unification function which always fails. But, this does not achieve any improvement since such a unification function will make Aσ always fail. Since an abstract domain for an analysis is much simpler than the concrete domain, some information about a set of substitutions is lost when the set of substitutions is approximated by an abstract substitution. It is difficult to design a unification function which approximates the normal unification function from below based on abstract substitutions because abstract substitutions are inaccurate descriptions of sets of substitutions while such a unification function, we believe, needs accurate descriptions of sets of substitutions.

Summary
We have presented and justified a simple solution to the problem of forward abstract interpretation of normal logic programs and derived generic abstract semantics lfpF ♭ P and lfpF ⋄ P of normal logic programs. The solution is simple and it amounts to replacing the negation as failure rule with an unconditional derivation rule. lfpF ♭ P and lfpF ⋄ P can be specialised for various analyses. An analysis can be thought of as a series of approximations of the operational semantics as shown below. An arrow from A to B reads as "A is approximated by B".

SLDNF VSLDNF
To specialise either lfpF ♭ P or lfpF ⋄ P for an analysis, one has to find out the corresponding abstract domain and corresponding concretisation function, to provide a function for computing abstract identity substitutions, a function for computing the least upper bounds, and a function for computing abstract unifications. The abstract domain and the concretisation function must satisfy C1-C2, the function for computing abstract identity substitutions must satisfy C3, and the function for computing abstract unifications must satisfy C4.
We deal with negation as failure by approximating SLDNF with a transition system. The way negation as failure is dealt with may be generalised to deal with built-in predicate !. Although, we have not dealt with other built-in predicates, we believe that the generic abstract semantics can be augmented to deal with these built-in predicates in the way they are dealt with in [3]. Proof: Let aρ ≡ a ′ and φρ ≡ φ ′ . If a ′ φ ′ and bψ unify then there is a substitution θ such that a ′ φ ′ θ ≡ bφθ. We have vars(a ′ ) ∩ dom(ψ) = ∅ and rang(ψ) ∩ dom(φ ′ ) = ∅ and vars(b) ∩ dom(φ ′ ) = ∅. Hence, a ′ ψφ ′ θ ≡ bψφ ′ θ. Therefore, aρ and b unify.
The following equation results from equation 42 and the definition of ρ 3 .
The following equation results from equation 45 and the definition of ρ 4 .
. By corollary 10.3, Aρ A and B unify, and We also have rang(ρ 1 Lemma 10.5 Let θ 1 and θ 2 be two substitutions and Va set of variables.
Lemma 10.6 Let E 1 and E 2 be two sets of equations, and θ 1 and θ 2 be two substitutions. If Proof: See [5] Proof of lemma 3.1 (p.8): VSLDNF and SLDNF deals with negative literals in the same manner. Therefore, it remains to prove for the cases where the leftmost literals are positive. The proof has two parts. The first part corresponds to procedure-entry and the second part to procedure-exit.


extfieldsofstudy: Biology Medicine

text:
Optimization of phosphorus localization by EFTEM of nucleic acid containing structures

Energy Filtered Transmission Electron Microscopy (EFTEM) has been used to study nucleic acids localization in unstained thin sections of virus-infected cells. For this purpose, phosphorus maps (P-maps) have been obtained by applying the N-windows Egerton model for background subtraction from data acquired by a non-dedicated TEM Jeol 1200EXII equipped with a post-column PEELS Gatan 666–9000 and a Gatan Image Filter (GIF-100). To prevent possible errors in the evaluation of elemental maps and thus incorrect nucleic acid localization, we have studied different regions of swine testis (ST) cells with similar local density containing either high concentration of nucleic acids (condensed chromatin and ribosomes) or a very low concentration (mitochondria). Special care was taken to optimize the sample preparation conditions to avoid as much as possible the traditional artifacts derived from this source. Selection of the best set of pre-edge images for background fitting was also considered in order to produce “true P-maps”. A new software for interactive processing of images series has been applied to estimate this set. Multivariate Statistical Analysis was used as a filtering tool to separate the “useful information” present in the inelastic image series (characteristic signal) from the “non-useful information” (noise and acquisition artifacts). The reconstitution of the original image series preserving mainly the useful information allowed the computation of P-maps with improved signal-to-noise ratio (SNR). This methodology has been applied to study the RNA content of maturation intermediate coronavirus particles found inside infected cells.

We are interested in the study of viral morphogenesis and, especially, in the incorporation of the nucleic acid into the morphogenetic intermediates. There are several classical approaches to this problem, such as cytochemical methods and in situ hybridization. Nevertheless, these methodologies have low efficiency and sensitivity for RNA localization. Direct observation of nucleic acids with higher efficiency in ultrathin sections of virus-infected cells is thus a challenging objective that could be reached using in situ spectroscopic methods by the analysis of the P distribution, based on the specific elemental concentration of phosphorus in nucleic acids (around 3 at.%).
Phosphorus-maps (P-maps) in cellular nuclei components can be obtained by X-ray spectroscopy as reported, for example, by Le Furgey et al. (1992) using cryofixed and cryodehydrated frozen sections, and by Quintana and Bonnet (1994a,b) using cryofixed, cryosubstituted and cryoembedded sections. In these cases the main drawback is the long acquisition time required to produce a data set (from one to several hours). Electron Energy Loss Spectroscopy (EELS) possesses higher sensitivity and spatial resolution than X-ray microanalysis for light elements (Leapman and Hunt, 1991;Krivanek et al., ]992). It has been used to obtain P-maps of nucleic acid (n.a.)-containing structures since 1980 (Ottensmeyer and Andrew, 1980). Recent implementation of commercially available incolumn and post-column electron energy loss spectrometers has increased the use of energy-filtered transmission electron microscopy (EFTEM), with special emphasis on chemical mapping.
One of the main problems when dealing with elemental map computation in EFTEM is the subtraction of a nonnegligible background that lies under the characteristic elemental signal. This is especially importan t in the case of elements being present at a very low concentration, where the absolute value of the characteristic signal is much smaller than the background. The choice of the best ¶Corresponding author. background subtraction method therefore becomes critical. Background subtraction problems in EFTEM can be summarized as shown in Fig. 1. Case (a) represents background subtraction from a model that is correctly fitted to the preedge images. In contrast, cases (b) and (c) represent incorrect adjustments that will render incorrect maps. Case (b) gives rise to overestimation of the elemental map (this includes the characteristic signal and part of the background), and case (c) leads to underestimation of the elemental map. Among the different methods currently accepted for map extraction, one of the most widely used models the background by the power law, B = A × E -R (Egerton, 1975). This method involves the computation of two parameters (A and R) and is also known as the "three-window" method, as it requires the acquisition of three images, two below the characteristic energy loss edge of the element (pre-edge images) and one above this energy loss value (post-edge image). It has been subsequently extended to N preedge and M post-edge images (Jeanguillaume et al., 1978;Bonnet et al., 1988). Other mathematical formulae have been also used to model the background (Ottensmeyer, 1986;Bonnet et al., 1988;Ottensmeyer and Frankland, 1988;Tenailleau and Martin, 1992). Negative results obtained in the case of P detection in mitochondrial dense granules originated from rat cultivated chondrocytes (Trebbia and Mory, 1990), however, suggested that in the case of P-maps in biological sections, the power law is not valid in the region of the pre-edge images in the L2,3 transition in P (100 to 135 eV), due to the tail of the very intense "plasmon peak". The plasmon influence is even more important if the sample possesses a high mass-thickness (high thickness and/or high density in stained samples). This situation is similar to that shown in Fig. l(c), in which P-maps could be under-estimated.
For this reason, some authors continue to use another approach for background subtraction that is based on the acquisition of only two images (two-window methods): (1) The scaled subtraction of one pre-edge image from the post-edge one (Ottensmeyer and Andrew, 1980;Korn et al., 1983). (2) The ratio between the post and the pre-edge images (also known as the jump method), used mainly in Material Science to avoid crystal diffraction effects (Krivanek et al., 1992;Hofer et al., 1995). Both methods increase the signal-to-noise ratio (SNR) of the maps, and they are presently used for this reason (Olins et al., 1996, Beniac et al., 1997a. In spite of rendering a good SNR, scaled two-window methods may produce false positive signals in high density areas, irrespective of the presence of P (Leapman, 1986). This is particularly relevant in preparations treated with heavy metal salts (osmium, uranium or lead). In this case, the computed maps can be considered a mixture of density and elemental P-map, not allowing separation of both signals (Bonnet et al., 1988;Bonnet, 1995), a case similar to that shown in Fig. lb. Cellular components P-maps have been a good test for background subtraction methods, as phosphorus represents less than 0.5% in mass concentration in these biological samples. By means of the spectrum-image acquisition technique in an STEM, reliable P-maps with good SNR were built of DNA in the head of a bacteriophage (Shuman et al., 1986, Colliex et al., 1994 using a three-window method for background subtraction. This technique requires, however, long acquisition time (around 22 minutes for 32x64 pixel images (Shuman et al., 1986) or 20 minutes for 64x64 pixel images (Colliex et al., 1994). More recently, using a TEM equipped with an in-column spectrometer, it has been possible to obtain P-maps of nucleic acid-containing structures with a high SNR by applying the three-window method (Vazquez-Nin et al., 1996). Electron spectroscopic imaging of sectioned viruses has provided high-contrast imaging and an improvement of the resolution of the viral particles, also allowing a better detectability of the immunolabeling markers (Ozel et al., 1990). Also, P-maps were obtained using a two-window method to study the organization of encapsidated DNA in vaccinia virus (Harauz et al., 1995). Interpretation problems arose in this case due to the fact that the samples were conventionally fixed and embedded.
In a previous study, our post-column PEELS and Image Filter (IF) was characterized and reliable Fe-maps were produced from images acquired in a few seconds (Quintana et al., 1997). Using this set-up, we have studied P-map computation using very thin unstained sections of cryosubstituted and HM23 resin cryoembedded swine testis (ST) cells, infected with a coronavirus. After checking the background subtraction method to separate the P-signal from mass-thickness contribution, we have applied Multivariate Phosphorous Maps by EFTEM 299 Statistical Analysis and, in particular, Factorial Analysis of Correspondence (FAC) (Bonnet et al., 1988;Bonnet and Trebbia, 1992;Trebbia and Mory, 1990;Bonnet, 1995) to the series of pre-and post-L2.3 P-edge images. Such factorial filtering allows noise reduction and elimination of artifacts that might have been produced in image acquisition and thus enables presentation of clearer and more reliable images of the P-containing structures. Once the methods were tested using cellular components of known elemental composition, we studied the RNA distribution of intracellular coronavirus particles.

Sample preparation
Monolayers of ST cells infected with the transmissible gastroenteritis coronavirus (TGEV) were produced as described in Risco et al. (1995). After collection, cells were fixed in situ with a mixture of 2% glutaraldehyde and 2% tannic acid in 0.4 M HEPES buffer (pH 7.5), for 1 h at room temperature. Fixed monolayers were removed from the dishes in the fixative and transferred to Eppendorf tubes. After centrifugation in a microcentrifuge and washing with HEPES buffer, small pellets of fixed cells were cryoprotected with glycerol and applied to 1 mm 2 pieces of filter paper, blotted with filter paper for 15 s, and quickly frozen in home-made equipment (Quintana, 1991) using commercial liquid propane cooled by liquid nitrogen at -196°C. Vitrified specimens were stored in liquid nitrogen until use. For freeze-substitution, samples were transferred to a Reichert Jung (Leica, Austria) AFS freeze-substitution unit, and maintained 24 h at -90°C in pure methanol for complete substitution of the water in the sample, according to established procedures (Grief et al., 1994;Quintana, 1994). Samples were then processed for cryoembedding in Lowicryl HM23 at -60°C. Polymerization was done with ultraviolet light for 24 h at -60°C and a further 12 h at room temperature. Ultra-thin (20-30 nm) sections were mounted on uncoated 400-mesh copper grids. Some sections were coated with a thin layer of carbon to increase the stability against the electron radiation.

Instruments
The microscope used was a TEM Jeol 1200EX II with a conventional tungsten gun. The microscope is equipped with a Gatan anti-contaminator model 651N and a ± 60 ° tilting goniometer. The optical characteristics of this configuration are: focal length = 5 mm, Cc = 3.9 mm, and Cs = 5.6 mm. The microscope is operated at 120 kV. This instrument has been equipped with a PEELS Gatan 666-9000 and a Gatan Image Filter (GIF-100) (Krivanek et al., 1995a).

Experimental conditions
Unfiltered bright field images, Z-loss images and inelastic filtered images of 512 x 512 pixels were recorded using the slow-scan CCD and the Gatan Digital Micrograph software working at 16 bits. The experimental conditions were:. emission current = 7-8/zA. condenser aperture = 300 #m. semi-illumination angle = 2 mrad. objective aperture = 40/xm. acceptance half-angle = 4 mrad. semicollection angle = 4.5 mrad. aperture entrance of the spectrometer = 3 mm.. spot size = 1; defocused mode in unfiltered or Z-loss images, focused mode in filtered images (minimun diameter of the iluminated area = 2/~m) All digital images were corrected for dar k current and gain variations of the SS-CCD camera using Digital Micro-t graph software.
The microscope magnification ranged from 600 to 3000x. Taking into account the image magnification due to the GIF optical system (20x), the total magnificatior~ varied from 12000 (2 nm/pixel) to 60000 (0.4 nm/pixel). I The acquisition time was 0.5 s for unfiltered and Z-loss images and 3 to 4 s for energy-filtered images.
P-maps can be obtained using two characteristic inner shell ionization edges, the L23 at 135 eV and the K at 2149 eV. Although the K ionization edge has a better sig-I nal:background ratio (SBR) than the L2.3 edge, it has lower intensity. We have thus chosen the L2.3 edge, !n spite of its smaller SBR.
Energy-filtered images were recorded belo ~ and above the ionization edge L2,3 of P from 95 to 155 e'~ with a rE = 10eV energy window slit. The energy losses of these images were selected by raising the high w~ltage of the microscope. This procedure ensures no char ge in image focusing. Due to differences in optimum fccus between inelastic images and bright field images, ine astic images were acquired with a focus adjusted after tile ionization edge, around 145 eV, by using a real-time CCD camera.

Computer analysis of the series of inelasti~ images i Preprocessing
Inelastic images belonging to each series wgre drift-corrected by cross-correlation algorithms. Only lhe common area from all images in each series was considffred for processing. A median filter (neighborhood: 3 x ~pixels) was applied to the images (Bonnet et al., 1988).

Map extraction Background subtraction
We have used the extension of the three-wir~dow method applied to N pre-images and M post-images (J~anguillaume et al., 1978;Bonnet et al., 1988). This methgd (Egerton, 1975) involves the fitting of the following expression B=A X E -R to the background below the edge of interest (E is the energy loss and A and R the fitting parameters that are computed, pixel by pixel, from two or more pre-edge images). The background image under the post-edge image !s then computed by extrapolation and the characteristic signal is extracted by subtraction.
We have used a program developed for the analysis of image sequences, whatever their origin (Bonne~ and Zahm,

Image series factorial analysis of correspondence ( FA C)
FAC belongs to Multivariate Statistical Analysis (MSA), a group of methods devised to analyse information from the whole data set at once. FAC can be used to discard redundant information and to display graphically correlation and anti-correlation among different images of the series, as well as for the correlation and anti-correlation among image pixels, without an explicit model of the data. The only implicit assumption in this approach is to consider the whole data set as a linear combination of several underlying components (factorial axes).
MSA can be applied hierarchically to classify the information contained in the data set. In the case of a series of inelastic images acquired below and above a characteristic edge, the information corresponds to: • the characteristic signal • the background • the noise and the acquisition artifacts If, as a consequence of the analysis, it is possible to identify some of the underlying components as "useful", it is then possible to reconstitute the data set using only such information, therefore filtering the rest of the information. In that sense, components not considered would correspond to noise and acquisition artifacts and would be removed (Bonnet et al., 1988;Trebbia and Bonnet, 1990;Trebbia and Mory, 1990;Bonnet and Trebbia, 1992;Bonnet, 1995).
Software applied was developed in a version for 16-bit images that runs on a SUN workstation.

Final data handling and presentation
After data treatment, the histograms of images and maps were centred (average + 3 × standard deviation) and final computed images at 8 bits were transferred in an LZW compression TIFF format to a PC, to be printed using a high-resolution graphic card. As this representation did not allow visualization of the contrast changes among the different series images, we have represented the first series of images using the variance of the 155 eV image as an standard for all the images. Final hard copies were obtained in a Laser Printer HP4M with a resolution of 3200 dpi.

P-maps on test objets
Two different series of inelastic filtered images of ultrathin unstained sections of ST cells infected with TGEV coronavirus were used to test the background subtraction method: a) Low magnification series (12 000 × ), containing part of a cell and embedding resin. Images show (Fig. 2) part of the nucleus with peripheral condensed chromatin (chr), the cytoplasm (cyt) containing some ribosomes and a few extracellular viruses (v) attached to the plasma membrane of the cell. In this series, structures containing higher concentration of n.a. (chromatin, ribosomes and viruses) correlate with regions of higher local density. b) Intermediate magnification series (24 000 × ) of ST cells (Fig. 3) containing cytoplasm (cyt), one mitochondrion (mit) and ribosomes in the rough endoplasrnic reticulum (rer). In this series, the mitochondrion, witO a very low n.a. content, has a similar local density to ~e ribosomes in the rer.
Structural data were extracted from the inelastic darkfield-like images acquired at an energy lost; of approximately 200 eV, which correspond to the struCture-sensitive contrast images (Reimer and Messemer, 1490 ). In these images ( Fig. 2a and Fig. 3a), the darker region~ are of higher mass thickness. For P-map computation, inelastic images were acquired before and after the L2,3 P icharacteristic edge at 135 eV. Representative images of ~he series are shown in Fig. 2b-f and Fig. 3b-f.
Using the software described in Materials ~md Methods, different ROIs were selected, including conde)lsed chromatin, (circular region of 25 pixels radius), resin (circular region of 25 pixels radius), rer ribosomes (9 circular regions of 5 pixels radius each) and mitochondria (cir( ular region of 45 pixels radius). After displaying the signal a a function of energy loss within every ROI and applyin~ the Egerton power law to the different subsets of pre-edg e images, the A, R and X 2 parameters were computed in ',ach case. Fit quality was estimated by the X 2 value non mlized to the number (A t) of pre-edge images used. Results of some regions are shown in Table 1.
The best fit was obtained for the subset ]composed of images at energy loss values of 115, 125 ahd 135 eV in series 1 (Fig. 2b, c, d) and of images with energy loss values of 105, 125 and 135 eV in series 2 (F~g. 3b, ~, d}'. ..... Plots shown in Fig. 4a correspond to the s6t of pre-edge images of series 1 that produced the best fit iin chromatin and resin), together with the estimated background extrapolated beyond the characteristic energy loss edge. Fig. 4b presents the image set for series 2 in the c~se of rer and mitochondria. In both cases, in ROIs corresponding to structures containing a high n.a. concentration (chromatin and the rer ribosomes), the 145 eV and 155 eV posi-edge images possess values well above the background curate, indicating the presence of phosphorus. In the case of ROIs with a low n.a. content (mitochondria), or without n.a. (resin), these values are close to the background curve. This is better observed in Fig. 4c, which plots the net intensity after background substraction, showing much higher vaiues for chromatin than for resin in the post-edge images 0f series 1. P-maps computed using the N-windows imethod with three pre-edge images and two post-edge images are shown in Fig. 2g and 3h. Cellular structures known to contain high n.a. levels exhibit strong signals in the P-maps (notice, for example, the chromatin and viriOns in Fig. 2g and the ribosomes of rer cisternae in Fig. 311, while some other cellular structures of similar local density known to contain low n.a. levels, totally disappear ira the P-maps (mitochondrion in Fig. 3h, for example).

Factorial filtering
FAC has been applied to a set of pre-and post-edge images previously selected as described above for each case. The contribution of each factorial axis to the total variance is shown in Table 2.
Image and image pixel coordinates over factorial axis were computed. Fig. 5 shows image coordinates of series 1 on axis 1 vs. energy loss. Pixel coordinates over factorial axis, after conversion to "gray levels", can be mapped and displayed as "factorial images". Factorial images allowed visualization of the different sources of information in the original data set. Factorial images (F1 and F2) of series 1 are shown in Fig. 2h and i, while the first factorial image of series 2 is shown in Fig. 3g.
From the energy loss point of view, axis 1 (about 70% of the total variance) shows that the post-edge images correlate well among them and anti-correlate with the pre-edge images. Regarding the subcellular compartments, axis 1 differentiates nucleic acid-containing structures from the rest of the areas. Factorial images from axis 2 and 3 only presented noise (see Fig. 2i which represents factorial image from axis 2, from series 1).
Image series were finally reconstituted using the information contained in the factorial axes 1 and 0 (the factorial axis 0 carrying the information of the average image computed from the original data set after normalization). We have verified that this reconstitution does not cause any undesirable effects in the estimation of the background model, as it does not modify either the average and standard deviation values of the images or the average values of the R-map obtained from the pre-edge images ( Table 3). The reconstituted R-map from series 1 is shown in Fig. 2k. P-maps obtained with reconstituted images are shown in Fig. 2j and Fig. 3i. The enhancement of the signal-to-noise ratio of these maps with respect of the original ones ( Fig. 2g and Fig. 3h) is clearly observed and allows the definition of the boundaries of the different structural elements that are obscured in the original images.

Stud), of the P distribution of intracellular virions
The methods described above were applied to series of inelastic images of intracellular virions. Z-loSs and structure-sensitive contrast images of a group of virions are shown in Fig. 6a and b respectively. In these images, TGEV viral particles with two different sizes are visible. Their internal structure is indistinguishable in the Z-loss image, while some hints of internal differences appeared in the structure-sensitive contrast image. No significant difference was observed in the x2/N value as a function of the pre-edge image number (3, 4 or 5) considered!when fitting the background (Table 1).
Plots presented in Fig. 7 correspond to the power law fit of background over 5 pre-edge images in 2 ROIs, corresponding to viruses and cytoplasm. As in the previous test series, images obtained at 145 and 155 eV ( Fig. 6f and g,  respectively) showed values above the extrapolated background curve in virus regions, thus indicating the presence  of P. In ROIs selected within cytoplasm, corresponding values are essentially within the background curve, suggesting absence of P. The P-map obtained with 5 pre-edge images and 2 post-edge images is shown in Fig. 6h. FAC was applied to all seven images used to obtain the Pmap. In Table 2, the percentages of variance of the first five factorial axes can be seen. Images of this series were reconstituted with the information contained on factorial axes 0, 1 and 2. The resulting P-map (Fig. 6i) presents a clear enhancement of the SNR when compared to the first one obtained (Fig. 6h). These P-maps show that the large virions have a peripheral phosphorus signal distribution (as the central region seems devoid of P-signal), while the small virions present a more homogeneous internal distribution of the P-signal.

DISCUSSION
We have studied the possibility of obtaining true P-maps of biological samples, trying to avoid false P-signals due mainly to high density structures on one side and loss of true P-signals on the other, which would lead to missing out of important information. To this end, we have tested different well-characterized samples that have allowed us to make a qualitative assessment of processing methods used to build P-maps.
The main problem when obtaining low concentration elemental maps by EELS is the very low SBR. It is therefore critical to optimize sample preparation conditions as well as data acquisition for a specific instrument to increase the SBR. As background intensity depends on mass-thickness, a reduction of section thickness, together with the use of low density embedding media, would lead to background intensity reduction. To this end, we have used ultra-thin sections (30 nm) and Lowicryl HM23 as embedding medium (density near one) in our studies. The specific elemental signal can be increased by: a) the optimization of the acquisition parameters b) increasing the acquisition time (limited by the radiation damage tolerance of the sample) c) optimizing the model applied to the background subtraction d) decreasing noise and acquisition artifacts Regarding acquisition parameter optimization, (Krivaneket et al., 1995b) we have used the conditions for the best spatial resolution attainable by our instrument, as described previously (Quintana et al., 1997). The acquisition time was adjusted as a compromise among the SNR, the radiation damage and the mechanical and magnetic stability of the sample and the instrument. Once these parameters were fixed, we concentrated our effort on points c and d.
The presence of drifts is usual in instruments not fully dedicated to microanalysis, due to environmental, mechanical and magnetic perturbations, as it is in our case. As a consequence, the energy loss values at which the images are acquired do not always correspond to the real ones. It is then very useful to be able to select, from among the pre-edge images of a series, those which best fit the model of the background to compute the P-maps. Best fit was chosen by means of the minimum x2/N criteria. For instance, in the second series we did not consider the image at 115 eV, and in the third series it was possible to detect that the image at 125 eV was slightly outside of the estimated background curve (Fig. 7). Another consequence of the presence of drift is the need to centre the images before their processing, a procedure that we perform by crosscorrelation.
The possibility of using more than one post-edge image increases the characteristic signal value and consequently the SNR of the maps. In our case, we have only used two post-edge images because of the proximity of the L2,3 edge of the sulphur at 165 eV.
To test the background model, two different test series were used. In the first, the P-map obtained by applying the N-window method to three pre-edge and two post edgeimages showed the presence of a clear positive P-signal in areas that contained nucleic acids, although the values for resin are not null (Fig. 4c). However, the areas with high Psignal correlate with areas of high "natural" local density in the sample, so the possibility could not be completely excluded that the signal might be a mixture of characteristic signal and mass-thickness (see model b in Fig. 1).
We performed a second test series in Which, together with the structures containing high n.a. iconcentrations (ribosomes in the rer), there was an organ~lle with high local density (mitochondria) and very low iconcentrations of n.a. Curves for background fitting in the hnalysed ROIs (mitochondria and rer) and the P-map (obtained using three pre-edge images and two post-edge image!) showed that there was only P-signal in the ribosomes and not in the mitochondria.
This methodology yields true P-maps w~ich, nevertheless, possess a low SNR. Using factorial filtering of inelastic images, SNR of P-maps can be enhanced. ]=AC has been used previously in the hierarchical classification of the information in a series of pre-and post-edge EELS images 306 C. Quintana et al. (Trebbia and Mory, 1990), as well as in other types of image analysis (Bretaudiere and Frank, 1986). In our case, FAC has proved to be a successful tool for filtering. Reconstitution of images has been performed preserving only useful information (characteristic signal and background) that can be present in one factorial axis (series 1 and 2, containing approximately 70% of the global variance) or in two axes, as in the case of virus-containing samples (38% of the global variance). The criteria used to select the number of axes for the reconstitution process were based on the study of the factorial images. Only axes corresponding to those factorial images possessing "organized information" (Bonnet and Trebbia, 1992) should be used for reconstitution. Noise reduction and suppression of acquisition artifacts is thus achieved and consequently, an important increment of the SNR in the filtered P-maps.
Once we tested our system for P-map production, we then tried to use this method for the detection of nucleic acids in intracellular viruses. In our studies, considerable care has been taken with specimen preparation, since in a previous work from our group the structural preservation provided by freeze-substitution has been decisive to characterize the two types of viral-related particles that assemble in coronavirusinfected cells (Risco et al., 1998). In this extended structural work, it was demonstrated that two types of TGEV virions accumulate in infected cells: large viral particles (size of the viral core around 68-80 nm) exhibit an internal clear centre and dense periphery, while small virions (size of the viral core around 50-65 nm) are homogeneously dense inside. To define whether these differences in density are due to different arrangements of the viral RNA, a suitable method for mapping nucleic acids is needed. Encapsidation of the viral genome is one of the most difficult steps to characterize when studying the sequence of viral assembly at the structural level, since RNA is usually detected with methods of variable efficiency. Only a small percentage of sectioned viral particles react with the probes used in in situ hybridization (ISH) or with RNase-colloidal gold complexes (Risco et al., 1998). An additional problem of ISH is that the simultaneous detection of protein cannot be achieved in most cases, since proteolysis is often necessary to unmask nucleic acid molecules, frequently complexed with viral proteins within the virion. P-maps obtained on sections provide direct information of the RNA distribution, in spite of the presence of proteins complexed with viral proteins within the virion. Our results show two different distributions of phosphorus (and, hence, of RNA) in the viral particles analysed: peripheral (larger virions) or central (smaller virions) arrangement. According to the data obtained in our previous structural study, the small virions are the final product of assembly (infectious mature virions), while the large viral particles most likely represent a precursor form that assembles at early steps in morphogenesis. P-maps indicate, then, that a major change in RNA organization inside the viral particle takes place during the structural maturation suffered by TGEV virions during morphogenesis.
The results presented here show that mapping nucleic acids in viruses is a biological problem that EFTEM can address, providing useful information on viral structure and morphogenesis. These results open up the possibility for further studies to follow the different steps involved in the RNA incorporation into viral particles during morphogenesis and the maturation processes involved. It is also clear that future improvements would demand an increment of the P detection sensitivity by enhancement of the SNR. We are presently carrying out several studies that could be useful to this end, such as the increment in the number of acquired images in the 105-155 eV range of energy loss, and the testing of other background models different from the Egerton power law.


A Pattern-based Machine Translation System Extended by Example-based Processing

In this paper, we describe a machine translation system called PalmTree which uses the "pattern based" approach as a fundamental framework. The pure pattern-based translation framework has several issues. One is the performance due to using many rules in the parsing stage, and the other is inefficiency of usage of translation patterns due to the exact-matching. To overcome these problems, we describe several methods; pruning techniques for the former, and introduction of example-based processing for the latter.

Introduction
While the World-Wide Web (WWW) has quickly turned the Internet into a treasury of information for every netizen, non-native English speakers now face a serious problem that textual data are more often than not written in a foreign language. This has led to an explosive popularity of machine translation (MT) tools in the world.
Under these circumstances, we developed a machine translation system called PalmTree I which uses the pattern-based translation [6,7] formalism.
The key ideas of the pattern-based MT is to employ a massive collection of diverse transfer knowledge, and to select the best translation among the translation candidates (ambiguities). This is a natural extension of the example-based MT in the sense that we incorporate not only sentential correspondences (bilingual corpora) but every other level of linguistic (lexical, phrasal, and collocational) expressions into the transfer knowledge. It is also a rule-based counterpart to the word n-grams of the stochastic MT since our patterns intuitively captures the frequent collocations.
Although the pattern-based MT framework is promising, there are some drawbacks. One is the speed, since it uses many rules when parsing. The other is inefficiency of usage of translation patterns, since it uses the exact-match when matching translation patterns with the input. We will describe several methods for accelerating the system performance for the former, and describe the extension by using the example-based processing [4,8] for the latter. 2 Pattern-based Translation Here, we briefly describe how the pattern-based translation works. (See [6,7] for details.) A translation pattern is a pair of source CFG-rule and its corresponding target CFG-rule. The followings are examples of translation patterns. The (pl) is a translation pattern of an English colloquial phrase "take a look at," and (p2) and (p3) are general syntactic translation patterns. In the above patterns, a left-half part (like "A B C =~ D") of a pattern is a source CFG-rule, the righthalf part (like "A ¢:= B C D") is a target CFG-rule, and an index number represents correspondence of terms in the source and target sides and is also used to indicate a head term (which is a term having the same index as the left-hand side 2 of a CFG-rule). Further, some features can be attached as matching conditions for each term.
The pattern-based MT engine performs a CFGparsing for an input sentence with using source sides of translation patterns. This is done by using chart-type CFG-parser. The target structure is constructed by the synchronous derivation which generates a target structure by combining target sides of translation patterns which are used to make a parse. Figure 2 shows how an English sentence "She takes a look at him" is translated into Japanese.
2we call the destination of an arrow of a CFG rule description the left-hand side or LHS, on the other hand, we call the source side of an arrow the right-hand side or RHS.  In this figure, a dotted line represents the correspondence of terms in the source side and the target side. The source part of (p3) matches "She" and "him," the source part of (pl) matches a segment consisting "take a look at" and a NP("him") made from (p3), and finally the source part of (p2) matches a whole sentence. A target structure is constructed by combining target sides of (pl), (p2), and (p3). Several terms without lexical forms are instantiated with translation words, and finally a translated Japanese sentence "kanojo(she) ha(sub j) kare(he) wo(dobj) miru(see)" will be generated.

Pruning Techniques
As mentioned earlier, our basic principle is to use many lexical translation patterns for producing natural translation. Therefore, we use more CFG rules than usual systems. This causes the slow-down of the parsing process. We introduced the following pruning techniques for improving the performance.

Lexical Rule Preference Principle
We call a CFG rule which has lexical terms in the right-hand side (RHS) a lexical rule, otherwise a normal rule. The lexical rule preference principle (or LRPP} invalidates arcs made from normal rules in a span in which there are arcs made from both normal rules and lexical rules. Further, lexical rules are assigned cost so that lexical rules which has more lexical terms are preferred. For instance, for the span [take, map] of the following input sentence, He takes a look at a map. if the following rules are matched, (rl) take:verb a look at NP (r2) take:verb a NP at NP (r3) take:verb NP at NP (r4) VERB NP PREP NP then, (r4) is invalidated, and (rl),(r2), and (r3) are preferred in this order.

Left-Bound Fixed Exclusive Rule
We generally use an exclusive rttle which invalidates competitive arcs made from general rules for a very special expression. This is, however, limited in terms of the matching ability since it is usually implemented as both ends of rules are lexical items. There are many expression such that left-end part is fixed but right-end is open, but these expressions cannot be expressed as exclusive rules. Therefore,  Examples of LBFE rules are as follows: NP ~ DET own NP NOUN +--as many as NP NP ~ most of NP

Preproeessing
Preprocessing includes local bracketing of proper nouns, monetary expressions, quoted expressions, Internet addresses, and so on. Conversion of numeric expressions and units, and decomposition of unknown hyphenated words are also included in the preprocessing. A bracketed span works like an exclusive rule, that is, we can ignore arcs crossing a bracketed span. Thus, accurate preprocessing not only improved the translation accuracy, but it visibly improved the translation speed for longer sentences.

Experiments
To evaluate the above pruning techniques, we have tested the speed and the translation quality for three documents. Table 1 shows the speed to translate documents with and without the above pruning techniques. 4 The fourth row shows the 3This is not an LBFE rule in practice. 4please note that the time shown in this table was recorded about two years ago and the latest version is much faster.
number of sentences tested with pruning which become worse than sentences without pruning and sentences with pruning which become better than without pruning.
This shows the speed with pruning is about 2 times faster than one without pruning at the same time the translation quality with pruning is kept in the almost same level as one without pruning.. 4 Extension by Example-based Processing One drawback of our pattern-based formalism is to have to use many rules in the parsing process. One of reasons to use such many rules is that the matching of rules and the input is performed by the exact-matching. It is a straightforward idea to extend this exact-matching to fuzzy-matching so that we can reduce the number of translation patterns by merging some patterns identical in terms of the fuzzy-matching. We made the following extensions to the pattern-based MT to achieve this examplebased processing.

Example-based Parsing
If a term in a RHS of source part of a pattern has a lexical-form and a corresponding term in the target part, then it is called a ]uzzy-match term, otherwise an exact-match term. A pattern writer can intentionally designate if a term is a fuzzy-match term or an exact-match term by using a doublequoted string (for fuzzy-match) or a single-quoted string (for exact-match).
For instance, in the following example, a word make is usually a fuzzy-match term since it has a corresponding term in the target side (ketsudansuru), but it is a single-quoted string, so it is an exact-match term. Words a and decision are exactmatch terms since they has no corresponding terms in the target side. (1) When a term TB has both LexB and POSB,  LexB is the same as LeXA, and PosB is the same as PosA.
5A matched-term inherits a lexical-form of a term it matches. (1-2) TB is a fuzzy-match term, the semantic distance of LexB and LexA is smaller than a criterion, and PosB is the same as ROSA.
(2) When a term TB has only LexB,  LexB is the same as LeXA.  LexB is a fuzzy-match term, the semantic distance of LexB and LexA is smaller than a criterion.
(3) When TB has only PosB, then PosB is the same as RosA.

Prioritization of Rules
Many ambiguous results are given in the parsing, and the preference of these results are usually determined by the cost value calculated as the sum of costs of used rules. This example-based processing adds fuzzy-matching cost to this base cost. The fuzzy-matching cost is determined to keep the following order.

Modification of Target Side of Rules
Lexical-forms written in the target side may be different from translation words of matched input word, since the fuzzy-matching is used. Therefore, we must modify the target side before constructing a target structure.
Suppose that a RHS term tt in the target side of a pattern has a lexical-form wt, tt has a corresponding term t, in the source side, and G matches an input word wi. If wt is not a translation word of wi, then wt is replaced with translation words of wi. Figure 3 shows a translation example by using example-based processing described above.

Translation Example
In this example, the following translation patterns are used. The pattern (p4) matches a phrase "take a taxi," since "taxi" and "bus" are semantically similar. By combining target parts of these translation patterns, a translation "PRON ha basu ni noru" is generated. In this translation, since "basu(bus)" is not a correct translation of a corresponding source word "taxi," it is changed to a correct translation word "takusi(taxi)." Further, PRON is instantiated by "watashi" which is a translation of "I." Then a correct translation "watashi ha takusi ni noru" is generated.

Discussion
Unlike most of existing MT approaches that consist of three major components[I, 2] -analysis, transfer, and generation -the pattern-based MT is based on a synchronous model [5,3] of translation. That is, the analysis of a source sentence is directly connected to the generation of a target sentence through the translation knowledge (i.e., patterns). This simple architecture makes it much easier to customize a system for improving translation quality than the conventional MT, since the management of the ambiguities in 3-component architecture has to tackle the exponential combination of overall ambiguities. In this simple model, we can concentrate on a single module (a parser with synchronous derivation), and manage most of translation knowledge in a uniform way as translation patterns.
Although it is easier to add translation patterns in our system than previous systems, it is difficult for non-experts to specify detailed matching conditions (or features). Therefore, we made a pattern compiler which interprets a simple pattern which a non-expert writes and converts it into the full-scale patterns including necessary matching conditions, Shown in the above example, it is very easy for nonexperts to write these simple patterns. Thus, this pattern compiler enable non-experts to customize a system. In conventional MT systems, an expert is usually needed for each component (analysis, transfer, and generation). These advantages can reduce the cost of development and customization of a MT system, and can largely contribute to rapidly improve the translation quality in a short time.
Further, we have shown the way to integrate example-based processing and pattern-based MT. In addition to reduce the total number of translation patterns, this combination enables us to make a more robust and human-like MT system thanks to the easy addition of translation pattern. 6 Conclusion In this paper, we have described a pattern-based MT system called PalmTree. This system can break 6practically, some conditional features are attached into verb terms. the current ceiling of MT technologies, and at the same time satisfy three essential requirements of the current market: efficiency, scalability, and easeof-use.
We have described several pruning techniques for gaining better performance. Further we described the integration of example-based processing and pattern-based MT, which enables us to make more robust and human-like translation system.