scholarly journals Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages

2006 ◽  
pp. 297-312 ◽  
Author(s):  
Jürgen Giesl ◽  
Stephan Swiderski ◽  
Peter Schneider-Kamp ◽  
René Thiemann
Keyword(s):  
Programming Languages ◽  
Term Rewriting ◽  
Termination Analysis

PATTERN MATCHING CODE MINIMIZATION IN REWRITING-BASED PROGRAMMING LANGUAGES

2002 ◽  
Vol 13 (06) ◽  
pp. 873-887
Author(s):  
NADIA NEDJAH ◽  
LUIZA DE MACEDO MOURELLE
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Term Rewriting ◽  
Directed Acyclic Graphs ◽  
Tree Automaton ◽  
Minimal Tree ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
Acyclic Graphs ◽  
Space Requirements

We compile pattern matching for overlapping patterns in term rewriting systems into a minimal, tree matching automata. The use of directed acyclic graphs that shares all the isomorphic subautomata allows us to reduce space requirements. These are duplicated in the tree automaton. We design an efficient method to identify such subautomata and avoid duplicating their construction while generating the dag automaton. We compute some bounds on the size of the automata, thereby improving on previously known equivalent bounds for the tree automaton.

scholarly journals Subtree matching by pushdown automata

2010 ◽  
Vol 7 (2) ◽  
pp. 331-357 ◽  
Author(s):  
Tomás Flouri ◽  
Jan Janousek ◽  
Bořivoj Melichar
Keyword(s):  
Programming Languages ◽  
Theorem Proving ◽  
Systematic Approach ◽  
Finite Automata ◽  
Term Rewriting ◽  
Mechanical Theorem Proving ◽  
Pushdown Automaton ◽  
String Pattern ◽  
Pushdown Automata ◽  
Mechanical Theorem

Subtree matching is an important problem in Computer Science on which a number of tasks, such as mechanical theorem proving, term-rewriting, symbolic computation and nonprocedural programming languages are based on. A systematic approach to the construction of subtree pattern matchers by deterministic pushdown automata, which read subject trees in prefix and postfix notation, is presented. The method is analogous to the construction of string pattern matchers: for a given pattern, a nondeterministic pushdown automaton is created and is then determinised. In addition, it is shown that the size of the resulting deterministic pushdown automata directly corresponds to the size of the existing string pattern matchers based on finite automata.

R2M: A RECONFIGURABLE REWRITE MACHINE

1994 ◽  
Vol 04 (01n02) ◽  
pp. 171-180
Author(s):  
R. RAMESH
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Parallel Architecture ◽  
Term Rewriting ◽  
Fixed Number ◽  
Main Memory ◽  
Input Size ◽  
Computational Paradigm ◽  
Rewrite Rules ◽  
Parallel Pattern

Term rewriting is a popular computational paradigm for symbolic computations such as formula manipulation, theorem proving and implementations of nonprocedural programming languages. In rewriting, the most demanding operation is repeated simplification of terms by pattern matching them against rewrite rules. We describe a parallel architecture, R2M, for accelerating this operation. R2M can operate either as a stand-alone processor using its own memory or as a backend device attached to a host using the host’s main memory. R2M uses only a fixed number (independent of input size) of processing units and fixed capacity auxiliary memory units, yet it is capable of handling variable-size rewrite rules that change during simplification. This is made possible by a simple and reconfigurable interconnection present in R2M. Finally, R2M uses a hybrid scheme that combines the ease, and efficiency of parallel pattern matching using the tree representation of terms, and the naturalness of their dag representation for replacements.

scholarly journals Multi-Dimensional Interpretations for Termination of Term Rewriting

2021 ◽  
pp. 273-290
Author(s):  
Akihisa Yamada
Keyword(s):  
General Framework ◽  
Term Rewriting ◽  
Termination Analysis ◽  
Interpretation Method

AbstractInterpretation methods constitute a foundation of termination analysis for term rewriting. From time to time remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper we introduce a general framework, the multi-dimensional interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover and verify its significance through experiments.

Transformation techniques for context-sensitive rewrite systems

2004 ◽  
Vol 14 (4) ◽  
pp. 379-427 ◽  
Author(s):  
JÜRGEN GIESL ◽  
AART MIDDELDORP
Keyword(s):  
Functional Programming ◽  
Term Rewriting ◽  
Lazy Evaluation ◽  
Transformation Techniques ◽  
Termination Analysis ◽  
Rewrite Systems ◽  
Context Sensitive ◽  
Term Rewrite Systems ◽  
Huge Variety

Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.

scholarly journals On Unfolding for Programs Using Strings as a Data Type

10.29007/m8rr ◽  
2018 ◽  
Author(s):  
Andrei Nemytykh
Keyword(s):  
Programming Languages ◽  
Term Rewriting ◽  
Computation Model ◽  
Abstract Machine ◽  
Rewriting Systems ◽  
Word Equation ◽  
Semantic Tree ◽  
Long Time ◽  
One Step ◽  
Transformation Methods

As a rule, program transformation methods based on semantics unfolda semantic tree of a given program. Sometimes that allows to optimize the program or to prove its certain properties automatically.Unfolding is one of the basic operations, which is a meta-extension of one step of the abstract machine executing the program.This paper is interested in unfolding for programs based on pattern matching and manipulating the strings. The corresponding computation model originates from Markov's normal algorithms and extends this theoretical base.Even though algorithms unfolding programs were being intensively studied for a long time in the context of variety of programming languages, as far as we know, the associative concatenation was stood at the wayside of the stream.We define a class of term rewriting systems manipulating with strings anddescribe an algorithm unfolding the programs from the class. The programming language defined by this class is algorithmic complete.Given a word equation, one of the algorithms suggested in this paper results in a description of the corresponding solution set.

scholarly journals On Tree Pattern Matching by Pushdown Automata

10.14311/1113 ◽  
2009 ◽  
Vol 49 (2) ◽  
Author(s):  
T. Flouri
Keyword(s):  
Programming Languages ◽  
Pattern Matching ◽  
Systematic Approach ◽  
Term Rewriting ◽  
Pushdown Automaton ◽  
Tree Pattern ◽  
Tree Pattern Matching ◽  
String Pattern ◽  
Pushdown Automata ◽  
Mechanical Theorem

Tree pattern matching is an important operation in Computer Science on which a number of tasks such as mechanical theorem proving, term-rewriting, symbolic computation and non-procedural programming languages are based on. Work has begun on a systematic approach to the construction of tree pattern matchers by deterministic pushdown automata which read subject trees in prefix notation. The method is analogous to the construction of string pattern matchers: for given patterns, a non-deterministic pushdown automaton is created and then it is determinised. In this first paper, we present the proposed non-deterministic pushdown automaton which will serve as a basis for the determinisation process, and prove its correctness. 

Sign in / Sign up

Export Citation Format

Share Document