Usos de cuasi-PER / relaciones difuncionales / relaciones en zig-zag?

15

Dados los conjuntos y , una relación difuncional entre ellos se define como una relación que satisface la siguiente propiedad:UNsi ()UN×si

Si y y , entonces . unsiunsiunsiunsi

Las relaciones difuncionales son una generalización del concepto de relaciones de equivalencia parcial que permiten definir una noción de igualdad a partir de diferentes conjuntos. Como resultado, también se conocen como cuasi-PER (QPER), y también se conocen como relaciones en zig-zag, debido a la siguiente imagen:imagen de un zigzag

Estoy escribiendo un documento que los usa, pero he tenido problemas para localizar buenas referencias para su uso en semántica.

  1. Martin Hoffman los usa en la corrección de las transformaciones de programas basadas en efectos .
  2. He visto menciones (pero no buenas referencias) que afirman que Tennant y Takeyama también han propuesto su uso.

Son una idea tan bonita que tengo problemas para creer que mi uso particular de ellos es original. Realmente agradecería cualquier referencia adicional.

Neel Krishnaswami
fuente
Johan van Benthem usó el término relaciones en zig-zag en su disertación para una noción diferente similar a la bisimulación.
Vijay D
Aquellos que se preguntan cómo Neel usó QPERs (como yo) podrían querer ver "Internalización de la parametricidad relacional en el cálculo extensivo de construcciones" de él y Dreyer.
Blaisorblade

Respuestas:

8

Makoto Takeyama y yo enviamos lo siguiente a [email protected] el 5 de enero de 1996:

Asunto: ¿qué es una relación de refinamiento de datos?

Queridos: ¿alguien todavía está interesado en el refinamiento de datos?

Recientemente, Mak y yo hemos estado analizando nuevamente una idea que consideramos hace muchos meses. La motivación es caracterizar las relaciones lógicas relevantes para mostrar el refinamiento de datos. Esto se estimuló al darse cuenta de que las relaciones lógicas se pueden usar para mostrar la "seguridad" de las interpretaciones abstractas (vea la Sección 2.8 del capítulo de Jones y Nielson en el volumen 4 del Manual de lógica en CS), pero tales relaciones son más generales que aquellos utilizados para mostrar el refinamiento de datos.

Mi razonamiento es el siguiente. Si una relación R está estableciendo un refinamiento de datos entre (entre) conjuntos, entonces debe inducir relaciones de equivalencia (parciales) en cada uno de los conjuntos, con estas clases de equivalencia en correspondencia uno a uno, y cada elemento de una clase de equivalencia debe estar relacionado con todos los elementos de las clases de equivalencia correspondientes en los otros dominios de interpretación. La idea es que cada clase de equivalencia representa un valor "abstracto"; En una interpretación completamente abstracta, las clases de equivalencia son singletons.

Podemos dar una condición simple para asegurar que una relación n-aria R induzca esta estructura. Defina v ~ v 'en el dominio V si existe un valor x en algún otro dominio X (y valores arbitrarios ... en los otros dominios) tal que R (..., v, ..., x, ... ) y R (..., v ', ..., x, ...). Esto define relaciones simétricas en cada uno de los dominios. Imponer la transitividad local nos daría pers en cada dominio, pero esto no sería suficiente porque queremos asegurar la transitividad a través de las interpretaciones. La siguiente condición logra esto: si v_i ~ v'_i para todo i, entonces R (..., v_i, ...) iff R (..., v'_i, ...) Yo llamo a esto "zig- integridad de zag "; en el caso n = 2, dice que si R (a, c) y R (a ', c') entonces R (a, c ') iff R (a', c).

Proposición. Si R y S son relaciones completas en zig-zag, también lo son R x S y R -> S.

Proposición. Supongamos que t y t 'son términos de tipo th en contexto pi, y R es una relación lógica completa en zig-zag; entonces, si el juicio de equivalencia t = t 'se interpreta como sigue:

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

Esta interpretación satisface los axiomas y las reglas habituales para la lógica equitativa.

La intuición aquí es que los términos deben ser "equivalentes" tanto dentro de una única interpretación (V_i) como entre interpretaciones; es decir, los significados de t y t 'están en la misma clase de equivalencia inducida por R, sin importar qué interpretación se use.

Preguntas:

  1. ¿Alguien ha visto este tipo de estructura antes?

  2. ¿Cuáles son las generalizaciones naturales de estas ideas a otras proposiciones y categorías semánticas "arbitrarias"?

Bob Tennent [email protected]

Bob Tennent
fuente
6

No sé sobre el campo de la semántica, pero el concepto que mencionas es crucial en la complejidad de contar.

RRmetrometro(X,y,y)=metro(y,y,X)=XXy

FF

ΓΓΓΓ

Tyson Williams
fuente
Más precisamente, el concepto es equivalente a tener un polimorfismo de Mal'tsev para las relaciones binarias, pero tener un polimorfismo de Mal'tsev, naturalmente, se puede aplicar a cualquier aridad, mientras que esta formulación es específica de las relaciones binarias. Además, solo para enfatizar: esto no solo se aplica al conteo, sino a cualquier estudio algebraico de clases de relaciones. Por ejemplo, los polimorfismos de Mal'tsev son cruciales en el estudio de lenguajes de restricción manejables (que son clases de relaciones) incluso en ausencia de consideraciones de conteo.
András Salamon
@ AndrásSalamon Mi respuesta es sobre relaciones ternarias, no binarias. ¿Cómo define un polimorfismo de Mal'tsev para relaciones distintas a las ternarias?
Tyson Williams
Se aplica un polimorfismo componente. La aridad de las tuplas no importa.
András Salamon
k3
No estoy seguro de a qué se opone, pero le dije que " tener un polimorfismo de Mal'tsev" se puede aplicar a cualquier arity.
András Salamon