کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
4952070 1442004 2017 19 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
On concurrent behaviors and focusing in linear logic
ترجمه فارسی عنوان
در رفتارهای همزمان و تمرکز در منطق خطی
کلمات کلیدی
منطق خطی، برنامه ریزی محدودیت همزمان سیستم های اثبات شده، تمرکز چند فوکوس نقاط ثابت،
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Concurrent Constraint Programming (CCP) is a simple and powerful model of concurrency where processes interact by telling and asking constraints into a global store of partial information. Since its inception, CCP has been endowed with declarative semantics where processes are interpreted as formulas in a given logic. This allows for the use of logical machinery to reason about the behavior of programs and to prove properties of them. Nevertheless, the logical characterization of CCP programs exhibits normally a weak level of adequacy since proofs in the logical system may not correspond directly to traces of the program. In this paper, we study different encodings from CCP into intuitionistic linear logic (ILL) and we compare the level of adequacy attained in each. By relying on a focusing discipline, we show that it is possible to give a logical characterization to CCP with the highest level of adequacy. Moreover, we show how to characterize maximal-parallelism semantics for CCP by relying on a multi-focusing discipline for ILL. These results, besides giving proof techniques for CCP, entail (safe) optimizations for the execution of CCP programs. Finally, we show how to interpret CCP procedure calls as fixed points in ILL, thus opening the possibility of reasoning by induction about properties of CCP programs.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 685, 15 July 2017, Pages 46-64
نویسندگان
, ,