Context term calculus for rewriting systems

R.S. Shevchenko

Abstract


In this paper, a calculus of context-full terms is proposed. Calculus extends the traditional algebraic signatures, used in term rewriting systems, by so-called constructions, that works with context: context constructor, resolving a context value and binding term to context with compatibility checking. Such extension allows to refining algorithms connected with analysis and transformations of source code in the more natural form, because f the structure of the sense in the modern programming language defined in hierarchical contexts, which can be directly mapped to context-full term in rewriting rule. Type analysis for a programming language can be implemented as checking for context compatibility. In such way, relative simple mechanism, which unites term rewriting and context analysis can be received. The approach is illustrated by defining rules for typing in context-full term formalism.

Problems in programming 2018; 2-3: 021-030

 


Keywords


software development automation; term rewriting; type systems; programming languages; code analysis; termware

References


Jan Willem Klop and Vincent van Oostrom and Femke van Raamsdonk. Combinatory Reduction Systems: introduction and survey. Theoretical Computer Science. Vol. 121. 1993. P. 279-308.

https://doi.org/10.1016/0304-3975(93)90091-7

Doroshenko A., Shevchenko R. A rewriting framework for rule-based programming dynamic applications. Fundamenta Informaticae. 2006. Vol. 72. N 1-3. P. 95-108.

Dan Dougherty, Pierre Lescanne, Luigi Liquori, Frédéric Lang. Addressed Term Rewriting Systems: Syntax, Semantics, and Pragmatics. Electronic Notes in Theoretical Computer Science. Vol. 127, Issue 5, 27 May 2005. P. 57-82.

https://doi.org/10.1016/j.entcs.2004.12.042

Cirstea, Horatiu and Kirchner, Claude and Liquori, Luigi. Rewriting Calculus with(out) Types. Proceedings of the fourth workshop on rewriting logic and applications. Electronic Notes in Theoretical Computer Science, Sep. 2002.

C. Barry Jay and Delia Kesner. Pure Pattern Calculus. ACM Trans. Program. Lang. Syst. 2005. P. 263-274.

Martin Bravenboer and Karl Trygve Kalleberg and Rob Vermaas and Eelco Visser. {Stratego/XT 0.17}. {A} language and toolset for program transformation. Science of Computer Programming. Vol. 72. 2008. P. 52-70.

https://doi.org/10.1016/j.scico.2007.11.003

Pfenning, F. and Elliott, C., Higher-order Abstract Syntax. Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation. PLDI-88. 1998. P. 199-208.

https://doi.org/10.1145/960116.54010

Bove, Ana; Peter Dybjer . Dependent Types at Work. LerNet ALFA Summer School. 2008: P. 57-99.

https://doi.org/10.1007/978-3-642-03153-3_2

Rinus Plasmeijer and Marko van Eekelen, Keep it Clean: A unique approach to functional programming. ACM Sigplan Notices, June 1999.

https://doi.org/10.1145/606666.606670

Eric Reed. Patina: A Formalization of the Rust Programming Language. University of Washington. Technical Report. 2015.

Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, Andy McNeil, Deny Capabilities for Safe, Fast Actors. Causality Ltd., Imperial College London, 2015.

https://doi.org/10.1145/2824815.2824816

Nada Amin and Tiark Rompf. Collapsing Towers of Interpreters. Proc. ACM Program. Lang. 2, POPL, Article 33 (January 2018). 33 p.

https://doi.org/10.1145/3158140




DOI: https://doi.org/10.15407/pp2018.02.021

Refbacks

  • There are currently no refbacks.