Каковы различия между логическими отношениями и симуляциями?

29

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

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

Хунцзин Лян
источник
1
Возможно, вы захотите предоставить ссылки на эти статьи, которые вы прочитали. Это бы прояснило, какие конкретные примеры сбивают вас с толку.
Марк Хаманн
1
Для логических отношений я прочитал недавнюю статью Хура и Дрейера «Логическое отношение Крипке между ML и сборкой» (POPL'11). Также я прочитал классические главы в книге Пирса "Продвинутые темы в типах и языках программирования". Я считаю, что логические отношения определяются индуктивно в структуре типов языка, но что, если язык не имеет структуры типов (например, C)? (Кажется, это еще один вопрос.)
Хунцзинь Лян
1
Для моделирования я прочитал оригинальную статью «Алгебраические законы недетерминизма и параллелизма» Хеннесси и Милнера. Кутавас и Ванд "Маленькие противоречия для рассуждений о императивных программах высшего порядка" (POPL'06) для меня непостижимы, и я не уверен, почему они назвали свой метод "бисимуляцией".
Хунцзинь Лян
3
было бы лучше, если бы вы включили информацию, которую вы предоставили в комментариях в посте. Вы можете редактировать свой вопрос, нажав на ссылку редактирования под вопросом.
Каве
1
@HongjinLiang: Если у вас нет структуры типов (или если у вас есть рекурсивные типы), вы можете использовать пошаговые индексированные логические отношения - с логическими отношениями вы используете индукцию по типам, а с пошаговой индексацией вы делаете индукцию по шагам наблюдения. Вы найдете указатели в исследовательском отчете Амала Ахмеда: ccs.neu.edu/home/amal/ahmed-research.pdf . (Еще один обзор исследований логических отношений - это доклад Дерека Дрейера и его исследовательское заявление: mpi-sws.org/~dreyer/research.pdf ).
Blaisorblade

Ответы:

20

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

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

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

Милнер подхватил эту идею в малоизвестной, но очень фундаментальной статье под названием « Алгебраическое понятие симуляции между программами » в 1971 году. Хоар знал об этом и использовал ее, придумав « Доказательство правильности представлений данных » в 1972 году (но использовал функции абстракции вместо отношений, потому что он думал, что они были "проще"). Позже он отозвал утверждение о простоте и вернулся к использованию отношений в « Уточнение уточнения данных ». Рейнольдс использовал реляционные рассуждения в « Ремесле программирования»Глава 5 (1981). Он думал, что отношения были более естественными и общими, чем функции абстракции. Если вы вернетесь и прочитаете эту главу, вы обнаружите, что идеи реляционной параметризации скрываются в ожидании открытия. Конечно же, два года спустя, Рейнольдс опубликовал «Типы, абстракции и параметрический полиморфизм» (1983).

Похоже, что все эти идеи не имеют ничего общего с типами, но они действительно имеют. Языки и модели с состоянием имеют встроенную абстракцию данных. Вам не нужно определять «абстрактный тип данных», чтобы скрыть информацию. Вы просто объявляете локальную переменную и скрываете ее. Мы можем научить его первокурсникам на уроках Java в первые несколько недель. Нет пота.

MMMMXXRF(X)F(X)F(R)

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

А как насчет логических отношений тогда? На первый взгляд логические отношения представляются более общей идеей. В то время как параметричность говорит о том, как связать переменные типа в одной и той же модели, логические отношения, по-видимому, связывают типы в разных моделях. (Дейв Кларк написал блестящее изложение этого ранее.) Но я чувствую (и это все еще необходимо продемонстрировать), что это пример какой-то формы параметричности высшего типа, которая еще не сформулирована. Оставайтесь с нами для большего прогресса в этом направлении.


[Примечание добавлено] Связь между логическими отношениями и симуляциями обсуждается в нашей недавней статье « Логические отношения и параметризация: программа Рейнольдса для теории категорий и языков программирования» .

Удай Редди
источник
F(R)Rfunctor F
FR:XXF(R):F(X)F(X)F(R)F(R)
14

Одно из ключевых отличий состоит в том, что логические отношения используются в качестве метода для показа того, что класс программ (например, входные данные для компилятора) соответствуют другому классу программ (например, выходным данным компилятора), тогда как используются отношения моделирования показать соответствие между двумя программами.

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

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

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

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

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

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

Дэйв Кларк
источник
Большое спасибо за ваше подробное объяснение! Я прочитаю ваши рекомендации и постараюсь выяснить, какие глубокие связи / различия между ними.
Хунцзинь Лян
Вы уверены в утверждении «Вы показываете, что программа P и симуляция программы Q и эта программа Q могут симулировать программу P, и у вас есть бисимуляция?»? Пусть A = (a. (B + c)) + (a.b + ac) и B = a.b + ac, когда, насколько я могу судить, A похож на B, B похож на A, но A и Б не бизоподобны.
Андрас Саламон
@ Андрас: Вы правы. Мое утверждение недостаточно точное. Разница устраняется фразой «Могут присутствовать некоторые дополнительные условия».
Дейв Кларк
Хеннесси и Милнер определили три вида отношений эквивалентности в своей первоначальной статье для бисимуляции и привели несколько примеров, чтобы проиллюстрировать их различия. Ваше оригинальное утверждение на самом деле является средним в их статье, которое слабее, чем бисимуляция, и сильнее, чем следовая эквивалентность. Я не уверен, какая эквивалентность лучше. Может быть, это зависит от практического использования.
Хунцзин Лян
Моделирование также используется в качестве метода доказательства для уточнения данных между двумя типами данных. Каждое из этих имитационных доказательств относится к целым классам программ. Смотрите, например, [1] для деталей. Это говорит о том, что различие между этими двумя понятиями еще более размыто. [1]: CAR Hoare, He J и JW Sanders. Уточнение в уточнении данных. Письма Обработки Информации , 25: 71-76, 1987.
Кай
8

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

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

Самсон Абрамский использовал логические отношения для доказательства правильности и прекращения анализа строгости для ленивого лямбда-исчисления ( Абстрактная интерпретация, Логические отношения и Кан-расширения ). Он также показал, что логические отношения определяют функции абстракции в смысле связи Галуа абстрактной интерпретации. Совсем недавно Backhouse и Backhouse показали, как построить соединения Galois для типов высшего порядка из соединений Galois для базовых типов, и что эти конструкции могут быть эквивалентно описаны с помощью логических отношений ( Logical Relations и Galois Connections ). Таким образом, в конкретном контексте типизированных функциональных языков эти два понятия эквивалентны.

Имитационные отношения характеризуют сохранение свойств между структурами Крипке для различных модальных и временных логик. Вместо типов у нас есть модальности в логике. Симуляционные отношения также определяют связи Галуа и, следовательно, абстракции. Можно спросить, имеют ли эти абстракции специальные свойства. Ответ заключается в том, что стандартные абстракции являются надежными, а абстракции, основанные на отношениях моделирования, завершены. Понятие полноты относится к связям Галуа, которые могут не совпадать с интуитивной интерпретацией. Это направление работы было разработано Дэвидом Шмидтом ( Структурно-сохраняющие бинарные отношения для абстракции программы ), а также Франческо Ранзато и Франческо Таппаро ( Обобщенное сильное сохранение посредством абстрактной интерпретации ).

Виджай Д
источник
Ваш ответ очень полезен, чтобы связать понятия с абстрактной интерпретацией. Спасибо!
Хунцзинь Лян
Искренний вопрос: я не эксперт, но разве Рейнольдс (1983, «Типы, абстракция и параметрический полиморфизм») уже не определяет логические отношения, которые являются связями Галуа (Раздел 6)? Единственные различия, которые я замечаю: он не произносит термин «связь Галуа», а только эквивалентные «сопряженные функторы между частичными порядками, рассматриваемыми как категории», и он ограничивает области. OTOH, Backhouse и Backhouse ссылаются на Рейнольдса, но не обсуждают это утверждение, так или иначе.
Blaisorblade
6

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

π

Мартин Бергер
источник
Ваша ссылка действительно хороша! Я не слышал логических отношений для параллельных программ раньше. Спасибо! Я предполагаю, что сложность определения логического отношения заключается в поиске структуры типов. При одинаковой структуре типов логические отношения могут быть определены между различными языками программирования. С другой стороны, для моделирования требуются программы моделирования с помощью системы перехода состояний, что может быть непросто, если программы написаны для разных моделей состояний.
Хунцзин Лян
Здравствуйте! Да, найти подходящую структуру типов не всегда легко. Вы можете определить симуляции, используя разные системы переходов для двух исчислений, которые вы хотите сравнить. Можно утверждать, что определение слабого моделирования делает именно это. Все, что вам действительно нужно для определения симуляции, это отношение для сравнения меток перехода.
Мартин Бергер