We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner;firstly we...
详细信息
ISBN:
(纸本)1581137052
We present an extension of first-order term rewriting systems, which involves variable binding in the term language. We develop the systems called binding term rewriting systems (BTRSs) in a stepwise manner;firstly we present the term language, then formulate equational logic, and finally define rewrite systems by two styles: rewrite logic and pattern matching styles. The novelty of this development is that we follow an initial algebra approach in an extended notion of σ-algebras in various functor categories. These are based on Fiore-Plotkin-Turi's presheaf semantics of variable binding and Lüth-Ghani's monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs are initial algebras in suitable categories. Finally, we discuss our design choice of BTRSs from a semantic perspective.
Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint...
详细信息
ISBN:
(纸本)1581137052
Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current implementations only extend Herbrand equation solvers. In this paper we show how to define CHR programs that extend arbitrary solvers and fully interact with them. In the process, we examine how to compile such programs to perform as little recomputation as possible, and describe how to build index structures for CHR constraints that are modified automatically when variables in the underlying solver change. We report on the implementation of these techniques in the HAL compiler, and give empirical results illustrating their benefits.
This paper describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities fro...
详细信息
ISBN:
(纸本)1581137052
This paper describes a method for transforming any given set of Datalog rules into an efficient specialized implementation with guaranteed worst-case time and space complexities, and for computing the complexities from the rules. The running time is optimal in the sense that only useful combinations of facts that lead to all hypotheses of a rule being simultaneously true are considered, and each such combination is considered exactly once. The associated space usage is optimal in that it is the minimum space needed for such consideration modulo scheduling optimizations that may eliminate some summands in the space usage formula. The transformation is based on a general method for algorithm design that exploits fixed-point computation, incremental maintenance of invariants, and combinations of indexed and linked data structures. We apply the method to a number of analysis problems, some with improved algorithm complexities and all with greatly improved algorithm understanding and greatly simplified complexity analysis.
We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders. First, we introduce typed binding signatures and develop a theory of typed abstr...
详细信息
ISBN:
(纸本)1581137052
We investigate a framework for representing and reasoning about syntactic and semantic aspects of typed languages with variable binders. First, we introduce typed binding signatures and develop a theory of typed abstract syntax with binders. Each signature is associated to a category of "presentation" models, where the language of the typed signature is the initial model. At the semantic level, types can be given also a computational meaning in a (possibly different) semantic category. We observe that in general, semantic aspects of terms and variables can be reflected in the presentation category by means of an adjunction. Therefore, the category of presentation models is expressive enough to represent both the syntactic and the semantic aspects of languages. We introduce then a metalogical system, inspired by the internal languages of the presentation category, which can be used for reasoning on both the syntax and the semantics of languages. This system is composed by a core equational logic tailored for reasoning on the syntactic aspects;when a specific semantics is chosen, the system can be modularly extended with further "semantic" notions, as needed.
We present a new evaluation strategy for functional logic programs described by weakly orthogonal conditional term rewriting systems. Our notion of weakly orthogonal conditional rewrite system extends a notion of Berg...
详细信息
ISBN:
(纸本)1581137052
We present a new evaluation strategy for functional logic programs described by weakly orthogonal conditional term rewriting systems. Our notion of weakly orthogonal conditional rewrite system extends a notion of Bergstra and Klop and covers a large part of programs defined by conditional equations. Our strategy combines the flexibility of logic programming (computation of solutions for logic variables) with efficient evaluation methods from functional programming. In particular, it is the first known narrowing strategy for this class of programs that evaluates ground terms deterministically. This is achieved by a transformation of conditional term rewriting systems (CTRS) into unconditional ones which is sound and complete w.r.t. the semantics of the original CTRS. We show that the transformation preserves weak orthogonality for the terms of interest. This property allows us to apply a relatively efficient evaluation strategy for weakly orthogonal unconditional term rewriting systems (parallel narrowing) on the transformed programs.
Early resolution mechanisms proposed for tabling such as OLDT rely on suspension and resumption of subgoals to compute fixpoints. Recently, a new resolution framework called linear tabling has emerged as an alternativ...
详细信息
ISBN:
(纸本)1581137052
Early resolution mechanisms proposed for tabling such as OLDT rely on suspension and resumption of subgoals to compute fixpoints. Recently, a new resolution framework called linear tabling has emerged as an alternative tabling method. The idea of linear tabling is to use iterative computation rather than suspension to compute fixpoints. Although linear tabling is simple, easy to implement, and superior in space efficiency, the current implementations are several times slower than XSB, the state-of-the-art implementation of OLDT, due to re-evaluation of looping subgoals. In this paper, we present a new linear tabling method and propose several optimization techniques for fast computation of fixpoints. The optimization techniques significantly improve the performance by avoiding redundant evaluation of subgoals, re-application of clauses, and reproduction of answers in iterative computation. Our implementation of the method in B-Prolog not only consumes an order of magnitude less stack space than XSB for some programs but also compares favorably well with XSB in speed.
We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role ...
详细信息
ISBN:
(纸本)1581137052
We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for the module language. We first consider a "plain" notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrate the notions of: module intrachecking (each module is typechecked in isolation and its interface, which is the set of typings of the defined identifiers, is inferred);interface interchecking (when linking modules, typechecking is done just by looking at the interfaces);interface specialization (interface intrachecking may require to specialize the typing listed in the interfaces);principal interfaces (the principal typing property for the type system of modules);and separate typechecking (looking at the code of the modules does not provide more type information than looking at their interfaces). Then we illustrate some limitations of the "plain" framework and extend the module language and the type system in order to overcome these limitations. The decidability of the system is shown by providing algorithms for the fundamental operations involved in module intrachecking and interface interchecking.
Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions a...
详细信息
ISBN:
(纸本)1581137052
Substitution in the lambda calculus is a complex operation that traditional presentations of beta contraction naively treat as a unitary operation. Actual implementations are more careful. Within them, substitutions are realized incrementally through the use of environments. However, environments are usually not accorded a first-class status within such systems in that they are not reflected into term structure. This approach does not allow the smaller substitution steps to be intermingled with other operations of interest on lambda terms. Various new notations for lambda terms remedy this situation by proposing an explicit treatment of substitutions. Unfortunately, a naive implementation of beta reduction based on such notations has the potential of being costly: each use of the substitution propagation rules causes the creation of a new structure on the heap that is often discarded in the immediately following step. There is, thus, a tradeoff between these two approaches. This paper discusses these tradeoffs and offers an amalgamated approach that utilizes recursion in rewrite rule application but also suspends substitution operations where profitable.
Outermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension (known as weakly) deals with non-inductiv...
详细信息
ISBN:
(纸本)1581137052
Outermost-needed rewriting/narrowing is a sound and complete optimal demand-driven strategy for the class of inductively sequential constructor systems. Its parallel extension (known as weakly) deals with non-inductively sequential constructor systems. In this paper, we present natural rewriting, a suitable extension of (weakly) outermost-needed rewriting which is based on a refinement of the demandness notion associated to the latter, and we extend it to narrowing. Intuitively, natural rewriting (narrowing) always reduces (narrows) the most often demanded position in a term. We formalize the strategy for left-linear constructor systems though, for the class of inductively sequential constructor systems, natural rewriting (narrowing) behaves even better than outermost-needed rewriting (narrowing) in the avoidance of failing computations. With regard to inductively sequential constructor systems, we introduce a larger class of systems called inductively sequential preserving where natural rewriting and narrowing preserve optimality for sequential parts of the program. We also provide a prototype interpreter of natural rewriting and narrowing.
In this paper we propose a typed, purely functional calculus for state (with second-class locations) in which types reflect the dichotomy between reading from and writing into the global store. This is in contrast to ...
详细信息
ISBN:
(纸本)1581137052
In this paper we propose a typed, purely functional calculus for state (with second-class locations) in which types reflect the dichotomy between reading from and writing into the global store. This is in contrast to the usual formulation of state via monads, where the primitives for reading and writing introduce the same monadic type constructor. We hope to argue that making this distinction is useful, simple, and has strong logical foundations. Our type system is based on the proof-term calculus for constructive modal logic S4, which has two modal type operators: € for necessity and for possibility. We extend this calculus with the notion of names (which stand for locations) and generalize to indexed families of modal operators (indexed by sets of names). Then, the modal type €CA classifies computations of type A which read from store locations listed in the set C. The dual type CA classifies computations which first write into the locations from C and than use the changed store to obtain a value of type A. There are several benefits to this development. First, the necessitation fragment of the language is interesting in its own: it formulates a calculus of dynamic binding. Second, the possibility operator is a monad, thus forcing the single-threading of memory writes, but not of memory reads (as these are associated with €). Finally, the different status of reads and writes gives rise to a natural way of expressing the allocation of uninitialized memory while also providing guarantees that only initialized locations are dereferenced.
暂无评论