Verwendung von Quasi-PERs / difunktionellen Beziehungen / Zick-Zack-Beziehungen?

15

Bei gegebenen Mengen und B wird eine difunktionelle Beziehung ( ) A × B zwischen ihnen als eine Beziehung definiert, die die folgende Eigenschaft erfüllt:EINB ()A×B

Wenn und a 'b ' und a b ' , dann ist a 'b . ababeinbeinb

Difunktionale Beziehungen sind eine Verallgemeinerung des Konzepts der partiellen Äquivalenzbeziehungen, die es ermöglicht, einen Begriff der Gleichheit aus verschiedenen Mengen zu definieren . Infolgedessen werden sie auch als Quasi-PERs (QPERs) und aufgrund des folgenden Bildes auch als Zick-Zack-Beziehungen bezeichnet:Bild eines Zickzacks

Ich schreibe eine Arbeit, in der sie verwendet werden, aber ich hatte Probleme, gute Referenzen für ihre Verwendung in der Semantik zu finden.

  1. Martin Hoffman verwendet sie zur Korrektheit von effektbasierten Programmtransformationen .
  2. Ich habe Erwähnungen (aber keine guten Referenzen) gesehen, die behaupten, dass Tennant und Takeyama ihre Verwendung ebenfalls vorgeschlagen haben.

Sie sind so eine hübsche Idee, dass ich Schwierigkeiten habe zu glauben, dass meine besondere Verwendung von ihnen originell ist. Ich würde mich über weitere Referenzen sehr freuen.

Neel Krishnaswami
quelle
Johan van Benthem verwendete in seiner Dissertation den Begriff Zick-Zack-Beziehungen für einen anderen Begriff ähnlich der Bisimulation.
Vijay D
Diejenigen, die sich fragen, wie Neel (wie ich) QPERs verwendet hat, möchten vielleicht einen Blick auf "Internalizing Relational Parametricity in the Extensional Calculus of Constructions" von ihm und Dreyer werfen.
Blaisorblade

Antworten:

8

Makoto Takeyama und ich haben am 5. Januar 1996 Folgendes an [email protected] gesendet:

Betreff: Was ist eine Datenverfeinerungsbeziehung?

Sehr geehrte Damen und Herren, ist noch jemand an einer Datenveredelung interessiert?

Kürzlich haben Mak und ich uns wieder eine Idee angesehen, über die wir uns vor vielen Monaten Gedanken gemacht haben. Die Motivation besteht darin, die logischen Beziehungen zu charakterisieren, die für die Darstellung der Datenverfeinerung relevant sind. Dies wurde durch die Erkenntnis angeregt, dass logische Beziehungen verwendet werden können, um die "Sicherheit" abstrakter Interpretationen aufzuzeigen (siehe Abschnitt 2.8 des Kapitels von Jones und Nielson in Band 4 des Handbuchs der Logik in CS), aber solche Beziehungen sind allgemeiner als Diejenigen, die zur Anzeige der Datenverfeinerung verwendet wurden.

Meine Argumentation lautet wie folgt. Wenn eine Relation R eine Datenverfeinerung zwischen (zwischen) Mengen herstellt, muss sie (teilweise) Äquivalenzrelationen auf jeder der Mengen mit diesen Äquivalenzklassen in einer Eins-zu-Eins-Korrespondenz und jedem Element einer Äquivalenzklasse induzieren muss sich auf alle Elemente der entsprechenden Äquivalenzklassen in den anderen Interpretationsbereichen beziehen. Die Idee ist, dass jede Äquivalenzklasse einen "abstrakten" Wert darstellt; In einer vollständig abstrakten Interpretation sind die Äquivalenzklassen Singletons.

Wir können eine einfache Bedingung geben, um sicherzustellen, dass eine n-äre Beziehung R diese Struktur induziert. Definieren Sie v ~ v 'in Domäne V, falls in einer anderen Domäne X ein Wert x existiert (und in den anderen Domänen beliebige Werte ...), so dass R (..., v, ..., x, ... ) und R (..., v ', ..., x, ...). Dies definiert symmetrische Beziehungen für jede der Domänen. Die Durchsetzung der lokalen Transitivität würde uns dann für jede Domäne Pers geben, aber dies würde nicht ausreichen, da wir die Transitivität für alle Interpretationen sicherstellen möchten. Die folgende Bedingung erreicht dies: wenn v_i ~ v'_i für alle i, dann R (..., v_i, ...) wenn R (..., v'_i, ...) nenne ich dies "zickzack zack Vollständigkeit "; im Fall n = 2 heißt es, wenn R (a, c) & R (a ', c'), dann R (a, c '), wenn R (a', c).

Vorschlag. Wenn R und S Zick-Zack-Beziehungen sind, sind dies auch R x S und R -> S.

Vorschlag. Angenommen, t und t 'sind Terme vom Typ th im Kontext pi, und R ist eine vollständige logische Zick-Zack-Beziehung; dann, wenn die Äquivalenzbeurteilung t = t 'wie folgt interpretiert wird:

für alle u_i in V_i [[pi]]
impliziert R ^ {pi} (..., u_i, ...), dass für alle i V_i [[t]] u_i ~ V_i [[t ']] u_i

Diese Interpretation erfüllt die üblichen Axiome und Regeln für die Gleichungslogik.

Die Intuition hier ist, dass die Ausdrücke sowohl innerhalb einer einzigen Interpretation (V_i) als auch über Interpretationen hinweg "äquivalent" sein sollen; dh die Bedeutungen von t und t 'liegen in derselben R-induzierten Äquivalenzklasse, unabhängig davon, welche Interpretation verwendet wird.

Fragen:

  1. Hat jemand diese Art von Struktur schon einmal gesehen?

  2. Was sind die natürlichen Verallgemeinerungen dieser Ideen auf andere Sätze und "willkürliche" semantische Kategorien?

Bob Tennent [email protected]

Bob Tennent
quelle
6

Ich kenne mich mit Semantik nicht aus, aber das Konzept, das Sie erwähnen, ist entscheidend für die Komplexität des Zählens.

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

FF

ΓΓΓΓ

Tyson Williams
quelle
Genauer gesagt entspricht das Konzept einem Mal'tsev-Polymorphismus für binäre Beziehungen, aber ein Mal'tsev-Polymorphismus kann natürlich auf jede Arität angewendet werden, während diese Formulierung für binäre Beziehungen spezifisch ist. Nur um es zu betonen: Dies gilt nicht nur für das Zählen, sondern für jede algebraische Untersuchung von Beziehungsklassen. Zum Beispiel sind Mal'tsev-Polymorphismen auch ohne Berücksichtigung von Zählungsaspekten für das Studium von tractable constraint languages ​​(Klassen von Beziehungen) von entscheidender Bedeutung.
András Salamon
@ AndrásSalamon Meine Antwort bezieht sich auf ternäre Beziehungen, nicht auf binäre. Wie definieren Sie einen Mal'tsev-Polymorphismus für andere als ternäre Beziehungen?
Tyson Williams
Ein Polymorphismus wird komponentenweise angewendet. Die Anzahl der Tupel spielt keine Rolle.
András Salamon
k3
Ich bin mir nicht sicher, gegen was Sie Einwände erheben, aber ich sagte, dass " mit einem Mal'tsev-Polymorphismus" auf jede Arität angewendet werden kann.
András Salamon