Transformational Approach to Inverse Computation in Term Rewriting
We deals with inverse computations of term rewriting systems (TRSs) by a transformational approach. In this talk, we first give an algorithm to generate a deterministic conditional TRS that computes inverses of functions defined by a given constructor TRS. We next give a transformation from deterministic conditional TRSs to TRSs with extra variables. At last, we show that narrowing simulates reduction sequences of the TRSs with extra variables, that is, inverse computations are done.
Proxima - A presentation-oriented editor for structured documents
Proxima is a generic editor that can be used for building a wide range of editors. Sample applications are language-specific source editors with derived type information in the source, WYSIWYG word-processing editors, mathematical-formula editors, but also tax-form applications, or tree browsers.
Proxima supports editing on the document structure as well as on the presentation. Thus, besides a mapping from the document to the presentation (the presentation mapping), we also need a mapping from the presentation to the document (the interpretation mapping). The presentation is specified by an attribute grammar, whereas the interpretation is specified by a combinator parser. The implementation of the presentation and interpretation mappings is facilitated by a layered architecture.
In the talk, I will present an overview of the layered architecture of the Proxima system. Furthermore, I will give a demonstration of several editors that have been implemented with Proxima.
More information on Proxima, as well as a preliminary version of my PhD thesis, is available at:
The Size-change Principle for Program Termination
The size-change termination principle is a simple yet powerful principle for (conservatively) proving termination for first order functional programs operating on values from a data domain for which there exists a well-founded ordering (e.g. lisp lists). The core idea is to observe how the arguments in a function call relate to the parameters; If every valid infinite call sequence causes infinite decrease in some data value (i.e. violates the well-foundedness assumption), then the program must terminate.
Lexicographical orders, indirect function calls and permuted arguments (descent that is not in-situ) are handled automatically without relying on user supplied argument orderings or using theorem-proving not certain to terminate at analysis time. If a program cannot be declared terminating by the analyzer, the call sequences that potentially lead to non-termination can be uncovered.
Even though the core idea is simple, providing a good size approximation (abstraction of the changes in argument sizes) is not trivial since one has to be able to provide size bounds on functions in order to properly handle nested (non-recursive) function calls. In this talk I present a size-analysis based on abstract interpretation and linear programming.
A working prototype analyzer has been implemented and is available online.
Xi: An XML Transformation System
A Tree Calculus for XML Queries and its Linear-time
Evaluation
(Joint work with Atsushi Ohori and Keishi Tajima)
The paper presents a declarative query language for tree structures, which cover the core of semistructured data, in particular XML. The language allows the user to write a query on tree structures by simply specifying the desired condition on a subset of nodes, and the preference measure. The system finds the subset that is true of the condition and has the highest measure. This paradigm of queries can represent, not to speak of simple top-one queries, a wide range of interesting queries, which are difficult or impossible to write in existing proposals for XML queries. A straightforward evaluation of such a query, however, takes exponential time and space. The major contribution of this paper is to show that whenever a query satisfies certain conditions, we can transform it into a recursive tree traversal program with linear time complexity.
An Algebraic Interface for GETA Search Engine
(Joint work with T. Murakami, S. Nishioka, A. Takano, and
M. Takeichi)
GETA is a library that implements high performance method for associative computation to be used as a basis of various document processing including searching or clustering. We proposed an algebraic view for the GETA engine as well as an actual interface which connects the high level view with the underlying efficient library. Users can write highly abstract programs in a calculational way through the interface and utilize program transformation techniques formalized as algebraic laws. The interface incorporates the algebraic operations into GETA basic operations which can be executed quite efficiently.
Back to ToPS's Home Page