All a b c d e f g h i j k l m n o p q r s t u v w x y z Other

Previous Page 6 Next

Displaying 101 – 120 of 138

Showing per page

Polynomials over the reals in proofs of termination : from theory to practice

Salvador Lucas (2005)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

This paper provides a framework to address termination problems in term rewriting by using orderings induced by algebras over the reals. The generation of such orderings is parameterized by concrete monotonicity requirements which are connected with different classes of termination problems: termination of rewriting, termination of rewriting by using dependency pairs, termination of innermost rewriting, top-termination of infinitary rewriting, termination of context-sensitive rewriting, etc. We...

Polynomials over the reals in proofs of termination : from theory to practice

Salvador Lucas (2010)

RAIRO - Theoretical Informatics and Applications

This paper provides a framework to address termination problems in term rewriting by using orderings induced by algebras over the reals. The generation of such orderings is parameterized by concrete monotonicity requirements which are connected with different classes of termination problems: termination of rewriting, termination of rewriting by using dependency pairs, termination of innermost rewriting, top-termination of infinitary rewriting, termination of context-sensitive rewriting, etc. We...

Positioned agents in eco-grammar systems with border markers and pure regulated grammars

Miroslav Langer, Alica Kelemenová (2012)

Kybernetika

In this paper we follow our previous research in the field of positioned agents in the eco-grammar systems and pure grammars. We extend model of the positioned eco-grammar systems by boundary markers and we introduce bordered positioned eco-grammar systems (BPEG systems, for short) and that way we show one of the possible answers to the question stated in [9]. Namely we compare generative power of the BPEG systems with three types of pure regulated grammars with appearance checking.

Rewriting on cyclic structures: Equivalence between the operational and the categorical description

Andrea Corradini, Fabio Gadducci (2010)

RAIRO - Theoretical Informatics and Applications

We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. – but for the case of circular redexes , for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and...

String Assembling Systems

Martin Kutrib, Matthias Wendlandt (2012)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

We introduce and investigate string assembling systems which form a computational model that generates strings from copies out of a finite set of assembly units. The underlying mechanism is based on piecewise assembly of a double-stranded sequence of symbols, where the upper and lower strand have to match. The generation is additionally controlled by the requirement that the first symbol of a unit has to be the same as the last symbol of the strand generated so far, as well as by the distinction...

String Assembling Systems

Martin Kutrib, Matthias Wendlandt (2012)

RAIRO - Theoretical Informatics and Applications

We introduce and investigate string assembling systems which form a computational model that generates strings from copies out of a finite set of assembly units. The underlying mechanism is based on piecewise assembly of a double-stranded sequence of symbols, where the upper and lower strand have to match. The generation is additionally controlled by the requirement that the first symbol of a unit has to be the same as the last symbol of the strand generated so far, as well as by the distinction...

Substitution systems associated with the dynamical system (𝒜, Tf)*

Maria de Fátima Correia, Carlos Ramos, Sandra Vinagre (2012)

ESAIM: Proceedings

We consider the dynamical system (𝒜, Tf), where 𝒜 is a class of differential real functions defined on some interval and Tf : 𝒜 → 𝒜 is an operator Tfφ := fοφ, where f is a differentiable m-modal map. If we consider functions in 𝒜 whose critical values are periodic points for f then, we show how to define and characterize a substitution system associated with (𝒜, Tf). For these substitution systems, we compute the growth rate of the...

Termination checking with types

Andreas Abel (2004)

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications

The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces Λ μ + , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose soundness is...

Currently displaying 101 – 120 of 138