Navegación

Búsqueda

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 - Proving termination properties of conditional rewrite systems

Conditional Term Rewriting Systems (CTRSs) extend Term Rewriting Systems (TRSs) conditional part c to each rewrite rule l → r, thus obtaining a conditional rewrite rule l → r ⇐ c. The addition of such conditional parts c substantially increases the expressiveness of programming languages that use them and often clarifies the purpose of the rules to make programs more readable and self-explanatory. Computations with CTRSs are defined by means of an Inference System where each rewriting step s →R t requires a proof. This proof-theoretical definition of the operational semantics suggests a natural definition of the termination behavior of R as the absence of infinite proof trees. The notion of operational termination captures this idea, meaning that, given an initial goal, an interpreter will either succeed in finite time in producing a closed proof tree, or will fail in finite time, not being able to close or extend further any of the possible proof trees, after exhaustively searching all such proof trees. Besides implying termination in the usual ‘horizontal’ sense (i.e., as the absence of infinite sequences of rewrite steps), operational termination also captures a ‘vertical’ dimension of the termination behavior which is missing in the usual “without infinite reduction sequences” definition of termination. In [1] we define the notion of V-termination, which captures such a vertical dimension of the termination behavior of CTRSs. We provide a uniform definition of termination and V-termination of CTRSs as the absence of specific kinds of infinite proof trees. We prove that operational termination is just the conjunction of termination and V-termination. We use these results to develop a methodology to prove or disprove termination, V-termination, and operational termination of CTRSs by extending the Dependency Pair (DP) approach for TRSs and generalize the DP approach to all aforementioned termination properties of CTRSs.

Autores: Salvador Lucas / José Meseguer / 
Palabras Clave:

4 - A tool for the automatic generation of logical models of order-sorted first-order theories

Semantics-based program analysis guarantees that the obtained knowledge about focused program features matches the real behaviour of the program. Automation of the analyses requires abstraction mechanisms to approximate the (usually undecidable) program semantics and targeted properties. In this setting, the logical notions of interpretation of a logic language and model of a theory provide an appropriate framework for abstraction in the sense that the corresponding analyses will be sound and, when relying on some decidable theory, amenable for automation. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. Such theories are very helpful in the semantic description of most programming languages. The current version of the tool systematically exploits (and relies on) the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted convex matrix interpretations. The system is available as a web application and can be used to give support to users interested in checking properties of software modules provided
that they are able to describe the property as an order-sorted first-order theory whose satisfiability guarantees the property. Examples of such properties are partial correctness, program termination, etc. The paper illustrates the use of the tool by means of simple case studies.

Autores: Raúl Gutiérrez  / Salvador Lucas  / Patricio Reinoso / 
Palabras Clave: Abstraction - Logical models - Order-sorted first-order logic - Program analysis - termination

5 - 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

6 - 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

7 - 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

8 - 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

9 - 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

10 -

11 -

12 -

13 - 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

14 - 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

15 - 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