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

Dados os conjuntos e , uma relação difuncional entre eles é definida como uma relação que satisfaz a seguinte propriedade:$A$$B$ $(\sim) \subseteq A \times B$

Se e e , então . $a \sim b$$a' \sim b'$$a \sim b'$$a' \sim b$

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:

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.

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]

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

R$R$$R$$R$$m$$m(x,y,y) = m(y,y,x) = x$$x$$y$

$\mathcal{F}$$\mathcal{F}$

$\Gamma$$\Gamma$$\Gamma$$\Gamma$