Búsqueda avanzada

El autor Salvador Lucas ha publicado 15 artículo(s):

1 - Productivity of rewrite systems without transformations

Termination of programs, i.e., the absence of infinite computations, ensures the existence of normal forms for all initial expressions, thus providing an essential ingredient for the definition of a normalization semantics for functional programs. In lazy functional languages, though, infinite data structures are often delivered as the outcome of computations. For instance, the list of all prime numbers can be returned as a neverending stream of numerical expressions or data structures. If such streams are allowed, requiring termination is hopeless. In this setting, the notion of productivity can be used to provide an account of computations with infinite data structures, as it “captures the idea of computability, of progress of infinite-list programs” (B.A. Sijtsma, On the Productivity of Recursive List Definitions, ACM Transactions on Programming Languages and Systems 11(4):633- 649, 1989). However, in the realm of Term Rewriting Systems, which can be seen as (first-order, untyped, unconditional) functional programs, termination of Context-Sensitive Rewriting (CSR) has been showed equivalent to productivity of rewrite systems through appropriate transformations. In this way, tools for proving termination of CSR can be used to prove productivity. In term rewriting, CSR is the restriction of rewriting that arises when reductions are allowed on selected arguments of function symbols only. In this paper we show that well-known results about the computational power or CSR are useful to better understand the existing connections between productivity of rewrite systems and termination of CSR, and also to obtain more powerful techniques to prove productivity of rewrite systems.

Autores: Salvador Lucas / 
Palabras Clave: context-sensitive rewriting - functional programming - productivity - termination

2 - Automatic generation of logical models for order-sorted first-order theories in program analysis

Computations are often viewed as proofs of specific sentences in some computational logic describing the operational semantics of the programming language or computational system. Since the semantics of programs (i.e., the set of such specific sentences that are provable in the logic) is usually incomputable, and most program properties undecidable, abstraction is essential in program analysis. Abstractions can be formalized as semantic models which should be automatically generated in a push-the-button-and-wait style of program analysis and verification. We investigate the automatic generation of numerical models for order-sorted first-order logics and its use in program analysis. Our development systematically uses the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of sorted signatures by means of appropriately adapted convex matrix interpretations. Such numerical interpretations permit the use of existing algorithms and tools from linear algebra (e.g., Farkas’ Lemma), real algebraic geometry, and arithmetic constraint solving in the implementation of the analyses.

Autores: Salvador Lucas / 
Palabras Clave: Abstraction - Logical models - Order-sorted first-order logic - Program analysis - termination

3 - Use of logical models for proving operational termination in general logics (Tutorial)

A declarative programming language is based on some logic L and its operational semantics is given by a proof calculus which is often presented in a natural deduction style by means of inference rules. Declarative programs are theories S of L and executing a program is proving goals G in the inference system I(S) associated to S as a particularization of the inference system of the logic. The usual soundness assumption for L implies that every model M of S also satisfies G. In this setting, the operational termination of a declarative program is quite naturally defined as the absence of infinite proof trees in the inference system I(S). Proving operational termination of declarative programs often involves two main ingredients: (i) the generation of logical models M to abstract the program execution (i.e., the provability of specific goals in I(S)), and (ii) the use of well-founded relations to guarantee the absence of infinite branches in proof trees and hence of infinite proof trees, possibly taking into account the information about provability encoded by M. In this paper we show how to deal with (i) and (ii) in a uniform way. The main point is the synthesis of logical models where well-foundedness is a side requirement for some specific predicate symbols.

Autores: Salvador Lucas / 
Palabras Clave: Abstraction - Logical models - Operational Termination

4 - Some applications of context-sensitive rewriting (Tutorial)

The appropriate selection of the arguments of functions that can be evaluated in function calls improves the evaluation of such calls in a number of different ways: efficiency, speed, termination behavior, etc. This is essential in the conditional if-then-else operator. Other operators like sequencing (;) or choice (+) that are used in concurrent and/or imperative languages require a similar treatment. The (lazy) list constructor ‘cons’ of functional languages is another well-known example. At the syntactic level we can specify this by just associating a set mu(f) of indices of evaluable arguments to each function symbol ‘f’ by means of a mapping mu which we call a replacement map. For instance, we let mu(if-then-else)={1} to specify that only the boolean argument ‘b’ of a conditional expression (if b then e else e’) is necessarily evaluated. We can write mu(;)={1} to avoid computations on S2 in a sequence S1;S2, and mu(+)={} to say that processes should not be executed as part of a choice expression. In the realm of term rewriting, context-sensitive rewriting is the restriction of rewriting that arises when these syntactic replacement restrictions are taken into account. It has been used to improve the termination behavior of reduction-based computation systems and programs. It has been shown useful as an operational notion to model or simulate the executions of various formalisms and calculi. Some computational properties of context-sensitive rewriting (remarkably termination) have been used to characterize or verify computational properties of important rewriting strategies like innermost, outermost, demand-driven, and lazy rewriting. Context-sensitive rewriting has also been shown useful to develop verification techniques and tools for variants of rewriting like order-sorted or conditional rewriting. Consequently, it is also useful for analyzing computational properties of programs written in sophisticated rewriting-based programming languages such as OBJ*, CafeOBJ, Maude, Elan, etc., where related language constructions are used. This paper provides an overview of the theory of context-sensitive rewriting and some of its applications.

Autores: Salvador Lucas / 
Palabras Clave: context-sensitive rewriting - infinitary normalization - normalization - replacement restrictions - rewriting semantics - termination

5 - Analysis of Rewriting-Based Systems as First-Order Theories (Trabajo ya publicado)

Computational systems based on a first-order language that can be given a *canonical model* which captures provability in the corresponding calculus can often be seen as first-order theories S, and computational properties of such systems can be formulated as first-order sentences F that hold in such a canonical model of S. In this setting, standard results regarding the *preservation* of satisfiability of different classes of first-order sentences yield a number of interesting applications in program analysis. In particular, properties expressed as existentially quantified boolean combinations of atoms (for instance, a set of *unification problems*) can then be *disproved* by just finding an *arbitrary* model of the considered theory plus the *negation* of such a sentence. We show that rewriting-based systems fit into this approach. Many computational properties (e.g., infeasibility and non-joinability of critical pairs in (conditional) rewriting, non-loopingness, or the secure access to protected pages of a web site) can be investigated in this way. Interestingly, this semantic approach succeeds when specific techniques developed to deal with the aforementioned problems fail.

Autores: Salvador Lucas / 
Palabras Clave: Logical models - Program analysis - Rewriting-based systems

6 - Directions of Operational Termination (Trabajo original)

A theory S in a logic supplied with an inference system is operationally terminating if no goal has an infinite well-formed proof tree. Well-formed proof trees are those which an interpreter would incrementally build when trying to solve a condition at a time from left to right. For this reason, infinite well-formed proof trees have a unique infinite branch which is called the spine. This paper introduces the notion of a directed proof tree for S and a set of formulas Δ, which we call a direction. Intuitively, a direction Δ is intended to collect formulas that are infinitely often used in the spine of an infinite well-formed proof tree (which is then called Δ-directed) due to the repeated use of some specific inference rules. Then we introduce the notion of Δ-directed operational termination of a theory as the absence of Δ-directed proof trees. This new notion permits the definition of different termination properties which can be useful to distinguish different computational behaviors. It also gives a new characterization of operational termination of a (finite) theory S as the conjunction of the Δ-directed operational termination of S for each direction Δ in a (finite) set of directions.

Autores: Salvador Lucas / 
Palabras Clave: General Logics - Operational Termination - Program Termination

7 - The 2D Dependency Pair Framework for conditional rewrite systems (Trabajo ya publicado)

Different termination properties of conditional term rewriting systems have been recently described emphasizing the bidimensional nature of the termination behavior of conditional rewriting. The absence of infinite sequences of rewriting steps (termination in the usual sense), provides the horizontal dimension. The absence of infinitely many attempts to launch the subsidiary processes that are required to check the rule’s condition and perform a single rewriting step has been called V-termination and provides the vertical dimension. We have characterized these properties by means of appropriate notions of dependency pairs and dependency chains. In this paper we introduce a 2D Dependency Pair Framework for automatically proving and disproving all these termination properties. Our implementation of the framework as part of the termination tool MU-TERM and the benchmarks obtained so far suggest that the 2D Dependency Pair Framework is currently the most powerful technique for proving operational termination of conditional term rewriting systems.

Autores: Salvador Lucas / José Meseguer / Raúl Gutiérrez / 
Palabras Clave: Conditional term rewriting - dependency pairs - Operational Termination - Program analysis

8 -

9 -

10 -

11 - Using Well-Founded Relations for Proving Operational Termination

In this paper, we study *operational termination*, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.

Autores: Salvador Lucas / 
Palabras Clave: Declarative languages - Logical models - Operational Termination - Program analysis - Well-foundedness

12 - Proving Program Properties as First-Order Satisfiability

Program semantics can often be expressed as a (many-sorted) first-order theory $S$, and program properties as sentences $varphi$ which are intended to hold in the *canonical model* of such a theory, which is often incomputable. Recently, we have shown that properties $varphi$ expressed as the existential closure of a boolean combination of atoms can be *disproved* by just finding a model of $S$ and the *negation* $negvarphi$ of $varphi$. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theories. In this paper we extend our previous results to emph{arbitrary} properties, expressed as sentences without any special restriction. Consequently, one can prove a program property $varphi$ by just *finding a model* of an appropriate theory (including $S$ and possibly something else) and an appropriate first-order formula related to $varphi$. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.

Autores: Salvador Lucas / 
Palabras Clave: First-Order Logic - Logical models - Program analysis

13 - infChecker: A Tool for Checking Infeasibility

Given a CTRS R and terms s and t, we say that the reachability condition s = t isfeasible if there is a substitution sigma instantiating the variables in s and t such that the reachability test sigma(s) ->*R sigma(t) succeeds; otherwise, we call it infeasible. Given a sequence of reachability conditions (s1 = t1),…,(sn = tn), where n > 0, we say that the sequence is R-feasible if there is a substitution such that all the reachability tests sigma(si) ->*R sigma(ti) are satised.In [5, 6] we presented an approach to deal with infeasibility using a semantic criterion. In this paper we present infChecker, a new tool for checking infeasibility conditions of CTRSs based on this approach. We succesfully participated in the 2019 Confuence Competition in the INF (infeasibility) category, being the most powerful tool for checking both infeasibility and feasibility.

Autores: Raúl Gutiérrez / Salvador Lucas / 
Palabras Clave: Conditional term rewriting - First-Order Logic - infeasibility

14 - The origins of the halting problem

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., +A8A), in his paper Turing was not concerned with halting machines+ADs (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+ADs and (iii) from 1936 to 1958, when considering the literature of the field no paper refers to any +IBw-halting problem+IB0 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 +A7s–calculus), and (v) Kleene, who essentially formulated, in his 1952 book, what we know as the halting problem now.

Autores: Salvador Lucas / 
Palabras Clave: Halting problem - Printing problem - Program Termination

15 - A characterization of local confluence of conditional term rewriting systems

When using non-deterministic reduction-based systems, guaranteeing that two diverging steps can be eventually rejoined is crucial for a faithful use in most applications. This property of reduction systems is called local confluence. Gérard Huet provided a characterization of local confluence for term rewriting systems. In conditional term rewriting systems, reduction steps may depend on the satisfaction of specific conditions in rules. Although conditional rewriting was introduced and used already in the 1970s and deeply investigated in the early 1980s, only partial characterizations or sufficient conditions of local confluence of conditional term rewriting have been obtained so far. In this paper, we char- acterize local confluence of conditional rewrite systems as the joinability of a set of conditional pairs including the usual conditional critical pairs and a new kind of pairs we call conditional variable pairs.

Autores: Salvador Lucas / 
Palabras Clave: Automated reasoning - Conditional rewriting - Confluence - First-Order Logic - Program analysis