Document Open Access Logo

The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Author Yohji Akama

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.6.pdf
  • Filesize: 0.49 MB
  • 19 pages

Document Identifiers

Author Details

Yohji Akama

Cite As Get BibTex

Yohji Akama. The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.6

Abstract

For the lambda-calculus with surjective pairing and terminal type, Curien and Di Cosmo, inspired by Knuth-Bendix completion, introduced a confluent rewriting system of the naive rewriting system. Their system is a confluent (CR) rewriting system stable under contexts. They left the strong normalization (SN) of their rewriting system open. By Girard's reducibility method with restricting reducibility theorem, we prove SN of their rewriting, and SN of the extensions by polymorphism and (terminal types caused by parametric polymorphism). We extend their system by sum types and eta-like reductions, and prove the SN. We compare their system to type-directed expansions.

Subject Classification

Keywords
  • reducibility method
  • restricted reducibility theorem
  • sum type
  • typedirected expansion
  • strong normalization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. A. Abel, T. Coquand, and P. Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. In P. Audebaud and C. Paulin-Mohring, editors, Proceedings of the 9th International Conference on Mathematics of Program Construction (MPC'08), pages 29-56, 2008. Google Scholar
  2. A. Abel, T. Coquand, and M. Pagano. A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Logical Meth. in Comput. Sci., 7(2:4):1-57, 2011. Google Scholar
  3. Y. Akama. On Mints' reductions for ccc-calculus. In M. Bezem and J. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculus and Applications, volume 664 of LNCS, pages 1-12. Springer-Verlag, 1993. Google Scholar
  4. V. Balat, R. Di Cosmo, and M. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In Proceedings of the 31st Symposium on Principles of Programming Languages (POPL 2004), pages 64-76. ACM Press, Jann 2004. Google Scholar
  5. A. Beckmann. Exact bounds for lengths of reductions in typed λ-calculus. J. Symb. Logic, 66(3):1277-1285, 2001. Google Scholar
  6. F. Blanqui. Computability closure: ten years later. In H. Common-Lundh, C. Kirchner, and H. Kirchner, editors, Rewriting, Computation and Proof, volume 4600 of LNCS, pages 68-88. Springer, 2007. Google Scholar
  7. F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive-data-type systems. Theoret. Comput. Sci., 272:41-68, 2002. Google Scholar
  8. D. Čubrić. On free ccc. Distributed on the types mailing list, 1992. Google Scholar
  9. P.-L. Curien and R. Di Cosmo. A confluent reduction system for the lambda-calculus with surjective pairing and terminal object. J. Funct. Programming, 6(2):299-327, 1996. A preliminary version appeared with the same authors and the same title in: J. Leach Albert, B. Monien, and M. Rodriguez Artalejo, editors, Proceedings of International Colloquium on Automata, Languages and Programming (ICALP), Vol. 510 of LNCS, pages 291-302. Springer-Verlag, 1991. Google Scholar
  10. R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Math. Structures Comput. Sci., 4:1-48, 1994. Google Scholar
  11. D. Dougherty and R. Subrahmanyam. Equality between functionals in the presence of coproducts. In Proceedings of the 10th Symposium on Logic in Computer Science, pages 282-291. IEEE Computer Society Press, 1995. Google Scholar
  12. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, 1989. Google Scholar
  13. H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994. Available as LFCS Report ECS-LFCS-94-304. Google Scholar
  14. H. Goguen. A syntactic approach to eta equality in type theory. In Proceedings of the 32nd Symposium on Principles of Programming Languages (POPL 2005), pages 75-84. ACM Press, Jan. 2005. Google Scholar
  15. M. Haigya. From programming-by-example to proving-by-example. In T. Ito and A. R. Meyer, editors, Proceedings of Theoretical Aspects of Computer Software, volume 526 of LNCS, pages 387-419. Springer-Verlag, 1991. Google Scholar
  16. R. Harper and F. Pfenning. On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log., 6(1):61-101, 2005. Google Scholar
  17. R. Hasegawa. Categorical data types in parametric polymorphism. Math. Structures Comput. Sci., 4(1):71-109, 1994. Google Scholar
  18. W. A. Howard. Assignment of ordinals to terms for primitive recursive functionals of finite type. In A. Kino, J. Myhill, and R. Vesley, editors, Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y., 1968), pages 443-458. North-Holland, Amsterdam, 1970. Google Scholar
  19. D. Ilik. The exp-log normal form of types: Decomposing extensional equality and representing terms compactly. In Proceedings of the 44th Symposium on Principles of Programming Languages (POPL 2017), pages 387-399. ACM Press, Jan. 2017. Google Scholar
  20. B. Jay and N. Ghani. The virtue of eta-expansion. J. Funct. Programming, 5(2):135-154, 1995. Google Scholar
  21. J.-P. Jouannaud and A. Rubio. Polymorphic higher-order recursive path orderings. J. ACM, 54(1):1-48, 2007. Google Scholar
  22. Z. Khasidashvili and V. van Oostrom. Context-sensitive conditional expression reduction systems. Electr. Notes Theor. Comput. Sci., 2:167-176, 1995. Google Scholar
  23. J. W. Klop. Combinatory reduction systems. Technical report, Mathematical center tracts, 1980. Google Scholar
  24. C. Kop. Higher Order Termination. PhD thesis, Vrije University, 2012. Google Scholar
  25. S. Lindley. Extensional rewriting with sums. In S. Ronchi Della Rocca, editor, Proceedings of the 8th International Conference on Typed Lambda Calculus and Applications, volume 664 of LNCS, pages 255-271. Springer, 2007. Google Scholar
  26. Z. Luo. Computation and Reasoning, volume 11 of International Series of Monographs on Computer Science. Oxford University Press, 1994. Google Scholar
  27. S. Mac Lane. Why commutative diagrams coincide with equivalent proofs. In Algebraists' Homage: Papers in Ring Theory and Related Topics (New Haven, Conn., 1981), volume 13, pages 387-401. Amer. Math. Soc., Providence, R.I., 1982. Google Scholar
  28. G. Mints. Closed categories, and proof theory. Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI), 68:83-114, 145, 1977. Google Scholar
  29. G. Mints. Teorija categorii i teoria dokazatelstv. I. In Aktualnye Problemy Logiki i Metodologii Nauky, pages 252-278. 1979. Google Scholar
  30. G. Mints. Proof theory and category theory. In Selected Papers in Proof Theory, pages 157-182. Bibliopolis, Naples; North-Holland Publishing Co., Amsterdam, 1992. Google Scholar
  31. G. Pottinger. The church rosser theorem for the typed lambda-calculus with surjective pairing. Notre Dame J. of Formal Logic, 22(3):264-268, 1981. Google Scholar
  32. S. Sarkar. Metatheory of LF extended with dependent pair and unit types. CMU-CS-05-179, School of Computer Science, Carnegie Mellon University, 2005. Google Scholar
  33. G. Scherer. Deciding equivalence with sums and the empty type. In Proceedings of the 44th Symposium on Principles of Programming Languages (POPL 2017), pages 374-386. ACM Press, Jan. 2017. Google Scholar
  34. K. Schütte. Proof Theory, volume 225 of Grundlehren der Mathematischen Wissenschaften. Springer-Verlag, Berlin-New York, 1977. Google Scholar
  35. Y. Toyama. On the church-rosser property of term rewriting systems. Technical report 17672, NTT ECL, Dec. 1981. In Japanese. Google Scholar
  36. V. van Oostrom. Developing developments. Theor. Comput. Sci., 175:159-181, 1997. Google Scholar
  37. V. van Oostrom and H. Zantema. Triangulation in rewriting. In A. Tiwari, editor, Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12), volume 15 of LIPIcs, pages 240-255. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: http://dx.doi.org/10.4230/LIPIcs.RTA.2012.240.
  38. H. Yokouchi. On Categorical Models of the Lambda Calculus. PhD thesis, Tokyo Institute of Technology, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact