An Executable Rewriting Logic Semantics of K-Scheme
From FSL
This paper is part of our ongoing work on Rewriting Logic Semantics, providing a concise description of the functional language K-Scheme, a dialect of Scheme based on the R5RS specification. The implementation is available on the K-Scheme project page, as well as an online interface to try examples.
[edit] An Executable Rewriting Logic Semantics of K-Scheme
- An Executable Rewriting Logic Semantics of K-Scheme
- Patrick Meredith, Mark Hills and Grigore Rosu
- 8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
- Abstract. This paper presents an executable rewriting logic semantics of K-Scheme, a dialect of Scheme based (partially) on the informal definition given in the R5RS report. The presented semantics follows the K language definitional style but is almost entirely equational (it contains one rule which could be made into an equation if unspecified order of procedure application sub-term evaluation is removed), so it can also be regarded as an algebraic denotational specification with an initial model/algebra semantics of K-Scheme. Equational specifications can be executed on common rewrite engines, provided that equations are oriented into rewrite rules, typically from left-to-right. While, in theory, equational specifications can leave certain behaviors underspecified, thus allowing more algebras as models, in practice they need to completely specify all the desired behaviors if one wants to use their associated rewrite systems as ``interpreters, or ``implementations. To become executable, K-Scheme overspecifies certain features left undefined on purpose in R5RS. In spite of overspecifying for executability reasons, the rewriting logic semantics in this paper is the most complete formal definition of a language in the Scheme family that we are aware of, in the sense that it provides definitions for more Scheme language features than any other similar attempts. The presented executable definition of K-Scheme can serve as a platform for experimentation with variants and extensions of Scheme, for example concurrency. The Maude system is used in this paper, but other rewrite engines could have been used as well. Even though, on paper, K rewrite-based definitions tend to be as compact and high-level as reduction-based definitions with evaluation contexts, their complete translation in Maude as executable specifications is rather verbose and low-level. An automated translator from K to Maude is under development, which will reduce the size of K definitions several times compared to their Maude equivalent, and will certainly increase their readability. The complete Maude specification is public, together with a web-based interface to ``execute K-Scheme programs without having to download Maude.
