How to prove decidability of equational theories with second-order computation analyser SOL. (2019)

• Record Type: Journal Article
• Authors: HAMANA, MAKOTO
• Is Part Of: Journal of functional programming. Volume 29(2019)
• Publication Date: 2019
• Subjects: Functional programming (Computer science) -- Periodicals
• DOI: 10.1017/S0956796819000157
• Languages: English
• ISSNs: 0956-7968

Abstract

Abstract: We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool, i.e. Second-Order Laboratory, which assists the proofs of confluence and strong normalisation of computation rules derived from second-order algebraic theories. To cover various examples in programming language theory, we combine and extend both syntactical and semantical results of the second-order computation in a non-trivial manner. We demonstrate how to prove decidability of various algebraic theories in the literature. It includes the equational theories of monad and λ-calculi, Plotkin and Power's theory of states and bits, and Stark's theory of π-calculus. We also demonstrate how this methodology can solve the coherence of monoidal categories. Video Abstract: A video abstract can be found at: https://vimeo.com/365486403