Usos de quase-PERs / relações difuncionais / relações em zig-zag?

15

Dados os conjuntos e , uma relação difuncional entre eles é definida como uma relação que satisfaz a seguinte propriedade:AB ()A×B

Se e e , então . abababab

Relações difuncionais são uma generalização do conceito de relações de equivalência parcial que permitem definir uma noção de igualdade a partir de diferentes conjuntos. Como resultado, eles também são conhecidos como quase-PERs (QPERs) e também são conhecidos como relações em zig-zag, devido à seguinte imagem:foto de um ziguezague

Estou escrevendo um artigo que os utiliza, mas tive problemas para localizar boas referências para uso em semântica.

  1. Martin Hoffman os utiliza na correção de transformações de programas baseados em efeitos .
  2. Eu já vi menções (mas nenhuma boa referência) alegando que Tennant e Takeyama também propuseram seu uso.

Eles são uma idéia tão bonita que tenho dificuldade em acreditar que meu uso particular deles seja original. Eu realmente aprecio quaisquer outras referências.

Neel Krishnaswami
fonte
Johan van Benthem usou o termo relações em zigue-zague em sua dissertação para uma noção diferente, semelhante à bisimulação.
Vijay D
Aqueles que se perguntam como Neel usou QPERs (como eu) podem querer ver "Internalizando a parametridade relacional no cálculo extensional de construções" dele e de Dreyer.
Blaisorblade

Respostas:

8

Makoto Takeyama e eu enviamos o seguinte para [email protected] em 5 de janeiro de 1996:

Assunto: o que é uma relação de refinamento de dados?

Querido pessoal: alguém ainda está interessado no refinamento de dados?

Recentemente, Mak e eu estivemos analisando novamente uma idéia que consideramos há muitos meses. A motivação é caracterizar as relações lógicas relevantes para mostrar o refinamento dos dados. Isso foi estimulado pela constatação de que relações lógicas podem ser usadas para mostrar "segurança" de interpretações abstratas (consulte a Seção 2.8 do capítulo de Jones e Nielson no volume 4 do Handbook of Logic in CS), mas essas relações são mais gerais do que aqueles usados ​​para mostrar refinamento de dados.

Meu raciocínio é o seguinte. Se uma relação R está estabelecendo um refinamento de dados entre conjuntos (entre), deve estar induzindo relações de equivalência (parcial) em cada um dos conjuntos, com essas classes de equivalência na correspondência um a um e todos os elementos de uma classe de equivalência deve estar relacionado a todos os elementos das classes de equivalência correspondentes nos outros domínios de interpretação. A ideia é que cada classe de equivalência represente um valor "abstrato"; em uma interpretação totalmente abstrata, as classes de equivalência são singletons.

Podemos fornecer uma condição simples para garantir que uma relação n-ária R induza essa estrutura. Defina v ~ v 'no domínio V se existir um valor x em algum outro domínio X (e valores arbitrários ... nos outros domínios), de modo que R (..., v, ..., x, ... ) e R (..., v ', ..., x, ...). Isso define relações simétricas em cada um dos domínios. A imposição de transitividade local nos daria pers em cada domínio, mas isso não seria suficiente porque queremos garantir a transitividade nas interpretações. A seguinte condição alcança isso: se v_i ~ v'_i para todos os i, então R (..., v_i, ...) iff R (..., v'_i, ...) eu chamo isso de "zig- perfeição zag "; no caso n = 2, diz que se R (a, c) e R (a ', c') então R (a, c ') e se R (a', c).

Proposição. Se R e S são relações completas em zigue-zague, também são R x S e R -> S.

Proposição. Suponha que t e t 'são termos do tipo th no contexto pi, e R é uma relação lógica completa em zigue-zague; então, se o julgamento de equivalência t = t 'for interpretado da seguinte maneira:

para todos os u_i em V_i [[pi]],
R ^ {pi} (..., u_i, ...) implica que, para todos os i, V_i [[t]] u_i ~ V_i [[t ']] u_i

essa interpretação satisfaz os axiomas e regras usuais da lógica equacional.

A intuição aqui é que os termos devem ser "equivalentes", tanto dentro de uma única interpretação (V_i) quanto entre interpretações; isto é, os significados de t e t 'estão na mesma classe de equivalência induzida por R, independentemente da interpretação usada.

Questões:

  1. Alguém já viu esse tipo de estrutura antes?

  2. Quais são as generalizações naturais dessas idéias para outras proposições e categorias semânticas "arbitrárias"?

Bob Tennent [email protected]

Bob Tennent
fonte
6

Não conheço o campo da semântica, mas o conceito que você menciona é crucial na complexidade da contagem.

RRmm(x,y,y)=m(y,y,x)=xxy

FF

ΓΓΓΓ

Tyson Williams
fonte
Mais precisamente, o conceito é equivalente a ter um polimorfismo de Mal'tsev para relações binárias, mas ter um polimorfismo de Mal'tsev naturalmente pode ser aplicado a qualquer aridade, enquanto essa formulação é específica para relações binárias. Além disso, apenas para enfatizar: isso não se aplica apenas à contagem, mas a qualquer estudo algébrico de classes de relações. Por exemplo, os polimorfismos de Mal'tsev são cruciais no estudo de linguagens de restrição tratáveis ​​(que são classes de relações), mesmo na ausência de considerações de contagem.
András Salamon
@ AndrásSalamon Minha resposta é sobre relações ternárias, não binárias. Como você define um polimorfismo de Mal'tsev para outras relações que não o ternário?
Tyson Williams
Um polimorfismo é aplicado componente a componente. A aridade das tuplas não importa.
András Salamon
k3
Não sei ao que você está objetando, mas disse que " ter um polimorfismo de Mal'tsev" pode ser aplicado a qualquer aridade.
András Salamon