WWW.KNIGA.SELUK.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА - Книги, пособия, учебники, издания, публикации

 

Московский Государственный Университет им. М. В. Ломоносова

Механико-математический факультет

Кафедра математической логики и теории алгоритмов

Харитонов Александр Валентинович

Линейная логика

Реферат по истории математики

(по работе Roberto Di Cosmo, Dale Miller, Linear Logic)

Москва

2010 год

1 Введение

Линейная логика представляет собой уточнение классической и интуиционистской логик. Вместо того, чтобы фокусироваться на истинности, как классическая логика, или на доказуемости, как интуиционизм, линейная логика акцентирует внимание на том, что формулы можно интерпретировать как ресурсы. Чтобы достичь этого, линейная логика не допускает применять обычные структурные правила сжатия и ослабления ко всем формулам, допуская их лишь для формул, помеченных определёнными модальностями. Линейная логика содержит полностью инволютивное отрицание, сохраняя при этом конструктивную интерпретацию в сильном смысле.

Линейная логика также доставляет новую интуицию для понимания природы доказательств в классической и интуиционистской логиках. Из-за своей сфокусированности на ресурсах, линейная логика нашла множество применений в информатике.

Помимо этого, с появлением линейной логики началась новая волна интереса к так называемым субструктурным логикам логикам, в которых мало (или вообще нет) структурных правил. Это связано с тем, что значительная часть известных субструктурных логик консервативно вкладывается в подходящий фрагмент линейной логики либо полностью, либо значительными фрагментами, представляющими отдельный интерес.

Для этих логик линейная логика предоставляет единообразные средства для рассуждения о доказуемости, такие, как, например, сети доказательств. С другой стороны, другие субструктурные логики также оказывают влияние на теорию сетей доказательств: для некоторых исчислений были придуманы гораздо более элегантные конструкции сетей, чем для фрагмента, который дал этой теории начала мультипликативной линейной логики.

Другая сторона линейной логики, которая частично освещена в статье это её теоретико-игровые семантики. Через них линейная логика оказывается связана с огромным числом разделов современной теоретической информатики от собственно теории игр до колмогоровской сложности. И. Межировым в 2006 г. была получена сложностная игровая семантика для линейной логики, которая позже оказалась тесно связанной с логикой интерактивной вычислимости Г. Джапаридзе.

Наконец, линейная логика в силу своей ориентированности на ресурсы предоставляет инфраструктуру для построения новых логических и функциональных языков программирования.

1.1 Немного истории Линейная логика была введена Жаном-Ивом Жираром в его основополагающей работе [19]. Хотя первоначальное открытие этой новой логики и произошло из семантического анализа системы F (или полиморфного -исчисления), всю систему линейной логики можно рассматривать, как смелую попытку согласовать красоту и симметрию систем классической логики со стремлением к конструктивным доказательствам, которое привело к интуиционизму.

В самом деле, можно представить первый фрагмент линейной логики, известный, как мультипликативная аддитивная линейная логика (MALL), как результат двух простых наблюдений:

• В секвенциальном исчислении для классической логики, правила для связок и и или, а также правило сечения (Cut) и правило для импликации могут быть представлены эквивалентным образом либо в аддитивной форме (когда контексты посылок совпдаают), либо в мультипликативной форме (когда они различаются). В классической логике эти представления эквивалентны в силу доступности некоторых так называемых структурных правил, а именно, сжатия и ослабления.

• Неконструктивные доказательства, которые можно построить в классической логике, на самом деле используют одно из этих структурных правил, если их записать в секвенциальном исчислении.

Таким образом, если мы хотим устранить неконструктивные доказательства, сохранив при этом симметрию секвенциального исчисления, в отличие от интуиционистской логики, мы можем попытаться устранить правила сжатия и ослабления. Сделав это, мы получим по две разные версии каждой связки: по аддитивной версии для и и или, и по мультипликативной версии их же, причём они более не эквивалентны. Эти новые связки называются & (аддитивное и), (аддитивное или), (мультипликативное и) и ` (мультипликативное или).

Это удвоение связок на самом деле даёт гораздо более ясно понять конфликт между классической и интуиционистской логикой: закон исключённого третьего, например (A или не-A), считается очевидностью в классическом мире и абсурдом в интуиционистском. Но в линейной логике этот закон можно проинтерпретировать двояко, аддитивным (A ¬A) и мультипликативным (A ` ¬A) образом: аддитивный вариант невыводим, и соответствует интуиционистской интерпретации дизъюнкции; мультипликативный вариант тривиально доказуем и соответствует тавтологии (A влечёт A), которая вполне допустима и в интуиционизме.

Дизъюнктивное свойство, важнейшее для конструктивизма, также оказывается тривиально выводимым для аддитивной дизъюнкции.

В этом более богатом языке мы можем найти способ представить одновременно и нужды интуиционизма, и элегантность классической логики: отрицание инволютивно, секвенции симметричны, связки определимы друг через друга, модели просты, но в то же время можно доказать теоремы корректности и полноты для некоторого кодирования, погружающего интуиционизм в линейную логику. Сравните эти свойства с отсутствием их аналогов в интуиционизме, где отрицание неинволютивно, секвенции несимметричны и связки не всегда выражаются друг через друга. Также модели Крипке значительно более сложно устроены, чем булевы алгебры.

1.2 Линейная логика и информатика Логика, или, по крайней мере, теория доказательсв, сфокусирована на системах формальных доказательств: интуиционистском исчислении предикатов, классическом исчислении предикатов, арифметике, исчислениях более высокого порядка и многообразии похожих непротиворечивых и структурированных множеств правил построения процессов. Интуиционистская и конструктивная логика начались, когда люди увидели возможность чтения формулы A B, как если вы дадите мне A, я дам вам B, что значительно отличается от классического прочтения B верно всегда, когда верно A.

Информатика, в свою очередь, фокусируется на механизмах вычисления: применении функций, обработке исключений, вызове методов в объектно-ориентированных языках, присваивании значений переменным и подобным наборам правил построения процессом. Отличие от логики здесь в том, что механизмы этих процессов должны быть указаны явно: функция типа A B даёт формальное описание того, как преобразовать A в B.

В некоторый момент эти науки встретились. Люди осознали, что множество импликативных интуиционистских выводов являлось, по сути, функциональным языком под названием -исчисление с простыми типами :

язык программирования представлял собой логику, а логика язык программирования. Эта памятная встреча была названа изоморфизмом Карри-Говарда ([26]).

Линейная логика начинается с дальнейшей эволюции прочтения A B : теперь оно означает дайте мне столько A, сколько мне нужно, и я дам вам одно B. Понятие копирования, центральное в идее вычисления, теперь встроено в логику.

Эта новая точка зрения открывает новые возможности, включая:

• Новые формулы, выражающие уточнённые свойства операций, как, например, дайте мне одно A и я дам вам B. Приложения здесь имеются во множестве сфер, среди которых представление знания в искусственном интеллекте, улучшенное логическое программирование, в котором используется способность линейной логики кодировать состояние алгоритма, анализ классической логики и её вычислительных интерпретаций, а именно, механизмов исключений в языках порграммирования, с помощью погружений в линейную логику, улучшенные темпоральные логики, анализ линейности.

• Новые правила, выражающие ограничения на использование копий. Ярчайшим результат этого – существование фрагмента линейной логики для полиномиальных вычислений.

• Новые способы представления доказательств.

2 Системы доказательств Основные пропозициональные связки линейной логики делятся на аддитивные и мультипликативные. Классическая конъюнкция и её единица, и, разделяется на аддитивные & ( с ) и ( аддитивную истину ) и мультипликативные ( тензор ) и 1 ( единицу ). Похожим образом, классическая дизъюнкция со своей единицей, и, разделяются на аддитивные ( аддитивное или ) и 0 ( ноль ) и мультипликативные ` ( пар ) и ( мультипликативную ложь ).

Отрицание можно рассматривать одним из двух способов, в зависимости от представления линейной логики. Его можно рассматривать, как примитивную пропозициональную связку без ограничений на вхождения в формулу. С другой стороны, так как между отрицанием и всеми пропозициональными связками, экспоненциалами и кванторами имеется двойственность де Моргана, его также можно вводить как специальную систему, которая применяется только к атомарным формулам. Импликации также обыкновенно вводятся в линейной логике с помощью определений: линейная импликация B C может быть определена, как ¬B ` C, а интуиционистская импликация B C как !B C. Операторы ! и ? называются модальностями или экспоненциалами. Термин экспоненциал здесь особенно подходит, поскольку, аналогично обычной взаимосвязи между потенцированием, сложением и умножением, линейная логика поддерживает эквивалентности !(B&C) (!B!C) и ?(B C) = (?B`?C), а также 0-арные версии этих эквивалентностей, а именно, (! 1) и (?0 ). Бинарная эквивалентность B C здесь означает, что в линейной логике выводима 2.1 Секвенциальное исчисление На рисунке 1 представлено двустороннее секвенциальное исчисление для линейной логики. Заметьте, что здесь отрицание является полноценной логической связкой: его вхождения в формулу не ограничены и есть правила для введения отрицания и справа, и слева.

Здесь и левая, и правая стороны секвенций представляют собой мультимножества формул: таким образом, порядок формул в этих контекстах не имеет значения, но их количества имеют. Заметьте, что правила ослабления и сокращения доступны только для формул с экспоненциалом ! слева или с ? справа в секвенции. Подразумеваются обычные предположения для введения справа и слева: в частности, переменная y не должна быть свободной в формулах в заключении секвенции в этих правилах вывода. Кванторы здесь подразумеваются первого порядка: варианты линейной логики высших порядков могут быть сконструированы стандартным образом.

Правило сечения (cut) может быть устранено, не нарушая полноты. Двойственным образом, можно устранить также применения правила init, кроме применений к атомарным формулам.

2.2 Сфокусированный поиск доказательств В работе [8] была доказана важная теорема о нормальной форме структуры доказательств без сечения. Андреоли называет неатомарную формулу синхронной, если её внешняя логическая связка есть, &,, `, ? или, и синхронной, если её внешняя логическая связка есть 0,, 1,, ! или.

Рассматривая поиск доказательств в качестве модели вычислений, можно считать формулы в секвенции агентами, которые могут действовать независимо или сообща с другими агентами в своём окружении: действия агента определяются с помощью чтения правила, в котором он вводится, снизу вверху. Если асинхронная формула встречается в правой части секвенции, она может эволюционировать, не влияя на доказуемость и не взаимодействуя со своим контекстом. Например, агент (B `C) с помощью применения правила введения ` справа превращается в двух агентов B и C (работающих параллельно). Похожим образом, агент (B&C) порождает (с помощью применения правила введения & справа) два идентичных мира (секвенции), которые различаются лишь тем, что B находится в одном из этих миров, а C в другом.

С другой стороны, если мы посмотрим на синхронную формулу, как на агента, чья эволюция определяется соответствующим правилом введения справа, то доказуемая секвенция приобретёт возможность эволюционировать в недоказуемую (например, применением правила введения справа). Конкретные формы этих правил вывода зависят от контекста формулы. Например, применимость правила введения 1 справа требует, чтобы окружающий контекст был пустым, а применение правила введения справа может зависеть от того, каким способом окружающий агента контекст делится на две разных секвенции. Таким образом, эволюция таких агентов зависит от синхронизации с остальными частями контекста.

Рассмотрим теперь представление линейной логики в виде одностороннего исчисления секвенций, в котором все правила введения связок вводят их справа. С помощью классификации связок, описанной выше, становится возможным показать, что поиск доказательства может быть структурирован в следующие фазы без потери полноты. Асинхронная фаза происходит, если в секвенции имеется асинхронная формула. В этой фазе поиск применяет правила введения связок справа в любом порядке, пока асинхронные формулы не исчезнут. В синхронной фазе выбирается одна из синхронных формул, которая становится фокусом этой фазы, то есть, Рис. 2: Система сфокусированных доказательств для линейной логики.

правила введения связок применяются к ней и ко всем синхронным подформулам, которые она порождает.

Рисунок 2 иллюстрирует систему сфокусированных доказательств для линейной логики. Заметьте, что разные фазы представлены разными стрелками: стрелка вверх обозначает асинхронную фазу, а стрелка вниз синхронную. Атомарные формулы в этой системе имеют полярность, и в рисунке 2 A обозначает положительные атомарные формулы, а отрицание A отрицательные. В этой системе доказательств, обозначает множество формул, а и L мультимножества формул. Так как L участвует только в правилах, включающих стрелку вверх, L также может обозначать список, то есть, на формулах справа от стрелки вверх можно ввести любой порядок, так как введение асинхронных формул может быть произведено в любом порядке. Доказательства, которые получаются с помощью этих правил вывода, называются сфокусированными доказательствами. Результат [8] заключается в том, что эта система полна в линейной логике.

2.3 Сети доказательств Доказательства, представленные в виде секвенциальных выводов, содержат массу деталей, которые иногда не являются интересными: представьте, например, сколько существует различных, но не очень интересно различающихся, способов сформировать доказательство, (A1 ` A2 ),..., (An1 ` An ) из вывода, A1,..., An. Этот неприятный факт следует из последовательной природы доказательств в исчислении секвенций: если мы хотим применить множество S, состоящее из n правил, к разным частям секвенции, мы не можем их применить в один шаг, даже если они не взаимодействуют друг с другом! Мы должны упорядочить их, то есть выбрать линейный порядок на S и применить правила в n шагов согласно этому порядку. Такая последовательная природа секвенциального исчисления является значительным препятствием, например, в доказательствах устранимости сечения, когда требуется учесть также все неинтересные выводы.

Возникает естественный вопрос: Существует ли представление доказательств, которое асбтрагируется от таких неинтересных деталей? В случае интуиционистского исчисления высказываний аналогичный вопрос разрешается положительным образом с помощью систем естественного вывода, которые сильно связаны с системой вычислений, известной, как -исчисление, с помощью изоморфизма Карии-Говарда.

Для линейной логики, такое сжатое представление доказательств доставляют сети доказательств, графоподобные структуры, которые обладают особенно хорошими свойствами для фрагмента MLL. Первый шаг к этому представлению преобразовать всё секвенциальное исчисление с помощью инволютивности отрицания в одностороннюю систему, в которой секвенции имеют вид. Как следствие, количество правил уменьшается вдвое в силу того, что система становится односторонней, но сохраняется вся выразительность логики, так как доказуемость остаётся той же.

С каждым доказательством в несимметричном секвенциальном исчислении для MLL можно связать сеть доказательства с теми же заключениями по индукции следующим образом:

• С доказательством, заключающимся в одном аксиомном правиле, мы ассоциируем аксиомную связь:

• Для доказательства, полученного применением правила сечения к доказательствам P1 и P2, сначала построим по индуктивному предположению сети для P1 и P2 и свяжем их связью сечения:

• Для доказательства, полученного применением правила тензора к доказательствам P1 и P2, сначала построим по индуктивному предположению сети для P1 и P2 и свяжем их тензорной связью:

• Для доказательства, полученного применением правила пара к доказательству P1, построим по индуктивному предположению сеть для P1 и добавим к ней связь пара:

Всё это можно должным образом формализовать с помощью гиперграфов (формулы будут вершинами, а связи ориентированными гиперрёбрами между гипотезами и заключениями), и формально определить сеть доказательства можно, как гиперграф, по индукции построенный по некоторому выводу в секвенциальном исчислении для MLL. Заметим, что существует очень много гиперграфов, не являющихся сетями доказательств.

Если посмотреть на сеть доказательств, построенную из выводов, (A1 ` A2 ),..., (An1 ` An ), полученных из, A1,..., An, станет видно, что в ней не осталось никаких следов порядка применения правил. В некотором смысле, сети доказательств классы эквивалентности выводов в исчислении секвенций по отношению порядка правил вывода, чьи применения коммутируют.

Представьте, что кто-то принёс вам огромный гиперграф, построенный из связей, определённых выше, и заявляет, что это на самом деле сжатое представление доказательства какой-нибудь знаменитой открытой математической проблемы. Как можно проверить, что это на самом деле представление доказательства, а не просто случайная структура?

Проверка сети на корректность проблема, которая сводится к восстановлению последовательной истории построения вашей структуры, соответствующей выводу в секвенциальном исчислении, и она кажется на первый взгляд очень сложной: перывый критерий корректности для сетей доказательств в MLL, называвшийся критерием долгого блуждания, и представленный в первоначальной статье Жирара, экспоненциален, как и критерий ACC (ацикличности и связности) Даноса и Ренье, найденный позже. Несмотря на всё это, существует гораздо более эффективный критерий критерий сокращаемости, найденный Даносом и Ренье, который недавно был переформулирован Геррини, Мартини и Масини в виде следующего элегантного критерия разбора графа: гиперграф является сетью доказательства тогда и только тогда, когда он редуцируется к одиночной вершине типа net с помощью правил редукции графа на рисунке 3.

Наивная проверка этого критерия может занять квадратичное время (каждое применение правила может потребовать обход всего графа, чтобы найти редуцируемое выражение, и количество шагов, которые необходимо сдлеать, равно количеству гиперрёбер в графе), но один из результатов Геррини показывает, как производить эту проверку за почти линейное время. Известно множество других критериев корректности, некоторые из которых также линейны, как, например, критерий Муравского и Онга, полученный из критерия для интуиционистской MLL.

Устранять сечение на сетях доказательств можно особенно простым и элегантным образом: в силу их параллельной природы, сечения можно устранять локально с помощью двух правил упрощения:

• Аксиомный ход:

• Мультипликативный ход:

Эти ходы являются правилами преобразования сетей доказательств, и критерии корректности позволяют легко проверить, что все они сохраняют корректность, и, как следствие, процесс редукции полученной сети доказательств соответствует некоторому секвенциальному доказательству исходной секвенции.

Таким образом, устранение сечения в сетях доказательств для MLL может быть произведено за линейное время, что даёт простой и элегантный результат об устранимости сечения для всего фрагмента MLL.

Сетевой подход может быть распространён на большие подмножества линейной логики, но для них менее ясно, как получить такие же элегантные результаты, как для MLL: первоначальная система, предложенная в [19], работает, например, для MELL, ассоциируя с четырьмя экспоненциальными правилами следующие конструкции гиперграфов:

• Сокращение:

• Ослабление:

• Оставление:

• Продвижение. Здесь вводится понятие бокса, упорядочивающей метки вокруг части сети доказательства, представленной на рисунках с графами прямоугольником, обводящим сеть доказательства заключений A Хотя эта конструкция и связанные с ней правила редукции графа удивительно похожи на -исчисление с явными подстановками, как впервые заметили Ди Космо и Кеснер ([16]), они слишком похожи на соответствующие правила секвенциального исчисления: присущий MLL элегантный эффект параллелизации не переносится сюда должным образом, и правила редукции графа включают боксы и не являются локальными.

Начиная с работы Даноса и Ренье в [15] было сделано много предложений для того, чтобы восстановить удовлетворительную систему, но здесь мы хотим упомянуть крайне элегантный подход Геррини, Мартини и Массини [21], который красиво показывает связь между двухуровневыми системами доказательств для модальной логики, собственными сетями доказательств для MELL и оптимальной редукцией в -исчислении.

Расширение сетей доказательств, которое позволило бы иметь дело с аддитивными связками, имеет в настоящее время несколько технических реализаций, ни одна из которых не кажется канонической или хотя бы удовлетворительной. Поддержка аддитивных связок в подобных системах доказательств является сейчас областью активных исследований.

3 Семантика К семантике линейной логике есть два разных подхода. Во-первых, имеются различные семантические структуры, характеризующие истину в модели. С помощью таких подходов можно установить корректность и полноту (некоторых фрагментов) линейной логики. Более новый семантический подхо к линейной логике включает в себя установление семантики напрямую для доказательств. Мы кратко описываем эти два подхода и даём ссылки на литературу.

3.1 Доказуемостные семантики Один из подходов к построению корректной и полной семантики для фрагментов линейной логики ассоциирует с формулой множество всех контекстов, с помощью которых можно доказать эту формулу. Конечно, может быть, что подобное множество должно быть более абстрактным и обладать различными свойствами замкнутости. Фазовая семантика Жирара [19] доставляет пример такой семантики: у таких семантик обнаружились некоторые приложения в информатик, например, для построения контрпримеров и в качестве инструмента, который помогает установить, что данная параллельная система не может эволюционировать в другую, обладающую некоторыми свойствами ([18]). Схожим образом, семантики в стиле Крипке были построены Аллвейном и Данном в [6] и Ходасом и Миллером в [24]. Определённые частично упорядоченные алгебраические структуры под названием квантали также служили ранними семантическими моделями для частей линейной логики ([43]).

3.2 Семантики доказательств Применяя аналогию формулы есть типы, которая так популярна и плодотворна в теоретической информатике, логическая система становится в соответствие с типизированным вычислительным методом (как, например, исчисление с типами), ассоциируя с каждым доказательством формулы программу, имеющую своим типом ту самую формулу. Например, доказательство тавтологии A A соответствует программе f un(x : A).x : A A, тождественной функции на объектах типа A. Именно поэтому в конструктивных логических системах и в линейной логике доказательства так важны, до той степени, что построение и изучение моделей доказательств привлекает гораздо больше внимания, чем построение и изучение моделей доказуемости: нам недостаточно знать того, что формула доказуема, мы на самом деле хотим знать вычислительное содержание её доказательства.

Было предложене много моделей доказательств в линейной логике: мы считаем, что на сегодняшний день, наиболее простые и интуитивные конструкции основаны на так называемых реляционных семантиках, в которых формулы интерпретируются, как мультимножества, секвенции как кортежи мультимножеств, а доказательства как отношения над множеством интерпретаций секвенций. При желании можно дать полностью теоретико-множественную семантику, не прибегая к мультимножествам, с помощью когерентных множеств, множеств со специальным отношением когерентности, как впервые показано Жираром в [19]. Для линейной логики есть интересные теоретико-категорные модели, как, например, -автономные категории ([10]) и гиперкогерентности ([17]).

Другой подход к семантике доказательств изложен в Геометрии взаимодействия Жирара, и он позволяет получить полностью алгебраическую характеризацию доказательств: с каждой сетью доказательства можно связать матрицу частичной перестановки, соответствующую связям сечения, и матрицу M, соответствующую чистой сети, элементы которой содержат выражения, построенные из так называемой динамической алгебры, которые описывают возможные пути внутри чистой сети. Сеть доказательств становится возможным полностью описать с помощью формулы выполнения которая, в случае MLL, является инвариантом процесса нормализации. Интересные связи с результатами из теории потоков данных показаны в ранней работе Абрамского и Ягадесана [2].

Отдельного упоминания заслуживает исключительно богатая область исследований, которая образовалась вокруг так называемой игровой семантики, сильная связь которой с линейной логикой была обнаружена довольно рано А. Блассом ([12]). В этом подходе формулы интерпретируются, как игры, логические связки как конструкторы игр, а доказательства как стратегии, описывающие, как игрок отвечает на ходы противника.

Вводя должные ограничения на правила игры, можно предоставить довольно точную семантику (технически говоря, полностью абстрактную модель) различных возможностей реальных языков программирования, откуда и происходит гигантский интерес к этой области на протяжении последних лет. См., например, [2], [3], [27].

3.3 Сложность Огромное количество исследовательских работ было посвящено изучению сложности и разрешимости различных фрагментов пропозициональной линейной логики. Известно, что:

• Проблема доказуемости в MLL NP-полна ([28]) • Проблема доказуемости в MALL PSPACE-полна ([35]) • Проблема доказуемости в LL неразрешима ([34]) • Вопрос разрешимости MELL остаётся открытым: из того, что проблема достижимости в сетях Петри сводится к проблеме доказуемости в MELL ([22]) следует, что последняя должна быть по меньшей мене EXPSPACE-сложна.

Для тех, кто забудет, что новизна линейной логики содержится в том, как обслуживаются формулы без структурных правил, будет удивительным то, что эти результаты останутся верными, даже если рассматривать фрагменты этих логик, в которых допустимы только константы, и нет пропозициональных переменных ([29], [36]). В самом деле, существует погружение произвольных формул в формулы, содержащие только константы, сохраняющее доказуемость.

Хороший обзор сложностных результатов, окружающих линейную логику, содержится в работе [34].

4 Влияние на информатику Когда интуиционизм был впервые предложен в начале прошлого века, он бросил вызов традиционному способу ведения дел в математике. Использование закона исключённого третьего и доказательств от противного считались подозрительными и проблематичными, особенно в присутствии бесконечности. По мере того, как вопросы интуиционистской логики развились в конструктивную математику, появились новые конструктивные подходы к таким областям, как топология, алгебра и анализ. Поскольку линейная логика содержит в себе динамику доказательств (алгоритмов) и ресурсов, она в основном оказала влияние не на традиционную математику, а на информатику. Перед тем, как описать природу этого влияния, мы очертим применения логики в информатике в общем.

Логика играет различные роли в спецификации вычислений. Мы можем выделить следующие широко различающиеся подходы и отметить, какие из ролей подверглись влиянию линейной логики.

В подходе вычисление, как модель, вычисления кодируются в математические структуры и состоят из таких частей, как вершины, переходы и состояния. Логика используется во внешнем смысле, чтобы делать утверждения о этих структурых. То есть, вычисления используются в качестве моделей логических выражений.

Интенсиональные операторы, такие, как модальности темпоральной и динамической логики или тройки логики Хора, часто используются для выражения предложений об изменении состояния. Это использование логики для представления вычислений и рассуждения о них, вероятно, является самым старым и наиболее успешным. На эту роль логики линейная логика не оказала существенного влияния.

В подходе вычисление, как вывод, фрагменты синтаксиса логики (такие, как формулы, термы, типы и доказательства) напрямую используются в качестве элементов описываемого вычисления. В этой, более редкой, постановке задачи существует два сильно различных подхода к моделированию вычисления: нормализация доказательства и поиск доказательства.

Ниже мы описываем значительное влияние, которое линейная логика оказала на оба этих подхода.

4.1 Нормализация доказательства Подход к моделированию вычислений через нормализацию доказательства рассматривает состояние вычисления, как терм доказательства, а процесс вычисления как нормализацию (-редукцию, устранение сечения).

Функциональное программирование может быть объяснено через нормализацию доказательств в качестве своего теоретического основания ([37]), и она была использована для обоснования проектирования новых функциональных языков программирования, например, в [1]. Линейная логика доставляет этому подходу к спецификации вычислений новые типы и новые декларативные способы статического понимания того, как ресурсы могут быть использованы в вычислении. Она также предоставляет привлекательный способ формализации двойственности между функцией и окружением, которое предоставляет ей аргументы.

Линейная логика также является мощным теоретическим инструментом в области оптимальной редукции.

Проблема построения эффективных (оптимальных) интерпретаторов -исчисления, которая оставалась открытой довольно долго после того, как её сформулировал Дж. Дж. Леви, впервые была решена в [33] с помощью изощрённой реализации графа разделений, включающей довольно внушительное количество правил. Используя идеи и интуицию из линейной логики, многие авторы переделали решение Лампинга, упрощая его, что привело к богатой теории, связанной с теорией в Геометрии Взаимодействия. Для интересующихся хорошим обзором послужит книга Асперти и Геррини Оптимальная реализация функциональных языыков программирования.

Уточнение интуиционистской логики, которое даёт линейная логика, и двойственности линейной логики предоставляют среду, в которой функцию и её окружение можно воспринимать, как похожие сущности, которые взаимодействуют двойственным образом. Например, функция типа может быть смоделирована процессом, который поглощает значение типа из своего окружения и преобразует его в значение типа. В линейной логике, эта импликация эквивалентна своей контрапозиции: тип ¬ ¬ позволяет интерпретировать ту же самую функцию, как процесс, который преобразует спрос на значение типа в спрос на значение типа (заметим, что это не случается с фкнкциями интуиционистского типа, поскольку, например, входной аргумент может быть пустым) ([14]). Недавние успешные применения игровых семантик для моделирования функциональных вычислений похожим образом связаны с двойственной трактовкой функции и окружения ([2], [27]).

Наконец, в области, трактующей вычисления, как нормализации доказательств, с помощью линейной логики было получено теоретико-типовое описание полиномиальных по времени рекурсивных функций. Например, М. Хоффманн ([25]) ввёл -исчисление с модальными и линейными типами, которое расширило алгебру функций [11] на высшие типы. Типы, основанные на линейной логике, также использовались в функциональных программах: см. [23], [42].

4.2 Поиск доказательства Подход поиска доказательства рассматривает состояние вычисления, как секвенцию (структурированный набор формул), а процесс вычисления как процесс поиска доказательства этой секвенции: изменения, происходящие в секвенциях, моделируют динамику вычисления. Логическое программирование может быть объяснено с помощью поиска доказательства в качестве теоретического основания, и линейная логика предоставляет этому подходу к спецификации вычислений новые комбинаторы для построения логических программ, новые способы описывать богатую динамику динамическим образом, и новые декларативные способы описания параллельных вычислений. (См. в [40] обзор языков программирования, основанных на линейной логике).

С помощью полноты сфокусированной системы доказательств можно получить декларативное объяснение части операционной семантики логического програмирования внутри линейной логики. Например, рассмотрим подмножество L всех формул линейной логики, содержащих только связки, &,, и. (заметим, что если к этому списку добавить, то станет возможным закодировать все связки линейной логики.) Можно показать, что поиск доказательств, не включающих правило сечения, в L может быть разделено на фазы. Исходя из секвенции ; G, где множество формул (предполагается, что ко всем формулам неявно применён !), мультимножество формул, а G формула (все формулы из L), поиск доказательства происходит следующим образом.

• Если G не атомарна, то эта секвенция может быть получена только введением связки справа в качестве последнего шага. С данным набором связок, все правила введения справа обратимы и фаза редукции цели в точности соответствует асинхронной фазе сфокусированных доказательств.

• Если G атомарна, поиск доказательства выделяет одну формулу из контекста слева.

• Как только выделена формула для фокуса, все правила введения слева применяются только к ней и ко всем положительным подформулам, которые будут порождены. Эта фаза обратного сцепления соответствует синхронной фазе построения сфокусированного доказательства.

Говоря формально, эти фазы можно описать с помощью следующих правил вывода. Заматим, что здесь введена новая секвенциальная стрелка: она помечена формулой-результатом применения правила введения слева.

Заметим также, что правило для введения слева требует разбиения ограниченного контекста 1, 2 на две части (если читать правило сверху вниз). Таких разбиений, конечно, 2n, если в контексте содержится n различных формул.

В частности, мы получаем ещё один язык для спецификации вычислительных систем, помимо, например, сетей Петри, исчислений процессов, -исчисления, и т.д. Так как линейная логика, по сути, является логикой с разработанной теорией доказательств и семантиками самого различного рода, из мета-теории самой линейной логики можно извлечь широкое множество способов рассуждать о вычислениях.

Так как исчисления секвенций для линейной логики используют мультимножества формул, в поиске доказательств можно напрямую кодировать трансформации мультимножеств. Так как многие вычисления естественным образом представляются в виде трансформации мультимножеств, стало возможным обозначить множественные связи между линейной логикой и сетями Петри ([22]), исчислениями процессов ([7], [38]) и криптографическими протоколами ([13], [39]).

5 Варианты линейной логики 5.1 Другие интерпретации модальности Экспоненциалы ! и ? в линейной логике значительно менее высечены в камне, чем остальные связки. Действительно, если использовать традиционные представления секвенциальных исчислений, экспоненциалы не каноничны : если ввести их копии, например, ! и ?, с теми же правилами, как для исходных связок, невозможно показать, что ! эквивалентно !, а ? эквивалентно ?, в то время, как для остальных связок такое свойство тривиально выполняется.

В этом отношении, ! и ? напоминают связки и модальной логики, и становится возможным и интересным изучать варианты логических правил для этих связок. Например, элементарная линейная логика получается заменой правил ввода ! и ? одним правилом, вводящим ! и ? одновременно. Как следствие, в ELL можно закодировать в точности те функции над натуральными числами, которые нормализуются за время, ограниченное элементарной функцией.

Помимо этого, существует лёгкая линейная логика ([20]), мягкая линейная логика ([31]) и множество других (см., например, [9]).

5.2 Некоммутативная линейная логика Хотя линейная логика и отвергает неограниченное применение структурных правил ослабления и сокращения, она позволяет неограниченное использование структурного правила обмена. Секвенциальное исчисление, в котором нет неограниченного применения правила обмена, имеет секвенции, левые и правые контексты которых суть списки; порядок формул в контексте становится выразительным средством логики. В этом случае, мультипликативные дизъюнкция и конъюнкция могут стать некоммутативными.

Одна из первых логик, отвергающих все три структурных правила, была описана в [32]. Хотя эта логика содержит две импликации, в ней отсутствует отрицание для экспоненциалов. Многие недавние статьи предлагают некоммутативные расширения линейной логики, и в настоящий момент ни одно из этих предложений не кажется каноническим. За примерами расширений см [43], [4], [41], [5].

Список литературы [1] Abramsky, S., 1993, "Computational interpretations of linear logic Theoretical Computer Science, 111: 3-57.

[2] Abramsky, S., and Jagadeesan, R., 1994, "New Foundations for the Geometry of Interaction Information and Computation, 111(1): 53-119.

[3] Abramsky, S., and Melli`s, Paul-Andr, 1999, "Concurrent Games and Full Completeness 14th Annual Symposium on Logic in Computer Science, Trento, Italy, IEEE Computer Society Press., pp. 431-442.

[4] Abrusci, V. M., 1991, "Phase semantics and sequent calculus for pure non-commutative classical linear propositional logic Journal of Symbolic Logic, 56(4): 1403-1451.

[5] Abrusci, V.M., and Ruet, P., 1999, "Non-Commutative Logic I: The Multiplicative Fragment Annals of Pure Applied Logic, 101(1): 29-64.

[6] Allwein, G. and Dunn, J.M., 1993, "Kripke Models for Linear Logic Journal of Symbolic Logic, 58(2): 514-545.

[7] Andreoli, J.-M. and Pareschi, R., 1991, "Linear objects: Logical processes with built-in inheritance New Generation Computing, 9(3-4): 445-473.

[8] Andreoli, J.-M., 1992, "Logic programming with focusing proofs in linear logic Journal of Logic and Computation, 2(3): 297-347.

[9] Baillot, P., and Terui, K., 2004, "Light Types for Polynomial Time Computation in Lambda-Calculus LICS Turku, Finland, IEEE Computer Society Press, pp. 266-275.

[10] Barr, M., 1991, "*-Autonomous categories and linear logic Mathemathical Structures in Computer Science, 1(2):

159-178.

[11] Bellantoni, S. and Cook, S., 1992, "A New Recursion-Theoretic Characterization of the Polytime Functions Computational Complexity, 2: 97-110.

[12] Blass, A., 1992, "A game semantics for linear logic Annals Pure Applied Logic, 56: 183-220.

[13] Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., and Scedrov, A., 1999, "A meta-notation for protocol analysis in R. Gorrieri (ed.), Proceedings of the 12th IEEE Computer Security Foundations Workshop CSFW 1999, Los Alamitos, CA: IEEE Computer Society Press, pp. 55-69.

[14] Curien, P.-L., 2003, "Symmetry and interactivity in programming Bulletin of Symbolic Logic, 9(2): 169-180.

[15] Danos, V., Regnier, L., 1993, "Proof-nets and Hilbert space in J.-Y. Girard, Y. Lafont, and L. Regnier (eds.), Advances in Linear Logic, Cambridge: Cambridge University Press, 1995, pp. 307-328.

[16] Di Cosmo, R., and Kesner, D., 1997, "Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract) in Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, CA: IEEE Computer Society Press, pp. 35-46.

[17] Ehrhard, T., 1993, "Hypercoherences: A Strongly Stable Model of Linear Logic Mathematical Structures in Computer Science, 3(4): 365-385.

[18] Fages, F., Ruet, P., and Soliman, S., 2001, "Linear Concurrent Constraint Programming: Operational and Phase Semantics Information and Computation, 165(1): 14-41.

[19] Girard, J.-Y., 1987, "Linear logic Theoretical Computer Science, 50: 1-102.

[20] –––, 1998, "Light Linear Logic Information and Computation, 143(2):175-204.

[21] Guerrini, S., Martini, S., and Masini, A., 2003, "Coherence for sharing proof-nets Theor. Comput. Sci., 294(3): 379-409. Guglielmi, A., and Strassburger, L., 2001, "Non-commutativity and MELL in the Calculus of Structures Computer Science Logic, Lecture Notes in Computer Science, vol. 2142, Springer Verlag, pp. 54-68.

[22] Gunter, C. A., and Gehlot, V., 1989, "Nets as Tensor Theories in G. De Michelis (ed.), Proceedings of the Tenth International Conference on Application and Theory of Petri Nets, Lecture Notes in Computer Science n. 616, Springer-VerlagBonn, pp. 174-191.

[23] Guzman, J.C. and Hudak, P., 1990, "Single-threaded polymorphic lambda calculus in Proceedings of the Fifth IEEE Symposium on Logic in Computer Science, Philadelphia, IEEE Computer Society Press.

[24] Hodas, J., and Miller, D., 1994, "Logic programming in a fragment of intuitionistic linear logic Information and Computation, 110(2): 327-365.

[25] Hofmann, M., 2003, "Linear types and non-size increasing polynomial time computation Information and Computation, 183(1): 57-85.

[26] Howard, W.A., 1980, "The formulae-as-type notion of construction, 1969 in J.P. Seldin and R. Hindley (eds.), To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, New York: Academic Press, pp.

479-490.

[27] Hyland, J.M.E., and Ong, C.-H.L., 2000, "On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully

Abstract

and universal game model Information and Computation, 163: 285-408.

[28] Kanovich, M.I., 1992, "Horn Programming in Linear Logic is NP-Complete in Proceedings of the Seventh Annual Symposium on Logic in Computer Science, Santa Cruz, IEEE Computer Society Press, pp. 200-210.

[29] –––, 1994, "Simulating Linear Logic with 1-Linear Logic Technical Report 94-08, Laboratoire de Mathmatiques Discrtes, University of Marseille, 1994.

[30] Kobayashi, N., Shimizu, T., and Yonezawa, A., 1999, "Distributed concurrent linear logic programming Theoretical Computer Science, 227(1-2): 185-220.

[31] Lafont, Y., 2004, "Soft linear logic and polynomial time Theoretical Computer Science, 318(1-2): 163-180.

[32] Lambek, J., 1958, "The mathematics of sentence structure American Mathematical Monthly, 65: 154-169.

[33] Lamping, J., An algorithm for optimal lambda-calculus reductions. 17th Annual Symposium on Principles of Programming Languages, San Francisco, ACM Press, pages 16–30, 1990.

[34] Lincoln, P., 1995, "Deciding provability of linear logic formulas Proceedings of the Workshop on Advances in Linear Logic, J.-Y. Girard, Y. Lafont, and L. Regnier (eds.), Cambridge: Cambridge University Press, pp. 197-210.

[35] Lincoln, P., Mitchell, J., Scedrov, A., and Shankar, N., 1992, "Decision problems for propositional linear logic Annals of Pure and Applied Logic, 56: 239-311.

[36] Lincoln, P., and Winkler, T., 1994, "Constant-Only Multiplicative Linear Logic is NP-Complete Theoretical Computer Science, 135:155-169.

[37] Martin-Lf, P., 1982, "Constructive Mathematics and Computer Programming Sixth International Congress for Logic, Methodology, and Philosophy of Science, Amsterdam, North-Holland, pp. 153-175.

[38] Miller, D., 1996, "Forum: A multiple-conclusion specication language Theoretical Computer Science, 165(1):

201-232.

[39] –––, 2003, "Encryption as an abstract data-type: An extended abstract in I. Cervesato (ed.), 16th Workshop on Foundations of Computer Security, Asilomar, IEEE Computing Society, pp. 3-14, 2003.

[40] –––, 2004, "Overview of linear logic programming Linear Logic in Computer Science, T. Ehrhard, J.-Y. Girard, P. Ruet, and P. Scott (eds.) (London Mathematical Society Lecture Note 316), Cambridge: Cambridge University Press, pp. 119-150.

[41] Retor, C., 1997, "Pomset logic: a non-commutative extension of classical linear logic Typed Lambda Calculi and Applications, Lecture notes in Computer Science vol. 1210, Spreinger Verlag, pp. 300-318.

[42] Wadler, P., 1991, "Is there a use for linear logic? Proceedings of ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation, New Haven, ACM Press, pp. 255-273, 1991.

[43] Yetter, D.N., 1990, "Quantales and (noncommutative) linear logic Journal of Symbolic Logic, 55(1): 41-64.





Похожие работы:

«Содержание 1 Организационно-правовое обеспечение образовательной деятельности 2 Структура подготовки магистров 3 Содержание подготовки магистров 3.1. Анализ рабочего учебного плана и рабочих учебных программ 3.2 Организация учебного процесса 3.3 Информационно-методическое обеспечение учебного процесса 3.4 Воспитательная работа 4 Качество подготовки магистров 4.1 Анализ качества знаний студентов по результатам текущей и промежуточной аттестации. 15 4.2 Анализ качества знаний по результатам...»

«СБОРНИК РАБОЧИХ ПРОГРАММ Магистерская программа: Системы автоматизированного проектирования Содержание Страница М.1.1 Интеллектуальные системы 2 М.1.2 Методы оптимизации 9 М.1.3 Модели и методы анализа проектных решений 17 М.1.4 Промышленная логистика 25 М.1.5.1 Геометрическое моделирование в САПР 35 М.1.5.2 Модели дискретных процессов в САПР 44 М.2.1 Вычислительные системы 56 М.2.2 Технология разработки программного обеспечения 64 М.2.3 Современные проблемы информатики и вычислительной техники...»

«Введение в концепцию логического программирования. Лекция 1. Специальности : 230105, 010501 Концепция логического программирования. Логическое программирование – один из подходов к информатике, при котором в качестве языка высокого уровня используется логика предикатов первого порядка в форме фраз Хорна. Языки логического программирования (рис. 1) являются языками более высокого уровня, чем алгоритмические (Паскаль, Си) и функциональные (Лисп, CLOS). Терминология логического программирования...»

«1 1. Цель освоения дисциплины Дисциплина Геоинформационные системы формирует у обучающихся студентов-специалистов очной формы обучения знания и практические навыки в создании и ведении геоинформационных систем (ГИС), а также вырабатывает компетенции, которые дают возможность профессионально участвовать в производственно-технологической, проектной и организационно-управленческой деятельности. Цель изучения дисциплины Геоинформационные системы – формирование у студентов: – материалистического...»

«Федеральное агентство связи Федеральное государственное образовательное бюджетное учреждение высшего профессионального образования Поволжский государственный университет телекоммуникаций и информатики Кафедра философии Конспект лекций по учебной дисциплине ИСТОРИЯ по всем направлениям подготовки бакалавров Часть I. Из тумана далекого прошлого к Российской империи (I тысячелетие – XVII в.) Самара – 2012 УДК Ипполитов Г. М. История. Конспект лекций: В IV частях. Часть I. Из тумана далекого...»

«“School Goes Digital” -1Преподавание физики в школах, академических лицеях и ВУЗах с использованием информационно-компьютерных технологий Лилия Владимировна Николенко, координатор по вопросам электронного образования пилотной инициативы “School Goes Digital” Интернет-проекта UNDP E-mail: iqmena@edunet.uz Физическая наука всегда лежит в первооснове всех достижений человеческой цивилизации, компьютерная техника и Интернет не исключение. Однако зачастую складывается парадоксальная ситуация, когда...»

«Анатолий Ефимович Тарас Боевая машина: Руководство по самозащите — 2 Боевая машина – 2 Боевая машина: Руководство по самозащите: Харвест; Минск; 1997 ISBN 985-433-162-8 Аннотация В этой книге исчерпывающим образом раскрыты проблемы психологии, тактики и техники самообороны от хулиганских и преступных посягательств. Главный акцент сделан при этом на выработке умения входить в надлежащее психическое состояние и на использовании в качестве оружия не только своего тела, но и различных предметов,...»

«2 СОДЕРЖАНИЕ 1. ОРГАНИЗАЦИОННО-МЕТОДИЧЕСКИЙ РАЗДЕЛ 1.1. Цель государственного экзамена 1.2. Процедура проведения государственного экзамена 2. СОДЕРЖАНИЕ ПРОГРАММЫ ГОСУДАРСТВЕННОГО ЭКЗАМЕНА. 7 2.1. Вопросы к государственному экзамену 2.2. Образец экзаменационного билета 3. СПИСОК ИСПОЛЬЗУЕМОЙ ЛИТЕРАТУРЫ ДЛЯ ПОДГОТОВКИ К ГОСУДАРСТВЕННОМУ ЭКЗАМЕНУ 3 1. ОРГАНИЗАЦИОННО-МЕТОДИЧЕСКИЙ РАЗДЕЛ 1.1. Цель государственного экзамена Государственный экзамен по специальности 080801.65 Прикладная информатика в...»

«ІІ. ІСТОРІЯ ФІЛОСОФІЇ Клаус Вигерлинг (Германия)1 К ЖИЗНЕННОЙ ЗНАЧИМОСТИ ФИЛОСОФИИ – ПО ПОВОДУ ОДНОГО СТАРОГО ФИЛОСОФСКОГО ВОПРОСА В статье производится ревизия современного состояния философии, анализируется её значение на основании философского анализа умозаключений, сделанных Гуссерлем, Хёсле. Данная статья подготовлена на основе двух докладов, которые были сделаны в университете Баня-Лука (Босния-Герцоговина). Ключевые слова: философия, жизненный мир, первоосновы, современное состояние...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ МОСКОВСКОЙ ОБЛАСТИ АКАДЕМИЯ СОЦИАЛЬНОГО УПРАВЛЕНИЯ АНАЛИЗ РЕЗУЛЬТАТОВ ЕДИНОГО ГОСУДАРСТВЕННОГО ЭКЗАМЕНА ПО ПРЕДМЕТАМ ПО ВЫБОРУ НА ТЕРРИТОРИИ МОСКОВСКОЙ ОБЛАСТИ В 2013 ГОДУ Сборник методических материалов АСОУ 2013 Анализ результатов единого государственного экзамена по предметам по выбору на территории Московской области в 2013 г.: Сборник методических материалов. – М.: АСОУ, 2013. – 178 с. Сборник содержит анализ результатов единого государственного экзамена 2013 г. на...»

«1. Цель и задачи дисциплины 1.1. Цель изучения дисциплины Правовая информатика и кибернетика Учебный курса Правовая информатика и кибернетика предназначен для студентов юридического факультета Кубанского государственного аграрного университета, изучение дисциплины, согласно календарно-тематическому плану, предусмотрено на 4 курсе очной и заочной форм обучения по направлению подготовки 030501.65 юриспруденция, степень (квалификация) специалист. Основной целью преподавания курса Правовая...»

«Высшее профессиональное образование БАКАЛАВРИАТ И. Ю. БАЖЕНОВА ЯЗЫКИ ПРОГРАММИРОВАНИЯ Под редакцией профессора В. А. Сухомлина Учебник для студентов учреждений высшего профессионального образования, обучающихся по направлениям Фундаментальная информатика и информационные технологии и Информационная безопасность 1 УДК 004.43(075.8) ББК 32.973-018.1я73 Б163 Р е ц е н з е н т ы: профессор кафедры педагогических технологий и методики обучения Московского государственного гуманитарного университета...»

«:гентство овязи Федора_ттьное € еверо -1{авказский филиа_тт государственного образовательного бтодкетного г{рех(дения федера-тльного вь1с1пего профоссионального образования ]!1осковского технического университота связи и информатики смк_о-1.02-01-14 скФ мтуси смк_о_1.02-01'!4 Фтчёт о самообследовании утввРкдА!о мтуси Аир9крр скФ мецко отчвт самообследовании скФ мтуси смк_о_1.02-0|- Берсия 1. Ростов-на-Аону ]- / Фамшлия/|1одппсь Аата.(олэкность [.[1.Беленький щ }Р ?а/4а. €оставил }ам....»

«Международный консорциум Электронный университет Московский государственный университет экономики, статистики и информатики Евразийский открытый институт И.А. Киселева Моделирование рисковых ситуаций Учебно-практическое пособие Москва 2007 1 519.86 УДК 65.050 ББК 44 К Киселева И.А. МОДЕЛИРОВАНИЕ РИСКОВЫХ СИТУАЦИЙ: Учебно-практическое пособие / Евразийский открытый институт. – М.: МЭСИ, 2007. – 102 с. Данное пособие предназначено для студентов экономических вузов. Большое внимание в нем уделено...»

«5 марта 2008 года N 205-ПК ПЕРМСКИЙ КРАЙ ЗАКОН О БИБЛИОТЕЧНОМ ДЕЛЕ В ПЕРМСКОМ КРАЕ Принят Законодательным Собранием Пермского края 21 февраля 2008 года Настоящий Закон является правовой основой организации, сохранения и развития библиотечного дела в Пермском крае, устанавливает принципы деятельности библиотек, гарантирующие права человека на свободный доступ к информации, духовное развитие, приобщение к ценностям национальной и мировой культуры, а также на культурную, научную, образовательную и...»

«КООРДИНАЦИЯ И САМООРГАНИЗАЦИЯ В МНОГОАГЕНТНЫХ СИСТЕМАХ В.И.Городецкий Санкт-Петербургский институт информатики и автоматизации РАН Лаборатория интеллектуальных систем В.Городецкий. Координация и самоорганизация в МАС, Поспеловские чтения (декабрь 2009) Содержание 1. Принципы и методы координации поведения агентов МАС. Примеры: Управление воздушным движением и др. 2. Введение: самоорганизация, эмерджентность, принципы самоорганизации 3. Самоорганизация в многоагентных системах 4. Примеры...»

«Федеральное агентство по здравоохранению и социальному развитию ФГУ Центральный научно-исследовательский институт организации и информатизации здравоохранения Росздрава Оценка эпидемической ситуации по туберкулезу и анализ деятельности противотуберкулезных учреждений (Пособие для врачей фтизиатров и пульмонологов) Москва, 2007 2 УДК ББК ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ЗДРАВООХРАНЕНИЮ И СОЦИАЛЬНОМУ РАЗВИТИЮ ФГУ ЦЕНТРАЛЬНЫЙ НАУЧНО-ИССЛЕДОВАТЕЛЬСКИЙ ИНСТИТУТ ОРГАНИЗАЦИИ И ИНФОРМАТИЗАЦИИ ЗДРАВООХРАНЕНИЯ...»

«Уход за детьми Первого года жизни Справочник для молодых родителей Данное издание предназначено для молодых родителей. В нем можно найти советы по уходу за ребенком в течение первого года жизни, рекомендации о том, что делать при первых заболеваниях, что делать и куда обращаться за помощью, информацию о службах и услугах Региональной Санитарной Службы, о присутствии культурных посредников-переводчиков в Семейных консультациях и Отделениях, помогающих молодым мамам-иностранкам и семьям...»

«МИНИСТЕРСТВО ЗДРАВООХРАНЕНИЯ РФ НИЖЕГОРОДСКИЙ ГОСУДАРСТВЕННЫЙ МЕДИЦИНСКИЙ ИНСТИТУТ А.В. СУВОРОВ АЯ ИЧЕСК КЛИН Я ГРАФИ ИО ОКАРД Р ЭЛЕКТ Издательство НГМИ НИЖНИЙ НОВГОРОД, 1993 Киев – 1999 УДК 616.12–008.3–073.96 Суворов А. В. Клиническая электрокардиография. – Нижний Новгород. Изд-во НМИ, 1993. 124 с. Илл. Книга Суворова А. В. является хорошим, полным пособиемучебником для врачей кардиологов, терапевтов и студентов старших курсов мединских институтов по всем разделам электрокардиографии....»

«ТУБЕРКУЛЕЗ В РОССИЙСКОЙ ФЕДЕРАЦИИ 2011 г. Аналитический обзор статистических показателей, используемых в Российской Федерации и в мире Москва 2013 УДК 616-002.5-312.6(047) ББК 55.4 Т81 Т81 Туберкулез в Российской Федерации 2011 г. Аналитический обзор статистических показателей, используемых в Российской Федерации и в мире. – М., 2013. – 280 с. Аналитический обзор является совместным изданием Министерства здравоохранения Российской Федерации, Федерального государственного бюджетного учреждения...»














 
© 2014 www.kniga.seluk.ru - «Бесплатная электронная библиотека - Книги, пособия, учебники, издания, публикации»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.