Document Open Access Logo

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Authors Alejandro Díaz-Caro , Gilles Dowek

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.14.pdf
  • Filesize: 0.54 MB
  • 23 pages

Document Identifiers

Related Versions

  • A variant of the system presented in this paper, has been published in https://arxiv.org/abs/1303.7334v1 (LSFA 2012 [Alejandro Díaz-Caro and Gilles Dowek, 2013]), with a sketch of a subject reduction proof but no normalisation or consistency proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Type theory
  • Mathematics of computing → Lambda calculus
Keywords
  • Simply typed lambda calculus
  • Isomorphisms
  • Logic
  • Cut-elimination
  • Proof-reduction

Metrics

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

Abstract

We define a fragment of propositional logic where isomorphic propositions, such as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.

Cite As Get BibTex

Alejandro Díaz-Caro and Gilles Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.14

Author Details

Alejandro Díaz-Caro
  • Instituto de Ciencias de la Computación (CONICET-Universidad de Buenos Aires), Ciudad Autónoma de Buenos Aires, Argentina
  • Universidad Nacional de Quilmes, Bernal (Buenos Aires), Argentina
Gilles Dowek
  • Inria, LSV, ENS Paris-Saclay, France

Funding

Partially supported by ECOS-Sud A17C03, PICT 2015-1208, and the French-Argentinian laboratory SINFIN.

References

  1. Pablo Arrighi and Alejandro Díaz-Caro. A System F Accounting for Scalars. Logical Methods in Computer Science, 8(1:11), 2012. Google Scholar
  2. Pablo Arrighi, Alejandro Díaz-Caro, and Benoît Valiron. The Vectorial Lambda-Calculus. Information and Computation, 254(1):105-139, 2017. Google Scholar
  3. Pablo Arrighi and Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In Andrei Voronkov, editor, Proceedings of RTA 2008, volume 5117 of LNCS, pages 17-31, 2008. Google Scholar
  4. Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Logical Methods in Computer Science, 13(1:8), 2017. Google Scholar
  5. Gérard Boudol. Lambda-Calculi for (Strict) Parallel Functions. Information and Computation, 108(1):51-127, 1994. Google Scholar
  6. Kim B. Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231-247, 1992. Google Scholar
  7. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. A Relational Semantics for Parallelism and Non-Determinism in a Functional Setting. Annals of Pure and Applied Logic, 163(7):918-934, 2012. Google Scholar
  8. Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 76(2-3):95-120, 1988. Google Scholar
  9. Ugo de'Liguoro and Adolfo Piperno. Non Deterministic Extensions of Untyped λ-calculus. Information and Computation, 122(2):149-177, 1995. Google Scholar
  10. Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Adolfo Piperno. A filter model for concurrent λ-calculus. SIAM Journal on Computing, 27(5):1376-1419, 1998. Google Scholar
  11. Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. Google Scholar
  12. Roberto Di Cosmo. A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 15(5):825-838, 2005. Google Scholar
  13. Alejandro Díaz-Caro and Gilles Dowek. Non determinism through type isomorphism. In Delia Kesner and Petrucio Viana, editors, Proceedings of LSFA 2012, volume 113 of EPTCS, pages 137-144, 2013. Google Scholar
  14. Alejandro Díaz-Caro and Gilles Dowek. Typing quantum superpositions and measurement. In Carlos Martín-Vide, Roman Neruda, and Miguel A. Vega-Rodríguez, editors, Proceedings of TPNC 2017, volume 10687 of LNCS, pages 281-293, 2017. Google Scholar
  15. Alejandro Díaz-Caro and Pablo E. Martínez López. Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of λ^+. In Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, IFL '15, pages 9:1-9:11. ACM, 2015. Google Scholar
  16. Alejandro Díaz-Caro and Barbara Petit. Linearity in the non-deterministic call-by-value setting. In Luke Ong and Ruy de Queiroz, editors, Proceedings of WoLLIC 2012, volume 7456 of LNCS, pages 216-231, 2012. Google Scholar
  17. Gilles Dowek, Thérèse Hardin, and Claude Kirchner. Theorem proving modulo. Journal of Automated Reasoning, 31(1):33-72, 2003. Google Scholar
  18. Gilles Dowek and Ying Jiang. On the expressive power of schemes. Information and Computation, 209:1231-1245, 2011. Google Scholar
  19. Gilles Dowek and Benjamin Werner. Proof normalization modulo. The Journal of Symbolic Logic, 68(4):1289-1316, 2003. Google Scholar
  20. Jacques Garrigue and Hassan Aït-Kaci. The typed polymorphic label-selective λ-calculus. In Proceedings of POPL 1994, ACM SIGPLAN, pages 35-47, 1994. Google Scholar
  21. Herman Geuvers, Robbert Krebbers, James McKinna, and Freek Wiedijk. Pure Type Systems without Explicit Contexts. In Karl Crary and Marino Miculan, editors, Proceedings of LFMTP 2010, volume 34 of EPTCS, pages 53-67, 2010. Google Scholar
  22. Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Cambridge University Press, 1989. Google Scholar
  23. Per Martin-Löf. Intuitionistic type theory. Studies in proof theory. Bibliopolis, 1984. Google Scholar
  24. Michele Pagani and Simona Ronchi Della Rocca. Linearity, non-determinism and solvability. Fundamental Informaticae, 103(1-4):173-202, 2010. Google Scholar
  25. Jonghyun Park, Jeongbong Seo, Sungwoo Park, and Gyesik Lee. Mechanizing Metatheory without Typing Contexts. Journal of Automated Reasoning, 52(2):215-239, 2014. Google Scholar
  26. Mikael Rittri. Retrieving library identifiers via equational matching of types. In Proceedings of CADE 1990, volume 449 of LNCS, pages 603-617, 1990. Google Scholar
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013. Google Scholar
  28. Lionel Vaux. The algebraic lambda calculus. Mathematical Structures in Computer Science, 19(5):1029-1059, 2009. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact