Hostname: page-component-6bf8c574d5-w79xw Total loading time: 0 Render date: 2025-02-21T02:15:02.675Z Has data issue: false hasContentIssue false
  • English
  • Français

How to prove decidability of equational theories with second-order computation analyser SOL

Part of: ICFP2017 JFP Research Articles

Published online by Cambridge University Press:  24 December 2019

MAKOTO HAMANA Open the ORCID record for MAKOTO HAMANA [Opens in a new window]
MAKOTO HAMANA*
Affiliation:
Gunma University, Kiryu, Gunma, Japan (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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
Type
Regular Paper
Information
Journal of Functional Programming , Volume 29 , 2019 , e20
Copyright
© Cambridge University Press 2019 

References

Aoto, T. & Toyama, Y. (2012) A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. Logic. Method. Comput. Sci. 8(1), 1–29.Google Scholar
Baader, F. & Nipkow, T. (1998) Term Rewriting and All that. Cambridge University Press.CrossRefGoogle Scholar
Baxter, L. (1977) The Complexity of Unification. PhD Thesis, Department of Computer Science, University of Waterloo.Google Scholar
Benton, N. & Hyland, M. (2003) Traced premonoidal categories. Theor. Inform. Appl. 37(4), 273–299.CrossRefGoogle Scholar
Benton, P. N., Bierman, G. M. & de Paiva, V. (1998) Computational types from a logical perspective. J. Funct. Program. 8(2), 177–193.CrossRefGoogle Scholar
Bird, R. & Moor, O. D. (1996) Algebra of Programming. Prentice-Hall.CrossRefGoogle Scholar
Blanqui, F. (2000) Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000). LNCS, vol. 1833. Springer, pp. 47–61.CrossRefGoogle Scholar
Blanqui, F. (2016) Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theor. Comput. Sci. 611, 50–86.CrossRefGoogle Scholar
Chakravarty, M. M. T., Keller, G. & Peyton Jones, S. L. (2005a) Associated type synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26–28, 2005, pp. 241–253.Google Scholar
Chakravarty, M. M. T., Keller, G., Peyton Jones, S. L. & Marlow, S. (2005b) Associated types with class. In Proceedings of POPL’05, Long Beach, California, USA, January 12–14, 2005, pp. 1–13.CrossRefGoogle Scholar
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J. & Talcott, C. L. (2007) All About Maude - A High-Performance Logical Framework, How to Specify, program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer.Google Scholar
Coquand, T. (1992) Pattern matching with dependent types. In Proceedings of the 3rd Workshop on Types for Proofs and Programs.Google Scholar
Damas, L. & Milner, R. (1982) Principal type-schemes for functional programs. In Proceedings of POPL’82, pp. 207–212.CrossRefGoogle Scholar
Diaconescu, R. & Futatsugi, K. (2002) Logical foundations of CafeOBJ. Theor. Comput. Sci. 285(2), 289–318.CrossRefGoogle Scholar
Fiore, M. (2002) Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proceedings of PPDP’02. ACM, pp. 26–37.CrossRefGoogle Scholar
Fiore, M. (2008) Second-order and dependently sorted abstract syntax. In Proceedings of LICS’08, pp. 57–68.CrossRefGoogle Scholar
Fiore, M. & Hamana, M. (2013) 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.CrossRefGoogle Scholar
Fiore, M. & Hur, C.-K. (2010) Second-order equational logic. In Proceedings of CSL’10. LNCS, vol. 6247, pp. 320–335.Google Scholar
Fiore, M. & Mahmoud, O. (2010) Second-order algebraic theories. In Proceedings of MFCS’10. LNCS, vol. 6281, pp. 368–380.CrossRefGoogle Scholar
Fiore, M., Plotkin, G. & Turi, D. (1999) Abstract syntax and variable binding. In Proceedings of LICS’99, pp. 193–202.CrossRefGoogle Scholar
Fiore, M. P. & Campos, M. D. (2013) The algebra of directed acyclic graphs. In Coecke, B., Ong, L., & Panangaden, P. (eds), Computation, Logic, Games, and Quantum Foundations. LNCS, vol. 7860, pp. 37–51.CrossRefGoogle Scholar
Fiore, M. P., Moggi, E. & Sangiorgi, D. (1996) A fully-abstract model for the pi-calculus. In 11th Logic in Computer Science Conference (LICS’96). IEEE, pp. 43–54. Information and Computation 179, 76–117 (2002).CrossRefGoogle Scholar
Gibbons, J. (1995) An initial-algebra approach to directed acyclic graphs. In Proceedings of MPC’95. LNCS, vol. 947, pp. 282–303.Google Scholar
Gibbons, J. & Hinze, R. (2011) Just do it: simple monadic equational reasoning. In Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19–21, 2011, pp. 2–14.CrossRefGoogle Scholar
Girard, J.-Y. (1989) Proofs and Types. Cambridge University Press. translated and with appendices by Paul Taylor, Yves Lafont.Google Scholar
Goguen, J., Winkler, T., Meseguer, J. & Futatsugi, K. (2000) Introducing OBJ. In Goguen, J. & Malcolm, G. (eds), Software Engineering with OBJ. ADFM, vol. 2, pp. 3–167.CrossRefGoogle Scholar
Hamana, M. (2004) Free Σ-monoids: a higher-order syntax with metavariables. In Asian Symposium on Programming Languages and Systems (APLAS’04). LNCS, vol. 3302, pp. 348–363.CrossRefGoogle Scholar
Hamana, M. (2005) Universal algebra for termination of higher-order rewriting. In Rewriting Techniques and Application (RTA’05). LNCS, vol. 3467, pp. 135–149.CrossRefGoogle Scholar
Hamana, M. (2007) Higher-order semantic labelling for inductive datatype systems. In Proceedings of 9th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’07). ACM, pp. 97–108.CrossRefGoogle Scholar
Hamana, M. (2010) Semantic labelling for proving termination of combinatory reduction systems. In Proceedings of WFLP’09. LNCS, vol. 5979, pp. 62–78.CrossRefGoogle Scholar
Hamana, M. (2011) Polymorphic abstract syntax via Grothendieck construction. In FoSSaCS’11. LNCS, vol. 3467, pp. 381–395.CrossRefGoogle Scholar
Hamana, M. (2016) Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories. In Proceedings of FSCD’16. The Leibniz International Proceedings in Informatics (LIPIcs), vol. 52, 21:1–21:18.Google Scholar
Hamana, M. (2017) How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. Proc. ACM Program. Lang. 1(22), 1–28.CrossRefGoogle Scholar
Hamana, M. (2018) Polymorphic rewrite rules: confluence, type inference, and instance validation. In Proceedings of 14th International Symposium on Functional and Logic Programming (FLOPS’18). LNCS, vol. 10818, 99–115.Google Scholar
Hasegawa, M. (2005) Classical linear logic of implications. Math. Struct. Comput. Sci. 15(2), 323–342.CrossRefGoogle Scholar
Huet, G. (1980) Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821.CrossRefGoogle Scholar
Jouannaud, J., Kirchner, H. & Remy, J. (1983) Church–Rosser properties of weakly terminating term rewriting systems. In Proceedings of the 8th International Joint Conference on Artificial Intelligence, pp. 909–915.Google Scholar
Kelly, G. M. (1964) On mac lane’s conditions for coherence of natural associativities, commutativities, etc. J. Alg. 1(4), 397–402.CrossRefGoogle Scholar
Knuth, D. & Bendix, P. (1970) Simple word problems in universal algebras. In Computational Problem in Abstract Algebra. Oxford: Pergamon, pp. 263–297. Included also in Automation of reasoning 2, Springer (1983), pp. 342–376.Google Scholar
Libal, T. & Miller, D. (2016) Functions-as-constructors higher-order unification. In Proceedings of FSCD 2016. Leibniz International Proceedings in Informatics (LIPIcs), vol. 52, pp. 26:1–26:17.Google Scholar
Lindley, S. (2007) Extensional rewriting with sums. In Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26–28, 2007. Proceedings, pp. 255–271.CrossRefGoogle Scholar
Lindley, S. & Stark, I. (2005) Reducibility and ⊤⊤-lifting for computation types. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings, pp. 262–277.CrossRefGoogle Scholar
Mac Lane, S. (1963) Natural associativity and commutativity. Rice Univ. Stud. 49(4), 28–46. Available at: http://hdl.handle.net/1911/62865.Google Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer-Verlag.CrossRefGoogle Scholar
Mayr, R. & Nipkow, T. (1998) Higher-order rewrite systems and their confluence. Theor. Comput. Sci. 192(1), 3–29.CrossRefGoogle Scholar
Melliès, P.-A. (2010) Segal condition meets computational effects. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11–14 July 2010, Edinburgh, UK, 150–159.CrossRefGoogle Scholar
Miller, D. (1991) A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Comput. 1(4), 497–536.CrossRefGoogle Scholar
Milner, R. (1996) Semantic ideas in computing. In Wand, I. and Milner, R. (eds), Computing Tomorrow. Cambridge University Press.CrossRefGoogle Scholar
Milner, R. (1999) Communicating and Mobile Systems - The π-Calculus. Cambridge University Press.Google Scholar
Moggi, E. (1988) Computational Lambda-Calculus and Monads. LFCS ECS-LFCS-88-66. University of Edinburgh.Google Scholar
Moggi, E. (1991) Notions of computation and monads. Inform. Comput. 93, 55–92.CrossRefGoogle Scholar
Nipkow, T. (1991) Higher-order critical pairs. In Proceedings of 6th IEEE Symposium on Logic in Computer Science, pp. 342–349.CrossRefGoogle Scholar
Ohta, Y. & Hasegawa, M. (2006) A terminating and confluent linear lambda calculus. In Rewriting Techniques and Application (RTA’06). LNCS, vol. 1833, pp. 166–180.CrossRefGoogle Scholar
Peyton Jones, S. L., Tolmach, A. & Hoare, T. (2001) Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell Workshop 2001.Google Scholar
Pfenning, F. & Elliott, C. (1988) Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN’88 Symposium on Language Design and Implementation, pp. 199–208.CrossRefGoogle Scholar
Plotkin, G. & Power, J. (2002) Notions of computation determine monads. In Proceedings of FoSSaCS’02, pp. 342–356.CrossRefGoogle Scholar
Plotkin, G. D. (1975) Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125–159.CrossRefGoogle Scholar
Prehofer, C. (1995) Solving Higher-Order Equations From Logic to Programming. PhD Thesis, Technische Univerität München.Google Scholar
Sabry, A. & Wadler, P. (1997) A reflection on call-by-value. ACM Trans. Program. Lang. Syst. 19(6), 916–941.CrossRefGoogle Scholar
Sheard, T. & Jones, S. P. (2002) Template metaprogramming for Haskell. In Proceedings of the Haskell Workshop 2002.Google Scholar
Stark, I. (1996) A fully abstract domain model for the π-calculus. In Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pp. 36–42.CrossRefGoogle Scholar
Stark, I. (2008) Free-algebra models for the π-calculus. Theor. Comput. Sci. 390(2–3), 248–270.CrossRefGoogle Scholar
Staton, S. (2009) Two cotensors in one: presentations of algebraic theories for local state and fresh names. Electr. Notes Theor. Comput. Sci. 249, 471–490.CrossRefGoogle Scholar
Staton, S. (2013a) An algebraic presentation of predicate logic. In Proceedings of FoSSaCS’13. LNCS, vol. 7794, pp. 401–417.CrossRefGoogle Scholar
Staton, S. (2013b) Instances of computational effects: an algebraic perspective. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS, vol. 2013, p. 519.CrossRefGoogle Scholar
Staton, S. (2015) Algebraic effects, linearity, and quantum programming languages. In Proceedings of POPL’15, pp. 395–406.CrossRefGoogle Scholar
van de Pol, J. (1994) Termination proofs for higher-order rewrite systems. In the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA’93). LNCS, vol. 816, pp. 305–325.Google Scholar
Wadler, P. 1990 (June) Comprehending monads. In ACM Conference on Lisp and Functional Programming, pp. 61–78.Google Scholar
Yokoyama, T., Hu, Z. & Takeichi, M. (2003) Deterministic higher-order patterns for program transformation. In Logic Based Program Synthesis and Transformation, 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25–27, 2003, Revised Selected Papers, 128–142.Google Scholar
Yokoyama, T., Hu, Z. & Takeichi, M. (2004a) Deterministic second-order patterns. Inf. Process. Lett. 89(6), 309–314.CrossRefGoogle Scholar
Yokoyama, T., Hu, Z. & Takeichi, M. (2004b) Deterministic second-order patterns for program transformation. Comput. Soft. 21(5), 71–76. In Japanese.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.