کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4662593 1633546 2007 54 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Weak typed Böhm theorem on IMLL
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
پیش نمایش صفحه اول مقاله
Weak typed Böhm theorem on IMLL
چکیده انگلیسی

In the Böhm theorem workshop on Crete, Zoran Petric called Statman’s “Typical Ambiguity theorem” the typed Böhm theorem. Moreover, he gave a new proof of the theorem based on set-theoretical models of the simply typed lambda calculus.In this paper, we study the linear version of the typed Böhm theorem on a fragment of Intuitionistic Linear Logic. We show that in the multiplicative fragment of intuitionistic linear logic without the multiplicative unit (for short IMLL) the weak typed Böhm theorem holds. The system IMLL exactly corresponds to the linear lambda calculus with multiplicative pairing. The system IMLL also exactly corresponds to the free symmetric monoidal closed category without the unit object. As far as we know, our separation result is the first one with regard to these systems in a purely syntactical manner.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 145, Issue 1, January 2007, Pages 37-90