Makoto Hamana
Skip Abstract Section
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 SOL, 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 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 lambda-calculi, Plotkin and Power's theory of states, and Stark's theory of pi-calculus.
- F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
Cross Ref
- L. Baxter. The complexity of unification. PhD thesis, Department of Computer Science, University of Waterloo, 1977.Google Scholar
- N. Benton and M. Hyland. Traced premonoidal categories. Theoretical Informatics and Applications, 37(4):273–299, 2003. Google ScholarCross Ref
- P. N. Benton, Gavin M. Bierman, and Valeria de Paiva. Computational types from a logical perspective. J. Funct. Program., 8 (2):177–193, 1998. Google ScholarDigital Library
- R. Bird and O. D. Moor. Algebra of Programming. Prentice-Hall, 1996. Google ScholarCross Ref
- F. Blanqui. Termination and confluence of higher-order rewrite systems. In Rewriting Techniques and Application (RTA 2000), LNCS 1833, pages 47–61. Springer, 2000. Google ScholarCross Ref
- F. Blanqui. Termination of rewrite relations on λ-terms based on Girard’s notion of reducibility. Theor. Comput. Sci., 611: 50–86, 2016. Google ScholarDigital Library
- M. M. T. Chakravarty, G. Keller, and S. L. Peyton Jones. Associated type synonyms. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, pages 241–253, 2005a. Google ScholarDigital Library
- M. M. T. Chakravarty, G. Keller, S. L. Peyton Jones, and S. Marlow. Associated types with class. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 1–13, 2005b. Google ScholarDigital Library
- T. Coquand. Pattern matching with dependent types. In Proc. of the 3rd Work. on Types for Proofs and Programs, 1992.Google Scholar
- M. Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proc. of PPDP’02, pages 26–37. ACM Press, 2002. Google ScholarDigital Library
- M. Fiore. Second-order and dependently-sorted abstract syntax. In Proc. of LICS’08, pages 57–68, 2008. Google ScholarDigital Library
- M. Fiore and M. Hamana. Multiversal polymorphic algebraic theories: Syntax, semantics, translations, and equational logic. In Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, pages 520–529, 2013. Google ScholarDigital Library
- M. Fiore and C.-K. Hur. Second-order equational logic. In Proc. of CSL’10, LNCS 6247, pages 320–335, 2010.Google Scholar
- M. Fiore and O. Mahmoud. Second-order algebraic theories. In Proc. of MFCS’10, LNCS 6281, pages 368–380, 2010. Google ScholarCross Ref
- M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. of LICS’99, pages 193–202, 1999. Google ScholarCross Ref
- M.P. Fiore, E. Moggi, and D. Sangiorgi. A fully-abstract model for the pi-calculus. In 11th Logic in Computer Science Conf. (LICS’96), pages 43–54. IEEE, 1996. Information and Computation 179, 76-117 (2002). Google ScholarDigital Library
- J. Gibbons and R. Hinze. 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, pages 2–14, 2011. Google ScholarDigital Library
- J.-Y. Girard. Proofs and types. Cambridge University Press, 1989. translated and with appendices by Paul Taylor, Yves Lafont.Google ScholarDigital Library
- M. Hamana. Free Σ-monoids: A higher-order syntax with metavariables. In Asian Symposium on Programming Languages and Systems (APLAS’04), LNCS 3302, pages 348–363, 2004.Google ScholarCross Ref
- M. Hamana. Universal algebra for termination of higher-order rewriting. In Rewriting Techniques and Application (RTA’05), LNCS 3467, pages 135–149, 2005. Google ScholarDigital Library
- M. Hamana. Higher-order semantic labelling for inductive datatype systems. In Proc. of 9th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’07), pages 97–108. ACM Press, 2007. Google ScholarDigital Library
- M. Hamana. Semantic labelling for proving termination of combinatory reduction systems. In Functional and (Constraint) Logic Programming (WFLP’09), LNCS 5979, pages 62–78, 2010. Google ScholarDigital Library
- M. Hamana. Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories. In Proc. of FSCD’16, volume 52 of the Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1–21:18, 2016.Google Scholar
- M. Hasegawa. Classical linear logic of implications. Mathematical Structures in Computer Science, 15(2):323–342, 2005. Google ScholarDigital Library
- G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of ACM, 27(4): 797–821, 1980. Google ScholarDigital Library
- G. P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27–57, 1975. Google ScholarCross Ref
- J. Jouannaud, H. Kirchner, and J. Remy. Church-Rosser properties of weakly terminating term rewriting systems. In Proceedings of the 8th International Joint Conference on Artificial Intelligence, pages 909–915, 1983.Google Scholar
- D. Knuth and P. Bendix. Simple word problems in universal algebras. In Computational Problem in abstract algebra, pages 263–297. Pergamon Press, Oxford, 1970. included also in Automationof reasoning 2, Springer (1983), pp.342-376. Google ScholarCross Ref
- T. Libal and D. Miller. Functions-as-Constructors Higher-Order Unification. In Proc. of FSCD 2016, volume 52 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:17, 2016.Google Scholar
- S. Lindley and I. Stark. Reducibility and ⊤⊤-lifting for computation types. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, pages 262–277, 2005.Google Scholar
- R. Mayr and T. Nipkow. Higher-order rewrite systems and their confluence. Theor. Comput. Sci., 192(1):3–29, 1998. Google ScholarDigital Library
- P.-A. Melliès. 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, United Kingdom, pages 150–159, 2010. Google ScholarDigital Library
- D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497–536, 1991. Google ScholarCross Ref
- R. Milner. Semantic ideas in computing. In Computing tomorrow. Cambridge University Press, 1996. Google ScholarCross Ref
- R. Milner. Communicating and mobile systems - the π -calculus. CUP, 1999.Google Scholar
- E. Moggi. Computational lambda-calculus and monads. LFCS ECS-LFCS-88-66, University of Edinburgh, 1988.Google Scholar
- E. Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991. Google ScholarDigital Library
- T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342–349, 1991. Google ScholarCross Ref
- Y. Ohta and M. Hasegawa. A terminating and confluent linear lambda calculus. In Rewriting Techniques and Application (RTA’06), LNCS 1833, pages 166–180, 2006. Google ScholarDigital Library
- S. L. Peyton Jones, A. Tolmach, and T. Hoare. Playing by the rules: rewriting as a practical optimisation technique in GHC. In Haskell Workshop 2001, 2001.Google Scholar
- F. Pfenning and C. Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN ’88 Symposium on Language Design and Implementation, pages 199–208, 1988. Google ScholarDigital Library
- G. Plotkin and J. Power. Notions of computation determine monads. In Proc. of FoSSaCS’02, pages 342–356, 2002. Google ScholarCross Ref
- G. D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125–159, 1975. Google ScholarCross Ref
- J. van de Pol. Termination proofs for higher-order rewrite systems. In the First International Workshop on Higher-Order Algebra, Logic and Term Rewriting (HOA’93), LNCS 816, pages 305–325, 1994.Google Scholar
- D. Prawitz. Ideas and results in proof theory. In Proceedings of the 2nd Scandinavian Logic Symposium, number 63 in Studies in Logics and the Foundations of Mathmatics, pages 235–307, 1971. Google ScholarCross Ref
- C. Prehofer. Solving Higher-Order Equations: From Logic to Programming. PhD thesis, Technische Univerität München, 1995.Google Scholar
- A. Sabry and P. Wadler. A reflection on call-by-value. ACM Trans. Program. Lang. Syst., 19(6):916–941, 1997. Google ScholarDigital Library
- I. Stark. A fully abstract domain model for the π -calculus. In Proc. of the Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 36–42, 1996. Google ScholarCross Ref
- I. Stark. Free-algebra models for the π -calculus. Theor. Comput. Sci., 390(2-3):248–270, 2008. Google ScholarDigital Library
- S. Staton. Two cotensors in one: Presentations of algebraic theories for local state and fresh names. Electr. Notes Theor. Comput. Sci., 249:471–490, 2009. Google ScholarDigital Library
- S. Staton. An algebraic presentation of predicate logic. In Proc. of FoSSaCS’13, LNCS 7794, pages 401–417, 2013a. Google ScholarDigital Library
- S. Staton. Instances of computational effects: An algebraic perspective. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, page 519, 2013b.Google ScholarCross Ref
- S. Staton. Algebraic effects, linearity, and quantum programming languages. In Proc. of POPL’15, pages 395–406, 2015. Google ScholarDigital Library
- P. Wadler. Comprehending monads. In ACM Conference on Lisp and Functional Programming, pages 61–78, Nice, France, June 1990. Google ScholarDigital Library
- T. Yokoyama, Z. Hu, and M. Takeichi. 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, pages 128–142, 2003.Google Scholar
- T. Yokoyama, Z. Hu, and M. Takeichi. Deterministic second-order patterns. Inf. Process. Lett., 89(6):309–314, 2004a. Google ScholarDigital Library
- T. Yokoyama, Z. Hu, and M. Takeichi. Deterministic second-order patterns for program transformation. Computer Software, 21(5):71–76, 2004b. in Japanese.Google Scholar
Index Terms
- How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation
Recommendations
Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus
PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative ProgrammingWe observe that normalization by evaluation for simply-typed lambda-calculus with weak coproducts can be carried out in a weak bi-cartesian closed category of presheaves equipped with a monad that allows us to perform case distinction on neutral terms ...
Intuitionistic differential nets and lambda-calculus
We define pure intuitionistic differential proof nets, extending Ehrhard and Regnier s differential interaction nets with the exponential box of Linear Logic. Normalization of the exponential reduction and confluence of the full one is proved. These ...
Second-order algebraic theories
MFCS'10: Proceedings of the 35th international conference on Mathematical foundations of computer scienceFiore and Hur [10] recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a formal ...
Comments