A fibrational framework for substructural and modal logics. (English) Zbl 1434.03040
Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 25, 22 p. (2017).
Summary: We define a general framework that abstracts the common features of many intuitionistic substructural and modal logics/type theories. The framework is a sequent calculus/normal-form type theory parametrized by a mode theory, which is used to describe the structure of contexts and the structural properties they obey. In this sequent calculus, the context itself obeys standard structural properties, while a term, drawn from the mode theory, constrains how the context can be used. Product types, implications, and modalities are defined as instances of two general connectives, one positive and one negative, that manipulate these terms. Specific mode theories can express a range of substructural and modal connectives, including non-associative, ordered, linear, affine, relevant, and cartesian products and implications; monoidal and non-monoidal functors, (co)monads and adjunctions; \(n\)-linear variables; and bunched implications. We prove cut (and identity) admissibility independently of the mode theory, obtaining it for many different logics at once. Further, we give a general equational theory on derivations/terms that, in addition to the usual \(\beta\eta\)-rules, characterizes when two derivations differ only by the placement of structural rules. Additionally, we give an equivalent semantic presentation of these ideas, in which a mode theory corresponds to a 2-dimensional cartesian multicategory, the framework corresponds to another such multicategory with a functor to the mode theory, and the logical connectives make this into a bifibration. Finally, we show how the framework can be used both to encode existing existing logics/type theories and to design new ones.
For the entire collection see [Zbl 1372.68017].
For the entire collection see [Zbl 1372.68017].
MSC:
| 03B38 | Type theory |
| 03B45 | Modal logic (including the logic of norms) |
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
| 03F05 | Cut-elimination and normal-form theorems |
| 03G30 | Categorical logic, topoi |
References:
| [1] | Andreas Abel. The next 700 modal type assignment systems. In {\it International Conference} {\it on Types for Proofs and Programs (TYPES)}, 2015. |
| [2] | Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient in ductive types. In {\it ACM SIGPLAN-SIGACT Symposium on Principles of Programming} {\it Languages}, 2016. · Zbl 1347.68045 |
| [3] | Robert Atkey. A {\it λ}-calculus for resource separation. In {\it Automata, Languages and Pro-} {\it gramming: 31st International Colloquium, ICALP 2004}, volume 3142 of {\it Lecture Notes in} {\it Computer Science}, pages 158-170. Springer, 2004. · Zbl 1098.68023 |
| [4] | Nuel D. Belnap Jr. Display logic. {\it Journal of Philosophical Logic}, 11:375-417, 1982. · Zbl 0509.03008 |
| [5] | Nick Benton. A mixed linear and non-linear logic: Proofs, terms and models. In {\it Computer} {\it Science Logic}, volume 933 of {\it LNCS}. Springer-Verlag, 1995. · Zbl 1044.03543 |
| [6] | Nick Benton and Philip Wadler. Linear logic, monads and the lambda calculus. In {\it IEEE} {\it Symposium on Logic in Computer Science}. IEEE Computer Society Press, 1996. |
| [7] | G. Bierman and V.C.V. de Paiva. On an intuitionistic modal logic. {\it Studia Logica}, 65:383- 416, 2000. · Zbl 0963.03033 |
| [8] | Iliano Cervesato and Frank Pfenning. A linear logical framework. {\it Information and Com-} {\it putation}, 179(1):19-75, 2002. · Zbl 1031.03056 |
| [9] | Karl Crary. Higher-order representation of substructural logics. In {\it ACM SIGPLAN Inter-} {\it national Conference on Functional Programming}, pages 131-142. ACM, 2010. · Zbl 1323.68461 |
| [10] | Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In {\it Kurt Godel Colloquium}, LNCS, pages 159-171. Springer, 1993. · Zbl 0793.03061 |
| [11] | Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, and Tim Rev ell. Bifibrational functorial semantics for parametric polymorphism. In {\it Proceedings of} {\it Mathematical Foundations of Program Semantics}, 2015. |
| [12] | Claudio Hermida. Fibrations for abstract multicategories. Fields Institute Communications; available from http://sqig.math.ist.utl.pt/pub/HermidaC/fib-mul.pdf, 2002. · Zbl 1067.18007 |
| [13] | Fritz Hörmann. Fibered multiderivators and (co)homological descent. Available from http: //arxiv.org/abs/1505.00974, 2015. · Zbl 1380.55017 |
| [14] | Joachim Lambek. The mathematics of sentence structure. {\it The American Mathematical} {\it Monthly}, 65:154-170, 1958. · Zbl 0080.00702 |
| [15] | Daniel R. Licata and Michael Shulman. Adjoint logic with a 2-category of modes. In {\it Logical} {\it Foundations of Computer Science}, 2016. · Zbl 1477.03267 |
| [16] | Daniel R. Licata, Michael Shulman, and Mitchell Riley.A fibrational framework for substructural and modal logics (extended version). Available from http://dlicata.web. wesleyan.edu/, 2017. · Zbl 1434.03040 |
| [17] | Conor McBride. I got plenty o’ nuttin’. {\it A List of Successes That Can Change the World:} {\it Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday}, pages 207-233, 2016. · Zbl 1343.68060 |
| [18] | Paul-André Meliès and Noam Zeilberger. Functors are type refinement systems. In {\it ACM} {\it SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, 2015. · Zbl 1345.68112 |
| [19] | Paul-André Meliès and Noam Zeilberger.A bifibrational reconstruction of lawvere’s presheaf hyperdoctrine. In {\it IEEE Symposium on Logic in Computer Science}, 2016. · Zbl 1395.03040 |
| [20] | Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponen tials. In {\it Principles and Practice of Declarative Programming}, 2009. |
| [21] | Peter W. O’Hearn and David J. Pym. The logic of bunched implications. {\it Bulletin of} {\it Symbolic Logic}, 5(2):215-244, 1999. · Zbl 0930.03095 |
| [22] | Frank Pfenning. A structural proof of cut elimination and its representation in a logical framework. Technical Report CMU-CS-94-218, Department of Computer Science, Carnegie Mellon University, 1994. |
| [23] | Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. {\it Mathe-} {\it matical Structures in Computer Science}, 11:511-540, 2001. · Zbl 0997.03020 |
| [24] | Jason Reed. Names are (mostly) useless: Encoding nominal logic programming techniques with use-counting and dependent types.Talk at Working on Mechanizing Metatheory (WMM), 2008. |
| [25] | Jason Reed. {\it A Hybrid Logical Framework}. PhD thesis, Carnegie Mellon University, 2009. · Zbl 1278.03049 |
| [26] | :19 |
| [27] | :20 |
| [28] | :21 that {\it π}({\it e}) = {\it β }and {\it e}[FR∗{\it /x}0] ≡ {\it d}. We take as our {\it e }the derivation split ∆ = {\it x}0 in {\it d}. This lies over {\it β}, and we calculate {\it e}[FR∗{\it /x}0] = (split ∆ = {\it x}0 in {\it d})[1{\it α}∗({\it x/x}){\it /x}0] ≡ (1{\it β}[1{\it α}{\it /x}0])∗({\it d}[ {\it }{\it x/x}]) ≡ (1{\it β}[{\it α/x}0])∗({\it d}) ≡ {\it d} by the {\it β}-law for F and unit laws. It remains to show uniqueness. Suppose we have some derivation {\it e}0 such that {\it π}({\it e}0) = {\it β }and {\it e}0[FR∗{\it /x}0] ≡ {\it d}. By the {\it η}-law for F, we have {\it e}0≡ split ∆ = {\it x}0 in {\it e}0[FR∗{\it /x}0] ≡ split ∆ = {\it x}0 in {\it d }= {\it e} as required. We now turn to the pullback property for morphisms. Let {\it β, β}0∈ M({\it π}Γ{\it , q, π}Γ0; {\it πC}) and let {\it s }:: {\it β }⇒ {\it β}0 be a morphism. Further suppose that we have derivations {\it d }:: Γ{\it , }∆{\it , }Γ0‘{\it β}[{\it α/x} 0] {\it C }and {\it d}0:: Γ{\it , }∆{\it , }Γ0‘{\it β}0[{\it α/x}0]{\it C }such that ({\it s}[1{\it α}{\it /x}0])∗({\it d}0) ≡ {\it d}. This describes a morphism {\it T }: {\it d }⇒ {\it d}0 in D(Γ{\it , }F{\it α}(∆){\it , }Γ0; {\it C}) that lies over {\it s}[1{\it α}{\it /x}0]. This latter transformation is the result of applying the functor −[{\it α/x}0] to {\it s}. We now must find a morphism {\it S }in D(Γ{\it , }∆{\it , }Γ0; {\it C}) that lies over {\it s}, and such that the ∗ functor −[FR{\it /x}0] applied to the morphism {\it S }yields {\it T }. We know that for {\it S }to lie over {\it s}, its underlying structural transformation must be {\it s}. The action of −[FR∗{\it /x}0] on {\it S }then takes {\it s} to {\it s}[1{\it α}{\it /x}0] as expected. By the previous argument for objects, we know that {\it S }must have domain split ∆ = {\it x}0 in {\it d} and codomain split ∆ = {\it x}0 in {\it d}0. We can verify that choosing the underlying transformation {\it s }gives a well-defined 2-morphism {\it S }: (split ∆ = {\it x}0 in {\it d}) ⇒ (split ∆ = {\it x}0 in {\it d}0): {\it s}∗(split ∆ = {\it x}0 in {\it d}0) ≡ split ∆ = {\it x}0 in {\it s}∗(split ∆ = {\it x}0 in {\it d}0)[FR∗{\it /x}0] ≡ split ∆ = {\it x}0 in {\it s}∗(split ∆ = {\it x}0 in {\it d}0)[(1{\it α})∗(FR∗){\it /x}0] ≡ split ∆ = {\it x}0 in ({\it s}[1{\it α}{\it /x}0])∗(split ∆ = {\it x}0 in {\it d}0[FR∗{\it /x}0]) ≡ split ∆ = {\it x}0 in ({\it s}[1{\it α}{\it /x}0])∗({\it d}0) ≡ split ∆ = {\it x}0 in {\it d} where we have used the {\it η}-law followed by the {\it β}-law. We conclude that all squares of the given form are pullback squares, and so every {\it α }has an opcartesian lift. Therefore {\it π }is an opfibration. The proof that {\it π }is also a fibration is very similar, using U types instead of F types.J |
| [29] | :18 |
| [30] | :22 |
| [31] | Jason Reed. A judgemental deconstruction of modal logic. Available from www.cs.cmu. edu/ jcreed/papers/jdml.pdf, 2009. |
| [32] | Jason Reed and Frank Pfenning.A constructive approach to the resource seman tics of substructural logics.Available from http://www.cs.cmu.edu/ jcreed/papers/ rp-substruct.pdf, 2009. |
| [33] | Greg Restall. {\it An introduction to substructural logics}. Routledge, 2000. · Zbl 1028.03018 |
| [34] | Urs Schreiber. Differential cohomology in a cohesive infinity-topos. {\it arXiv}, 2013. arXiv: 1310.7930. |
| [35] | Urs Schreiber and Michael Shulman. Quantum gauge field theory in cohesive homotopy type theory. In {\it Workshop on Quantum Physics and Logic}, 2012. · Zbl 1464.81043 |
| [36] | Michael Shulman. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. arXiv:1509.07584, 2015. · Zbl 1390.03014 |
| [37] | Univalent Foundations Program. {\it Homotopy Type Theory: Univalent Foundations Of Math-} {\it ematics}. Available from homotopytypetheory.org/book, 2013. · Zbl 1298.03002 |
| [38] | Vladimir Voevodsky. A very short note on homotopy {\it λ}-calculus. http://www.math.ias. edu/vladimir/files/2006_09_Hlambda.pdf, September 2006. |
| [39] | Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. · Zbl 1100.68548 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
