Philippe A Martin

Lim

Evaluating Ontology Completeness via SPARQL and Relations-between-classes based Constraints

Keywords: constraints, ontology completeness, OWL, SPARQL

This article first distinguishes constraints from rules, and descriptive constraints from prescriptive ones. Both kinds can be used to calculate a constraint-based completenesses (as opposed to a real-world-based completeness), i.e. evaluating how much of a knowledge base is complete with respect to some constraints, e.g. for evaluating how well this base follows given ontology design patterns or best practices. Such evaluations may also guide knowledge elicitation and modelisation. This article explores the ways constraints can be represented via relations between classes, hence via any knowledge representation language (KRL) that has an expressiveness at least equal to RDF or RDFS. Compared to the popular practice of both representing and checking constraints via queries, this approach is as simple, offers more possibilities for exploiting both knowledge and constraints, and permits the selection and use of inference engines adapted to the expressiveness of the exploited knowledge instead of the use of restricted or ad hoc constraint-validation tools. This approach is also modular in the sense it separates content from usage: the represented "content focused constraints" can then be exploited via few "content independent" queries, one for each usage and kind of constraint. This approach provides more possibilities.

I. INTRODUCTION

Knowledge representations (KRs) are formal descriptions enabling automatic logical inferencing, and thus automatic KR comparison, search, merge, etc. KRs are logic formulas, e.g. the binary predicates of 1st-order logic; these predicates are called triples or property instances in RDF and binary relations in Conceptual Graphs (CGs) [START_REF] Sowa | conceptual graphs summary. conceptual structures: current research and practice[END_REF]. For the purpose of clarity, this article uses the intuitive terminology of CGs: (information) objects are either types or individuals, and types are either relation types or concept types (classes and datatypes in RDF). A formal knowledge base (KB) is a collection of such objects written using a KR language (KRL). An ontology is a KB that is essentially about types, rather than about individuals.

Creating a KB or evaluating its quality -for knowledge sharing or exploitation purposes, or for designing or generating software, or evaluating their qualities -are difficult. Models and constraints (e.g. design patterns) help these tasks and can be stored into an ontology. E.g., the author of this article is building an ontology representing and organizing ontology design patterns as well as software design patterns. Reference [START_REF] Zaveri | Quality assessment for linked data: a survey[END_REF], a survey on quality assessment for Linked Data, provides many dimensions and metrics for evaluating the quality of KBs and hence helping the selection or design of KBs. One of the quality dimensions is the (degree of) completeness of a KB with respect to some criteria or constraints: concisely, "its completeness".

Evaluating this degree is common in various tasks or fields but is performed differently by different tools and sometimes in implicit or ad hoc ways. Examples of such tasks or fields are: i) the automatic/manual extraction of knowledge or the creation of a KB, ii) the exploitation of ontology design patterns, KB design libraries (e.g., the KADS library) or top-level ontologies (e.g., DOLCE), and iii) the evaluation of ontologies or, more generally, datasets. In this last field, as noted in [START_REF] Zaveri | Quality assessment for linked data: a survey[END_REF], completeness commonly refers to a degree to which the "information required to satisfy some given criteria or a given query" are present in the considered dataset. To complement this very general definition, this article distinguishes two kinds of completeness:

 Constraint-based completeness measures the percentage of elements in a dataset that satisfy explicit representations of what must or must not be represented in the dataset. These representations are constraints such as integrity constraints or, more generally, those expressed by ontology design patterns and schemas of databases or of structured documents. E.g.: the constraint that, in a particular dataset, at least one movie must be associated to each movie actor.

 Real-world-based completeness measures the degree to which certain real-world information are represented in the dataset. E.g., regarding movies associated to an actor, calculating the completeness may consist in dividing "the number of movies associated to this actor in the dataset" by "the number of movies he actually played in".

Either the missing information are found in a gold standard dataset or the degree is estimated via completeness oracles [START_REF] Galárraga | Enabling completeness-aware querying in SPARQL[END_REF], i.e. rules or queries estimating what is missing in the dataset to answer a given query correctly. The four kinds of completeness collected by [START_REF] Zaveri | Quality assessment for linked data: a survey[END_REF] -schema/property/population/interlinking completeness -assume a closed-world-assumption and a gold standard dataset. Thus, they are real-world based completenesses.

One way to define or calculate the constraint-based completeness of a KB is to divide "the number of statements satisfying the constraints in that KB" by "the total number of statements in the KB". As a variant, instead of statements only, one may want to consider objects, i.e. measure the percentage of objects for which all relations from/to them satisfy the constraints. Other variants may be defined by considering only certain kinds of objects or statements. Defining constraints via KRs, instead of via queries, permits the definition of "contentindependent (alias, domain-independent) queries" to exploit these constraints. Otherwise, a different (content-dependent) query has to be created for each variant of constraint based checking or completeness. Because of this lack of modularity, XXX-X-XXXX-XXXX-X/XX/$XX.00 ©20XX IEEE when stored in an ontology, content-dependent queries are also less easily organized than content-independent ones. This article does not address real-world based completeness but the techniques this article proposes may also be used for representing certain domain-specific parts of the rules used for calculating real-world based completeness. From now on, "completeness" refers to constraint-based completeness.

Section II explores the first research question of this article: what does the expression "must and must not be represented in the dataset" entail or, more precisely, given the "descriptive vs. prescriptive" distinction, what kinds of constraints need to be considered for evaluating constraint-based completeness via content-independent queries? Section III proposes an approach to answer a second research question: how to represent constraints in a KRL independent way -or, more precisely, in any KRL that has an expressiveness at least equal to RDF or RDFS -even though actually defining the semantics of some of these constraints would require much more expressive logics? The proposed solution relies i) on the representation of constraints via restricted constructs based on relations between classes (or to classes), e.g. rules using the rdfs:subClassOf relation for representing a restricted implication between the condition and conclusion of the rule, ii) on the use of certain special types for specifying that a statement is a constraint of a certain kind, and iii) on the exploitation of these types in content-independent queries. Such constraint representations can then be exploited via most inference engines and KR query languages instead of tools tied to a particular KRL or goal (knowledge acquisition, ontology design pattern application, ontology evaluation, etc.).

Section IV shows commands (queries or update requests) answering a third research question: how to implement the above cited approach in SPARQL or slight extensions of it. Section V.A illustrates applications or use cases for the given content-independent queries. It is actually a summary of Section IV in [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF], an unpublished extension of this article and a companion Web site for this article. Section V.B evaluates the proposed approach and compares it to other ones.

II. DEFINITIONS FOR THE CONSIDERED CONSTRAINTS

A. Considered Constraints: Just For Checks, Not Inferences

In this article, as in KIF (Knowledge Interchange Format) [START_REF] Genesereth | Knowledge interchange format, version 3.0, reference manual[END_REF], a rule is a statement that can be represented in the form "X =>> Y" where "=>>" is a restricted version of the logical implication ("=>"): it supports modus ponens, not modus tollens.

A rule allowing the derivation of a non-modal statement is a rule that can be represented in the form "X =>> Y" where Y does not include a modality (e.g., must). An example is "if x is a Person then x has a parent". If this statement and "Tom is a Person" are in a KB, an inference engine can derive the nonmodal statement "Tom has a parent".

Reference [START_REF] Chein | Graph-based Knowledge Representation -Computational Foundations of Conceptual Graphs[END_REF] defines constraints as positive or negative, respectively expressing statements of the form "if A, B must be true" and "if A, B must be false". Thus, [START_REF] Chein | Graph-based Knowledge Representation -Computational Foundations of Conceptual Graphs[END_REF] defines constraints as rules where the conclusion has a "must" modality. These are the kinds of constraints considered in this article, with the interpretation that in such constraints the "must" entails that the constraints can only be used for checking statements, i.e. that they are not rules allowing the derivation of non-modal statements. More formally, this means that such positive and negative constraints can respectively be translated into the forms "A ∧ ¬B =>> false" and "A ∧ B =>> false" where A and B do not contain a "must" modality and A may be empty. As an example, consider the positive constraint "if x is a Person, x must have a parent". From this constraint and the fact "Tom is a Person", an inference engine must not derive "Tom has a parent". It may derive "Tom must have a parent" but, in practice, such derivation is not made. As a somewhat opposite example, RDFS-aware engines do not exploit relations of type rdfs:domain or rdfs:range as relation signature constraints but as inference supporting statements: when a relation r has a type partially defined by an rdfs:domain (vs. rdfs:range) relation, RDFS-aware engines may infer a type for the source (vs. destination) of r.

In this article, constraints that are directly represented in a form ending by "=>> false" -or, equivalently, "=>> ⊥" -are called constraints in inconsistency-implying form. Not all KRLs allow to represent rules (instead of -or in addition toimplications); in those that do, representing negative constraints using the inconsistency-implying form is easy but using this form for representing positive constraints may not possible: the KRL may not permit the representation of the negation in the "¬B" part. This in why in this article i) negative constraints are represented in inconsistency-implying form, and ii) positive constraints are in the form "A =>> B" but with a representation supporting the distinction between a constraint and an actual rule. Furthermore, as in most rule-based systems, in the rest of this article the A and B parts share variables. More precisely, these parts are representations of relations from a same object (i.e. from a type or an individual, including a relation or a more complex statement since they are particular kinds of individuals).

In the research literature on constraints, these ones are generally not represented -or checked -via modal logic based KRLs but rather using queries, e.g. via SPARQL or the nonmonotonic-epistemic-logic query language EQL-Lite [START_REF] Calvanese | EQL-lite: effective first-order query processing in description logics[END_REF]. In (unidirectional) rule based systems, rules with empty conclusions (or "false" as conclusions) are handled like constraints. However, this is a particularity of these systems. It should not be relied upon for general knowledge representation purpose. For such a purpose, the special semantics of constraints has to be made explicit via special syntactic sugar or special types. Since KRLs rarely propose syntactic sugar for expressing constraints, a more generic approach for expressing that a statement is a constraint, as opposed to an inference supporting statement, is to state that this statement is an instance of a type expressing a particular kind of constraint (as explained in Section III.A). Then, these constraints can be retrieved and exploited by content-independent queries such as those provided below. These constraints can also be directly interpreted and exploited by inference engines designed to take into account the used constraint types. In any case, either i) constraints are not represented in a way they can be exploited as inference supporting statements, or ii) the results of these inferences must not be detrimental, i.e., must not influence the checking of constraints. Both techniques will be illustrated below.

B. Prescriptive (i.e. Not Using All Inferences) vs. Descriptive

As noted in [START_REF] Assmann | Ontologies, metamodels and modeldriven paradigm[END_REF], a common distinction between engineering models is whether they are i) descriptive of some reality, e.g. like most ontologies (e.g., by default, ontologies written in RDF or OWL), or ii) prescriptive of what must be in the considered dataset, as with system specifications, meta-models, XML schemas, database schemas, SHACL statements, etc. Similarly, this article distinguishes two kinds of constraints. First, like definitions or axioms, descriptive constraints enable inference engines to check the use of certain formal terms, if and only if these terms are used. On the other hand, prescriptive constraints enable inference engines to check that certain formal terms are actually used (not just inferred) or not used, under certain conditions. E.g., prescriptive constraints can be used for checking that if the instances of a type are defined as (necessarily) having certain relations, these relations are explicitly given by users whenever they create an instance of such a type. Here, "explicitly" emphasizes that these relations must not exist just because they were automatically deduced, e.g. by inheritance, but only because they were set by a user (manually or automatically). As an example, assume that a KB includes the rule "if x is a Person, x has a parent" and that a user enters that "John is a Person" in the base of facts of this KB (this base is the set of relations from/to individuals; for a description-logic based KB, this is its A-box). Even if this KB also includes the descriptive constraint "if x is a Person, x must have a parent in the represented world (descriptive-must)", an error message should not be given by a KB checking mechanism since this constraint is satisfied (by inferencing) without the user having to represent a parent for John. On the other hand, if the KB includes the prescriptive constraint "if x is a Person, x must have a parent in the base of facts (prescriptive-must)", the adding of a new person without a relation to a parent must be rejected. For constraints in inconsistency-implying form, there is no distinction between descriptive and prescriptive: they enable the detection of an incorrect KR whether it has been inferred or not.

To check a positive prescriptive constraint, any inference may be useful for testing the condition of this constraint, i.e. for matching objects in the KB against this condition. As illustrated in the previous paragraph, this is not the case when testing the main (alias, first) object of the conclusion of the constraint, i.e. the object whose relations are mandatory for all objects matching the condition of the constraint. When testing this first object, if some mechanism automatically associates relations to some of the checked objects -e.g., by dynamic lookup for inherited relations during each object matching, or by forward chaining saturation -this mechanism must be temporarily disabled or bypassed. However, disabling or changing these mechanisms (or, in other words, the used entailment regime [START_REF]W3C Recommendation[END_REF]) generally cannot be done in the middle of a query. E.g., SPARQL does not permit such a change. Hence, instead, bypassing methods are needed. Section III.B proposes one.

To sum up, such prescriptive constraints are original, enable checks that descriptive constraints cannot, and are not equivalent to the use of the closed world assumption. The techniques presented by this article for defining and checking prescriptive constraints can be performed with open-world assumption. Nonmodal logical expressions are only descriptive. E.g., simply stating that "any Person (necessarily) has a parent" is only descriptive. Content-independent queries, special procedures or inference engines exploiting prescriptive constraints need to distinguish them from descriptive ones via their types.

C. Descriptive Constraints Restricted To Named Individuals

When using a constraint to check if certain objects in a KB satisfy a methodology or an ontology design pattern, one might want to take into account automatically deduced relations but only if they are from or to named individuals ("IRIs" in RDF terminology), not if they are between anonymous individuals ("blank nodes" in RDF terminology). Such a "partly descriptive -partly prescriptive" constraint may be termed "descriptive but restricted to named individuals". It requires the author of the constraint to represent which individuals must be named.

Although RDFS provides the type rdfs:label for relations between an individual and its names, it does not provide a type for relating an individual to its identifiers (even though they are unique names) since IRIs (International Resource Identifiers) are directly interpreted as named individuals in RDF. OWL also does not provide such a relation type which could be used for distinguishing which individuals are (or must be) named from those who are not (or need not be). In OWL2-DL, this distinction can be made if each named individual is declared as instance of the class owl:NamedIndividual. However, doing so in OWL2 Full still does not permit to make the distinction. SPARQL supports the distinction via the operators isIRI and isBlank. Hence, the solution proposed in this article is to provide i) the relation type cstr:id for enabling the authors of a constraint to specify which individual must have an identifier (as illustrated in the second to last paragraph of Section III), and ii) a SPARQL update request permitting the adding of cstr:id relations to each named individual type in a KB (cf. Section IV.B). Thus, if some descriptive constraints use cstr:id relations and if this last SPARQL update request is run, these constraints will correctly be checked by content-independent queries for descriptive constraints (e.g., see Section IV.D.1).

III. APPROACH FOR REPRESENTING AND EXPLOITING THE CONSIDERED CONSTRAINTS

A. Using Constraint Types

Reference [START_REF] Tao | Integrity constraints in OWL[END_REF] shows that SPARQL queries can represent and check certain kinds of integrity constraints that exploit some forms of the Unique Name Assumption or Closed World Assumption. Instead, as explained in the introduction, the goal is here to enable the representation of constraints that i) can be exploited via content-independent queries, ii) can be represented via any KRL that has an expressiveness at least equal to RDF or RDFS, and iii) can be marked as descriptive or prescriptive (this distinction is not made in [START_REF] Tao | Integrity constraints in OWL[END_REF]).

To that end, the proposed approach is to introduce a few types for constraints. By setting instanceOf or subtypeOf relations from certain KRs to some of those types, KB authors can state that these KRs are constraints and can indicate which kind of constraints. Thus, these constraints can be exploited by content-independent queries or inference engines that understand the used constraint types. For these engines, the types change the way the statements must be interpreted. This approach is similar to the use of OWL2 types in RDF statements and their exploitation by OWL2-aware inference engines. The name of the proposed ontology of constraint types is CSTR. In this ontology, cstr:Constraint is the supertype of all types of constraints. Similarly, the type cstr:Prescriptive_constraint, a subtype of cstr:Constraint, enables one to state that some rules are actually prescriptive constraints or to retrieve all and only such constraints. The prefix "cstr:" in these identifiers is an abbreviation for the namespace http://www.webkb.org/kb/it/CSTR. Other types are later referred to, when needed. Presenting the rest of CSTR is not needed in this article.

B. Using "Clones Without Types" For Bypassing Certain Inferences When Checking The Conclusions Of Positive Prescriptive Constraints

For adequately checking positive prescriptive constraints Section II.B introduced the need for temporarily disabling or bypassing "inference mechanisms that automatically associate relations to objects" when testing the first object of the conclusion of the constraint. This subsection proposes a method to so. Statically (i.e. via a pre-treatment of the KB like the one given in Section IV.C) or dynamically (i.e. during the checking of such constraints), this method creates a "clone without type" of each object matching the condition of such a constraint and then, when checking its conclusion, does so on the clone instead of the original object. The clone has the same relations as the original object except for instanceOf relations (it has none; furthermore, if it is a named individual, it has an identifier different from the original object). Thus, by so using clones without types, "inferences exploiting types to associate relations to an object" are avoided. As an abbreviation, from now on, this is referred to as avoiding inheritance. In the case of RDFS or OWL entailments, "avoiding inheritance" means that, when searching relations associated to an object, the types of this object and their superclasses are not exploited. Creating clones without types is not necessarily easy since there may be information in the KB that lead certain inference engines to regenerate types for some clones. E.g., assuming there is an rdfs:domain relation from the relation type parent to Person, if an object of type Person is source of a parent relation and this object has its type removed, an inference engine may set it again. To avoid such a case, instead of using rdfs:domain or rdfs:range relations, one may write inconsistency-implying constraints that are equivalent to these relations except that they are usable only for checking purposes. When SPARQL is used for creating a clone without type, as illustrated in Section IV.C, another potential problem is that the whole KB is duplicated, not just one object. Finally, this method based on clones without types does not work if there are inferences that do not exploit types (e.g. via duck typing instead of inheritance) or if a forward chaining saturation on the KB is automatically run before the above cited pre-treatment. However, these last two cases are rare. This method relies on a temporary update of KRs before their checking by an inference engine. Thus, this method does not rely on a particular KRL, inference engine or tool feature. I.e., this solution is KRL independent and tool independent: it can be used with any KRL and any tool. Hence, depending on the domain and application, different inference engines can be reused to check or evaluate ontology completeness. However, with some query languages such as current standard versions of SPARQL, the temporary update cannot be done dynamically: a KB pre-treatment is necessary. This is a limitation since KB servers, e.g. SPARQL endpoints, rarely allow their users to modify a KB for checking it. With LDScript [START_REF] Corby | LDScript: a linked data script language[END_REF], an extension of SPARQL, the temporary update can be done dynamically. As with SPARQL, the whole KB is duplicated but now it is temporary and done every time an object is matched with the conclusion of a prescriptive constraint (cf. Section IV.D.2).

C. Representing Constraints Via Relations Between Classes 1) Approaches:

One way to represent and exploit (simple) rules in a KRL that has an expressiveness at least equal to RDF or RDFS is to use an rdfs:subClassOf relation for representing the implication between the condition and conclusion of a rule (as in OWL-ER [START_REF] Baget | Datalog+, RuleML and OWL 2: formats and translations for existential rules[END_REF], an intersection between OWL2, Datalog+ and RuleML). However then, either this implication must not be used for modus tollens or the results must not be detrimental. The situation is not much more complex when subclassOf rules are used as a way to represent constraints. There are three cases.

 If the conclusion is (equivalent to) owl:Nothing, i.e. if the inconsistency-implying form is used, the rule is semantically a constraint and, depending on the inference engines, modus tollens may or may not be a danger,  Otherwise, if a prescriptive constraint is represented, the "Clones Without Types" based method prevents the results of modus ponens or modus tollens to influence the checking of constraints (this is where these results could have been detrimental).

 Otherwise, i.e. if a descriptive constraint is represented, one must use an inference engine that does not exploit rules for modus ponens nor modus tollens when the condition of the rule is subtype of cstr:SubclassOf-based_constraint_condition or instance of cstr:Type_of_subclassOf-based_constraint_condition.

In other words, using subclassOf-based constraints when inferences based on subclassOf relations then have to be ignored is generally not relevant. However, the idea of using classes for representing the conditions and conclusion of a constraint without using variables is interesting. Here are two simple ways.

 The "subclassOf-analogous" way: it consists in relating the condition class and the conclusion class by a relation that is not a subclassOf one. To do so, CSTR proposes the relation types cstr:descriptive_constraint_conclusion and cstr:prescriptive_constraint_conclusion.

 The "individual-based constraint" way: it consists in creating a constraint individual and, from it, relations to express its type (i.e., descriptive vs. prescriptive) and the classes for its condition and its conclusion. To support this, CSTR proposes the relation types cstr:condition_class and cstr:conclusion_class. Here, the classes are not directly connected by a relation but indirectly connected. A type could be used instead of an individual but, in the general case, this would not bring more advantages.

A disadvantage of any solution using relations from/to classes when these relations are not subclassOf ones is that the result requires a KRL with an expressivity at least equal to RDF. For OWL-based representations, this means interpreting them with the RDF-Based Semantics, not the OWL2 Direct Semantics. Reference [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF], the companion Web site for this article, proposes and categorizes types and requests to represent and exploit constraints in the three above ways. Because of their similarities, in this article mainly only the requests for the last way are given and the CSTR ontology needs not be further detailed.

2) Examples of Individual-based Constraints:

In this article, the Turtle notation is used when SPARQL is not used since SPARQL is an extension of this notation. For clarity purposes, the names of relation types have a lowercase initial while other names have an uppercase initial. In SPARQL, Turtle or other graph-based notations, a statement of the form "SourceConcept rel1 DestConcept1a, DestConcept1b; rel2 DestConcept2a, DestConcept2b" can for example be read "SourceConcept has for rel1 DestConcept1a and DestConcept1b, and has for rel2 DestConcept2a, and has for rel2 DestConcept2b".

Here is the positive prescriptive constraint "if x is a Person, x must have a parent in the base of facts (prescriptive-must)" represented as an individual-based constraint (using CSTR): For the general descriptive version of this constraint, it is sufficient to replace "prescriptive" by "descriptive" in the previous representation. Here is a version where parents are restricted to be named individuals (i.e. to have a cstr:id relation): The negative constraint "if x is a Person_without_parent, x must not have a parent" may be translated into the inconsistencyimplying form "x is a Person_without_parent =>> false". Here is its representation as an individual-based constraint:

IV. IMPLEMENTATION IN SPARQL OR SLIGHT EXTENSIONS OF IT

In some extensions of SPARQL, e.g. LDScript [START_REF] Corby | LDScript: a linked data script language[END_REF], the next commands (queries or update requests) can be grouped into scripts or functions. Variable names begin by "?".

A. First Example of KB Pre-treatment: Creating "Identifier

Relations" for Named Individuals From each selected named individual, the next command adds a cstr:id relation with destination the identifier of that individual. Thus, as explained in Section II.C, queries checking descriptive constraints also work on those that include cstr:id relations, i.e. that have restrictions to named individuals. Here, only an individual that has a type with a superclass and that has other relations is selected since in practice only such an individual might violate a constraint. To search for individuals, just looking for each object that is not a relation and that does not have rdfs:Class as type would be an incomplete strategy and many conditions would have to be added for filtering out objects such as i) classes defined via an equivalence to a restriction, and ii) owl:Thing and some other types from OWL, RDFS or XSD.

B. Second Example of KB Pre-treatment: Creating "Clones

Without Types" of Objects For Exploiting These Objects Without Inheritance Mechanism Section III.B introduced a method for handling positive prescriptive constraints, i.e. for bypassing or avoiding the relation lookup mechanism above abbreviated as "inheritance". The next command implements the KB pre-treatment supporting the "clones without types" based method when, as is the case with SPARQL, i) a particular entailment regime cannot be changed within a query, and ii) clones cannot be temporarily created within a query. For the sake of clarity, this command assumes that the KB does not include user-defined 2nd-order types. For every object ?o in the KB, if this object is an individual, this command creates ?o2, a partial copy of ?o that has the same relations except for rdf:type relations. This partial copy has for identifier the one of ?o but with the suffix "_cloneWithoutType". This command also relates ?o to ?o2 by a relation of type cstr:cloneWithoutType.

C. Checking Individual-based Positive Descriptive Constraints

The next query lists every object violating at least one of the individual-based positive descriptive constraints -including those restricted to named individuals if cstr:id relations have been added to named individuals. As shown by the code, such an object satisfies two conditions. First, this object matches -hence, has for type -the condition of a constraint ?posConstr that is of type cstr:Descriptive_constraint. Second, this object does not match the conclusion of the constraint. This query requires a SPARQL engine with an entailment regime enabling the matching (alias, categorization) of an individual with respect to a class expression and thence the deduction of an rdf:type relation between them. In the code of the commands in this Section IV, such deduced rdf:type relations are highlighted in bold. For inferencing completeness purposes, such deductions require an entailment regime able to handle the expressiveness used in the constraints and the rest of the KB. The code for checking subclassOf-based or subclassOf-analogous positive descriptive constraints is similar.

SELECT ?objectNotMatchingPosConstr ?posConstr_condition ?posConstr_conclusion WHERE { ?posConstr rdf:type cstr:Descriptive_constraint; cstr:condition_class ?posConstr_condition; cstr:conclusion_class ?posConstr_conclusion. FILTER (?posConstr_conclusion != owl:Nothing) ?objectNotMatchingPosConstr rdf:type ?posConstr_condition. FILTER NOT EXISTS #no objects satisfying the conclusion { ?objectNotMatchingPosConstr rdf:type ?posConstr_conclusion } }

D. Checking Individual-based Positive Prescriptive Constraints

The next query assumes that the "clones without types" have been statically created as seen in Subsection B. In the rest of this Section IV, when a command has some code that has not been used in a previous command, this code is in italics. Here is the same query in LDScript, with an embedded query that temporarily creates the above cited partial copies "on the fly", thus removing the necessity to modify the KB.

FILTER (?x != ?objectNotMatchingPosConstr) } ) { xt:entailment(?g) } #triggers inferences on ?g }

The same "on the fly" cloning technique can be used for adding cstr:id relations to named individuals. Thus, this technique also permits the checking of constraints restricted to named individuals without having to modify the KB.

E. Checking Individual-based Inconsistency-implying Constraints

The next query lists every object violating an individualbased inconsistency-implying constraint.

SELECT ?objectMatchingNegConstr ?negConstr_condition WHERE { ?negConstr cstr:condition_class ?negConstr_condition; cstr:conclusion_class owl:Nothing. ?objectMatchingNegConstr rdf:type ?negConstr_condition. }

F. Checking SubclassOf-analogous Constraints

The usable content-independent queries here are identical to their counterparts in the last three subsections except for the initialization of ?posConstr_condition and There are other ways to write the queries. For example:  Instead of "FILTER (?posConstr_conclusion != owl:Nothing)", one may use "FILTER NOT EXISTS { ?posConstr_conclusion cstr:prescriptiveConclusion owl:Nothing }". The first way has the advantage of not being dependent on the chosen representation for constraint and hence this way minimizes the difference between the queries. On the other hand, with this way, owl:Nothing cannot be replaced by equivalent class expressions (in SPARQL).  In Subsection D, the line "?objectNotMatchingPosConstr cstr:cloneWithoutType ?cloneWithoutType" before "FILTER NOT EXISTS" could be replaced by the line "BIND( uri( concat( str(?objectNotMatchingPosConstr), "_cloneWithoutType" ) ) as ?cloneWithoutType )" within the "FILTER NOT EXISTS" block.

G. Checking SubclassOf-based Constraints

The previous queries do not rely on inference engines to take into account the special meaning of CSTR classes. Hence, as explained in Section III.C.1, these queries cannot be adapted for checking subclassOf-based constraints representing positive descriptive constraints. For prescriptive constraints, the queries are the same as their counterparts in the last four subsections except for the initialization of ?posConstr_condition and ?posConstr_conclusion. E.g., for a positive rescriptive constraint, this initialization now is:

?posConstr_condition rdfs:subClassOf cstr:SubclassOf-based_prescriptive_constraint_condition, ?posConstr_conclusion.

Except as a module for calculating the completeness degree of a KB, individual-based inconsistency-implying constraints are useless if, when building the KB, its consistency is already checked by an inference engine that delivers an error message when detecting that an object is instance of a subclass of owl:Nothing. By default, some Description Logic inference engines such as Corese [START_REF] Corby | LDScript: a linked data script language[END_REF] do not deliver error messages or warning messages when detecting such objects. Having to make inferences on instances of a subclass of owl:Nothing also makes Corese behaves abnormally, e.g., not listing such instances as results of the previous described queries when these instances violate positive constraints.

H. Checking Binary Relations Instead of Individuals

To list binary relations violating constraints -instead of individuals that have some relations violating constraints -it is sufficient to replace rdf:type by the "logical implication relation between statements" in the previous content-independent queries that check positive constraints. For referring to such relations, Tim Berners-Lee uses the type name log:implies [START_REF] Berners-Lee | N3logic: a logical framework for the world wide web[END_REF] in his Notation3 KRL. However, for this replacement to work, the used SPARQL engine must exploit an inference engine that can deduce the existence of such a relation when it exists between the matched statements. Description Logic inference engines generally do not do so.

Like queries on individuals, queries on relations can use additional filters. E.g., for the last query of Subsection G to operate only on negative facts, one may add at the end of its body:

?objectMatchingNegConstr rdf:type owl:NegativePropertyAssertion.

I. Evaluating the Completeness of a KB

A simple way to define or calculate a completeness degree for a KB is to divide "the number of relations (in the KB) that do not violate prescriptive constraints" by "the total number of relations". Another completeness degree may be obtained by dividing "the number of individuals that do not violate prescriptive constraints" by "the total number of individuals". The next query implements a variant of this last definition: instead of individuals, it exploits "objects that are source of at least one relation to another object". Furthermore, this query assumes that the constraints are represented as individual-based constraints. This query can be adapted to implement the above first definition via the method given in Subsection H. Similarly, descriptive constraints could also be taken into account.

V. APPLICATIONS, EVALUATION AND COMPARISONS

A. Examples of Applications or Use Cases

For designing subtype hierarchies, various research works such as [START_REF] Rector | Engineering use cases for modular development of ontologies in OWL[END_REF] advise the use of tree structures. However, [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF] shows that "systematically using subtype partitions (except for nonnatural types)" instead of tree structures has the same benefits with less disadvantages. It also shows that following this ontology design pattern (ODP) means using representations equivalent to relations of type sub:nonNaturalOrPartitionSubclass (or a subtype of it; the prefix "sub:" is an abbreviation for the namespace http://www.webkb.org/kb/it/SUB). Using only OWL2, [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF] fully defines this type as well as the other types necessary for stating a descriptive constraint for checking that the above cited ODP is systematically followed. Here is this constraint; it states that "if a class C1 has a subclass relation, all subclass relations from C1 must be of type sub:nonNaturalOrPartitionSubclass": This constraint can also be represented in inconsistencyimplying form, again only using types defined in OWL2:

sub:ClassWithSomeRel_subclassButNot-nonNaturalOrPartitionSubclass rdfs:subClassOf owl:Nothing.

Reference [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF] then generalizes this constraint (and the types it exploits) for checking all types of transitive relationships. More precisely, it proposes a SPARQL INSERT request that generates a descriptive constraint for each transitive relation type having a sub:nonNaturalOrPartitionTrRelType relation indicating which relation types must actually be used. E.g., this may be used to express that, instead of relations of type sub:subclass or sub:part, relations of type sub:nonNaturalOrPartitionSubclass or sub:partitionPart must respectively be used.

Similarly, [START_REF] Martin | Relations-between-classes based constraints and constraintbased ontology-completeness[END_REF] also proposes a SPARQL command which, for each instance of the type sub:MandatoryOutRelationType, generates prescriptive constraints for checking the systematic use of certain relation types. E.g., based on the following specification in the KB, the command generates a constraint indicating that every dividable object -i.e. every instance of sub:DividableThing -must be the source of a sub:part relation except for each object marked as an instance of sub:PartDestLeaf.

B. Evaluation and Comparisons

The originality of the approach proposed in this article is that it enables i) the representation of constraints independently of their exploitation (this one is represented within contentindependent queries), ii) the representation of both descriptive and prescriptive constraints with any KRL the expressiveness of which is at least equal to RDFS, and hence iii) the exploitation of most inference engines, especially via SPARQL queries.

Since the proposed approach relies on other methods and tools chosen by each user of the approach, it inherits from their theoretical or practical improvements. It would thus not be relevant to focus on theoretical aspects of a particular method or tool in this article. For a general comparison, [START_REF] Baget | Datalog+, RuleML and OWL 2: formats and translations for existential rules[END_REF] and [START_REF] Swan | Querying existential rule knowledge bases: decidability and complexity[END_REF] list theoretical points relevant to the proposed approach. Regarding the use of SPARQL to check constraints, [START_REF] Tao | Integrity constraints in OWL[END_REF] shows that SPARQL can be used for both expressing and validating integrity constraints based on some partial forms of the Unique Name Assumption and Closed World Assumption. It also shows that this validation is sound and complete when the expressiveness used for the constraints and the rest of the KB are respectively "SROIQ and SRI" or "SROI and SROIQ". In the proposed approach, queries are used only for validating constraints, not expressing them, but this is only a generalization of the approach of [START_REF] Tao | Integrity constraints in OWL[END_REF] which does not change the associated theoretical results. In [START_REF] Tao | Integrity constraints in OWL[END_REF], the used partial forms of the Unique Name Assumption and Closed World Assumption are specified in SPARQL via its operators EXISTS and NOT EXISTS plus the use of relations of type owl:sameAs or owl:differentFrom. These forms can similarly be expressed via the commands seen in Section IV and the use of relations of type owl:sameAs or owl:differentFrom in the constraints.

The proposed approach was validated experimentally by testing the degree to which a few constraints -including all those introduced in this article -were followed in i) the "family relationship" focused sample ontology given by the OWL2 Primer W3C document [START_REF]OWL 2 web ontology language primer[END_REF] and ii) a few ontologies from the Linked Data repository LOV. The validation came from finding the right constraint violations and completeness degrees via the proposed queries and, when necessary, KB pre-treatments.

Besides testing these constraints, queries and requests, another goal of this validation phase was to represent ontology design patterns or best practices (ODPs) as constraints. ODPs, e.g. those recommended by the W3C [START_REF]W3C Recommendation[END_REF] or those of the "ODP catalog" [START_REF] Odp | Ontology design patterns . org (ODP)[END_REF], are i) informal descriptions about how certain things should be represented, and/or ii) collections of types that should be reused whenever possible, or iii) lexical or syntactic rules to follow when importing or exporting formal or informal knowledge. Descriptive or prescriptive constraints are ways to represent "must be reused whenever possible" and hence ways to formalize and implement ODPs related to the second point. However, during the validation phase, no ODP satisfying the two following criteria was found: i) the ODP could be implemented via a constraint, and ii) the ODP was likely not to lead to a completeness degree close to 0% for a randomly chosen ontology. More generally, no widely followed ODP was found.

Querying a KB for detecting anti-patterns in it is analogous to querying it for detecting violations of ODPs in it. However, like the SPARQL based works of [START_REF] Roussey | Antipattern detection: how to debug an ontology without a reasoner[END_REF], many works on antipattern detection use queries essentially as a way not to use an expressive inference engine for detecting certain problems. Instead, the proposed approach exploits inference engines. With a sufficiently powerful KRL, any anti-pattern can be expressed as a negative constraint in inconsistency-implying form.

The introduction of this article summarized the strong distinction that exists between constraint-based completeness and represented-world-based completeness, and hence the reason why it would not be relevant to further compare the proposed approach with those of tools such as SWIQA and Sieve.

Since the proposed approach is based on a particular use of RDFS it should be compared to SHACL and SPIN.

 SHACL (SHApes Constraint Language) is a language ontology (such as OWL2) proposed by the W3C to enable the definition of constraints in RDF. SHACL does not reuse OWL2 to define constraints: it introduces new terms. It therefore does not support the reuse -for checking constraints -of inference engines that take into account the special meaning of OWL2 terms. Thus, inference engines dedicated to SHACL have to be used and a new KRL (SHACL) has to be learned. In addition, SHACL does not distinguish between descriptive constraints and prescriptive ones, and thus handles prescriptive constraints only very partially. E.g., handling the condition and conclusion of a prescriptive constraint generally require different entailment regimes (as explained in Section II.B) but with SHACL, only one regime can be specified for both the condition and conclusion. Furthermore, neither LDScript-like extensions nor SPARQL update requests can be used in SHACL. Thus, pre-treatments of the KB -including the one proposed in Section IV.B for prescriptive constraintshave to be specified via a KRL other than SHACL.

 SPIN (SParql Inferencing Notation) is a W3C language ontology that enables the storage of SPARQL queries in RDF and, via special relations such as spin:rule and spin:constraint, the (possibly recursive) calls of SPARQL queries or Javascript functions for adding nodes or values to the KB. Thus, SPIN enables procedural attachments in a KB and thereby also supports the extension of SPARQL. However, the use of SPIN requires a SPIN aware engine. The approach proposed in this article is KRL independent (hence not based on procedural attachments). SPIN could be used for storing the SPARQL commands proposed in Section IV and Section V.A, thus not only procedurally defining the types proposed for constraints but also providing a way to trigger such commands automatically. SPIN can also be used for checking constraints in other ways that are less modular (i.e., not using content-independent queries) or less logic-based (i.e., more procedural), hence in ways that offer less possibilities for knowledge comparison, translation, inferencing, reuse or exploitation. The widespread use of such other ways may be a reason why SHACL has been designed. This article provides a less restricted alternative. The author also works on a knowledge translation tool exploiting ontology based specifications of conversions, including for constraints.

Some transformation languages or systems exploit KRs. Such systems are presented in [START_REF] Zamazal | PatOMat -versatile framework for patternbased ontology transformation[END_REF] and [START_REF] Corby | STTL: a SPARQL-based transformation language for RDF[END_REF]. Although few of them explicitly have a function that detects KR patterns without also transforming the matched KRs (PatOMat [START_REF] Zamazal | PatOMat -versatile framework for patternbased ontology transformation[END_REF] is an exception), these languages or systems could easily be adapted to have such a function and hence be used for handling prescriptive constraints. However, all such systems appear to use rule-based languages with more expressiveness than what relations-between-classes based constraints allow. Typically, these languages allow the direct and explicit use of variables for relating objects shared by both the condition and conclusion of a rule. Indeed, using such languages can simplify the writing of prescriptive constraints. However, regarding what can be expressed and checked via constraints, this article shows that i) much can be achieved simply using relations-between-classes based constraints and SPARQL1.1, and ii) the power of the proposed approach then relies on the power of the inference engine used for object matching, rather than on the used language. Some transformation systems, like PatOMat [START_REF] Zamazal | PatOMat -versatile framework for patternbased ontology transformation[END_REF], issue SPARQL queries for detecting patterns, based on non-SPARQL specifications for patterns and their transformations. Some other transformation systems directly propose an extension of SPARQL such as STTL [START_REF] Corby | STTL: a SPARQL-based transformation language for RDF[END_REF] to write specifications for patterns and their transformations. For instance, as shown in [START_REF] Corby | Validating ontologies against OWL 2 profiles with the SPARQL template transformation language[END_REF], STTL can be combined with LDScript [START_REF] Corby | LDScript: a linked data script language[END_REF] to specify STTL queries (compiled into SPARQL queries) for detecting patterns and then transforming the results. However, [START_REF] Corby | Validating ontologies against OWL 2 profiles with the SPARQL template transformation language[END_REF] does not discuss the exploitation of object matching capabilities of inference engines and it does not distinguish between prescriptive constraints and non-prescriptive ones. To sum up, the SPARQL commands introduced in this article could also be reused in these transformation systems, although in an adapted form.

VI. CONCLUSION

This goal of this article -supporting constraint checking via few predefined content-independent queries, in a KRL independent and tool independent way -is original, useful for modularity as well as knowledge and tool reuse purposes, and applicable to various research fields. E.g., this support can help checking the following of ontology design patterns (ODPs), KB design libraries (e.g., the KADS library) or top-level ontologies (e.g., DOLCE) in order to validate the quality of a KB or, during its design, help elicit knowledge from experts.

The sections II and III answer the first two research questions: what kinds of constraints need to be considered for evaluating constraint-based completeness, and how to represent constraints in any KRL that has an expressiveness at least equal to RDF or RDFS? Section II and III do so via complementary means.

 First, by defining the original notion of "prescriptive constraint" for checking that some objects are explicitly given instead of possibly inferred as in descriptive constraints (the two constraint kinds thus form a partition).

 Second, by providing i) a general method to check prescriptive constraints, ii) types for distinguishing different kinds of constraints, and iii) three alternative structures for representing them via class expressions. The use of such expressions is both a way to permit the reuse of most KRLs and a way to reuse inference engines by exploiting calculated instanceOf relations  Third, by showing that both descriptive constraints and prescriptive constraints are i) necessary for evaluating constraint-based completeness via content-independent queries, and ii) in a sense, sufficient too for two reasons. First, descriptive constraints and prescriptive constraints form a (complete) partition. Second, more specialized distinctions, if needed, can still be expressed by specializing the given types and using further methods to take into account these more specialized types.

Section IV answers the third research question: how to implement the general approach with query languages such as SPARQL or slight extensions of it? Section V.A shows how some ODPs can be represented as descriptive constraints exploitable by content-independent queries. Both sections highlight the use of KB pre-treatments to counter-balance certain lack of expressiveness of some languages, e.g. for implementing inference bypassing methods or generating constraints. Section V.B evaluates the proposed techniques and compares the approach to other ones. A complement to this work will be to i) represent ODPs in several research areas (knowledge sharing, cooperation, security, etc.), using only relations between classes whenever possible, ii) organize them by relations of specialization or other kinds, and iii) test these ODPs via LDScript or more expressive languages.

[

  ] rdf:type cstr:Prescriptive_constraint; cstr:condition_class :Person; cstr:conclusion_class [rdf:type owl:Class; owl:equivalentClass [rdf:type owl:Restriction; owl:onProperty :parent; owl:someValuesFrom :Person] ].

[

  ] rdf:type cstr:Descriptive_constraint; cstr:condition_class :Person; cstr:conclusion_class [rdf:type owl:Class; owl:equivalentClass [rdf:type owl:Restriction; owl:onProperty :parent; owl:someValuesFrom :Named_person] ].

  sub:part rdf:type sub:MandatoryOutRelationType; sub:leafObjectType sub:PartDestLeaf; rdfs:domain sub:DividableThing.

ACKNOWLEDGMENT

Many thanks to Dr Olivier Corby (member of the Wimmics and SPARKS teams of, respectively, the INRIA and I3S CNRS laboratories at the University Côte d'Azur, France) for his questions and remarks on the approaches presented in this article and his help during the implementation of these approaches with SPARQL and LDScript via the Corese tool.


Roberto Bagnara Bugseng

Fred Mesnard
email: frederic.mesnard@univ-reunion.fr

Eventual Linear Ranking Functions

Keywords: termination analysis, ranking function, eventual linear ranking function

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

INTRODUCTION

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for mainstream programming languages such as C [START_REF] Cook | Termination proofs for systems code[END_REF] and Java [START_REF] Albert | Termination and cost analysis with COSTA and its user interfaces[END_REF][START_REF] Otto | Automated termination analysis of Java bytecode by term rewriting[END_REF][START_REF] Spoto | A termination analyzer for Java bytecode based on path-length[END_REF] with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming.

Beyond the specificities of the targeted programming languages and after several abstractions (see, e.g., [START_REF] Spoto | A termination analyzer for Java bytecode based on path-length[END_REF]), termination analysis of entire programs boils down to termination analysis of individual loops. Various categories of loops have been identified: for the purposes of this paper we focus on single-path linear constraint (SLC) loops [START_REF] Ben-Amram | On the linear ranking problem for integer linear-constraint loops[END_REF].

We first recall some notions and notations. For n ∈ N, we denote by Q n the n-dimensional vector space on the field of rational numbers Q. http://dx.doi.org/10.1145/2505879.2505884 .

A vector v ∈ Q n can be also interpreted as a matrix in Q n×1 and manipulated accordingly using the usual definitions for addition, multiplication (both by a scalar and by another matrix), and transposition, denoted by v T . For each i = 1, . . . n, vi denotes the i-th component of the (column) vector v = (v1, . . . , vn) T ∈ Q n . The scalar product of v, w ∈ Q n , denoted v, w , is the rational number

v T w = n X i=1 viwi.
Now, an SLC loop over n variables x1, . . . , xn has the form

while (B x ≤ b) do A " x x « ≤ c
where x = (x1, . . . , xn) T and x = (x 1 , . . . , x n ) T are column vectors of variables, B ∈ Z p×n is an integer matrix, b ∈ Z p , A ∈ Z q×2n and c ∈ Z q . Such a loop can be conveniently written as a constraint logic programming rule:

p(x) ← Bx ≤ b, A " x x « ≤ c, p(x ).
When variables take their values in Z (resp., Q), we call such loops integer (resp., rational ) loops. They model a computation that starts from a point x; if B x ≤ b is false, the loop terminates; otherwise, a new point x is chosen that satisfies

A " x x « ≤ c
and iteration continues replacing the values of x by the corresponding ones of x .

Loop termination can always be ensured by a ranking function ρ, a function from Z n or Q n to a well-founded set. As the range of ρ is well-founded, the computation terminates. To the best of our knowledge, decidability of universal termination of SLC loops (i.e., from any starting point and for any choice of the next point at each iteration) is an open question. Some sub-classes have been shown to be decidable [START_REF] Bozga | Deciding conditional termination[END_REF][START_REF] Braverman | Termination of integer linear programs[END_REF][START_REF] Tiwari | Termination of linear programs[END_REF]. For instance, Braverman proves that termination of loops where the body is a deterministic assignment x := Ax is decidable when the variables range over Q. The problem is open for the non-deterministic case, as stated in his paper. On the other hand, various generalizations have been shown to be undecidable [START_REF] Ben-Amram | On the termination of integer loops[END_REF].

A way to investigate loop termination is to restrict the class of the considered ranking functions. In the following section, we recall a well-known technique for computing linear ranking functions for rational SLC loops.

In Section 3 we present the main contribution of the paper, namely the definition of eventual linear ranking functions: these are linear functions that become ranking functions after a finite unrolling of the loop. 1 We shall see that the number of unrolling is not pre-defined, but depends on the data processed by the loop. Section 3 presents complete decision procedures for the existence of eventual linear ranking functions of SLC loops. The presentation is gradual and illustrates the algorithms by means of constraint logic programming (CLP) technology and dialogues with real CLP tools. Section 4 discusses related work and a preliminary experimentation conducted on the benchmarks proposed in two very recent papers. Section 5 concludes the paper.

LINEAR RANKING FUNCTIONS

We first define the notion of linear (resp., affine) ranking function for an SLC loop.

Definition 2.1. Let C be the SLC loop p(x) ← c(x, x ), p(x )
where p is an n-ary relation symbol. A linear (resp., affine) ranking function ρ for C is a linear (resp., affine) map from

Q n to Q such that ∀x, x : c(x, x ) =⇒ ρ(x) ≥ 1 + ρ(x ) ∧ ρ(x) ≥ 0.
In words, the continuation of the iteration, i.e., c(x, x ), entails that ρ stays positive and strictly decreases by at least 1 for each iteration. We point out that if c(x, x ) is not satisfiable, the loop ends immediately and any linear function is a ranking function. In the paper, we assume that c(x, x ) is satisfiable.

Remark 2.2. Definition 2.1 might seem too restrictive when working with rational numbers as one might prefer to replace the decrease by 1 by a decrease by ε, a fixed positive quantity. Actually, by multiplying such an ε-decrease ranking function by 1/ε, we see that the two definitions are equivalent with respect to the existence of a ranking function.

Remark 2.3. Although the class of affine ranking functions subsumes the class of linear ranking functions, any decision procedure for the existence of linear ranking functions can be extended to a decision procedure for the existence of affine ranking functions. To see this, note that an affine ranking function for

p(x) ← c(x, x ), p(x ) is a linear ranking function for p(x, y) ← c(x, x ), y = 1, y = 1, p(x , y ),
where y is distinct from the variables in x.

In this section, we focus on linear ranking functions for SLC loops. After the presentation of a formulation of Farkas' Lemma we consider the problem of verifying linear ranking functions, and then the detection of such ranking functions.

Farkas' Lemma

A linear inequation I over rational numbers is a logical consequence of a finite satisfiable conjunction S of linear inequations when I is a linear positive combination of the inequations of S. More formally, let S be 8 < :

a1,1x1 + • • • + a1,nxn + b1 ≥ 0 • • • + • • • + • • • + • • • ≥ 0 am,1x1 + • • • + am,nxn + bm ≥ 0.
and suppose that S has at least one solution. Farkas' Lemma states the equivalence of ∀x1, . . . , xn : S =⇒ (c1x1

+ • • • + cnxn + d ≥ 0) and ∃λ1 ≥ 0, . . . , λm ≥ 0 . " d ≥ X m i=1 λibi " ∧ n ĵ=1 " cj = X m i=1 λiai,j " .

Verification

Given an SLC loop C and a linear function ρ, we can easily check whether ρ is a ranking function for C by testing the unsatisfiability of

c(x, x ) ∧ ρ(x) < 1 + ρ(x ) or c(x, x ) ∧ ρ(x) < 0.
This test has polynomial complexity and can be done with a complete rational solver such as , e.g., CLP(Q) [START_REF] Holzbaur | OFAI clp(Q,R)[END_REF].

Example 2.4. For the SLC loop C:

p(x, y) ← x ≥ 0, y ≤ y -1, x ≤ x + y, y ≤ -1, p(x , y )
the linear function ρ(x, y) = x is a ranking function, as proved by the following SICStus Prolog session.

?-use_module(library(clpq)). % library(clpq) compiled true. ?-{X >= 0, Y1 =< Y -1, X1 =< X + Y, Y =< -1, X < 1 + X1}. false. ?-{X >= 0, Y1 =< Y -1, X1 =< X + Y, Y =< -1, X < 0}. false. ?-

Detection

Given an SLC loop, we would like to know whether it admits a linear ranking function ρ. This problem, which has been studied in depth [START_REF] Bagnara | The automatic synthesis of linear ranking functions: The complete unabridged version[END_REF][START_REF] Bagnara | A new look at the automatic synthesis of linear ranking functions[END_REF][START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF][START_REF] Sohn | Termination detection in logic programs using argument sizes (extended abstract)[END_REF], is decidable in polynomial time.

Let us consider Example 2.4 and formally ask whether there exists a ranking function of the form ρ(x, y) = ax + by: ∃a, b . ∀x, y, x , y :

( x ≥ 0, x ≤ x + y, y ≤ -1, y ≤ y -1 ) =⇒ ( ax + by ≥ 1 + ax + by , ax + by ≥ 0. ( 1
)
This formulation of the problem is executable by quantifier elimination on a symbolic computation system like Reduce [START_REF] Hearn | REDUCE: the first forty years[END_REF]: We obtain

1:
a 2 -ab ≥ 0 ∧ a -b = 0 ∧ a > 0 ∧ b = 0 ∧ (a 2 b -ab 2 ≤ 0 ∨ a 2 -ab = 0 ∨ a 2 -2ab -a + b 2 + b ≥ 0) ∧ (a 2 -ab = 0 ∨ a 2 -2ab -a + b 2 b ≥ 0),
and all values for a and b satisfying the above formula, such as a = 1 and b = 0, are equally good. Unfortunately, the complexity of the algorithms involved will prevent us from systematically obtaining such a result within acceptable time and memory bounds.

We now recall the most famous algorithm for this problem [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF]. 2 Considering a and b as parameters of the problem, we can apply Farkas' Lemma. For the strict decrease of the ranking function we have ∀x, y, x , y :

( x ≥ 0, x ≤ x + y, y ≤ -1, y ≤ y -1 ) =⇒ ax + by ≥ 1 + ax + by . (2)
Application of Farkas' Lemma to this problem can be depicted as follows:

λ1 : 1x + 0y + 0x + 0y + 0 ≥ 0 λ2 : 1x + 1y -1x + 0y + 0 ≥ 0 λ3 : 0x + 1y + 0x -1y -1 ≥ 0 λ4 : 0x -1y + 0x + 0y -1 ≥ 0 =⇒ ax + by -ax -by -1 ≥ 0
We know that formula (2) is equivalent to the existence of four non-negative rational numbers λ1, . . . , λ4 such that:

( a = λ1 + λ2, -a = -λ2, b = λ2 + λ3 -λ4, -b = -λ3, -1 ≥ -λ3 -λ4. (3)
2 See also [START_REF] Bagnara | The automatic synthesis of linear ranking functions: The complete unabridged version[END_REF][START_REF] Bagnara | A new look at the automatic synthesis of linear ranking functions[END_REF].

The positivity of the ranking function, that is, ∀x, y, x , y :

( x ≥ 0 x ≤ x + y y ≤ -1 y ≤ y -1 ) =⇒ ax + by ≥ 0 (4)
can be written as

λ 1 : 1x + 0y + 0x + 0y + 0 ≥ 0 λ 2 : 1x + 1y -1x + 0y + 0 ≥ 0 λ 3 : 0x + 1y + 0x -1y -1 ≥ 0 λ 4 : 0x -1y + 0x + 0y -1 ≥ 0 =⇒ ax + by + 0x + 0y + 0 ≥ 0.
By Farkas' Lemma, formula ( 4) is equivalent to the existence of four other non-negative rational numbers λ 1 , . . . , λ 4 such that:

8 > < > : a = λ 1 + λ 2 , 0 = -λ 2 , b = λ 2 + λ 3 -λ 4 , 0 = -λ 3 , 0 ≥ -λ 3 -λ 4 . (5)
Summarizing, by Farkas Lemma, formula ( 1) is equivalent to the conjunction of formulas ( 3) and ( 5):

∃a, b . ∃λ1, . . . , λ4, λ 1 , . . . , λ 4 ≥ 0 . 8 > > > > > > < > > > > > > : a = λ1 + λ2, -a = -λ2, b = λ2 + λ3 -λ4, -b = -λ3, a = λ 1 + λ 2 , 0 = -λ 2 , b = λ 2 + λ 3 -λ 4 , 0 = -λ 3 , -1 ≥ -λ3 -λ4, 0 ≥ -λ 3 -λ 4 . (6)
In theory, the problem of the existence of a linear ranking function is polynomial. Since computing one solution (that is, values for a and b) is not harder than determining its existence, a "witness" function, which would constitute a termination certificate, can also be computed in polynomial time.

The space of all linear ranking functions as defined in Definition 2.1, described by parameters a and b, can be obtained by elimination of λi and λ i from (6) using, e.g., the algorithm of Fourier-Motzkin. For example the SICStus Prolog program

fm(A, B) :- {L1 >= 0, L2 >= 0, L3 >= 0, L4 >= 0, LP1 >= 0, LP2 >= 0, LP3 >= 0, LP4 >= 0, A = L1 + L2, B = L2 + L3 -L4, A = L2, B = L3, 1 =< L3 + L4, A = LP1 + LP2, B = LP2 + LP3 -LP4, 0 = LP2, 0 = LP3, 0 =< LP3 + LP4}.
can be queried as follows:

| ?-fm(A, B). B = 0, {A >= 1}. | ?-
It can be shown that the computed answer is equivalent to the (significantly more involved) condition generated by Reduce.

EVENTUAL LINEAR RANKING FUNC-TIONS

In the previous section we have illustrated a method to decide the existence of a linear ranking function for a rational SLC loop, something that implies termination of the loop. Of course, the method cannot decide termination in all cases.

Example 3.1. The loop

p(x, y) ← x ≥ 0, y ≤ y -1, x ≤ x + y, p(x , y )
does not admit a linear ranking function.

Can we conclude that such loop does not always terminate? No, because it may admit a non-linear ranking function.

In this section we will extend the previous method so as to detect eventual linear ranking functions, that is, linear functions that behave as ranking functions after a finite number of executions of the loop body. Suppose that the considered SLC loop is always given with a linear function f (x, y) that increases at each iteration of the loop in the following sense:

Definition 3.2. Let C be the SLC loop p(x) ← c(x, x ), p(x ). A function f (x) is increasing for C if it is linear and satis- fies: ∀x, x : c(x, x ) =⇒ f (x ) ≥ 1 + f (x).
Example 3.3. Since y decreases by at least 1 at each iteration, the function f (x, y) = -y is increasing for the loop of Example 3.1.

Remark 3.4. The generalization to affine functions is useless. Moreover, as we are merely interested in the existence of an increasing function, the value of the increase (1 or ε > 0) is irrelevant.

We can now give the definition which is central to our paper. Definition 3.5. Let C be the rational SLC loop in clausal form

p(x) ← c(x, x ), p(x ),
where p is an n-ary relation; let also f (x) be a linear increasing function for C. An eventual linear ranking function ρ

for (C, f ) is a linear map of Q n to Q such that ∃k . ∀x, x : `c(x, x ) ∧ f (x) ≥ k =⇒ `ρ(x) ≥ 1 + ρ(x ) ∧ ρ(x) ≥ 0 ´.
For comparison with Definition 2.1, remark that the threshold k is existentially quantified and that f (x) ≥ k is imposed in the implication antecedent. It should also be noted that, if such a rational k exists, then each k ≥ k satisfies the condition of Definition 3.5. On the other hand, since, by hypothesis, f strictly increases at each iteration, there are two cases: either f is bounded from above by a constant, and thus the loop will terminate; or, after a finite number of iterations, f will cross the threshold k and ρ becomes a linear ranking function in the sense of Section 2 so that, again, the loop terminates.

Eventual linear ranking functions are a generalization of linear ranking functions. Proposition 3.6. Let C be an SLC loop. If ρ is a linear ranking function for C, then there exists an increasing function f such that (C, f ) has an eventual linear ranking function.

Proof. By hypothesis, there exists a linear ranking function ρ(x) for C. The linear function f (x) def = -ρ(x) is nonpositive and strictly increasing for C. Considering k = 1 it can be seen that the function ρ (x) def = 0 is an eventual linear ranking function for (C, f ).

The generalization is strict as the loop of Example 3.1 has no linear ranking function, but does have an eventual linear ranking function, as will be shown in the next section.

Detection given a Linear Increasing Function

As a first step towards full automation of the synthesis of eventual linear ranking functions, we assume that an SLC loop is given with a particular linear increasing function. Let us consider, e.g., the SLC loop of Example 3.1 and the increasing function of Example 3.3. Defining ρ(x, y) = ax + by, ρ is an eventual linear ranking function when ∃a, b, k . ∀x, y, x , y :

( x ≥ 0, x ≤ x + y, -y ≥ k, y ≤ y -1 ) =⇒ ( ax + by ≥ 1 + ax + by , ax + by ≥ 0.
This definition of the problem, that we will denote for brevity with ∃a, b, k . φ(a, b, k), is also solvable via quantifier elimination, hence the problem is decidable. Considering a, b and k as parameters, we can apply Farkas' Lemma as follows:

λ1 : 1x + 0y + 0x + 0y + 0 ≥ 0 λ2 : 1x + 1y -1x + 0y + 0 ≥ 0 λ3 : 0x + 1y + 0x -1y -1 ≥ 0 λ4 : 0x -1y + 0x + 0y -k ≥ 0 =⇒ ax + by -ax -by -1 ≥ 0 ax + by ≥ 0.
Hence, formula φ(a, b, k) is equivalent to the conjunction of formulas DEC(a, b, k), i.e., ∃λ1 ≥ 0, . . . , λ4 ≥ 0 .

( a = λ1 + λ2, -a = -λ2, b = λ2 + λ3 -λ4, -b = -λ3, -1 ≥ -λ3 -kλ4,
ensuring the decreasing of the ranking function, and the formula POS(a, b, k), that is,

∃λ 1 ≥ 0, . . . , λ 4 ≥ 0 . ( a = λ 1 + λ 2 , 0 = -λ 2 b = λ 2 + λ 3 -λ 4 , 0 = -λ 3 0 ≥ -λ 3 -kλ 4 ,
ensuring the positivity of the ranking function.

Let us focus on DEC(a, b, k). We observe that the product kλ4 leads to a non-linearity that we can circumvent by noting that, as λ4 ≥ 0, either λ4 = 0 (hence kλ4 = 0) or λ4 > 0. In the latter case, we introduce a new variable P = kλ4. We have the property: In our case, POS1(a, b) is equivalent to

∃λ 1 , λ 2 , λ 3 ≥ 0 . ( a = λ 1 + λ 2 , 0 = -λ 2 , b = λ 2 + λ 3 , 0 = -λ 3 , 0 ≥ -λ 3 ,
and POS2(a, b) to

∃λ 1 , λ 2 , λ 3 ≥ 0, λ 4 > 0, P . ( a = λ 1 + λ 2 , 0 = -λ 2 , b = λ 2 + λ 3 -λ 4 , 0 = -λ 3 , 0 ≥ -λ 3 -P .
Combining the previous results gives Proposition 3.9. Formula ∃k.φ(a, b, k) is equivalent to

[DEC1(a, b) ∨ DEC2(a, b)] ∧ [POS1(a, b) ∨ POS2(a, b)].
Proof. Thanks to the previous lemmata, it only remains to justify the equivalence between the formulas ∃k . φ(a, b, k) and ∃k . DEC(a, b, k) ∧ ∃k . POS(a, b, k).

(=⇒) Let k0 be a rational such that φ(a, b, k0). We have DEC(a, b, k0) and POS(a, b, k0) because Computing an eventual linear ranking function ρ and its associated threshold k can be done as follows:

• if DEC1(a) ∧ POS1(a) is satisfiable, we compute a solution a, ρ(x) = a, x is a standard linear ranking function and Proposition 3.6 applies;

• if DEC1(a) ∧ POS2(a) is satisfiable, we compute a solution a, λ , P and we take k = P /λ n ;

• if DEC2(a) ∧ POS1(a) is satisfiable, we compute a solution a, λ, P and we take k = P/λn;

• if DEC2(a)∧POS2(a) is satisfiable, we compute a solution a, λ, P , λ , P and we take k = max(P/λn, P /λ n ). We also provide a decision procedure for the existence of an eventual affine ranking function.

Corollary 3.12. The existence of an eventual affine ranking function for an SLC loop and associated increasing function, (C, f ), can be decided in polynomial time.

Proof. From C, p(x) ← c(x, x ), p(x ), we construct Ca, p(x, y) ← c(x, x ), y = 1, y = 1, p(x , y ), where y does not occur in x. Note that Ca is an SLC loop and that fa(x, y) = f (x) is an increasing function for Ca. Algorithm 1 applied to (Ca, fa) gives an answer in polynomial time.

If Algorithm 1 returns true then, by correctness, there exists a threshold k and an eventual linear function ρa(x, y) = a, x +by for (Ca, fa). We readily check that ρ(x) = a, x + b is an eventual affine ranking function for (C, f ) from k.

If Algorithm 1 returns false then, by completeness, there is no eventual linear ranking function for (Ca, fa). Assuming there exists an eventual affine ranking function ρ(x) = a, x +b from k for (C, f ), then ρa(x, y) = a, x +by should be an eventual linear ranking function from k for (Ca, fa), which is a contradiction. Hence there is no eventual affine ranking function for (C, f ).

Example 3.13. The SLC loop p(x, y) ← x ≥ -1, y ≤ y -1, x ≤ x + y, p(x , y ) associated to the linear increasing function f (x, y) = -y does not admit an eventual linear ranking function, but does admit ρ(x, y) = x + 1 as an eventual affine ranking function from k = 1.

Fully Automated Detection

We now consider the problem in its full generality: given an SLC loop C, does there exist an increasing function for C such that C admits an eventual linear ranking function?

Note that the space of increasing functions can be obtained as a convex set over their coefficients via the Farkas' Lemma and existentially quantified variables elimination. 3 Definition 3.14. Let C = `p(x) ← c(x, x ), p(x ) ´be an SLC loop. We denote by INC the set of vectors b such that f (x) = b, x is increasing for C. 3 See also [START_REF] Bagnara | A new look at the automatic synthesis of linear ranking functions[END_REF]Section 4.4].

Example 3.15. A linear ranking function does not exist for the SLC loop C p(x, y) ← x ≥ 0, x ≤ x + y, y ≤ -y -1, p(x , y ).

INC = ˘(b1, b2) ∈ Q × Q ˛b1 ≤ -2, b1 -2b2 =
( x ≥ 0, x ≤ x + y, b1x + b2y ≥ k, y ≤ -y -1 ) =⇒ ( a1x + a2y ≥ 1 + a1x + a2y , a1x + a2y ≥ 0.
This definition of the problem is denoted ∃a, k . φ(a, k). We can apply Farkas' Lemma as follows:

λ1 : 1x + 0y + 0x + 0y + 0 ≥ 0 λ2 : 1x + 1y -1x + 0y + 0 ≥ 0 λ3 : 0x -1y + 0x -1y -1 ≥ 0 λ : b1x + b2y + 0x + 0y -k ≥ 0 =⇒ a1x + a2y -a1x -a2y -1 ≥ 0 a1x + a2y ≥ 0.
Formula φ(a, k) is equivalent to the conjunction of formulas DEC(a, k), i.e., ∃λ1 ≥ 0, λ2 ≥ 0, λ3 ≥ 0, λ ≥ 0 .

( a1 = λ1 + λ2 + b1λ -a1 = -λ2, a2 = λ2 -λ3 + b2λ, -a2 = -λ3, -1 ≥ -λ3 -kλ,
ensuring the decreasing of the ranking function and POS(a, k), that is,

∃λ 1 ≥ 0, λ 2 ≥ 0, λ 3 ≥ 0, λ ≥ 0 . ( a1 = λ 1 + λ 2 + b1λ 0 = -λ 2 a2 = λ 2 -λ 3 + b2λ , 0 = -λ 3 0 ≥ -λ 3 -kλ ,
ensuring the positivity of the ranking function.

Let us focus on DEC(a, k). We observe that the products with λ lead to a non-linearity that we can circumvent by noting that, as λ ≥ 0, either λ = 0 or λ > 0. In the latter case, we introduce a vector p = (p1, p2) of two new variables where p1 = b1λ and p2 = b2λ together with, as previously, the new variable P = kλ. Formula ∃k . DEC(a, k) is equivalent to the disjunction DEC1(a)∨∃λ, p.DEC2(a, λ, p) where in our case, DEC1(a) is equivalent to

∃λ1 ≥ 0, λ2 ≥ 0, λ3 ≥ 0 . ( a1 = λ1 + λ2, -a1 = -λ2, a2 = λ2 -λ3, -a2 = -λ3, -1 ≥ -λ3,
and DEC2(a, λ, p) is equivalent to ∃λ1 ≥ 0, λ2 ≥ 0, λ3 ≥ 0, P .

( a1 = λ1 + λ2 + p1, -a1 = -λ2, λ > 0, a2 = λ2 -λ3 + p2, -a2 = -λ3, -1 ≥ -λ3 -P.
For the positivity condition, formula ∃k . POS(a, k) is equivalent to the disjunction POS1(a) ∨ ∃λ , p .POS2(a, p ) where we introduce a vector p = (p 1 , p 2 ) of two new variables where p 1 = b1λ , p 2 = b2λ together with, as previously, the new variable P = kλ . In our case, POS1(a) is equivalent to

∃λ 1 ≥ 0, λ 2 ≥ 0, λ 3 ≥ 0 . ( a1 = λ 1 + λ 2 , 0 = -λ 2 , a2 = λ 2 -λ 3 , 0 = -λ 3 , 0 ≥ -λ 3 ,
and POS2(a, λ , p ) to

∃λ 1 ≥ 0, λ 2 ≥ 0, λ 3 ≥ 0, P . ( a1 = λ 1 + λ 2 + p 1 , 0 = -λ 2 , λ > 0, a2 = λ 2 -λ 3 + p 2 , 0 = -λ 3 , 0 ≥ -λ 3 -P .
Back to our initial problem, the existence of an eventual linear ranking function is equivalent to the satisfiability of at least one of the following four systems:

1. DEC1(a) ∧ POS1(a): this case means that the increasing function and k are irrelevant. In other words, for each solution a, ρ(x) = a, x is a standard linear ranking function and Proposition 3.6 applies.

2. DEC1(a) ∧ POS2(a, λ , p ) ∧ p /λ ∈ INC: note that satisfiability of DEC1(a) ∧ POS2(a, λ , p ) is not sufficient, as its solution might lead to the coefficients b1 = p 1 /λ and b2 = p 2 /λ (λ is strictly positive by definition), which could correspond to a non-increasing linear function. The third conjunct, p /λ ∈ INC, ensures that we stay within the space of increasing functions.

3. DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS1(a): this case is symmetric to previous one.

4. DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS2(a, λ , p ) ∧ p/λ = p /λ : this case combines the two previous ones. Note that the condition ensures that we consider the same linear ranking function and the same increasing function both in DEC2 and in POS2. Exactly as in the previous section, if Algorithm 2 returns true then we can extract an increasing function f , a threshold k, and a linear function ρ. We can also generalize the approach to the fully automated detection of eventual affine ranking functions.

With respect to complexity, Algorithm 2 is not polynomial for two reasons. In step 1, computing the set INC of linear increasing functions for C requires elimination of existentially quantified variables. In step 2, formula φ2,2 leads to a non-linear system and we may have to check its satisfiability in step 10. Although decidable, we are not aware of the existence of polynomial algorithms for these problems.

Verification

Given C an SLC loop, an associated increasing function f , and a linear function ρ, we want to know whether ρ is a ranking function. We can run Algorithm 1, with the coefficients a fully instantiated. If needed, we can compute the threshold k as explained in Section 3.1. It follows that the verification problem is polynomial.

Implementation

We have implemented both algorithms in SICStus Prolog. However, as φ2,2 of Algorithm 2 leads to a non-linear system, we relaxed this formula to DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS2(a, λ , p ) ∧ p /λ ∈ INC, which is now linear. As shown in the following proposition, the existence of an eventual linear ranking function (hence termination) is preserved, but the associated increasing function is not linear. Proposition 3.17. Let C be an SLC loop and assume the truth of

DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS2(a, λ , p ) ∧ p /λ ∈ INC.
Then there exists a non-linear increasing function f such that ρ(x) = a, x is an eventual linear ranking function for (C,f ).

Proof. As DEC2(a, λ, p) ∧ p/λ ∈ INC is true, there exists an increasing function f d and a rational k d such that when the value of f d is beyond k d , ρ decreases. Similarly, as POS2(a, λ , p )∧p /λ ∈ INC is true, there exists an increasing function fp and a rational kp such that when the value of fp is beyond kp, ρ is non-negative. Let k = max(kp, k d ) and f (x) = min `fp(x), f d (x) ´. One readily checks that f is a non-linear increasing function for C and ρ is an eventual linear ranking function for (C, f ).

RELATED WORK AND EXPERIMENTS

As eventual linear ranking functions generalize linear ranking functions, we focus on related work that goes beyond linear ranking functions for SLC loops. In order to appreciate the relative power of the different methods, we report on the results obtained with our algorithms on the loops discussed in the papers where the other approaches were introduced.

The method proposed in [START_REF] Yi Chen | Termination proofs for linear simple loops[END_REF] repeatedly divides the state space to find a linear ranking function on each subspace, and then checks that the transitive closure of the transition relation is included in the union of the ranking relations. As the process may not terminate, one needs to bound the search.

[27] also proposes a test suite, upon which we tested our approach. Our implementation analyzes the complete test suite in less than 2 seconds on a standard desktop computer. As expected, every loop [27, Table 1] which terminates with a linear ranking also has an eventual linear ranking. Moreover, loops [START_REF] Bagnara | A new look at the automatic synthesis of linear ranking functions[END_REF][START_REF] Bozga | Deciding conditional termination[END_REF][START_REF] Bradley | The polyranking principle[END_REF][START_REF] Ganty | Proving termination starting from the end[END_REF][START_REF] Otto | Automated termination analysis of Java bytecode by term rewriting[END_REF][START_REF] Sohn | Termination detection in logic programs using argument sizes (extended abstract)[END_REF][START_REF] Spoto | A termination analyzer for Java bytecode based on path-length[END_REF][START_REF] Urban | The abstract domain of segmented ranking functions[END_REF][START_REF] Yi Chen | Termination proofs for linear simple loops[END_REF]28,31,32,35, and 36 admit an eventual linear ranking function (which is discovered without using neither φ2,2 nor its relaxation). These are all shown terminating with the tool of [START_REF] Yi Chen | Termination proofs for linear simple loops[END_REF]. On the other hand, loops 14, 34, and 38 do have a disjunctive ranking function (following the terminology of [START_REF] Yi Chen | Termination proofs for linear simple loops[END_REF]), but do not admit an eventual linear ranking function. [START_REF] Ganty | Proving termination starting from the end[END_REF] shows how to partition the loop relation into behaviors that terminate and behaviors to be analyzed in a subsequent termination proof after refinement. This work addresses both termination and conditional termination problems in the same framework. Concerning the benchmarks proposed in [17, Table 1], loops 6-41 all have an eventually linear ranking function except for loops 11, 14, 30, 34, and 38.

A method based on abstract interpretation for synthesizing ranking functions is described in [START_REF] Urban | The abstract domain of segmented ranking functions[END_REF]. Although the work contains no completeness result, the approach is able to discover piecewise-defined ranking functions.

Finally, let us point out that the concept of eventual termination appeared first in [START_REF] Bradley | The polyranking principle[END_REF][START_REF] Bradley | Termination of polynomial programs[END_REF]. The class loops studied in these works is wider but, as the technique of [START_REF] Bradley | Termination of polynomial programs[END_REF] relies on finite differences, this approach is incomplete. On the other hand, while [START_REF] Bradley | The polyranking principle[END_REF] is also based on Farkas' Lemma, it seems [A. R. Bradley, Personal communication, May 2013] that the polyranking approach cannot prove, e.g., termination of the SLC loop p(x, y) ← x ≥ 1, x = y, y = y -1, p(x , y ), which admits an eventual linear ranking function.

CONCLUSION AND FUTURE WORK

We have proposed a definition of eventual linear ranking function for SLC loops that strictly generalizes the concept of linear ranking function. We also defined two correct and complete algorithms for detecting such ranking functions under different hypotheses. The first algorithm shows that the mere knowledge of the right increasing function allows checking the existence or even synthesizing an eventual linear ranking function in polynomial time. The second algorithm decides the existence of an eventual linear ranking function in its full generality but is not polynomial. We have also explained how to extend the algorithms for deciding eventual affine ranking functions. The algorithms admit a simple formulation as a constraint logic program and have been fully implemented in SICStus Prolog inside the Bin-Term termination prover [START_REF] Spoto | A termination analyzer for Java bytecode based on path-length[END_REF].

We plan to incorporate the algorithms in the Parma Polyhedra Library [START_REF] Bagnara | The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[END_REF] and then in the ECLAIR static analyzer for C, C ++ and Java programs. 4 This will enable us to conduct an extensive experimental evaluation on real programs. Moreover, as ECLAIR already includes linearization of floating-point constraints [START_REF] Belaid | Boosting local consistency algorithms over floating-point numbers[END_REF] as well as other sophisticated reasoning techniques over floating-point numbers (such as, e.g., [START_REF] Bagnara | Symbolic path-oriented test data generation for floating-point programs[END_REF]), the way is paved to explore a very interesting direction for future work: synthesis of eventual linear ranking functions for loops controlled by floating-point quantities.

It has to be noted that a nice property of the notion of eventual (not necessarily linear) ranking function is its simplicity. This is important when functions that witness termination have to be provided (and/or understood) by humans. This is the case when annotating a C/ACSL program with loop variants [START_REF] Baudin | ACSL: ANSI/ISO C Specification Language[END_REF]: for the cases when a ranking function to be specified in a loop variant clause is not obvious, one could extend ACSL with a loop prevariant clause that allows the annotator to indicate a candidate increasing function. In the linear case, our first algorithm can efficiently decide whether the two clauses constitute a termination witness.

On the other hand, there obviously are, as indicated in Section 4, more complex classes of ranking functions and algorithms that allow to establish the termination of SLC loops that do not admit an eventual linear ranking functions. A proper assessment of the relative merits of these approaches, all extremely recent, requires an extensive experimental evaluation that, as mentioned already, is one of the main objectives for future work.

The verification of linear ranking functions for integer SLC loops, that is to say, checking the satisfiability of c(x, x ) ∧ ρ(x) < 1 + ρ(x ) and c(x, x ) ∧ ρ(x) < 0, is an NP-complete problem. Concerning the existence of linear ranking functions, as the Farkas' Lemma is not true for the integers, the method presented in Section 2 is not valid. The problem, which has been solved very recently in [START_REF] Ben-Amram | On the linear ranking problem for integer linear-constraint loops[END_REF], is coNP-complete, and the paper proposes an exponential-time algorithm. Extending the present approach to integer SLC loops is another interesting idea to consider for future work.

Lemma 3 . 7 .

 37 Formula ∃k . DEC(a, b, k) is equivalent to the disjunction DEC1(a, b) ∨ DEC2(a, b).In our case, DEC1(a, b) is equivalent to ∃λ1, λ2, λ3 ≥ 0 . ( a = λ1 + λ2, -a = -λ2, b = λ2 + λ3, -b = -λ3, -1 ≥ -λ3,and DEC2(a, b) is equivalent to∃λ1 ≥ 0, λ2 ≥ 0, λ3 ≥ 0, λ4 > 0, P . ( a = λ1 + λ2, -a = -λ2, b = λ2 + λ3 -λ4, -b = -λ3, -1 ≥ -λ3 -P.Proof. (=⇒) Let k be a rational number and λi's for 1 ≤ i ≤ 4 four non-negative rational numbers such that DEC(a, b, k) holds. If λ4 = 0 then DEC(a, b, k) simplifies to DEC1(a, b) which is true. If λ4 > 0, we take P = kλ4 and we can see that DEC2(a, b) is true. (⇐=) Assume first that DEC1(a, b) is true. Then, taking λ4 = 0 and k = 0 (any rational number would be fine for k), we see that ∃k . DEC(a, b, k) is true. Assume then that DEC2(a, b) is true. Taking k = P/λ4 (this is always possible as λ4 > 0), we observe that there exists k such that DEC(a, b, k) is true.For the positivity condition, we can prove in a similar way Lemma 3.8. Formula ∃k . POS(a, b, k) is equivalent to the disjunction POS1(a, b) ∨ POS2(a, b).

Algorithm 1 Theorem 3 . 10 .

 1310 φ(a, b, k) ⇐⇒ DEC(a, b, k) ∧ POS(a, b, k). (⇐=) Assume the existence of k d such that DEC(a, b, k d ) and the existence of kp such that POS(a, b, kp). Then the rational k0 = max(k d , kp) verifies DEC(a, b, k0) ∧ POS(a, b, k0) and shows that ∃k . φ(a, b, k). Back to our initial problem, the existence of an eventual linear ranking function is equivalent to the satisfiability of at least one of the following four linear systems: DEC1(a, b) ∧ POS1(a, b), DEC1(a, b) ∧ POS2(a, b), DEC2(a, b) ∧ POS1(a, b), DEC2(a, b) ∧ POS2(a, b), which we can decide in polynomial time. For our running example, DEC2(a, b) ∧ POS1(a, b) is satisfiable as proved by the following SICStus Prolog query: L2 >= 0, L3 >= 0, L4 > 0, A = L1 + L2, B = L2 + L3 -L4, A = L2, B = L3, 1 =< L3 + P, LP1 >= 0, LP2 >= 0, LP3 >= 0, A = LP1 + LP2, B = LP2 + LP3, 0 = LP2, 0 = LP3, 0 =< LP3}. The procedure we have informally outlined by means of examples is actually completely general. It is embodied in Algorithm 1, which is a (correct and complete) decision procedure for the existence of an eventual linear ranking function given a linear increasing function. Existence of an eventual linear ranking function, given a linear increasing function Require: C, an SLC loop p(x) ← c(x, x ), p(x ), and f , a linear increasing function for C Ensure: Returns true if and only if, for some vector a, ρ(x) = a, x is an eventual linear ranking function for (C, f ). 1: DEC(a, k) := Farkas for the decreasing of ρ 2: DEC1(a), DEC2(a) := linearization of DEC(a, k) 3: POS(a, k) := Farkas for the positivity of ρ 4: POS1(a), POS2(a) := linearization of POS(a, k) 5: if W 1≤i,j≤2 DECi(a) ∧ POSj(a) is satisfiable then 6Let C be an SLC loop and f an increasing function for C. Algorithm 1 decides in polynomial time the existence of an eventual linear ranking function for (C, f ).

Example 3 . 11 .

 311 Continuing with Example 3.1, here is the most general solution of DEC2(a, b) ∧ POS1(a, b): ?-{L1 >= 0, L2>= 0, L3 >= 0, L4 > 0, A = L1 + L2, B = L2 + L3 -L4, A = L2, B = L3, 1 =< L3 + P, LP1 >= 0, LP2 >= 0, LP3 >= 0, A = LP1 + LP2, B = LP2 + LP3, 0 = LP2, 0 = LP3, 0 =< LP3}. B = 0, L1 = 0, L3 = 0, LP2 = 0, LP3 = 0, {LP1 = L4, L2 = L4, A = L4, L4 > 0, P >= 1}. ?-One particular solution is b = 0 = λ1 = λ3 = λ 2 = λ 3 , a = 1 = λ 1 = λ2 = λ4, P = 1. Hence ρ(x, y) = x is an eventual linear ranking function from the threshold k = P/λ4 = 1.

  0 ¯induces the space of functions of the form f (x, y) = b1x + b2y, which are increasing for C.Let us consider the SLC loop of Example 3.15 associated to an increasing function f (x, y) = b1x + b2y induced by INC. Defining ρ(x, y) = a1x + a2y and considering b1 and b2 as parameters, ρ is an eventual linear ranking function when ∃a1, a2, k . ∀x, y, x , y :

For our running? 2 . 2

 22 example, the following SICStus Prolog query proves that DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS1(a) is satisfiable + L2 + P1, A1 = L2, L > 0, A2 = L2 -L3 + P2, A2 = L3, -1 >= -L3 -P, % INC: B1 =< -2, B1 -2*B2 = 0 P1 =< -2*L, P1 -2*P2 = 0, % POS1: LP1 >= 0, LP2 >= 0, LP3 >= 0, A1 = LP1 + LP2, 0 = LP2, A2 = LP2 -LP3, 0 = LP3, 0 >= -LP3}. The procedure we have informally outlined by means of examples is actually completely general and is embodied in Algorithm Algorithm Existence of an eventual linear ranking function Require: C, an SLC loop p(x) ← c(x, x ), p(x ) Ensure: Returns true if and only if there exists an increasing function f for C and ρ(x) = a, x such that ρ is an eventual linear ranking function for (C, f ). 1: INC := the space of increasing functions for C 2: DEC(a, k) := Farkas for the decreasing of ρ 3: DEC1(a), DEC2(a, λ, p) := linearization of DEC(a, k) 4: POS(a, k) := Farkas for the positivity of ρ 5: POS1(a), POS2(a, λ , p ) := linearization of POS(a, k) 6: φ1,1 := DEC1(a) ∧ POS1(a) 7: φ1,2 := DEC1(a) ∧ POS2(a, λ , p ) ∧ p /λ ∈ INC 8: φ2,1 := DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS1(a) 9: φ2,2 := DEC2(a, λ, p) ∧ p/λ ∈ INC ∧ POS2(a, λ , p ) ∧ p/λ = p /λ 10: if W 1≤i,j≤2 φi,j is satisfiable then 11: return true 12: else 13: return false 14: end if Theorem 3.16. Let C be an SLC loop. Algorithm 2 decides the existence of an increasing function f and a linear function ρ such that ρ is an eventual linear ranking function for (C, f ).

A preliminary version of this work, in French, was presented in[START_REF] Alezan | Détection des fonctions de rang linéaires à terme[END_REF].

Acknowledgments.

We are grateful to Anthony Alezan, Aaron R. Bradley, Étienne Payet, and some anonymous referees for their helpful comments.