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

Page 1

Displaying 1 – 13 of 13

Showing per page

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

Termination checking with types

Andreas Abel (2010)

RAIRO - Theoretical Informatics and 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 ...

Traces of term-automatic graphs

Antoine Meyer (2008)

RAIRO - Theoretical Informatics and Applications

In formal language theory, many families of languages are defined using either grammars or finite acceptors. For instance, context-sensitive languages are the languages generated by growing grammars, or equivalently those accepted by Turing machines whose work tape's size is proportional to that of their input. A few years ago, a new characterisation of context-sensitive languages as the sets of traces, or path labels, of rational graphs (infinite graphs defined by sets of finite-state...

Transducing by observing length-reducing and painter rules

Norbert Hundeshagen, Peter Leupold (2014)

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

The recently introduced model of transducing by observing is compared with traditional models for computing transductions on the one hand and the recently introduced restarting transducers on the other hand. Most noteworthy, transducing observer systems with length-reducing rules are almost equivalent to RRWW-transducers. With painter rules we obtain a larger class of relations that additionally includes nearly all rational relations.

Transformations of grammars and translation directed by L R parsing

Bořivoj Melichar, Nguyen van Bac (2002)

Kybernetika

The class of L R translation grammars is introduced. This class is characterized by a possibility to implement a formal translation as an algorithm directed by L R parsing. To perform a translation, the conventional L R parser is extended by a facility to perform output operations within the parsing actions shift and reduce. The definitions of Kernel ( R ) - and L R -translation grammars are presented. The transformations shaking-down and postponing that enable to transform some translation grammars into Kernel...

Tree-controlled grammars with restrictions placed upon cuts and paths

Jiří Koutný, Alexander Meduna (2012)

Kybernetika

First, this paper discusses tree-controlled grammars with root-to-leaf derivation-tree paths restricted by control languages. It demonstrates that if the control languages are regular, these grammars generate the family of context-free languages. Then, in a similar way, the paper introduces tree-controlled grammars with derivation-tree cuts restricted by control languages. It proves that if the cuts are restricted by regular languages, these grammars generate the family of recursively enumerable...

Two extensions of system F with (co)iteration and primitive (co)recursion principles

Favio Ezequiel Miranda-Perea (2009)

RAIRO - Theoretical Informatics and Applications

This paper presents two extensions of the second order polymorphic lambda calculus, system F, with monotone (co)inductive types supporting (co)iteration, primitive (co)recursion and inversion principles as primitives. One extension is inspired by the usual categorical approach to programming by means of initial algebras and final coalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino's categorical lambda calculus within the framework of parametric polymorphism....

Currently displaying 1 – 13 of 13

Page 1