Creating specialised integrity checks through partial evaluation of meta-interpreters

From an operational point of view, Gallagher's meta-interpreter lifts the ground representation to the non-ground one for resolution.

“From an operational point of view, this meta-interpreter lifts the ground representation to the non-ground one for resolution”

• cites [29] Gallagher, 1991, A system for specialising logic programsNot matched

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

• cites [30] Gallagher, 1993, Tutorial on specialisation of logic programs sourceDisputed

  In §6.2.1 (page unavailable), Gallagher describes an interpreter for programs represented as ground terms and says that all three arguments of its demo predicate are ground. The discussion of ground and non-ground representations also says that operations such as unification must be coded explicitly for the ground representation. This is contrary to the claim that the interpreter lifts the representation to a non-ground one for resolution. (LLM, conf=0.83)

  Checked by a reasoning model — may be wrong.

  Experimental — accuracy not yet measured

The non-ground representation has semantical problems.

“The non-ground representation also has semantical problems (although they were solved to some extent in [20,66,67]).”

• cites [20] De Schreye, 1992, A sensible least Herbrand semantics for untyped vanilla metaprogramming sourceNot checked — no full text of the source
• cites [66] Martens, 1995, Two semantics for definite meta-programs, using the non-ground representationNot checked — no full text of the source
• cites [67] Martens, 1995, Why untyped non-ground meta-programming is not (much of) a problem, J. Logic Programming sourceSupported

It is possible to combine the ground and non-ground representations.

“Sometimes however, it is possible to combine both approaches.”

• cites [29] Gallagher, 1991, A system for specialising logic programsNot matched

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

• cites [30] Gallagher, 1993, Tutorial on specialisation of logic programs sourceCould not verify

  Section 6.1 describes ground and non-ground representations as two approaches, while Section 6.2 discusses specializing programs that use the ground representation. Neither passage says the representations can be combined; searches for combining or mixing them found no such statement in our copy. Page numbers were not available. (LLM, conf=0.70)

  Experimental — accuracy not yet measured

A straightforward denotational semantics can be given to ITE-Prolog.

“However, the semantics of the if-then-else remains reasonably simple and a straightforward denotational semantics [38], in the style of [4,79], can be given to ITE-Prolog.”

• cites [38] N.D. Jones, A. Mycroft, Stepwise development of operational and denotational semantics for Prolog, in: Proceedings of the 1984 International Symposium on Logic Programming, Atlantic City, NJ, IEEE Computer Soc. Press, Silver Spring, MD, pp. 289–298.Not checked — no full text of the source
• cites [4] Baudinet, 1992, Proving termination of Prolog programs: A semantic approach, J. Logic Programming sourcePartly supported

  Sections 2 and 4 develop functional equations that characterize the meaning of Prolog programs, supporting the citation as an example of a semantics for Prolog. But the paper treats pure Prolog and Prolog with cut, not ITE-Prolog; it does not establish that a straightforward denotational semantics can be given to ITE-Prolog. The indexed passages provide no page numbers. (LLM, conf=0.82)

  Experimental — accuracy not yet measured
• cites [79] Proietti, 1991, Semantics preserving transformation rules for Prolog sourceNot checked — no full text of the source

Partial evaluation of ITE-Prolog can be situated somewhere between partial deduction of pure logic programs and partial evaluation of full Prolog.

“In summary, partial evaluation of ITE-Prolog, can be situated somewhere between partial deduction of pure logic programs (see [60,31,10,69,68] and systems like sP [30,29], sAGE [34,33] or more recently ECCE [50,51,57]) and partial evaluation of full Prolog (e.g. MIXTUs [83,82] or PADDY [76–78]).”

• cites [60] Lloyd, 1991, Partial evaluation in logic programming, J. Logic Programming sourceNot checked — no full text of the source
• cites [31] Gallagher, 1991, The derivation of an algorithm for program specialisation, New Gener. Comput. sourceNot checked — no full text of the source
• cites [10] Bruynooghe, 1992, A general criterion for avoiding infinite unfolding during partial deduction, New Gener. Comput. sourceNot checked — no full text of the source
• cites [69] Martens, 1994, Sound and complete partial deduction with unfolding based on well-founded measures, Theoret. Comput. Sci. sourceSupported
• cites [68] Martens, 1996, Automatic finite unfolding using well-founded measures, J. Logic Programming sourceSupported
• cites [83] Sahlin, 1993, Mixtus: An automatic partial evaluator for full Prolog, New Gener. Comput. sourceNot checked — no full text of the source
• cites [82] Sahlin, 1991, An Automatic Partial Evaluator for Full Prolog sourceNot checked — no full text of the source
• cites [76] Prestwich, 1992, The PADDY partial deduction systemNot matched

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

• cites [77] Prestwich, 1992, An unfold rule for full Prolog sourceNot checked — no full text of the source
• cites [78] Prestwich, 1993, Online partial deduction of large programs sourceSupported

By partially evaluating a meta-interpreter for certain transaction patterns, using a partial evaluation technique presented in earlier work, the authors automatically obtain very efficient specialised update procedures that execute faster than other integrity checking procedures proposed in the literature.

“By partially evaluating this meta-interpreter for certain transaction patterns, using a partial evaluation technique presented in earlier work, we are able to automatically obtain very efficient specialised update procedures, executing faster than other integrity checking procedures proposed in the literature.”

• Also stated in: § 1.2. Motivation and contribution · p. 4 · boosted

  “Through program specialisation, we developed specialised integrity checks which perform significantly better than the best general purpose integrity checking methods currently available.”

• cites [47] Leuschel, 1993, Self-Applicable Partial Evaluation in Prolog sourceNot checked — no full text of the source
• cites [48] Leuschel, 1994, Partial evaluation of the “real thing” sourceNot checked — no full text of the source

• AssumptionRests on an assumption: The selected integrity checking technique and the potential update patterns are static components of the application.

The resulting integrity checking method without specialisation is in general not competitive with LST.

“Nevertheless, the resulting method (without specialisation) is in general not competitive with LST.”

All derivations descending from the goal man(X), woman(X), which do not use Db+, have already been pruned at specialisation time.

“Similarly all derivations descending from the goal man(X), woman(X), which do not use Db+, have also already been pruned at specialisation time.”

The loss of efficiency resulting from not producing instantiated versions of checks was regained through specialisation.

“Our hope and expectation were that the loss of efficiency resulting from not producing instantiated versions of checks would automatically be regained through specialisation. An expectation which turned out to be completely justified.”

Partial evaluation can sometimes completely remove the overhead of the ground representation when using the mixed representation.

“Furthermore, as demonstrated by Gallagher in [29] and by the experiments in this paper, partial evaluation can in this way sometimes completely remove the overhead of the ground representation.”

• cites [29] Gallagher, 1991, A system for specialising logic programsNot matched

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

The LST method itself is not very amenable to program specialisation.

“We observed that this method itself is not very amenable to program specialisation.”

The simplified integrity checking method introduced by the authors does not produce instantiations of checks.

“We therefore introduced a simplified integrity checking method, which does not produce instantiations of checks.”

The specialised update procedure no longer has to calculate pos(U) and neg(U) for the concrete update U.

“Finally, the specialised update procedure no longer has to calculate pos(U) and neg(U) for the concrete update U.”

The specialised integrity checks were extensively faster than an efficient implementation of the LST method.

“The results showed that the specialised integrity checks were extensively faster than an efficient implementation of the LST method.”

Specialisation of tabled logic programs is far from obvious.

“specialisation of tabled logic programs is far from obvious”

These meta-interpreters can be executed without specialisation, in contrast to the original meta-interpreter presented in [29].

“Also note that, in contrast to the original meta-interpreter presented in [29], these meta-interpreters can be executed without specialisation.”

• cites [29] Gallagher, 1991, A system for specialising logic programsNot matched

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

In the example, P4 is obtained from P3 by unfolding the non-leftmost atom q(Y), thereby changing the sequence of computed answers.

“In the example below, P4 is obtained from P3 by unfolding the non-leftmost atom q(Y), thereby changing the sequence of computed answers.”

In Section 6.3, only 10% speedup is achieved using an existing partial evaluator for full Prolog.

“cf. the end of Section 6.3 where only 10% speedup is achieved using an existing partial evaluator for full Prolog”

For the example database with Db+ = {man(a) ←}, Db− = ∅, the LST method of [61] generates the simplified integrity constraints false ← man(a), woman(a) and false ← parent(a, Y), unmarried(a), independently of the facts in Db=.

“The LST method of [61] will then generate the following simplified integrity constraints:”

• cites [61] Lloyd, 1987, Integrity checking in stratified databases, J. Logic Programming sourceNot checked — no full text of the source

The original meta-interpreter of Fig. 6 would test whether there are facts matching woman(X) and only afterwards prune all irrelevant branches.

“whereas the original meta-interpreter of Fig. 6 would test whether there are facts matching woman(X) and only afterwards prune all irrelevant branches.”

Left-propagation of bindings is in general unsafe in the context of ITE-Prolog.

“As we have seen in the previous subsection, left-propagation of bindings is in general unsafe in the context of ITE-Prolog”

Unfolding inside the if-then-else is handled in a rather straightforward manner.

“Unfolding inside the if-then-else is also handled in a rather straightforward manner.”

A lot of these instantiations can be performed by the partial evaluation method, through pruning and safe left-propagation of bindings.

“Fortunately, a lot of these instantiations can be performed by the partial evaluation method, through pruning and safe left-propagation of bindings.”

The update pattern Db+ = {parent(A, B) ←}, Db− = ∅ offers less opportunities for specialisation than the previous update pattern.

“This update pattern offers less opportunities for specialisation than the previous one.”

The transformed clause will generate the same sequence of computed answers as the original clause.

“This clause will generate the same sequence of computed answers than the original clause”

• AssumptionThe authors state this as an assumption: The computed answers of parent/2 are always grounding substitutions.

The procedure obtained by running LST on a generic update will run considerably slower than the specialised update procedure in Fig. 9 obtained by LEUPEL.

“For instance, the above procedure will run (cf. Table 1 in the next subsection) considerably slower than the specialised update procedure in Fig. 9 obtained by LEUPEL.”

The specialised update procedures obtained by using the LEUPEL system performed between 1.6 and 5 times faster than the ones obtained by the fully automatic systems MIXTUS and PADDY.

“Also, the specialised update procedures obtained by using the LEUPEL system performed between 1.6 and 5 times faster than the ones obtained by the fully automatic systems MIXTUS and PADDY.”

With the default term_depth parameter, PADDY slowed down the ic-solve meta-interpreter by about 30%.

“With the default value, PADDY actually slowed down the ic-solve meta-interpreter by about 30%.”

Unfolding the same atom in the program P6 written with the cut leads to an incorrect specialised program in which, e.g., p(a) is no longer a consequence.

“However, unfolding the same atom in the program P6 written with the cut leads to an incorrect specialised program in which, e.g., p(a) is no longer a consequence.”

Compared with an unspecialised implementation of the well known approach by Lloyd et al. [61], the results show that big performance improvements, also reaching and exceeding 2 orders of magnitude, can be obtained.

“We also compared the specialised update procedures with an unspecialised implementation of the well known approach by Lloyd et al. in [61], and the results show that big performance improvements, also reaching and exceeding 2 orders of magnitude, can be obtained.”

• cites [61] Lloyd, 1987, Integrity checking in stratified databases, J. Logic Programming sourceNot checked — no full text of the source

The update procedures generated by LEUPEL perform extremely well.

“As can be seen from the benchmark tables, the update procedures generated by LEUPEL perform extremely well.”

Even for this rather simple example, the fully unfolded integrity constraints become quite numerous.

“So even for this rather simple example, the fully unfolded integrity constraints become quite numerous.”

Even for 838 facts in Table 7, ic-leupel still runs 25 times faster than ic-lst.

“However, even for 838 facts in Table 7, ic-leupel still runs 25 times faster than ic-lst.”

ic-leupel used from 43 to 318 times less heap space than ic-solve.

“We also measured heap consumption of ic-leupel, which used from 43 to 318 times less heap space than ic-solve.”

The partial evaluator LEUPEL and a prototype [49] based upon it can generate specialised update procedures fully automatically.

“We have drawn upon the techniques in [48] and presented the partial evaluator LEUPEL and a prototype [49] based upon it, which can generate specialised update procedure fully automatically.”

• cites [48] Leuschel, 1994, Partial evaluation of the “real thing” sourceNot checked — no full text of the source
• cites [49] Leuschel, 1995, Prototype partial evaluation system to obtain specialised integrity checks by specialising meta-interpreters sourceNot checked — no full text of the source

For efficiency reasons, the implementation still had to make use of a non-declarative verify construct.

“However, for efficiency reasons, the implementation still had to make use of a non-declarative verify construct.”

Speedups reached and exceeded 2 orders of magnitude when specialising the integrity checker for a given set of integrity constraints and a given set of rules.

“Speedups reached and exceeded 2 orders of magnitude when specialising the integrity checker for a given set of integrity constraints and a given set of rules.”

In the specialised integrity constraints for update man(a), parent(a, Y) has been duplicated 4 times.

“Note that the parent(a, Y) has been duplicated 4 times!”

For the update Db+ = {man(a)}, Db− = ∅, unifying the update literals with the body atoms gives the listed specialised integrity constraints.

“For the update Db+ = {man(a)}, Db− = ∅ we then get, by unifying the update literals with the body atoms, the following specialised integrity constraints:”

A lot of integrity checking can already be performed given an update pattern without knowing the actual, concrete update.

“The idea being, that a lot of the integrity checking can already be performed given an update pattern without knowing the actual, concrete update.”

• AssumptionRests on an assumption: The selected integrity checking technique and the potential update patterns are static components of the application.

Concentrating on potential updates has the advantage that one does not have to access the entire database for the update propagation.

“Concentrating on potential updates has the advantage that one does not have to access the entire database for the update propagation.”

For a lot of examples, such as databases with a large number of facts, concentrating on potential updates leads to very good efficiency.

“For a lot of examples, like databases with a large number of facts, this leads to very good efficiency (see, e.g., the experiments in [16,84]).”

• cites [16] Celma, 1994, Comparing and synthesizing integrity checking methods for deductive databasesNot checked — no full text of the source
• cites [84] Seljée, 1995, A new method for integrity constraint checking in deductive databases, Data Knowledge Eng. sourceNot checked — no full text of the source

Reengineering of the input program may be crucial for successful specialisation.

“The main lesson we learned from this work is that reengineering of the input program may indeed be crucial for successful specialisation.”

Specialised integrity checking can be implemented through a meta-interpreter, manipulating updates and databases as object level expressions.

“Specialised integrity checking can be implemented through a meta-interpreter, manipulating updates and databases as object level expressions.”

The difference in speed between the non-ground and ground representations currently reaches several orders of magnitude.

“This (currently) induces a difference in speed reaching several orders of magnitude”

• cites [56] Leuschel, 1995, Partial deduction of the ground representation and its application to integrity checking sourceNot checked — no full text of the source
• cites [51] Leuschel, 1997, Advanced Techniques for Logic Program SpecialisationNot matched

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

• AssumptionRests on an assumption: The main advantage of the non-ground representation is that the meta-program can use the underlying unification mechanism.
• AssumptionRests on an assumption: For the ground representation, an explicit unification algorithm is required.

A method based solely on Definition 2.3 is somewhat restricted in usefulness when the rules and integrity constraints change more often than the facts.

“It, however, also somewhat restricts the usefulness of a method based solely on Definition 2.3 when the rules and integrity constraints change more often than the facts.”

The above method is a refinement of the LST method in that Θ is used not only to simplify integrity constraints at the topmost level but throughout testing to prune non-relevant branches.

“The above method can be seen as a refinement of the LST method [61], in the sense that Θ is not only used to simplify the integrity constraints at the topmost level (i.e. affecting the bodies of integrity constraints), but is used throughout the testing of the integrity constraints to prune non-relevant branches.”

• cites [61] Lloyd, 1987, Integrity checking in stratified databases, J. Logic Programming sourceNot checked — no full text of the source

For the integrity checking method presented in the previous section, the same specialised update procedure can be used as long as the rules and integrity constraints do not change (i.e. Db+ and Db- only contain facts).

“Furthermore, for the integrity checking method we have presented in the previous section, the same specialised update procedure can be used as long as the rules and integrity constraints do not change (i.e. Db+ and Db- only contain facts).”

Let U be a database update such that there is no SLDNF-refutation before U for the goal ← false. Then ← false has an SLDNF-refutation after U iff ← false has a relevant refutation after U.

“Theorem 2.9 (Incremental integrity checking). Let U = (Db+, Db=, Db−〉 be a database update such that there is no SLDNF-refutation before U for the goal ← false. Then ← false has an SLDNF-refutation after U iff ← false has a relevant refutation after U.”

• Also stated in: § 2. Deductive databases and integrity checking · p. 10 · plain

  “In other words, if we know that the integrity constraints of a deductive database were not violated before an update, then we only have to search for a relevant refutation of ← false in order to check the integrity constraints after the update.”

The missing instantiations will often be performed by partial evaluation.

“As it will turn out, the missing instantiations will then often be performed by partial evaluation.”

The main reason LST is not amenable to specialisation is that one of its functionalities is to produce instantiated versions of the integrity checks.

“The main reason is that one of the functionalities in the LST method is to produce instantiated versions of the integrity checks.”

If there exists an incremental SLDNF-derivation after U for G, then G is potentially added by U.

“Lemma 2.7. Let G be a goal and U a database update. If there exists an incremental SLDNF-derivation after U for G, then G is potentially added by U.”

The difference in speed between the non-ground and ground representations can pose subtle problems for specialisation.

“and can pose some subtle problems for specialisation [56,51]”

• cites [56] Leuschel, 1995, Partial deduction of the ground representation and its application to integrity checking sourceNot checked — no full text of the source
• cites [51] Leuschel, 1997, Advanced Techniques for Logic Program SpecialisationNot matched

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

The absence of instantiations allows a rather simple implementation of the method as a meta-interpreter, amenable to effective partial evaluation.

“However, the absence of instantiations allows a rather simple implementation of the method as a meta-interpreter, amenable to effective partial evaluation.”

The reengineered and annotated integrity checker can be specialised over and over for different databases and different update patterns.

“In particular, in the case of our application, the reengineered (and annotated) integrity checker can be specialised over and over for different databases and different update patterns.”

No meta-interpreter using the full ground representation with explicit unification has been made to completely remove the overhead via partial evaluation.

“Performing a similar feat on a meta-interpreter using the full ground representation with explicit unification is much harder and has, to the best of our knowledge, not been accomplished yet”

• cites [34] Gurr, 1994, Specialising the ground representation in the logic programming language Gödel sourceNot checked — no full text of the source
• cites [33] Gurr, 1994, A Self-Applicable Partial Evaluator for the Logic Programming Language Gödel sourceNot checked — no full text of the source
• cites [9] Bowers, 1995, Towards fast and declarative meta-programmingNot matched

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

• cites [56] Leuschel, 1995, Partial deduction of the ground representation and its application to integrity checking sourceNot checked — no full text of the source

The method of relevant derivations used on its own has probably little practical value for larger databases.

“This means that, although the pruning is more refined, 9 the method used on its own has probably little practical value for larger databases.”

With the mixed representation, one can use the versatility of the ground representation for representing object level programs (but not goals), while still remaining reasonably efficient.

“With that technique we can use the versatility of the ground representation for representing object level programs (but not goals), while still remaining reasonably efficient.”

• AssumptionRests on an assumption: The ground representation can be treated in a purely declarative manner.

Some of the pruning will have already taken place during partial evaluation, resulting in little or no overhead due to the extra pruning complexity.

“Furthermore, some of the pruning will have already taken place during partial evaluation, resulting in little or no overhead due to the extra pruning complexity.”

One disadvantage of the non-ground representation is that it is more difficult to specify partial knowledge for partial evaluation.

“One disadvantage of the non-ground representation is that it is more difficult to specify partial knowledge for partial evaluation.”

• AssumptionRests on an assumption: For many applications, the non-ground representation requires the use of extra-logical built-ins (like var/1 or copy/2).

In the non-ground representation, partial knowledge that an atom will be of form man(T) with T unknown constant must be written as man(X), which is less precise than the ground representation's struct(man, [struct(C, [])]).

“In the ground representation this knowledge can be expressed as struct(man, [struct (C, [ ])]). However, in the non-ground representation we have to write this as man(X), which is unfortunately less precise”

In the context of extra-logical built-ins, unfolding a nonleftmost atom can change the program's behaviour.

“In the context of extra-logical built-ins this can change the program's behaviour.”

Without the copy in Fig. 3, the second meta-interpreter would incorrectly fail for the given query.

“Note that without the copy in Fig. 3 the second meta-interpreter would incorrectly fail for the given query.”

A partial evaluator for ITE-Prolog has to ensure the preservation of the sequence of computed answers.

“This implies that a partial evaluator for ITE-Prolog has to ensure the preservation of the sequence of computed answers.”

Such an integrity checker for fully recursive databases will not be amenable to effective specialisation using current techniques.

“Again, such an integrity checker will not be amenable to effective specialisation using current techniques.”

• AssumptionRests on an assumption: In fully recursive databases, a subsumption test (or something even more powerful) is required to perform loop checking inside the integrity checker.

The query `← incremental_solve (''(Db+, Db=, Db-〉'', ← false)` will succeed if the integrity of the database has been violated by the update.

“The query will succeed if the integrity of the database has been violated by the update.”

Once the if-then-else is added, there are no additional semantical difficulties in handling some simple built-in's like var/1, nonvar/1 and =../2 (but not built-in's like call/1 or assert/1 which manipulate clauses and goals).

“Indeed, once the if-then-else is added, there are no additional semantical difficulties in handling some simple built-in's like var/1, nonvar/1 and =../2 (but not built-in's like call/1 or assert/1 which manipulate clauses and goals).”

A simple implementation of an integrity checker that includes instantiation of goals but does not use subsumption tests will perform a lot of redundant checking and is hopelessly inefficient even after specialisation.

“either use a simple implementation without subsumption tests, but which will perform a lot of redundant checking and is hopelessly inefficient (even after specialisation)”

Even determinate unfolding can ruin termination of tabled logic programs.

“even determinate unfolding can ruin termination [58]”

• cites [58] M. Leuschel, B. Martens, K. Sagonas, Preserving termination of tabled logic programs while unfolding, in: N. Fuchs (Ed.), Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR'97), Leuven, Belgium, Lecture Notes in Computer Science, Springer, Berlin, to appear.Not matched

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

Collecting all solutions and performing subsumption tests to keep only the most general ones can only be done declaratively in the ground representation.

“The latter can only be done declaratively in the ground representation [55,56]”

• cites [55] Leuschel, 1995, Obtaining specialised update procedures through partial deduction of the ground representationNot matched

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

• cites [56] Leuschel, 1995, Partial deduction of the ground representation and its application to integrity checking sourceNot checked — no full text of the source

To preserve the sequence of computed answers, a problem related to the left-propagation of bindings must be addressed.

“In order to preserve the sequence of computed answers, we have to address a problem related to the left-propagation of bindings.”

Based on Theorem 2.9, one can stop resolving a goal G when it is not potentially added, unless an incremental resolution step has been performed earlier in the derivation.

“Based on Theorem 2.9, we know that we can stop resolving a goal G when it is not potentially added, unless we have performed an incremental resolution step earlier in the derivation.”

• cites Theorem 2.9Not matched

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

Because the if-then-else contains a local cut, its behaviour is sensitive to the sequence of computed answers of the test-part.

“Because the if-then-else contains a local cut, its behaviour is sensitive to the sequence of computed answers of the test-part.”

The disadvantage of using verify is that no instantiations at all are performed, which in general cuts down the search space dramatically.

“The disadvantage of using verify is of course that now no instantiations at all are performed (which in general cut down the search space dramatically).”

Using the clause representation implies that representing updates to a database becomes much more cumbersome.

“On the other hand, using the clause representation, implies that representing updates to a database becomes much more cumbersome.”

In the context of hierarchical databases and the paper's new integrity checking method, wrapping calls to potentially_added/2 into a verify(.) primitive solves the problem of duplicate and subsumed solutions.

“This will solve the problem of duplicate and subsumed solutions.”

For non-ground goals, the verify(.) primitive is not declarative.

“Unfortunately, for non-ground goals, the verify(.) primitive is not declarative.”

The computation rule and the search rule have to be fixed in order to give a clear meaning to the if-then-else.

“This means that the computation rule and the search rule have to be fixed in order to give a clear meaning to the if-thenelse.”

Using the clause representation requires encoding updates explicitly as meta-program clauses, thereby making dynamic meta-programming impossible.

“Basically we also have to encode the updates explicitly as meta-program clauses, thereby making dynamic meta-programming (see e.g. [35]) impossible.”

• cites [35] Hill, 1998, Meta-programming in logic programmingNot matched

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

Unfolding a nonleftmost atom in a clause might instantiate the atoms to the left of it or the head of the clause.

“For instance, unfolding a nonleftmost atom in a clause might instantiate the atoms to the left of it or the head of the clause.”

In the non-ground or mixed representation, extra-logical primitives like findall or numbervars are required.

“In the non-ground or mixed representation extra-logical primitives like findall (to collect all possible instantiations) or numbervars (for the subsumption tests) are required”

verify(Goal) can be translated into the Prolog if-then-else construct.

“Indeed, verify(Goal) can be translated into”

These instantiations can often be performed by program specialisation.

“However, as will see later, these instantiations can often be performed by program specialisation.”

This instantiation performed by the partial evaluator is in fact the reason for the extremely high speedup figures presented in the results of Section 6.

“This instantiation performed by the partial evaluator is in fact the reason for the extremely high speedup figures presented in the results of Section 6.”

The only way to improve the specialised update procedure for adding man() would be to add the information that the predicates in the intensional and the extensional database are disjoint.

“The only way to improve it, would be to add the information that the predicates in the intensional and the extensional database are disjoint.”

• AssumptionRests on an assumption: For most applications, the predicates in the intensional and the extensional database are disjoint.

The treatment of cuts requires some rather involved techniques.

“The treatment of cuts therefore requires some rather involved techniques (see [14], [83,82] or [77,76]).”

• cites [14] Bugliesi, 1989, Partial evaluation in Prolog: Some improvements about cutNot matched

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

• cites [83] Sahlin, 1993, Mixtus: An automatic partial evaluator for full Prolog, New Gener. Comput. sourceNot checked — no full text of the source
• cites [82] Sahlin, 1991, An Automatic Partial Evaluator for Full Prolog sourceNot checked — no full text of the source
• cites [77] Prestwich, 1992, An unfold rule for full Prolog sourceNot checked — no full text of the source
• cites [76] Prestwich, 1992, The PADDY partial deduction systemNot matched

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

• AssumptionRests on an assumption: The full cut can have an effect on all subsequent clauses defining the predicate under consideration.

In some cases, specialised update procedures can be improved by performing a safe left-propagation of bindings.

“In some cases we can also improve the specialised update procedures by performing a safe left-propagation of bindings.”

For range restricted database predicates, the computed answers of parent/2 are always grounding substitutions.

“This is always guaranteed for range restricted (see e.g. [13]) database predicates.”

• cites [13] Bry, 1991, Integrity verification in knowledge basesNot matched

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

It is therefore much easier to handle by a partial evaluator.

“It is therefore much easier to handle by a partial evaluator.”

• AssumptionRests on an assumption: The cut inside the if-then-else is local and does not affect the reachability and meaning of other clauses.

The second clause will be much more efficient - the call to parent will just succeed once for every child of A instead of succeeding for the entire parent relation.

“Therefore, the second clause will be much more efficient – the call to parent will just succeed once for every child of A instead of succeeding for the entire parent relation.”

Useless if-then-else tests often occur when predicates with output arguments are used inside the test-part of an if-then-else.

“The latter often occur when predicates with output arguments are used inside the test-part of an if-thenelse.”

• cites [48] Leuschel, 1994, Partial evaluation of the “real thing” sourceNot checked — no full text of the source

By unfolding, the scope of a cut can be changed, thereby altering its effect.

“By unfolding, the scope of a cut can be changed, thereby altering its effect.”

• AssumptionRests on an assumption: The full cut can have an effect on all subsequent clauses defining the predicate under consideration.

Specialised update procedures obtained by running LST on a generic update will in general only be slightly faster than fully re-checking the integrity constraints after each update.

“This means that the specialised update procedures we obtain by this technique will in general only be slightly faster than fully re-checking the integrity constraints after each update.”

Even using the current implementation, the time invested into partial evaluation should pay off rather quickly for larger databases.

“Still, even using the current implementation, the time invested into partial evaluation should pay off rather quickly for larger databases.”

• AssumptionRests on an assumption: The frequency with which updates and integrity checks are performed is significantly higher than that of remodelling and specialising the static part of the database.
• AssumptionRests on an assumption: Updates are often performed interactively, on-line, making acceptably fast execution important, while respecialisation would typically be performed in background, requiring less efficiency.

A disadvantage of using verify is that no instantiations at all are performed.

“At the end of Section 4 we pointed out that a disadvantage of using verify is that no instantiations at all are performed.”

Using annotations, combined with restricting attention to ITE-Prolog instead of full Prolog, pays off in better specialisation.

“This shows that using annotations, combined with restricting the attention to ITE-Prolog instead of full Prolog, pays off in better specialisation.”

There are some circumstances where bindings can be left-propagated without affecting the correctness of the specialised program.

“There are, however, some circumstances where bindings can be left-propagated without affecting the correctness of the specialised program.”

By Theorem 2.9, the derivation leading to ← woman(a), ¬married_woman(a) can be pruned and will never lead to a successful refutation, given that the database was consistent before the update.

“Hence, by Theorem 2.9, this derivation can be pruned and will never lead to a successful refutation, given the fact that the database was consistent before the update.”

• AssumptionRests on an assumption: The database was consistent before the update.

Given the available information, the simplification of the integrity constraints produced by the LST method in the example is not optimal.

“Given the available information, this simplification of the integrity constraints is not optimal.”

The larger the database becomes, the more time will be needed on the actual evaluation of the simplified constraints and not on the simplification.

“Of course, the larger the database becomes, the more time will be needed on the actual evaluation of the simplified constraints and not on the simplification.”

Even for relational databases with complex views, deductive database approaches such as the LST method [61] seem to be the most competitive ones available.

“However, even for relational databases - with complex views – the deductive database approaches, such as the LST method [61], seem to be the most competitive ones available.”

• cites [61] Lloyd, 1987, Integrity checking in stratified databases, J. Logic Programming sourceNot checked — no full text of the source

The mixed representation, in which the object program is represented using the ground representation but goals are lifted to the non-ground representation for resolution, has the advantage of using the flexibility of the ground representation for representing knowledge about the object program while using the efficiency of the non-ground representation for resolution.

“This approach has the advantage of using the flexibility of the ground representation for representing knowledge about the object program (in our case the deductive database along with the updates), while using the efficiency of the non-ground representation for resolution.”

Some existing integrity checking methods, such as the Lloyd-Sonenberg-Topor method [61], are not amenable to specialisation using current techniques.

“We have also argued why some existing integrity checking methods, like, e.g., the Lloyd-Sonenberg-Topor method [61], are not amenable to specialisation using current techniques.”

• cites [61] Lloyd, 1987, Integrity checking in stratified databases, J. Logic Programming sourceNot checked — no full text of the source

The relative difference between ic-lst and ic-leupel diminishes with a growing database.

“That is why the relative difference between ic-lst and ic-leupel diminishes with a growing database.”

The high speedups are also due to the fact that the partial evaluator performs part of the integrity checking.

“These high speedups are also due to the fact that the partial evaluator performs part of the integrity checking.”

Given proper care in writing a meta-interpreter, partial evaluation is capable of automatically generating highly specialised update procedures for hierarchical databases with negation.

“To summarise, we have shown that, given proper care in writing a meta-interpreter, partial evaluation is capable of automatically generating highly specialised update procedures for hierarchical databases with negation.”

The simpler alternative of mapping down intensional database relations to extensional ones through full unfolding of views and performing relational integrity checking on extensional database predicates tends to create extensive redundant multiplication of checks.

“The simpler alternative of mapping down intensional database relations to extensional ones (through full unfolding of the views) and performing relational integrity checking on the extensional database predicates, tends to create extensive redundant multiplication of checks.”

The resulting simplified integrity checks are not nearly as efficient as the specialised update procedure in Fig. 9, especially if a has a lot of children, which executes parent(a, Y) only once.

“The resulting simplified integrity checks are thus not nearly as efficient as our specialised update procedure in Fig. 9 (especially if a has a lot of children), which executes this parent(a, Y) only once.”

For more complicated examples, entire conjunctions will get duplicated, making the situation worse.

“For more complicated examples, entire conjunctions will get duplicated, making the situation worse.”