K: A Rewriting-Based Framework for Computations -- Preliminary version

Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11354 Copy

Description

Title

K: A Rewriting-Based Framework for Computations -- Preliminary version

Author(s)

Rosu, Grigore

Issue Date

2007-12

Keyword(s)

Computer Science

Abstract

K is a definitional framework based on term rewriting, in which programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of special list and/or set structures, called cells, which can be potentially nested. In addition to cells, K definitions contain equations capturing structural equivalences that do not count as computational steps, and rewrite rules capturing computational steps or irreversible transitions. Rewrite rules in K are unconditional, i.e., they need no computational premises (they are rule schemata and may have ordinary side conditions, though), and they are context-insensitive, so in K rewrite rules apply concurrently as soon as they match, without any contextual delay or restrictions. The distinctive feature of K compared to other term rewriting approaches in general and to rewriting logic in particular, is that K allows rewrite rules to apply concurrently even in cases when they overlap, provided that they do not change the overlapped portion of the term. This allows for truly concurrent semantics to programming languages and calculi. For example, two threads that read the same location of memory can do that concurrently, even though the corresponding rules overlap on the store location being read. The distinctive feature of K compared to other frameworks for true concurrency, like chemical abstract machines (Chams) or membrane systems (P-systems), is that equations and rewrite rules can match across multiple cells and thus perform changes many places at the same time, in one step. K provides special support for list cells that carry ``computational meaning'', called computations. Computations are special ``->''-separated lists ``$T_1 -> T_2 -> \cdots -> T_n$'' comprising computational tasks, thought of as having to be ``processed'' sequentially. Computation (structural) equations or heating/cooling equations, which technically are ordinary equations but which practically tend to have a special ``computational'' intuition (reason for which we use the ``equality'' symbol ``<=> `` instead of ``='' for them), allow to regard computations (finitely) many different, but completely equivalent ways. For example, in a language with an addition operation whose arguments can be evaluated in non-deterministic order, a computation a1 + a2 may also be regarded as a1 -> []+a2, with the intuition ``schedule a1 for processing and freeze a2 in freezer []+_'', but also as a2 -> a1+[]. Computations can be handled like any other terms in a rewriting environment, that is, they can be matched, moved from one place to another in the original term, modified, or even deleted. A term may contain an arbitrary number of computations, so K can be naturally used to define concurrent languages or calculi. Structural equations can rearrange computations, so that rewrite rules can match and apply. Equations and rules can apply anywhere, in particular in the middle of computations, not only at their top. However, rules corresponding to inherently sequential operations (such as reads/writes of variables in the same thread) must be designed with care, to ensure that they are applied only at the top of computations. K achieves, in one uniform framework, the benefits of both Chams and reduction semantics with evaluation contexts (context reduction), at the same time avoiding what may be called the ``rigidity to chemistry'' of the former and the ``rigidity to syntax'' of the latter. Any Cham and any context reduction definition can be captured in K with minimal (in our view zero) representational distance. K can support concurrent language definitions with either an interleaving or a true concurrency semantics. K definitions can be efficiently executed on existing rewrite engines, thus providing ``interpreters for free'' directly from formal language definitions. Additionally, general-purpose formal analysis techniques and tools developed for rewrite logic, such as state space exploration for safety violations or model-checking, give us corresponding techniques and tools for the defined languages, at no additional development cost.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11354

Owning Collections