Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOL
Pages 3 - 9
Abstract
We give an overview of the theory and practice of second-order rewriting. Second-order rewriting methods have been demonstrated as useful that is applicable to important notions of programming languages such as logic programming, algebraic effects, quantum computation, and cyclic computation. We explain foundation and evolution of second-order rewriting by presenting the framework of second-order computation systems. We also demonstrate our system SOL of second-order laboratory through various programming language examples.
References
[1]
Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)
[2]
Arkor, N., Fiore, M.: Algebraic models of simple type theories: a polynomial approach. In: Proceedings of LICS 2020, pp. 88–101. ACM (2020)
[3]
Blanqui F Bachmair L Termination and confluence of higher-order rewrite systems Rewriting Techniques and Applications 2000 Heidelberg Springer 47-61
[4]
Blanqui F Termination of rewrite relations on -terms based on Girard’s notion of reducibility Theor. Comput. Sci. 2016 611 50-86
[5]
Fiore M and Hur C-K Dawar A and Veith H Second-order equational logic (extended abstract) Computer Science Logic 2010 Heidelberg Springer 320-335
[6]
Fiore, M., Hamana, M.: Multiversal polymorphic algebraic theories: syntax, semantics, translations, and equational logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pp. 520–529 (2013)
[7]
Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of PPDP 2002, pp. 26–37. ACM Press (2002)
[8]
Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proceedings of LICS 2008, pp. 57–68 (2008)
[9]
Fiore M and Mahmoud O Hliněný P and Kučera A Second-order algebraic theories Mathematical Foundations of Computer Science 2010 2010 Heidelberg Springer 368-380
[10]
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proceedings of LICS 1999, pp. 193–202 (1999)
[11]
Fiore, M., Staton, S.: Substitution, jumps, and algebraic effects. In: Proceedings of the CSL-LICS 2014, pp. 41:1–41:10 (2014)
[12]
Hamana, M., Abe, T., Kikuchi, K.: Polymorphic computation systems: theory and practice of confluence with call-by-value. Sci. Comput. Program. 187(102322) (2020)
[13]
Hamana M Chin W-N Free -monoids: a higher-order syntax with metavariables Programming Languages and Systems 2004 Heidelberg Springer 348-363
[14]
Hamana M Giesl J Universal algebra for termination of higher-order rewriting Term Rewriting and Applications 2005 Heidelberg Springer 135-149
[15]
Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proceedings of PPDP 2007, pp. 97–108. ACM Press (2007)
[16]
Hamana, M.: Initial algebra semantics for cyclic sharing tree structures. Log. Methods Comput. Sci. 6(3(15)), 1–1–23 (2010)
[17]
Hamana M Escobar S Semantic labelling for proving termination of combinatory reduction systems Functional and Constraint Logic Programming 2010 Heidelberg Springer 62-78
[18]
Hamana M Hofmann M Polymorphic abstract syntax via Grothendieck construction Foundations of Software Science and Computational Structures 2011 Heidelberg Springer 381-395
[19]
Hamana M Cyclic datatypes modulo bisimulation based on second-order algebraic theories Log. Methods Comput. Sci. 2017 13 1-38
[20]
Hamana M How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation Proc. ACM Program. Lang. 2017 1 22 1-28
[21]
Hamana M Gallagher JP and Sulzmann M Polymorphic rewrite rules: confluence, type inference, and instance validation Functional and Logic Programming 2018 Cham Springer 99-115
[22]
Hamana, M.: How to prove decidability of equational theories with second-order computation analyser SOL. J. Funct. Program. 29(e20) (2019)
[23]
Hamana, M.: Modular termination for second-order computation rules and application to algebraic effect handlers. arXiv:1912.03434 (2020)
[24]
Klop, J.W.: Combinatory reduction systems. Ph.D. thesis, CWI. Mathematical Centre Tracts, vol. 127, Amsterdam (1980)
[25]
Staton, S.: An algebraic presentation of predicate logic. In: Proceedings of FOSSACS 201, pp. 401–417 (2013)
[26]
Staton, S.: Instances of computational effects: an algebraic perspective. In: Proceedings of LICS 2013, p. 519 (2013)
[27]
Staton, S.: Algebraic effects, linearity, and quantum programming languages. In: Proceedings of POPL 2015, pp. 395–406 (2015)
[28]
Yokoyama T, Hu Z, and Takeichi M Deterministic second-order patterns Inf. Process. Lett. 2004 89 6 309-314
Index Terms
- Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOL
Index terms have been assigned to the content through auto-classification.
Recommendations
Asymptotic Stability for Intermittently Controlled Second-Order Evolution Equations
Motivated by several works on ordinary differential equations, we are interested in the asymptotic stability of intermittently controlled partial differential equations. We give a condition of asymptotic stability for second-order evolution equations ...
Initial-Value Technique for Singularly Perturbed Boundary-Value Problems for Second-Order Ordinary Differential Equations Arising in Chemical Reactor Theory
An initial-value technique is presented for solving singularly perturbed two-point boundary-value problems for linear and semilinear second-order ordinary differential equations arising in chemical reactor theory. In this technique, the required ...
A second-order accurate numerical approximation for the fractional diffusion equation
Fractional order diffusion equations are generalizations of classical diffusion equations, treating super-diffusive flow processes. In this paper, we examine a practical numerical method which is second-order accurate in time and in space to solve a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sep 2020
228 pages
© Springer Nature Switzerland AG 2020.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 14 September 2020
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 26 Jan 2025