Кіріспе
Процесс калькулы
In theoretical computer science, the calculus (or pi calculus) is a process calculus. The calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation. The calculus has few terms and is a small, yet expressive language (see ). Functional programs can be encoded into the calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics. Extensions of the calculus, such as the spi calculus and applied , have been successful in reasoning about cryptographic protocols. Beside the original use in describing concurrent systems, the calculus has also been used to reason about business processes and molecular biology. (a precise definition is given in the following section):
concurrency, written , where and are two processes or threads executed concurrently. communication, where
input prefixing is a process waiting for a message that was sent on a communication channel named before proceeding as , binding the name received to the name Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation. output prefixing describes that the name is emitted on channel before proceeding as Typically, this models either sending a message on the network or a goto c operation. replication, written , which may be seen as a process which can always create a new copy of Typically, this models either a network service or a label c waiting for any number of goto c operations. creation of a new name, written , which may be seen as a process allocating a new constant x within The constants of are defined by their names only and are always communication channels. Creation of a new name in a process is also called restriction. the nil process, written , is a process whose execution is complete and has stopped. Although the minimalism of the calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first order functions, truth values, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public key cryptography. The applied due to Abadi and Fournet put these various extensions on a formal footing by extending the with arbitrary datatypes.
Теориялық компьютерлік ғылымда калькуль (немесе пи калькуль) – процесс калькулы. Калькуль арна атауларын арналардың өзі арқылы жіберуге мүмкіндік береді және осылайша есептеу кезінде желі конфигурациясы өзгеруі мүмкін бір мезгілдегі есептеулерді сипаттауға болады. Калькульдің терминдері аз, бірақ ол шағын, әрі экспрессивті тіл (қараңыз). Функционалдық бағдарламаларды калькульге кодтауға болады, ал кодтау есептеудің диалогтық табиғатына баса назар аударады, ойын семантикасымен байланыстар жасайды. Калькульдің кеңейтімдері, мысалы, спи калькуль және қолданбалы калькуль, криптографиялық протоколдарды талдауда сәтті қолданылды. Бір мезгілдегі жүйелерді сипаттаудағы бастапқы қолданылысынан басқа, калькуль бизнес-процестер мен молекулалық биологияны талдау үшін де қолданылған. (нақты анықтама келесі бөлімде берілген): бір мезгілде орындалатын екі процесс немесе жіп. Коммуникация, онда кіріс префиксі – бұл , деп аталатын коммуникациялық арнада жіберілген хабарламаны күтетін процесс, ал алынған атау атауға байланыстырылады. Әдетте, бұл желіден коммуникация күтетін процесс немесе "goto c" операциясымен бір рет қана қолданылатын "c" белгісін моделідейді. Шығарыс префиксі , бұл атаудың арна арқылы жіберілуін сипаттайды, содан кейін жүреді. Әдетте, бұл желіде хабарлама жіберуді немесе "goto c" операциясын моделідейді. Репликация, жазылуы , бұл әрқашан жаңа көшірмесін жасай алатын процесс ретінде қарастырылуы мүмкін. Әдетте, бұл желілік қызметті немесе кез келген сандағы "goto c" операцияларын күтетін "c" белгісін моделідейді. Жаңа атау құру, жазылуы , бұл x тұрақтысын бөлу процесі ретінде қарастырылуы мүмкін. -ның тұрақтылары тек олардың атауларымен анықталады және әрқашан коммуникациялық арналар болып табылады. Процесте жаңа атау жасау да шектеу деп аталады. Нөлдік процесс, жазылуы , – орындалуы аяқталған және тоқтаған процесс. Калькульдің минимализмі бізге бағдарламаларды дәстүрлі мағынада жазуға кедергі келтірсе де, калькульді кеңейту оңай. Атап айтқанда, рекурсия, циклдар және тізбекті композиция сияқты басқару құрылымдарын, сондай-ақ бірінші реттік функциялар, мәндік шамалар, тізімдер және бүтін сандар сияқты дерек типтерін анықтау оңай. Сонымен қатар, таратылымды немесе ашық кілттік криптографияны ескеретін калькульдің кеңейтімдері ұсынылды. Абади мен Фурнедің қолданған калькулі осы әртүрлі кеңейтімдерді еркін дерек типтерімен калькульді кеңейту арқылы формальды негізге қойды.
In theoretical computer science, the calculus (or pi calculus) is a process calculus. The calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation. The calculus has few terms and is a small, yet expressive language (see ). Functional programs can be encoded into the calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics. Extensions of the calculus, such as the spi calculus and applied , have been successful in reasoning about cryptographic protocols. Beside the original use in describing concurrent systems, the calculus has also been used to reason about business processes and molecular biology. (a precise definition is given in the following section):
concurrency, written , where and are two processes or threads executed concurrently. communication, where
input prefixing is a process waiting for a message that was sent on a communication channel named before proceeding as , binding the name received to the name Typically, this models either a process expecting a communication from the network or a label c usable only once by a goto c operation. output prefixing describes that the name is emitted on channel before proceeding as Typically, this models either sending a message on the network or a goto c operation. replication, written , which may be seen as a process which can always create a new copy of Typically, this models either a network service or a label c waiting for any number of goto c operations. creation of a new name, written , which may be seen as a process allocating a new constant x within The constants of are defined by their names only and are always communication channels. Creation of a new name in a process is also called restriction. the nil process, written , is a process whose execution is complete and has stopped. Although the minimalism of the calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first order functions, truth values, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public key cryptography. The applied due to Abadi and Fournet put these various extensions on a formal footing by extending the with arbitrary datatypes.
Кішкентай мысал
Төменде үш параллель компоненттен тұратын процестің шағын мысалы келтірілген. x арнасының аты тек алғашқы екі компонентке ғана белгілі. Алғашқы екі компонент x арнасы арқылы байланыса алады, ал y атауы z-ге байланыстырылады. Процестің келесі қадамы мынадай:
Қалған y-ға ешқандай әсер етпейді, себебі ол ішкі ауқымда анықталған. Екінші және үшінші параллель компоненттер енді z арнасының аты арқылы байланыса алады, ал v атауы x-ке байланыстырылады. Процестің келесі қадамы мынадай:
Жергілікті x атауы шығарылғандықтан, x ауқымы үшінші компонентті де қамтуға кеңейтіледі. Соңында, x арнасын x атауын жіберу үшін пайдалануға болады. Осыдан кейін бір мезгілде орындалатын барлық процестер тоқтатылады.
Тьюрингтің толықтығы
Калькуль – есептеудің әмбебап моделі. Бұл алғаш рет Милнер өзінің «Функциялар процестер ретінде» деген мақаласында атап өткен, онда ол сандар калькулесіндегі лямбда-калькулесінің екі кодтауын ұсынады. Бір кодтау құлшынысты (мәнді жіберу арқылы шақыру) бағалау стратегиясын, ал екінші кодтау қалыпты тәртіпті (атын беру арқылы шақыру) стратегиясын имитациялайды. Екеуінде де маңызды түсінік – ортаның байланыстарын модельдеу, мысалы, «x термине байланысты» – олардың байланыстары туралы сұранысқа жауап беретін көшірме агенттер ретінде, терминге қатынас жіберіп қайтарады. Осы кодтауларды мүмкін ететін калькульдің ерекшеліктері – атауларды беру және көшірме жасау (немесе, баламалы түрде, рекурсивті анықталған агенттер). Көшірме жасау/рекурсия болмаған жағдайда, калькуль Тьюринг толықтығынан қағылады. Бұл бисимуляция тепе-теңдігінің рекурсиясыз калькуль үшін және тіпті кез келген процестегі параллель компоненттер саны тұрақтымен шектелген шекті басқару калькулі үшін шешілетіндігінен көрінеді.
The features of the calculus that make these encodings possible are name passing and replication (or, equivalently, recursively defined agents). In the absence of replication/recursion, the calculus ceases to be Turing complete. This can be seen by the fact that bisimulation equivalence becomes decidable for the recursion free calculus and even for the finite control calculus where the number of parallel components in any process is bounded by a constant.
Калькульдегі екілік
Процесс калькуліне келетін болсақ, бұл калькуль бисимуляция тепе-теңдігінің анықтамасын беруге мүмкіндік береді. Калькульде бисимуляциялық тепе-теңдіктің (сондай-ақ бисимилярлық деп аталады) анықтамасы редукциялық семантикаға немесе таңбаланған өту семантикасына негізделуі мүмкін. Калькульде белгіленген бисимуляциялық тепе-теңдікті анықтаудың (кем дегенде) үш әртүрлі жолы бар: ерте, кеш және ашық бисимилярлық. Бұл калькульде мәндерді жіберу арқылы процестер жүзеге асырылатындығынан туындайды. Осы бөлімнің қалған бөлігінде біз процестерді және арқылы, ал процестердегі екілік қатынастарды арқылы белгілейміз.
Ашық екі ұқсастық
Бақытымызға орай, бұл мәселені шешетін үшінші анықтама бар, атап айтқанда, Сангиорги ұсынған ашық екіұқсастық. Процестердегі екілік қатынас ашық бисимуляция болып есептеледі, егер элементтердің кез келген жұбы үшін және кез келген атау алмастыруы мен кез келген әрекет үшін , егер онда, осындай болатын элемент табылуы керек, және . Егер жұпты қандай да бір ашық бисимуляция үшін жазуға болады деп айтылса, онда процестер ашық екіұқсас болады.
Processes and are said to be open bisimilar, written if the pair for some open bisimulation .
Ерте, кеш және ашық екі ұқсастық ерекшеленеді
Ерте, кеш және ашық екіұқсастық (бисимилярлық) өзгеше. Олардың кірігуі толық емес, сондықтан асинхронды π-есептеуі (пи-есептеуі) сияқты кейбір кіші есептеулерде кеш, ерте және ашық екіұқсастық бірдей болып келеді. Дегенмен, осы жағдайда асинхронды екіұқсастық түсінігі көбірек сәйкес келеді. Әдебиетте ашық екіұқсастық (бисимуляция) термині көбінесе күрделі түсінікке сілтеме жасайды, онда процестер мен қатынастар айырмашылық қатынастарымен индекстеледі; толық мәліметтер Сангиоргидің жоғарыда аталған мақаласында келтірілген.
In certain subcalculi such as the asynchronous pi calculus, late, early and open bisimilarity are known to coincide. However, in this setting a more appropriate notion is that of asynchronous bisimilarity. In the literature, the term open bisimulation usually refers to a more sophisticated notion, where processes and relations are indexed by distinction relations; details are in Sangiorgi's paper cited above.
Қолданбалар
Калькуль бір мезгілде жүретін жүйелердің әртүрлі түрлерін сипаттау үшін қолданылған. Шын мәнінде, кейбір соңғы қолданбалар дәстүрлі компьютерлік ғылымнан тысқары жатыр. 1997 жылы Мартин Абади мен Эндрю Гордон криптографиялық протоколдарды сипаттау және талдау үшін ресми белгі ретінде Spi calculus деп аталатын калькульдің кеңейтілген нұсқасын ұсынды. Spi calculus шифрлау және шифрды ашу үшін қарапайым элементтермен калькульді кеңейтеді. 2001 жылы Мартин Абади мен Седрик Фурне криптографиялық протоколдарды қолдануды жалпылап, қолданбалы калькульді жасады. Қазіргі уақытта қолданбалы калькульдің түрлеріне арналған көптеген жұмыстар бар, соның ішінде бірқатар тәжірибелік тексеру құралдары да бар. Бруно Бланшеттің ProVerif құралы – қолданбалы калькульді Бланшеттің логикалық бағдарламалау аясына аударуға негізделген мысал. Тағы бір мысал – Эндрю Гордон мен Алан Джеффридің Cryptyc құралы, ол Woo және Lam-ның сәйкестік туралы мәлімдемелер әдісін криптографиялық протоколдардың аутентификациялық қасиеттерін тексеруге болатын типтік жүйелердің негізі ретінде пайдаланады. 2002 жылға қарай Говард Смит пен Питер Фингар бизнес-процестерді модельдеу үшін калькульдің сипаттау құралына айналуына қызығушылық танытты. 2006 жылдың шілдесінде қауымдастықта бұл қаншалықты пайдалы болатыны талқыланды. Соңғы кезде калькуль Бизнес-процестерді модельдеу тілінің (BPML) және Microsoft-тың XLANG-інің теориялық негізін құрады. Калькуль молекулалық биологияда да қызығушылық тудырды. 1999 жылы Авив Регев пен Эхуд Шапиро жасушалық сигнализация жолын (РТК/МАПК каскады деп аталады) және әсіресе осы байланыс міндеттерін орындайтын молекулалық "легоны" калькульдің кеңейтілген нұсқасында сипаттауға болатынын көрсетті. Осы маңызды мақаладан кейін басқа авторлар минималды жасушаның толық метаболикалық желісін сипаттады. 2009 жылы Энтони Нэш пен Сара Калвала Dictyostelium discoideum агрегациясын басқаратын сигнал трандукциясын модельдеу үшін калькульдік аясты ұсынды.
Тарих
Калькульді 1992 жылы Робин Милнер, Жоахим Парроу және Дэвид Уокер Уффе Энгберг пен Могенс Нильсеннің идеялары негізінде жасаған. Ол Милнердің процесстік есептеуі CCS (Коммуникациялық жүйелердің есептеуі) жұмысының жалғасы болып табылады. Милнер өзінің Тьюринг лекциясында калькульдің дамуын акторлардағы мәндер мен процестердің біртектілігін қамтуға жасалған тытыну ретінде сипаттайды.