The so-called Hilbert’s Program , aiming at a full axiomatization of mathematics , fuelled the quest to provide an answer to the Entscheidungsproblem , the Decision Problem , aiming to find effective methods to obtain the truth value of logical sentences. Intuitively, when using such methods a halting behavior would be desirable, thus providing a clear answer to the prospective user. This was implicit in Hilbert’s finitist approach to the foundations of mathematics and practical use of logical methods. In 1936 the quest for such effective methods brought four different approaches: Kleene’s formulation of Gödel/Herbrand general recursion, Church’s λ -definability, Turing’s computation with automatic machines (a-machines), and Post’s machines. However, the halting issue was treated quite differently in those approaches. In particular, the technical meaning of “computation” was explicitly introduced by Turing in his 1936 paper and he payed no attention to halting computations there. This paper traces how the halting requirement became a stable part of the definition of computation which is often used today.

Abstract Generalized Term Rewriting Systems (GTRSs) extend Conditional Term Rewriting Systems by (i) selecting the arguments of function symbols on which rewritings are allowed and (ii) allowing for more general conditions in rules, namely, atoms defined by a set of Horn clauses. They are useful to model and analyze properties of computations with sophisticated languages like . Toyama proved that left-linear and almost parallel-closed Term Rewriting Systems (TRSs) are confluent. In this paper, we generalize and extend his result to GTRSs without requiring left-linearity . This improves Toyama’s result, as we show with some examples. Also, Toyama’s result entails confluence of weakly orthogonal TRSs, thus providing a syntactic criterion for proving confluence without requiring termination . We similarly introduce weakly V-orthogonal GTRSs, which are confluent. Weak V-orthogonality checking is implemented in the confluence tool , to improve its ability to deal with context-sensitive and conditional term rewriting systems.

This article describes the confluence framework, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically prove and disprove confluence of Generalized Term Rewriting Systems, where (i) only selected arguments of function symbols can be rewritten and (ii) a rather general class of conditional rules can be used. This includes, as particular cases, several variants of rewrite systems such as (context-sensitive) term rewriting systems, string rewriting systems, and (context-sensitive) conditional term rewriting systems. The divide-and-conquer modular strategy allows us to combine in a proof tree different techniques for proving confluence, including modular decompositions, checking joinability of (conditional) critical and variable pairs, transformations, etc., and auxiliary tasks required by them, e.g., joinability of terms, joinability of conditional pairs, etc.

Reduction-based systems are used as a basis for the implementation of programming languages, automated reasoning systems, mathematical analysis tools, etc. In such inherently non-deterministic systems, guaranteeing that diverging steps can be eventually rejoined is crucial for a faithful use in most applications. This property of reduction systems is called local confluence. In a landmark 1980 paper, Gérard Huet characterized local confluence of a Term Rewriting System as the joinability of all its critical pairs. In this paper, we characterize local confluence of Conditional Term Rewriting Systems, where reduction steps may depend on the satisfaction of specific conditions in rules: a conditional term rewriting system is locally confluent if and only if (i) all its conditional critical pairs and (ii) all its conditional variable pairs (which we introduce in this paper) are joinable. Furthermore, the logic-based approach we follow here is well-suited to analyze local confluence of more general reduction-based systems. We exemplify this by (i) including (context-sensitive) replacement restrictions in the arguments of function symbols, and (ii) allowing for more general conditions in rules. The obtained systems are called Generalized Term Rewriting Systems. A characterization of local confluence is also given for them.

Context-sensitive rewriting is a restriction of term rewriting where reductions are allowed on specific arguments of function symbols only, and then in particular positions of terms. Confluence is an abstract property of reduction relations guaranteeing that two diverging reduction sequences can always be joined into a common reduct. In this paper we investigate confluence of context-sensitive rewriting and present some novel results. In particular, a characterization of local confluence of context-sensitive rewriting as the joinability of an extended class of critical pairs which we introduce here. We also show that the treatment of joinability of critical pairs using theorem proving and solving feasibility problems is useful to automatically prove and disprove confluence of context-sensitive rewriting. Our techniques have been implemented in a new tool, CONFident. We show by means of benchmarks the impact of the new techniques discussed in the paper.

We characterize conditional rewriting as satisfiability in a Herbrand-like model of terms where variables are also included as fresh constant symbols extending the original signature. Confluence of conditional rewriting and joinability of conditional critical pairs is characterized similarly. Joinability of critical pairs is then translated into combinations of (in)feasibility problems which can be efficiently handled by a number of automatic tools. This permits a more efficient use of standard results for proving confluence of conditional term rewriting systems, most of them relying on auxiliary proofs of joinability of conditional critical pairs, perhaps with additional syntactical and (operational) termination requirements on the system. Our approach has been implemented in a new system: CONFident . Its ability to (dis)prove confluence of conditional term rewriting systems is witnessed by means of some benchmarks comparing our tool with existing tools for similar purposes.

Abstract Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments $$\mu (f)\subseteq \{1,\ldots ,k\}$$ μ ( f ) ⊆ { 1 , … , k } of k-ary function symbols f only. Terms which cannot be further rewritten in this way are called $$\mu $$ μ -normal forms. For left-linear term rewriting systems (TRSs), the so-called normalization via $$\mu $$ μ -normalization procedure provides a systematic way to obtain normal forms by the stepwise computation and combination of intermediate $$\mu $$ μ -normal forms. In this paper, we show how to obtain bounds on the derivational complexity of computations using this procedure by using bounds on the derivational complexity of context-sensitive rewriting. Two main applications are envisaged: Normalization via $$\mu $$ μ -normalization can be used with non-terminating TRSs where the procedure still terminates; on the other hand, it can be used to improve on bounds of derivational complexity of terminating TRSs as it discards many rewritings.

The halting problem is a prominent example of undecidable problem and its formulation and undecidability proof is usually attributed to Turing's 1936 landmark paper. Copeland noticed in 2004, though, that it was so named and, apparently, first stated in a 1958 book by Martin Davis. We provide additional arguments partially supporting this claim as follows: (i) with a focus on computable (real) numbers with infinitely many digits (e.g., π), in his paper Turing was not concerned with halting machines; (ii) the two decision problems considered by Turing concern the ability of his machines to produce specific kinds of outputs, rather than reaching a halting state, something which was missing from Turing's notion of computation; and (iii) from 1936 to 1958, when considering the literature of the field no paper refers to any “halting problem” of Turing Machines until Davis' book. However, there were important preliminary contributions by (iv) Church, for whom termination was part of his notion of computation (for the λ-calculus), and (v) Kleene, who essentially formulated, in his 1952 book, what we know as the halting problem now.

The semantics of computational systems (e.g., relational and knowledge data bases, query-answering systems, programming languages, etc.) can often be expressed as (the specification of) a logical theory Th. Queries, goals, and claims about the behavior or features of the system can be expressed as formulas φ which should be checked with respect to the intended model of Th, which is often huge or even incomputable. In this paper we show how to prove such semantic properties φ of Th by just finding a model A of Th∪{φ}∪Zφ, where Zφ is an appropriate (possibly empty) theory depending on φ only. Applications to relational and deductive databases, rewriting-based systems, logic programming, and answer set programming are discussed.

A declarative program P is a theory in a given computational logic L, so that computation with such a program is efficiently implemented as deduction in L. That is why inference systems are crucial: they both (i) define the logical semantics of a language in its underlying logic L, and (ii) specify the execution of programs in a correct implementation. The notion of operational termination (OT) of a declarative program P identifies termination with absence of infinite inference with P. We further develop the OT notion for declarative programs in general logics with schematic inference systems and characterize OT in terms of chains of proof jumps. We also generalize the Dependency Pair Framework for Term Rewriting Systems to an arbitrary schematic logic L, so that methods for proving declarative programs OT become available for a very wide range of declarative languages. We illustrate the usefulness of the general OT methods we propose by three case studies in three logics: that of Conditional Term Rewriting Systems, the Typed λ-calculus, and Membership Rewriting Logic. In particular, we show how various programs that could not be proved terminating with existing methods can be proved OT with the methods presented here.

Types (or sorts) are pervasive in computer science and in rewritingbased programming languages, which often support subtypes (subsorts) and subtype polymorphism. Programs in these languages can be modeled as order-sorted term rewriting systems (OS-TRSs). Often, termination of such programs heavily depends on sort information. But few techniques are currently available for proving termination of OS-TRSs; and they often fail for interesting OS-TRSs. In this paper we generalize the dependency pairs approach to prove termination of OS-TRSs. Preliminary experiments suggest that this technique can succeed where existing ones fail, yielding easier and simpler termination proofs

Nowadays, polynomial interpretations are an essential ingredient in the development of tools for proving termination. We have recently proven that polynomial interpretations over the reals are strictly better for proving polynomial termination of rewriting than those which only use integer coefficients. Some essential aspects of their practical use, though, remain unexplored or underdeveloped. In this paper, we compare the two current frameworks for using polynomial intepretations over the reals and show that one of them is strictly better than the other, thus making a suitable choice for implementations. We also prove that the use of algebraic real co-efficients in the interpretations suffice for termination proofs. We also discuss the use of algorithms and techniques from Tarski's first-order logic of the real closed fields for implementing their use in proofs of termination. We argue that more standard constraint-solving techniques are better suited for this. We propose an algorithm to solve the polynomial constraints which arise when specific finite subsets of rational (or even algebraic real) numbers are considered for giving value to the coefficients. We provide a preliminary experimental evaluation of the algorithm which has been implemented as part of the termination tool MU-TERM.

Abstract The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide methods for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated languages. On the basis of the uselessness of redundant arguments, we also propose an erasure procedure which may avoid wasteful computations while still preserving the semantics (under ascertained conditions). A prototype implementation of these methods has been undertaken, which demonstrates the practicality of our approach.

Many functional logic languages are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction mechanism of functional languages and the resolution principle of logic languages. Needed narrowing is an optimal evaluation strategy which constitutes the basis of modern (narrowing-based) lazy functional logic languages. In this work, we present the fundamentals of partial evaluation in such languages. We provide correctness results for partial evaluation based on needed narrowing and show that the nice properties of this strategy are essential for the specialization process. In particular, the structure of the original program is preserved by partial evaluation and, thus, the same evaluation strategy can be applied for the execution of specialized programs. This is in contrast to other partial evaluation schemes for lazy functional logic programs which may change the program structure in a negative way. Recent proposals for the partial evaluation of declarative multi-paradigm programs use (some form of) needed narrowing to perform computations at partial evaluation time. Therefore, our results constitute the basis for the correctness of such partial evaluators.

Advanced typing, matching, and evaluation strategy features, as well as very general conditional rules, are routinely used in equational programming languages such as, for example, ASF+SDF, OBJ, CafeOBJ, Maude, and equational subsets of ELAN and CASL. Proving termination of equational programs having such expressive features is important but nontrivial, because some of those features may not be supported by standard termination methods and tools, such as muterm, CiME, AProVE, TTT, Termptation, etc. Yet, use of the features may be essential to ensure termination. We present a sequence of theory transformations that can be used to bridge the gap between expressive equational programs and termination tools, prove the correctness of such transformations, and discuss a prototype tool performing the transformations on Maude equational programs and sending the resulting transformed theories to some of the aforementioned tools.

Context-sensitive rewriting (CSR) has recently emerged as an interesting and flexible paradigm that provides a bridge between the abstract world of general rewriting and the (more) applied setting of declarative specification and programming languages such as OBJ*, CafeOBJ, ELAN, and Maude. A natural approach to study properties of programs written in these languages is to model them as context-sensitive rewriting systems. Here we are especially interested in proving termination of such systems, and thereby providing methods to establish termination of e.g. OBJ* programs. For proving termination of context-sensitive re-writing, there exist a few transformation methods, that reduce the problem to termination of a transformed ordinary term rewriting system (TRS). These transformations, however, have some serious drawbacks. In particular, most of them do not seem to support a modular analysis of the termination problem. In this paper we will show that a substantial part of the well-known theory of modular term rewriting can be extended to CSR, via a thorough analysis of the additional complications arising from context-sensitivity. More precisely, we will mainly concentrate on termination (properties). The obtained modularity results correspond nicely to the fact that in the above languages the modular design of programs and specifications is explicitly promoted, since it can now also be complemented by modular analysis techniques.

Declarative languages such as OBJ, CafeOBJ, and Maude use syntactic annotations to introduce replacement restrictions aimed at improving termination or efficiency of computations. Unfortunately, there is a lack of formal techniques for proving such benefits. We show that context-sensitive rewriting and on-demand rewriting provide a suitable framework to address this problem. We provide methods to analyze termination of on-demand rewriting and apply them to analyze termination of OBJ, CafeOBJ, and Maude programs.

Functional logic languages combine the operational principles of the most important declarative programming paradigms, namely functional and logic programming. Inductively sequential programs admit the definition of optimal computation strategies and are the basis of several recent (lazy) functional logic languages. In this paper, we define a partial evaluator for inductively sequential functional logic programs. We prove strong correctness of this partial evaluator and show that the nice properties of inductively sequential programs carry over to the specialization process and the specialized programs. In particular, the structure of the programs is preserved by the specialization process. This is in contrast to other partial evaluation methods for functional logic programs which can destroy the original program structure. Finally, we present some experiments which highlight the practical advantages of our approach.