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.

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 Rewriting and narrowing for constructor systems with call-time choice semantics

2012 ◽  
Vol 14 (2) ◽  
pp. 165-213 ◽  
Author(s):  
FRANCISCO J. LÓPEZ-FRAGUAS ◽  
ENRIQUE MARTIN-MARTIN ◽  
JUAN RODRÍGUEZ-HORTALÁ ◽  
JAIME SÁNCHEZ-HERNÁNDEZ
Keyword(s):  
Term Rewriting ◽  
Point Of View ◽  
Rewriting Logic ◽  
Semantic Framework ◽  
Rewriting Systems ◽  
Functional Logic ◽  
One Step ◽  
Soundness And Completeness ◽  
Semantic Point ◽  
Simple Reduction

AbstractNon-confluent and non-terminating {constructor-based term rewriting systems are useful for the purpose of specification and programming. In particular, existing functional logic languages use such kinds of rewrite systems to define possibly non-strict non-deterministic functions. The semantics adopted for non-determinism is call-time choice, whose combination with non-strictness is a non-trivial issue, addressed years ago from a semantic point of view with the Constructor-based Rewriting Logic (CRWL), a well-known semantic framework commonly accepted as suitable semantic basis of modern functional logic languages. A drawback of CRWL is that it does not come with a proper notion of one-step reduction, which would be very useful to understand and reason about how computations proceed. In this paper, we develop thoroughly the theory for the first-order version of let-rewriting, a simple reduction notion close to that of classical term rewriting, but extended with a let-binding construction to adequately express the combination of call-time choice with non-strict semantics. Let-rewriting can be seen as a particular textual presentation of term graph rewriting. We investigate the properties of let-rewriting, most remarkably their equivalence with respect to a conservative extension of the CRWL-semantics coping with let-bindings, and we show by some case studies that having two interchangeable formal views (reduction/semantics) of the same language is a powerful reasoning tool. After that, we provide a notion of let-narrowing, which is adequate for call-time choice as proved by soundness and completeness results of let-narrowing with respect to let-rewriting. Moreover, we relate those let-rewriting and let-narrowing relations (and hence CRWL) with ordinary term rewriting and narrowing, providing in particular soundness and completeness of let-rewriting with respect to term rewriting for a class of programs which are deterministic in a semantic sense.

A categorical understanding of environment machines

1992 ◽  
Vol 2 (1) ◽  
pp. 23-59 ◽  
Author(s):  
Andrea Asperti
Keyword(s):  
Programming Languages ◽  
Category Theory ◽  
Functional Languages ◽  
Abstract Machine ◽  
Complete Reduction ◽  
Rewriting Systems ◽  
Definition Of ◽  
Categorical Semantics ◽  
Operational Aspects

AbstractIn the last two decades, category theory has become one of the main tools for the denotational investigation of programming languages. Taking advantage of the algebraic nature of the categorical semantics, and of the rewriting systems it suggests, it is possible to use these denotational descriptions as a base for research into more operational aspects of programming languages.This approach proves to be particularly interesting in the study and the definition of environment machines for functional languages. The reason is that category theory offers a simple and uniform language for handling terms and environments (substitutions), and for studying their interaction (through application).Several examples of known machines are discussed, among which the Categorical Abstract Machine of Cousineau et al. (1987) and Krivine's machine. Moreover, as an example of the power and fruitfulness of this approach, we define two original categorical machines. The first one is a variant of the CAM implementing a λ-calculus with both call-by-value and call-by-name as parameters passing modes. The second one is a variant of Krivine's machine performing complete reduction of λ-terms.

scholarly journals Semantics and strong sequentiality of priority term rewriting systems

1998 ◽  
Vol 208 (1-2) ◽  
pp. 87-110 ◽  
Author(s):  
Masahiko Sakai ◽  
Yoshihito Toyama
Keyword(s):  
Term Rewriting ◽  
Term Rewriting Systems ◽  
Rewriting Systems

scholarly journals Infinite normal forms for non-linear term rewriting systems

1995 ◽  
Vol 152 (2) ◽  
pp. 285-303
Author(s):  
Paola Inverardi ◽  
Monica Nesi
Keyword(s):  
Normal Forms ◽  
Term Rewriting ◽  
Linear Term ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
Non Linear

scholarly journals The Church-Rosser property for ground term-rewriting systems is decidable

1987 ◽  
Vol 49 (1) ◽  
pp. 43-79 ◽  
Author(s):  
Michio Oyamaguchi
Keyword(s):  
Term Rewriting ◽  
Ground Term ◽  
Term Rewriting Systems ◽  
Rewriting Systems ◽  
The Church
Sign in / Sign up

Export Citation Format

Share Document