Utilisations des quasi-PER / relations difonctionnelles / relations zig-zag?

15

Étant donné les ensembles et B , une relation difonctionnelle ( ) A × B entre eux est définie comme une relation satisfaisant la propriété suivante:UNEB ()UNE×B

Si et a b et a b , alors a b . unebunebunebuneb

Les relations difonctionnelles sont une généralisation du concept de relations d'équivalence partielle qui permettent de définir une notion d'égalité à partir de différents ensembles. En conséquence, ils sont également connus sous le nom de quasi-PER (QPER), et ils sont également connus sous le nom de relations en zig-zag, en raison de l'image suivante:photo d'un zigzag

J'écris un article qui les utilise, mais j'ai eu du mal à trouver de bonnes références pour leur utilisation en sémantique.

  1. Martin Hoffman les utilise dans l' exactitude des transformations de programme basées sur les effets .
  2. J'ai vu des mentions (mais pas de bonnes références) affirmant que Tennant et Takeyama ont également proposé leur utilisation.

Ils sont une si jolie idée que j'ai du mal à croire que mon utilisation particulière d'eux est originale. J'apprécierais vraiment toute autre référence.

Neel Krishnaswami
la source
Johan van Benthem a utilisé le terme relations en zig-zag dans sa thèse pour une notion différente similaire à la bisimulation.
Vijay D
Ceux qui se demandent comment Neel a utilisé les QPER (comme moi) voudront peut-être regarder "Internaliser la paramétricité relationnelle dans le calcul extensionnel des constructions" de lui et de Dreyer.
Blaisorblade

Réponses:

8

Makoto Takeyama et moi avons envoyé ce qui suit à [email protected] le 5 janvier 1996:

Objet: qu'est-ce qu'une relation d'affinement des données?

Cher tout le monde: quelqu'un est-il toujours intéressé par le raffinement des données?

Récemment, Mak et moi avons réexaminé une idée que nous avons envisagée il y a plusieurs mois. La motivation est de caractériser les relations logiques pertinentes pour montrer le raffinement des données. Cela a été stimulé par la prise de conscience que les relations logiques peuvent être utilisées pour montrer la «sécurité» des interprétations abstraites (voir la section 2.8 du chapitre de Jones et Nielson dans le volume 4 du Handbook of Logic in CS), mais ces relations sont plus générales que ceux utilisés pour montrer le raffinement des données.

Mon raisonnement est le suivant. Si une relation R établit un raffinement de données entre (parmi) ensembles, alors elle doit induire des relations d'équivalence (partielles) sur chacun des ensembles, avec ces classes d'équivalence en correspondance un à un, et chaque élément d'une classe d'équivalence doit être lié à tous les éléments des classes d'équivalence correspondantes dans les autres domaines d'interprétation. L'idée est que chaque classe d'équivalence représente une valeur "abstraite"; dans une interprétation entièrement abstraite, les classes d'équivalence sont des singletons.

On peut donner une condition simple pour s'assurer qu'une relation n-aire R induit cette structure. Définissez v ~ v 'dans le domaine V s'il existe une valeur x dans un autre domaine X (et des valeurs arbitraires ... dans les autres domaines) telles que R (..., v, ..., x, ... ) et R (..., v ', ..., x, ...). Ceci définit des relations symétriques sur chacun des domaines. Imposer la transitivité locale nous donnerait alors des pers sur chaque domaine, mais cela ne suffirait pas car nous voulons assurer la transitivité entre les interprétations. La condition suivante y parvient: si v_i ~ v'_i pour tout i, alors R (..., v_i, ...) ssi R (..., v'_i, ...) j'appelle cela "zig- zag complétude "; dans le cas n = 2, il dit que si R (a, c) & R (a ', c') alors R (a, c ') ssi R (a', c).

Proposition. Si R et S sont des relations complètes en zigzag, R x S et R -> S. le sont aussi.

Proposition. Supposons que t et t 'soient des termes de type th dans le contexte pi, et R est une relation logique complète en zig-zag; alors, si le jugement d'équivalence t = t 'est interprété comme suit:

pour tout u_i dans V_i [[pi]],
R ^ {pi} (..., u_i, ...) implique que, pour tout i, V_i [[t]] u_i ~ V_i [[t ']] u_i

cette interprétation satisfait les axiomes et les règles habituelles de la logique équationnelle.

L'intuition ici est que les termes doivent être "équivalents" à la fois au sein d'une même interprétation (V_i) et entre les interprétations; c'est-à-dire que les significations de t et t 'sont dans la même classe d'équivalence induite par R, quelle que soit l'interprétation utilisée.

Des questions:

  1. Quelqu'un a-t-il déjà vu ce genre de structure?

  2. Quelles sont les généralisations naturelles de ces idées à d'autres propositions et catégories sémantiques "arbitraires"?

Bob Tennent [email protected]

Bob Tennent
la source
6

Je ne connais pas le domaine de la sémantique, mais le concept que vous mentionnez est crucial dans la complexité du comptage.

Je n'ai pas vu de relation appelée relation difonctionnelleRRmm(X,y,y)=m(y,y,X)=XXy

FF

ΓΓΓΓ

Tyson Williams
la source
Plus précisément, le concept équivaut à avoir un polymorphisme de Mal'tsev pour les relations binaires, mais avoir un polymorphisme de Mal'tsev peut naturellement s'appliquer à n'importe quelle arité alors que cette formulation est spécifique aux relations binaires. Aussi, juste pour souligner: cela ne s'applique pas seulement au comptage, mais à toute étude algébrique des classes de relations. Par exemple, les polymorphismes de Mal'tsev sont cruciaux dans l'étude des langages de contraintes traitables (qui sont des classes de relations) même en l'absence de considérations de comptage.
András Salamon
@ AndrásSalamon Ma réponse concerne les relations ternaires, pas les relations binaires. Comment définissez-vous un polymorphisme de Mal'tsev pour des relations autres que ternaires?
Tyson Williams
Un polymorphisme est appliqué par composant. L'arité des tuples n'a pas d'importance.
András Salamon
k3
Je ne sais pas à quoi vous vous opposez, mais j'ai dit que " avoir un polymorphisme de Mal'tsev" peut être appliqué à n'importe quelle arité.
András Salamon