Использует квази-PER / дифункциональные отношения / зигзагообразные отношения?

15

С учетом множество и , A бифункционального соотношение между ними определяются как отношение , удовлетворяющее следующее свойство:B ( ) A × BAВ ()A×B

Если и a b и a b , то a b . abababaб

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

Я пишу статью, которая использует их, но у меня были проблемы с поиском хороших ссылок для их использования в семантике.

  1. Мартин Хоффман использует их в « Правильности трансформации программ на основе эффектов» .
  2. Я видел упоминания (но нет хороших ссылок), утверждающих, что Теннант и Такеяма также предложили их использование.

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

Нил Кришнасвами
источник
Йохан ван Бентем использовал термин зигзагообразные отношения в своей диссертации для другого понятия, похожего на бисимуляцию.
Виджай Д
Те, кто интересуется, как Нил использовал QPER (как и я), возможно, захотят взглянуть на «Интернализацию реляционной параметричности в исчислении экстенсиональных конструкций» от него и Драйера.
Blaisorblade

Ответы:

8

Макото Такеяма и я отправили 5 января 1996 г. на data-refinement@etl.go.jp следующее:

Тема: что такое отношение уточнения данных?

Уважаемые: кто-нибудь еще заинтересован в уточнении данных?

Недавно мы с Маком снова рассматривали идею, которую мы рассматривали много месяцев назад. Мотивация состоит в том, чтобы характеризовать логические отношения, относящиеся к отображению уточнения данных. Это было стимулировано осознанием того, что логические отношения могут использоваться для демонстрации «безопасности» абстрактных интерпретаций (см. Раздел 2.8 главы Джоунса и Нильсона в томе 4 «Руководства по логике в CS»), но такие отношения являются более общими, чем те, которые используются для отображения уточнения данных.

Мои рассуждения звучат следующим образом. Если отношение R устанавливает уточнение данных между (среди) множествами, то оно должно вызывать (частичные) отношения эквивалентности на каждом из множеств с этими классами эквивалентности в взаимно-однозначном соответствии и каждым элементом класса эквивалентности. должны быть связаны со всеми элементами соответствующих классов эквивалентности в других областях интерпретации. Идея состоит в том, что каждый класс эквивалентности представляет «абстрактное» значение; в полностью абстрактной интерпретации классы эквивалентности являются синглетонами.

Мы можем дать простое условие, гарантирующее, что n-арное отношение R индуцирует эту структуру. Определите v ~ v 'в области V, если существует значение x в некоторой другой области X (и произвольные значения ... в других областях), такое, что R (..., v, ..., x, ... ) и R (..., v ', ..., x, ...). Это определяет симметричные отношения на каждой из областей. В этом случае наложение локальной транзитивности дало бы нам персону в каждой области, но этого было бы недостаточно, потому что мы хотим обеспечить транзитивность в разных интерпретациях. Следующее условие достигает этого: если v_i ~ v'_i для всех i, то R (..., v_i, ...) тогда и только тогда, когда R (..., v'_i, ...) я называю это "зиг- заг-полнота "; в случае n = 2 это говорит о том, что если R (a, c) & R (a ', c'), то R (a, c ') тогда и только тогда, когда R (a', c).

Предложение. Если R и S - зигзагообразные полные отношения, то R x S и R -> S.

Предложение. Предположим, что t и t 'являются терминами типа th в контексте pi, а R является зигзагообразным полным логическим отношением; тогда, если суждение об эквивалентности t = t 'интерпретируется следующим образом:

для всех u_i в V_i [[pi]],
R ^ {pi} (..., u_i, ...) подразумевает, что для всех i, V_i [[t]] u_i ~ V_i [[t ']] u_i

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

Интуиция здесь заключается в том, что термины должны быть «эквивалентными» как в пределах одной интерпретации (V_i), так и в разных интерпретациях; то есть значения t и t 'находятся в одном и том же классе индуцированной R-эквивалентности, независимо от того, какая интерпретация используется.

Вопросов:

  1. Кто-нибудь видел такую ​​структуру раньше?

  2. Каковы естественные обобщения этих идей для других положений и «произвольных» семантических категорий?

Боб Теннент rdt@cs.queensu.ca

Боб Теннент
источник
6

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

Я не видел отношения называемого дифункциональным отношениемррмм(Икс,Y,Y)знак равном(Y,Y,Икс)знак равноИксИксY

FF

ΓΓΓΓ

Тайсон Уильямс
источник
Точнее, концепция эквивалентна наличию полиморфизма Мальцева для бинарных отношений, но наличие полиморфизма Мальцева, естественно, может быть применено к любой арности, тогда как эта формулировка специфична для бинарных отношений. Также, чтобы подчеркнуть: это относится не только к счету, но и к любому алгебраическому изучению классов отношений. Например, полиморфизмы Мальцева имеют решающее значение при изучении управляемых языков ограничений (которые являются классами отношений) даже в отсутствие подсчета соображений.
Андрас Саламон
@ AndrásSalamon Мой ответ о тройных отношениях, а не о бинарных. Как вы определяете полиморфизм Мальцева для отношений, отличных от троичных?
Тайсон Уильямс
Полиморфизм применяется компонентно. Арктичность кортежей не имеет значения.
Андрас Саламон
К3
Я не уверен, против чего вы возражаете, но я сказал, что « наличие полиморфизма Мальцева» может быть применено к любой артерии.
Андрас Саламон,