کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422041 685008 2008 20 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Proofs as Polynomials
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Proofs as Polynomials
چکیده انگلیسی

Girard's Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut-elimination. In previous work we introduced a typed version of GoI, called Multiobject GoI (MGoI) for multiplicative linear logic [Haghverdi, E. and Scott, P.J. (2005), Towards a Typed Geometry of Interaction, CSL2005 (Computer Science Logic), Luke Ong, Ed. SLNCS 3634, 216–231]. This was later extended to cover the exponentials by the first author [Haghverdi, E. (2006), Typed GoI for Exponentials. in: M. Bugliesi et al. (Eds.): Proc. of ICALP 2006, Part II, LNCS 4052, 384–395. Springer Verlag]. Our development of MGoI depends on a new theory of partial traces, as well as an abstract notion of orthogonality (related to work of Hyland and Schalk.) In this paper we recall the MGoI semantics for MLL, and discuss how it relates to denotational semantics of MLL in certain *-autonomous categories. Finally, we prove characterization theorems for the MGoI interpretation of MLL in partially traced categories with an orthogonality, and for the original untyped GoI interpretation of MLL in a traced unique decomposition category.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 218, 22 October 2008, Pages 53-72