乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T10:11:25Z","timestamp":1672395085270},"reference-count":46,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,10]]},"abstract":"It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models calledclassical categories<\/jats:italic>that is sound and complete and avoids this collapse by interpreting cut reduction by a poset enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatisation of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models calledDummett categories<\/jats:italic>. Examples of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category.<\/jats:p>Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.<\/jats:p>","DOI":"10.1017\/s0960129507006287","type":"journal-article","created":{"date-parts":[[2007,9,21]],"date-time":"2007-09-21T11:03:12Z","timestamp":1190372592000},"page":"957-1027","source":"Crossref","is-referenced-by-count":3,"title":["On categorical models of classical logic and the Geometry of Interaction"],"prefix":"10.1017","volume":"17","author":[{"given":"CARSTEN","family":"F\u00dcHRMANN","sequence":"first","affiliation":[]},{"given":"DAVID","family":"PYM","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,10,1]]},"reference":[{"key":"S0960129507006287_ref46","doi-asserted-by":"crossref","unstructured":"Wadler P. (2003) Call-by-value is dual to call-by-name. In: Proc. International Conference on Functional Programming. ACM SIGPLAN Notices 38 (9) 189\u2013201.","DOI":"10.1145\/944705.944723"},{"key":"S0960129507006287_ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"S0960129507006287_ref42","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/13.5.777"},{"key":"S0960129507006287_ref40","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"Prawitz","year":"1965"},{"key":"S0960129507006287_ref39","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0960129507006287_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"S0960129507006287_ref37","unstructured":"Ong C.-H. L. (1996) A semantic view of classical proofs. In: Proc. LICS 96, IEEE Computer Society Press, 230\u2013241."},{"key":"S0960129507006287_ref36","unstructured":"McKinley R. (2006) Categorical models of first-order classical proofs, Ph.D. thesis, University of Bath."},{"key":"S0960129507006287_ref35","unstructured":"Loader R. (1994) Models of Lambda Calculi and Linear Logic: Structural, Equational and Proof-theoretic Characterisations, Ph.D. thesis, St. Hugh's College, Oxford."},{"key":"S0960129507006287_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(80)90101-2"},{"key":"S0960129507006287_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00241-9"},{"key":"S0960129507006287_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00075-6"},{"key":"S0960129507006287_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_2"},{"key":"S0960129507006287_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(99)00180-2"},{"key":"S0960129507006287_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.10.028"},{"key":"S0960129507006287_ref6","unstructured":"Bellin G. , Hyland J. , Robinson E. and Urban C. (2004) Proof theory of classical propositional calculus (submitted)."},{"key":"S0960129507006287_ref16","volume-title":"Proof-theoretical coherence","author":"Dosen","year":"2004"},{"key":"S0960129507006287_ref13","doi-asserted-by":"crossref","unstructured":"Curien P.-L. and Herbelin H. (2000) The duality of computation. In: Proc. International Conference on Functional Programming, Montreal, IEEE.","DOI":"10.1145\/351240.351262"},{"key":"S0960129507006287_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1207-1"},{"key":"S0960129507006287_ref17","volume-title":"Elements of Intuitionism","author":"Dummett","year":"1977"},{"key":"S0960129507006287_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/BF01622878"},{"key":"S0960129507006287_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"S0960129507006287_ref44","unstructured":"Tan A. (1997) Full completeness for models of linear logic, Ph.D. thesis, University of Cambridge."},{"key":"S0960129507006287_ref34","doi-asserted-by":"crossref","unstructured":"Lamarche F. and Stra\u00dfburger L. (2004) Naming proofs in propositional classical logic (submitted).","DOI":"10.1007\/11417170_19"},{"key":"S0960129507006287_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"S0960129507006287_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(98)00110-8"},{"key":"S0960129507006287_ref45","volume-title":"Basic Proof Theory","author":"Troelstra","year":"1996"},{"key":"S0960129507006287_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129507006287_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_49"},{"key":"S0960129507006287_ref25","first-page":"329","article-title":"Geometry of interaction III: Accommodating the additives. In: Advances in Linear Logic (Ithaca, NY, 1993)","volume":"222","author":"Girard","year":"1995","journal-title":"London Math. Soc. Lecture Note Ser."},{"key":"S0960129507006287_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"S0960129507006287_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61604-7_44"},{"key":"S0960129507006287_ref3","first-page":"53","article-title":"New foundations for the geometry of interaction","volume":"111","author":"Abramsky","year":"1994","journal-title":"J. Pure Applied Algebra"},{"key":"S0960129507006287_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(95)00159-X"},{"key":"S0960129507006287_ref4","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0025"},{"key":"S0960129507006287_ref5","volume-title":"Logic for Concurrency and Synchronisation","author":"Bellin","year":"2003"},{"key":"S0960129507006287_ref9","first-page":"15","article-title":"Morphisms and modules for poly-bicategories","volume":"11","author":"Cockett","year":"2003","journal-title":"Theory and Applications of Categories"},{"key":"S0960129507006287_ref10","first-page":"85","article-title":"Proof Theory for Full Intuitionistic Linear Logic, and MIX Categories","volume":"3","author":"Cockett","year":"1997","journal-title":"Theory and Applications of Categories"},{"key":"S0960129507006287_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(00)00161-4"},{"key":"S0960129507006287_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(95)00160-3"},{"key":"S0960129507006287_ref18","unstructured":"Filinski A. (1989) Declarative continuations and categorical duality, Master's thesis, Computer Science Department, University of Copenhagen, DIKU Report 89\/11."},{"key":"S0960129507006287_ref19","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319615"},{"key":"S0960129507006287_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2005.03.016"},{"key":"S0960129507006287_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"S0960129507006287_ref26","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0960129507006287_ref28","doi-asserted-by":"crossref","unstructured":"Hasegawa M. (2002) Classical linear logic of implications. In: Proc. 11th Annual Conference of the European Association for Computer Science Logic (CSL'02), Edinburgh. Springer-Verlag Lecture Notes in Computer Science 2471.","DOI":"10.1007\/3-540-45793-3_31"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006287","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T02:32:36Z","timestamp":1556850756000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006287\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":46,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["S0960129507006287"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006287","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10]]}}}