Controlling generalization and polyvariance in partial deduction of normal logic programs

Probably not a substantial claim: may not pass S3 (load-bearing).

There is an interesting relation between the control techniques presented in the article and current practice in supercompilation.

“Next, there is an interesting relation between the control techniques presented in this article and current practice in supercompilation [Glück and Sørensen 1996;Sørensen and Glück 1995;Turchin 1986;Turchin 1988].”

• cites Glück and Sørensen 1996Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Sørensen and Glück 1995 sourceNot checked — no full text of the source
• cites Turchin 1986 sourceSupported

May combine two claims.

Very few abstract interpretations of logic programs use infinite domains of infinite height, and to the authors' knowledge all of them have some a priori limitation of precision, at least in practice.

“Very few abstract interpretations of logic programs use infinite domains of infinite height (some notable exceptions are Bruynooghe [1991], Janssens and Bruynooghe [1992], and Heintze [1992]), and to our knowledge all of them have some a priori limitation of the precision, at least in practice.”

• cites Bruynooghe [1991] sourceNot checked — no full text of the source
• cites Janssens and Bruynooghe [1992] sourceSupported
• cites Heintze [1992]Not checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

Neighborhoods of order n, forming the basis for generalization in full supercompilation [Turchin 1988], are essentially the same as classes of atoms or goals with an identical depth-n characteristic tree.

“It is also interesting to return to an observation already made in Section 4 of Martens and Gallagher [1995]: neighborhoods of order”

• cites Martens and Gallagher [1995] sourcePartly supported

  Section 4 (page unavailable) says that supercompilation neighborhoods reflect a computation history of order n and that this “seems to be related” to characteristic trees with depth bound n. It does not establish that neighborhoods are essentially the same as classes of atoms or goals with identical depth-n characteristic trees; the claim states the relationship more strongly than the source does. (LLM, conf=0.86)

  Experimental — accuracy not yet measured
• cites Turchin 1988Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

A similar use of the minimization algorithm is made by Winsborough [1992] and Puebla and Hermenegildo [1995].

“A similar use of this minimization algorithm is made by Winsborough [1992] and Puebla and Hermenegildo [1995].”

• cites Winsborough [1992] sourceNot checked — no full text of the source
• cites Puebla and Hermenegildo [1995] sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

Partial evaluation of functional-logic programs already features the use of homeomorphic embedding and m-trees.

“Indeed, partial evaluation of functional-logic programs [Alpuente et al. 1996;1997;Lafave and Gallagher 1997] already features the use of homeomorphic embedding and m-trees [Martens and Gallagher 1995].”

• cites Alpuente et al. 1996 sourceSupported
• cites Lafave and Gallagher 1997Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Martens and Gallagher 1995 sourcePartly supported

  Section 3 presents an m-tree-based algorithm for partial deduction, supporting the m-tree part of the attribution. The passages on termination and the algorithm do not describe using homeomorphic embedding; searches for that term and its use in termination found no supporting passage. The paper addresses logic-program partial deduction, while the functional-logic-program context is attached to the other citations in the sentence. (LLM, conf=0.85)

  Experimental — accuracy not yet measured

Probably not a substantial claim: may not pass S3 (load-bearing).

Puebla and Hermenegildo [1995], in a somewhat different context, studies polyvariant parallelization and specialization of logic programs based on abstract interpretation.

“The latter, in a somewhat different context, studies polyvariant parallelization and specialization of logic programs based on abstract interpretation.”

• cites Puebla and Hermenegildo [1995] sourceSupported

May combine two claims.

Plugging in a depth-bound-free local control strategy yields a fully automatic, concrete partial-deduction method that always terminates and produces precise and reasonable polyvariance, without resorting to ad hoc techniques.

“Plugging in a depth-bound-free local control strategy (see Bruynooghe et al. [1992] and Martens and De Schreye [1996]), we thus obtain a fully automatic, concrete partial-deduction method that always terminates and produces precise and reasonable polyvariance, without resorting to any ad hoc techniques.”

• cites Bruynooghe et al. [1992] sourceNot checked — no full text of the source
• cites Martens and De Schreye [1996] sourceSupported

Probably not a substantial claim: may not pass S3 (load-bearing).

The partial deduction of P with respect to à and ρα is m1(X) ← (1') and t ← m1([]), m1([b]) (2').

“Therefore the partial deduction of P with respect to à and ρ α is 7 (1') m 1 (X) ← (2') t ← m 1 ([]), m 1 ([b])”

The quote only partly states this claim.

In Example 2.4.2, the generalized atom member(a,[a|T]) has a different characteristic tree from member(a,[a,b]) and member(a,[a]), independently of the particular unfolding rule.

“Unfortunately, the generalized atom member (a, [a|T ]) has a different characteristic tree τ , independently of the particular unfolding rule.”

Probably not a substantial claim: may not pass S3 (load-bearing).

In Example 4.2.1, an unfolding rule based on well-founded measures could have continued unfolding more deeply for the first atom, thus avoiding the fake growing problem in this case.

“Indeed, in Example 4.2.1, an unfolding rule based on well-founded measures could have continued unfolding more deeply for the first atom, thus avoiding the fake growing problem in this case.”

May combine two claims.

In practice, the complexity of the transformation does not seem to be all that bad, especially since the experiments were conducted with a prototype not yet tuned for transformation speed.

“But as the experiments in Section 5 show, in practice, the complexity of the transformation does not seem to be all that bad, especially since the experiments were still conducted with a prototype which was not yet tuned for transformation speed.”

• cites Section 5Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Characteristic trees might be a vital asset when trying to solve the parsing problem that appears when unfolding metainterpreters with nontrivial object programs.

“In recent experiments, it also turned out that characteristic trees might be a vital asset when trying to solve the parsing problem [Martens 1994], which appears when unfolding metainterpreters with nontrivial object programs.”

• cites Martens 1994Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

In Example 4.1.1, imposing a depth bound of 100 yields termination, but 100 different characteristic trees and instantiations of the accumulator arise, and the algorithm produces 100 different versions of rev, one for each characteristic tree.

“Imposing a depth bound of say 100, we obtain termination; however, 100 different characteristic trees (and instantiations of the accumulator) arise, and the algorithm produces 100 different versions of rev : one for each characteristic tree.”

May combine two claims.

In Example 4.1.2, an infinite sequence of ever-growing characteristic trees results, giving nontermination without a depth bound and very unsatisfactory ad hoc specializations with it.

“An infinite sequence of ever-growing characteristic trees results, and again, as in Example 4.1.1,we obtain nontermination without a depth bound, and very unsatisfactory ad hoc specializations with it.”

May combine two claims.

In Example 4.2.1, the atoms in the leaves of the second tree are more general than those already met, and simply continuing partial deduction without generalization will lead to natural termination without any depth bound intervention.

“However, the atoms in the leaves of the second tree are more general than those already met, and simply continuing partial deduction without generalization will lead to natural termination without any depth bound intervention.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The authors' methods were successfully adapted to automatically control the recently developed conjunctive partial deduction.

“We can, however, already point out that our methods were successfully adapted to automatically control the recently developed conjunctive partial deduction (see Section 6).”

Probably not a substantial claim: may not pass S3 (load-bearing).

In the setting of unfolding metainterpreters with nontrivial object programs, a growing of the syntactic structure does not imply a growing of the characteristic tree.

“In such a setting a growing of the syntactic structure also does not imply a growing of the characteristic tree.”

May combine two claims.

ECCE-x outperforms the other systems for speed and code size, and has the best worst-case performance.

“the system ECCE-x clearly outperforms the others, for speed as well as for code size, while having the best worst-case performance.”

The quote only partly states this claim.

Removing the depth bound drastically decreases total transformation time by a factor of 42.

“a factor of 42.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The benchmark programs include a set of more involved and realistic examples, such as a model-elimination theorem prover and a metainterpreter for an imperative language.

“In addition to the benchmarks by Lam and Kusalik [1990] they contain a whole set of more involved and realistic examples, for example, such as a model-elimination theorem prover and a metainterpreter for an imperative language.”

• cites Lam and Kusalik 1990Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

For SP, the nontermination symbol means real nontermination; for MIXTUS, heap overflow after 20 minutes; for PADDY, a thorough system crash after 2 minutes.

“-⊥, SP: this means”

• cites Gallagher 1991 sourceNot checked — no full text of the source

May combine two claims.

Extensive experiments with an implementation of the method showed its practical value: it outperformed existing partial-deduction systems for speedup and code size while guaranteeing termination.

“Extensive experiments with an implementation of the method showed its practical value: outperforming existing partial-deduction systems for speedup as well as code size while guaranteeing termination.”

May combine two claims.

Removing the depth bound (ECCE-x) increases total speedup from 2.13 to 2.51 and weighted speedup from 2.23 to 2.75, while decreasing specialized code size from 235KB to 142KB.

“by removing the depth bound (ECCE-x) we increase the total speedup from 2.13 to 2.51 (and the weighted speedup from 2.23 to 2.75) while decreasing the size of the specialized code from 235KB down to 142KB.”

Probably not a substantial claim: may not pass S3 (load-bearing).

ECCE is publicly available.

“The system which integrates the ideas of this article, called ECCE, is publicly available [Leuschel 1996]”

• cites Leuschel 1996Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

ECCE is an implementation of a generic version of Algorithm 4.6.1 that allows the advanced user to change or implement the unfolding rule, the abstraction operator, and the nontermination detection method.

“The system which integrates the ideas of this article, called ECCE, is publicly available [Leuschel 1996] and is actually an implementation of a generic version of Algorithm 4.6.1, which allows the advanced user to change and even implement for example the unfolding rule as well as the abstraction operator and nontermination detection method.”

May combine two claims.

For some benchmarks the depth bound of 10 was too shallow, while for others it was too deep and caused excessive transformation times.

“for some benchmarks the depth bound of 10 was too shallow (e.g., relative) while for others it was too deep and resulted in excessive transformation times (e.g., model-elim.app).”

Probably not a substantial claim: may not pass S3 (load-bearing).

By adapting the settings of ECCE, one can simulate a global tree-oriented version of Algorithm 3.4.3 using depth bounds to ensure termination.

“But one can also simulate a (global tree-oriented) version of Algorithm 3.4.3using depth bounds to ensure termination.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

For some new benchmark tasks it is impossible to get big speedups; the goal of these tasks is to test whether no pessimization, code explosion, or nontermination occurs.

“For some of these new benchmark tasks it is impossible to get (big) speedups-the goal of these tasks consists in testing whether no pessimization, code explosion or nontermination occurs.”

May combine two claims.

ECCE's transformation times are reasonable and usually close to those of MIXTUS.

“the transformation times are reasonable and usually close to the ones of MIXTUS.”

May combine two claims.

The weighted speedup of ECCE-x is 2.75, and the speedup for the fully unfoldable benchmarks is 2.02.

“The weighted speedup of ECCE-x is 2.75, and the speedup for the fully unfoldable benchmarks is 2.02”

Probably not a substantial claim: may not pass S3 (load-bearing).

By adapting the settings of ECCE, one can obtain exactly Algorithm 4.6.1.

“For instance, by adapting the settings of ECCE, one can obtain exactly Algorithm 4.6.1.”

May combine two claims.

ECCE-x-10's transformation times, weighted speedup, and size of specialized code are not so good.

“Its transformation times, weighted speedup, and size of the specialized code are not so good.”

May combine two claims.

Algorithm 4.3.6 produces as output a characteristic tree τ such that if chtree(G, P, U) = τ_A (respectively τ_B), then for some U, chtree(G, P, U) = τ; the same holds for any τ_i arising during the execution.

“Lemma 4.3.8.Algorithm 4.3.6 terminates and produces as output a characteristic tree τ such that if chtree(G, P, U ) = τ A (respectively τ B ), then for some U , chtree(G, P, U ) = τ .The same holds for any τ i arising during the execution of Algorithm 4.3.6.”

May combine two claims.

For all i in {1, ..., n}, vi ≤ wi, and either the abstraction operator performs no modification (and v = w) or the well-founded measure hvecT strictly decreases.

“We have that ∀i ∈ {1, . . ., n} : v i ≤ w i and either the abstraction operator performs no modification (and v = w) or the well-founded measure hvec T strictly decreases.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The inverse of the mapping ., introduced in the proof of Proposition 4.4.9, is not total but still strictly monotonic.

“Also note that the inverse of the mapping ., introduced in the proof of Proposition 4.4.9, is not total but still strictly monotonic.”

• cites Proposition 4.4.9Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

The global tree in Figure 6 also contains two nodes which are variants of their parent node.

“The global tree in Figure6also contains two nodes which are variants of their parent node.”

• cites Figure 6Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

In the member program from Example 2.3.4, with A = member(a, [a]), τ = {1:1, 1:2} and τ' = {1:1}, γP(A, τ) = γP(A, τ') = {member(a, [a])}, but neither (A, τ) ca (A, τ') nor (A, τ') ca (A, τ) hold.

“Take the member program from Example 2.3.4,and let A = member (a, [a]), τ = { 1 : 1 , 1 : 2 } and τ = { 1 : 1 }.Then γ P (A, τ ) = γ P (A, τ ) = {member(a, [a])} (because the resolvent ← member (a, []) associated with 1 : 2 fails finitely), but neither (A, τ ) ca (A, τ ) nor (A, τ ) ca (A, τ ) hold.”

• cites Example 2.3.4Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

Although the abstraction operator chabs_P,U performs well in many practical cases, it does not always preserve characteristic trees, causing sometimes severe loss of precision and specialization.

“Unfortunately, although for a lot of practical cases chabs P,U performs quite well, it does not always preserve the characteristic trees, entailing a sometimes quite severe loss of precision and specialization.”

Classified as probably not a substantial claim.

The characteristic tree captures all the relevant aspects of specialization attained by local control for a particular atom.

“The characteristic tree captures all the relevant aspects of specialization, attained by the local control for a particular atom:”

Classified as probably not a substantial claim.

The set of concretizations associated with a characteristic atom is downward closed (closed under substitution).

“Note that by definition the set of concretizations associated with a characteristic atom is downward closed (or closed under substitution).”

May combine two claims.

An abstraction operator that uses the most specific generalization based on syntactic structure is unsatisfactory because it involves an ad hoc maximum number and because syntactic structure does not reflect context-dependent specialization behavior.

“This approach is however unsatisfactory.First, it involves an ad hoc maximum number, which might lead to either too much or too little polyvariance, depending on the context.Second, the msg is just based on the syntactic structure of the atoms to be specialized.This is generally not such a good idea.”

May combine two claims.

A specialization aspect not captured by a characteristic tree is how the atoms in the leaves of the associated SLDNF-tree are further specialized; global control and precision are not captured.

“A specialization aspect that does not materialize within a characteristic tree is how the atoms in the leaves of the associated SLDNF-tree are further specialized, i.e., the global control and precision are not captured.”

May combine two claims.

The paper solves the two problems of preserving characteristic trees upon generalization and eliminating the ad hoc depth bound.

“In the present article, we solve these two problems.”

May combine two claims.

The syntactic structures of atoms alone provide insufficient information for satisfactory control of polyvariance, and a refined abstraction operator should also take the associated SLDNF-trees into consideration.

“This illustrates that the syntactic structures of B and C alone provide insufficient information for a satisfactory control of polyvariance and that a refined abstraction operator should also take the associated SLDNF-trees into consideration.”

May combine two claims.

By examining only nonfailing branches, the characteristic tree does not capture how exactly some branches were pruned, but this is adequate and beneficial.

“By examining only the nonfailing branches we do not capture how exactly some branches were pruned.The following example illustrates why this is adequate and even beneficial.”

Classified as probably not a substantial claim.

The concretizations of an unconstrained characteristic atom are identical to the instances of its ordinary atom component.

“The concretizations of an unconstrained characteristic atom (A, τ A ) are identical to the instances of the ordinary atom A (because the concretizations are downward closed, and γ P (A, τ ) contains no atom strictly more general than A).”

May combine two claims.

Failure to preserve characteristic trees upon generalization may lead to significant losses in specialization and to problems for termination of the partial deduction process.

“This may lead to significant losses in specialization, as well as to problems for the termination of the partial deduction process.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The practical relevance and benefits of the proposed approach are illustrated through extensive experiments.

“The practical relevance and benefits of the work are illustrated through extensive experiments.”

Classified as probably not a substantial claim.

A is a precise concretization of chatom(A, P, U).

“Note that A is a precise concretization of chatom(A, P, U )”

May combine two claims.

Failing branches do not materialize within the resultants, and a single resultant can be used for atoms with the same characteristic tree without losing specialization.

“However, this is of no relevance, because the failing branches do not materialize within the resultants (i.e., the specialized code generated for the atoms), and furthermore the single resultant member (a, [a|T ]) ← could be used for both A and B without loosing any specialization.”

May combine two claims.

Algorithm 4.3.6 produces as output a characteristic tree τ such that if chtree(G, P, U) = τA or τB, then for some U, chtree(G, P, U) = τ.

“Algorithm 4.3.6 terminates and produces as output a characteristic tree τ such that if chtree(G, P, U ) = τ A (respectively τ B ), then for some U , chtree(G, P, U ) = τ .”

Probably not a substantial claim: may not pass S3 (load-bearing).

The partial deduction method of Gallagher [1991] was extended by de Waal [1994] by adorning characteristic trees with a depth-k abstraction of the corresponding atom component.

“the partial deduction method of Gallagher [1991] was extended by de Waal [1994] by adorning characteristic trees with a depth-k abstraction of the corresponding atom component.”

• cites Gallagher [1991] sourceNot checked — no full text of the source
• cites de Waal [1994]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

Normalizing characteristic trees by imposing a fixed (e.g., left-to-right) computation rule and delaying the selection of all negative literals to the end solves the problem of characteristic trees carrying too much information.

“A quite simple solution to this problem exists: after having performed the local unfolding we just have to normalize the characteristic trees by imposing a fixed (e.g., left-to-right) computation rule and delaying the selection of all negative literals to the end.”

May combine two claims.

Algorithm 4.6.1 can be seen as performing an abstract interpretation on an infinite domain of infinite height (the ascending chain condition of Cousot and Cousot [1992] is not satisfied) and without a priori limitation of precision.

“Algorithm 4.6.1 can also be seen as performing an abstract interpretation on an infinite domain of infinite height (i.e., the ascending chain condition of Cousot and Cousot [1992] is not satisfied) and without a priori limitation of the precision (i.e., if possible, we do not perform any abstraction at all and obtain simply the concrete results).”

• cites Cousot and Cousot [1992] sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

These nodes in the marked partial process tree only contain syntactical information corresponding to ordinary atoms (or rather goals).

“These nodes, however, only contain syntactical information corresponding to ordinary atoms (or rather goals; see Section 6).”

Probably not a substantial claim: may not pass S3 (load-bearing).

In Sørensen and Glück [1995], a generalization strategy for positive supercompilation (no negative information propagation while driving) is proposed.

“In the latter, a generalization strategy for positive supercompilation (no negative information propagation while driving) is proposed.”

• cites Sørensen and Glück [1995] sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The results and discussions of the article remain valid independently of whether the normalization of characteristic trees is applied or not.

“The results and discussions of this article remain valid, independently of whether this normalization is applied or not.”

May combine two claims.

The authors' method is free of ad hoc depth bounds and, without the Section 4.8 postprocessing, nevertheless obtains a similar effect to de Waal's depth-k abstraction.

“Our method is free of any such bounds and (without the Section 4.8 postprocessing) nevertheless obtains a similar effect.”

May combine two claims.

Computations influenced by one or more growing data structures are not so rare after all, and they cause ad hoc behavior of partial deduction where global control is founded on characteristic trees with a depth bound.

“Summarizing, computations influenced by one or more growing data structures are not so rare after all, and they cause ad hoc behavior of partial deduction, where the global control is founded on characteristic trees with a depth bound.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The global control method as laid out in Section 4 has considerable complexity as a possible drawback.

“Returning to the global control method as laid out in Section 4, one can observe that a possible drawback might be its considerable complexity.”

May combine two claims.

The msg for characteristic atoms is a most specific generalization and is unique up to variable renaming.

“Note that the above msg for characteristic atoms is indeed a most specific generalization (because msg(A 1 , A 2 ) and msg(τ 1 , τ 2 ) are most specific generalizations for the atom and characteristic tree parts respectively) and is still unique up to variable renaming.”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Such duplicated polyvariance is superfluous (in the context of simply running the resulting program) when it increases neither local nor global precision.

“Such”

Probably not a substantial claim: may not pass S3 (load-bearing).

The generalization strategy in Sørensen and Glück [1995] uses ¢ to compare nodes in a marked partial process tree, a notion originating from Glück and Klimov [1993] and corresponding to global trees in partial deduction.

“It uses ¢ to compare nodes in a marked partial process tree: a notion originating from Glück and Klimov • 241 [1993] and corresponding to global trees in partial deduction.”

• cites Glück and Klimov [1993] sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

Testing for well-quasi-ordering unavoidably entails searching and repeated comparisons with several ancestors.

“Testing for well-quasi-ordering, however, unavoidably does entail such searching and repeated comparisons with several ancestors.”

Classified as probably not a substantial claim.

The homeomorphic embedding relation ¢ as defined in Definition 4.4.2 is rather crude with respect to variables; all variables are treated as if they were the same variable.

“However, as can be observed in Example 4.4.3, the homeomorphic embedding relation ¢ as defined in Definition 4.4.2 is rather crude with respect to variables.In fact, all variables are treated as if they were the same variable, a practice which is undesirable in a logic programming context.”

Probably not a substantial claim: may not pass S3 (load-bearing).

A similar effect to normalization can be obtained, in the context of definite programs, via the trace terms of Gallagher and Lafave [1996].

“A similar effect can be obtained, in the context of definite programs, via the trace terms of Gallagher and Lafave [1996].”

• cites Gallagher and Lafave [1996] sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

The depth-k abstraction in de Waal's extension was done to increase polyvariance so that a monovariant postprocessing abstract interpretation phase detecting useless clauses can obtain a more precise result.

“This was done in order to increase the amount of polyvariance so that a (monovariant) postprocessing abstract interpretation phase (detecting useless clauses) can obtain a more precise result.”

• cites de Waal [1994]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

May combine two claims.

p(X, X) can be seen as standing for something like and(eq(X, Y), p(X, Y)), which clearly embeds p(X, Y), but the reverse does not hold.

“Indeed p(X, X) can be seen as standing for something like and(eq(X, Y ), p(X, Y )), which clearly embeds p(X, Y ), but the reverse does not hold.”

Probably not a substantial claim: may not pass S4 (based).

The conditions of Definition 4.4.8 are essential for the termination of Algorithm 4.6.1.

“The conditions of Definition 4.4.8 are essential for the termination of a Algorithm 4.6.1.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The complexity of the minimization algorithm is O(kn^2), where n is the maximum number of states and k is the number of symbols.

“As stated by Hopcroft and Ullman [1979], the complexity of this algorithm is O(kn 2 ), where n is the maximum number of states (in our case the number of characteristic atoms), and k is the number of symbols (in our case the maximum number of leaf atoms).”

• cites Hopcroft and Ullman [1979]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The generalization strategy as well as the generation of polyvariance in functional-logic partial evaluation remains entirely based on syntactic structure of the manipulated expressions.

“On the other hand, the generalization strategy as well as the generation of polyvariance remains entirely based on syntactic structure of the manipulated expressions.”

Probably not a substantial claim: may not pass S4 (based).

To the best of the authors' knowledge, this is the very first such method.

“To the best of our knowledge, this is the very first such method.”

May combine two claims.

The homeomorphic embedding relation of Definition 4.4.2 has to be adapted because some built-ins can dynamically construct infinitely many new constants and functors, so it is no longer a well-quasi-order.

“Also, the homeomorphic embedding relation ¢ of Definition 4.4.2(and the relations ¢ * and ¢ * ca based on it) has to be adapted.Indeed, some built-ins (like = ../2 or is/2) can be used to dynamically construct infinitely many new constants and functors, and thus ¢ is no longer a WQO.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Winsborough [1992] aims at minimizing polyvariance in the context of multiple specialization by optimizing compilers.

“The former aims at minimizing polyvariance in the context of multiple specialization by optimizing compilers.”

• cites Winsborough [1992] sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

MIXTUS-like unfolding seems to be a good compromise for standard partial deduction.

“The”

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

The quality of the specialization produced by any fully concrete instance of Algorithm 4.6.1 depends heavily on the quality of the specific local control used.

“the quality of the specialization produced by any fully concrete instance of Algorithm 4.6.1 will obviously also depend heavily on the quality of the specific local control used.”

May combine two claims.

With the removal of non-executable built-ins from generalized characteristic trees, the concretization definition for characteristic atoms scales up, and the technique ensures correct specialization.

“With that, the concretization definition for characteristic atoms scales up, and the technique will ensure correct specialization.”

• AssumptionThe authors state this as an assumption: The Prolog built-ins handled by ECCE are declarative.

May combine two claims.

The abstraction operator preserves the characteristic trees of the atoms to be specialized and ensures termination when the number of distinct characteristic trees is bounded, while providing fine-grained control of polyvariance.

“the abstraction operator of the algorithm preserves the characteristic trees of the atoms to be specialized and ensures termination (when the number of distinct characteristic trees is bounded) while providing a fine-grained control of polyvariance.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The global control techniques presented in the article can be extended and significantly contribute in the context of more powerful unfold/fold-like transformations.

“It turned out that the global control techniques presented in the current article can be extended and that they significantly contribute in that context too”

• cites Leuschel et al. [1996]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Glück et al. [1996]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Leuschel [1997a]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S1 (asserted), S3 (load-bearing), S4 (based). May combine two claims.

MIXTUS-like unfolding is the unfolding strategy explained by Sahlin [1991;1993], which in general unfolds deeply enough to solve the fully unfoldable problems, but also has safeguards against excessive unfolding and code explosion.

“-”

• cites Sahlin 1991Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

• cites Sahlin 1993 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

SP seems to employ a refined determinate unfolding rule, as indicated by the results for the benchmark depth.lambelow.

“Note however that SP seems to employ a refined determinate unfolding rule (as indicated for example by the results for the benchmark depth.lambelow).”

Borderline on S4 (based): unclear from the text.

The resulting specializer improves significantly upon earlier work with respect to speed and size of the specialized programs.

“The resulting specializer improves significantly upon earlier work with respect to speed and size of the specialized programs.”

Probably not a substantial claim: may not pass S3 (load-bearing).

The MIXTUS-like unfolding strategies of ECCE, MIXTUS, and PADDY differ slightly from each other, probably due to details not fully elaborated in Sahlin [1993] and Prestwich [1992a] and the different global control regimes.

“Note that the”

• cites Sahlin 1993 sourceNot checked — no full text of the source
• cites Prestwich 1992aNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

Sufficient memory was given to the Prolog system to prevent garbage collection.

“Sufficient memory was given to the Prolog system to prevent garbage collection.”

Probably not a substantial claim: may not pass S3 (load-bearing).

MIXTUS-like unfolding requires a number of ad hoc settings.

“It requires, however, a number of ad hoc settings.”

• cites Sahlin 1993 sourceNot checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

The benchmark programs were carefully selected and/or designed to cover a wide range of different application areas.

“The benchmark programs were carefully selected and/or designed in such a way that they cover a wide range of different application areas”

Probably not a substantial claim: may not pass S3 (load-bearing).

As proven by Leuschel [1997b], it is possible to perform the not-strict-instance test for the embedding relation recursively within the structure of the expressions.

“Furthermore, as proven by Leuschel [1997b], it is possible to perform the”

• cites Leuschel 1997bNot matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Transformation times of ECCE and MIXTUS include the time to write the specialized program to file; time for SP does not; for PADDY it is unknown.

“-Transformation times (TT): The transformation times of ECCE and MIXTUS include the time to write the specialized program to file.Time for SP does not, and for PADDY we do not know.”

Probably not a substantial claim: may not pass S2 (checkable). May combine two claims.

The ideas presented in the article make sense in theory on accounts of elegance, generality, precision, and termination, and they also pay off in practice.

“the ideas presented in this article do not only make sense in theory on accounts of elegance, generality, precision, and termination, but they also pay off in practice.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

All timings were for renamed queries, except for the original programs and for SP; SP does not rename the top-level query, putting SP at a disadvantage of about 10% in average for speed but at an advantage for code size.

“All timings were for renamed queries, except for the original programs and for SP (which does not rename the top-level query-this puts SP at a disadvantage of about 10% in average for speed, but at an advantage for code size).”

May combine two claims.

The framework and the algorithm can handle normal logic programs and place no restrictions on the unfolding rule.

“The framework and the algorithm can handle normal logic programs and place no restrictions on the unfolding rule.”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

The possibility of calling the specialized program in an unrenamed style was not used in the benchmarks, but avoids distortions in the code size figures.

“This possibility was not used in the benchmarks, but avoids distortions in the code size figures (with respect to MIXTUS and ECCE).”

Classified as probably not a substantial claim.

In computing averages and totals, the time and size of the original program were taken in case of nontermination, so MIXTUS, PADDY, and SP were not punished for nontermination.

“In computing averages and totals, the time and size of the original program were taken in case of nontermination (i.e., we did not punish MIXTUS, PADDY, and SP for the nontermination).”

Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

Determinate unfolding selects only, except once, atoms that match a single clause head, and is refined with a lookahead to detect failure at a deeper level.

“-Determinate unfolding: Only (except once) select atoms that match a single clause head.The strategy is refined with a”

May combine two claims.

Because any instance of an atom in the goal G is a precise concretization of a characteristic atom in Ã0, the conditions of Theorem 3.3.2 are satisfied for goals G whose atoms are instances of atoms in G, i.e., G is P-covered by Ãk.

“Hence, because any instance of an atom in the goal G is a precise concretization of a characteristic atom in Ã0 , the conditions of Theorem 3.3.2are satisfied for goals G whose atoms are instances of atoms in G, i.e., G is P -covered by Ãk .”

• cites Theorem 3.3.2Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

All results so far also hold for multisets of characteristic atoms.

“However, this poses no problems, as all results so far also hold for multisets of characteristic atoms.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Usually, atoms which are variants of one of their ancestor nodes will not be added to the global tree, as they do not give rise to further specialization.

“Usually, atoms which are variants of one of their ancestor nodes will not be added to the global tree, as they do not give rise to further specialization.”

Probably not a substantial claim: may not pass S3 (load-bearing).

Marlet [1994] also proposes to consider all possible numberings, but leading to n! complexity, where n is the number of variables in the terms to be compared.

“Marlet [1994] also proposes to consider all possible numberings, but (leading to n! complexity, where n is the number of variables in the terms to be compared).”

• cites Marlet [1994]Not checked — no full text of the source

Probably not a substantial claim: may not pass S3 (load-bearing).

The definition of . does not make the notion of an msg for characteristic trees, as well as Algorithm 4.3.6, superfluous.

“In other words, the definition of .does not make the notion of an msg for characteristic trees, as well as Algorithm 4.3.6,superfluous.”

• cites Algorithm 4.3.6Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.

Probably not a substantial claim: may not pass S3 (load-bearing).

The FAR filtering algorithm of Leuschel and Sørensen [1996] can be used to further improve the specialized program by removing the redundant argument of m1.

“The FAR filtering algorithm ofLeuschel and Sørensen [1996] can be used to further improve the specialized program by removing the redundant argument of m 1 .”

• cites Leuschel and Sørensen [1996]Not matched

  Couldn’t be matched to a paper in Crossref, so it can’t be checked.