Zastosowania quasi-PER / relacji dwufunkcyjnych / relacji zygzakowatych?

Biorąc pod uwagę zbiory i B , relacja difunkcyjna ( ∼ ) ⊆ A × B między nimi jest zdefiniowana jako relacja spełniająca następującą właściwość:$A$$B$ $(\sim) \subseteq A \times B$

Jeżeli oraz a ′ ∼ b ′ i a ∼ b ′ , to a ′ ∼ b . $a \sim b$$a' \sim b'$$a \sim b'$$a' \sim b$

Relacje difunkcyjne są uogólnieniem pojęcia relacji częściowej równoważności, które pozwalają zdefiniować pojęcie równości z różnych zbiorów. W rezultacie są one również znane jako quasi-PER (QPER) i są również znane jako relacje zygzakowate, z powodu następującego obrazu:

Piszę artykuł, który ich używa, ale miałem problem ze znalezieniem dobrych referencji pod kątem ich zastosowania w semantyce.

1. Martin Hoffman wykorzystuje je w poprawności transformacji programów opartych na efektach .
2. Widziałem wzmianki (ale bez dobrych referencji) twierdzące, że Tennant i Takeyama również zaproponowali ich użycie.

Są tak ładnym pomysłem, że nie mogę uwierzyć, że moje szczególne użycie ich jest oryginalne. Byłbym bardzo wdzięczny za wszelkie dalsze referencje.

Makoto Takeyama i ja wysłaliśmy następujące dane na [email protected] w dniu 5 stycznia 1996 r .:

Temat: czym jest relacja udoskonalenia danych?

Szanowni Państwo: ktoś nadal jest zainteresowany udoskonalaniem danych?

Ostatnio Mak i ja ponownie zastanawialiśmy się nad pomysłem, który rozważaliśmy wiele miesięcy temu. Motywacją jest scharakteryzowanie logicznych relacji związanych z udoskonalaniem danych. Stymulowało to uświadomienie sobie, że relacji logicznych można użyć do wykazania „bezpieczeństwa” abstrakcyjnych interpretacji (patrz sekcja 2.8 rozdziału autorstwa Jonesa i Nielsona w tomie 4 Podręcznika logiki w CS), ale takie relacje są bardziej ogólne niż używane do pokazywania zawężenia danych.

Moje rozumowanie jest następujące. Jeśli relacja R ustanawia uściślenie danych między (między) zbiorami, to musi indukować (częściowe) relacje równoważności na każdym ze zbiorów, przy czym te klasy równoważności w korespondencji jeden do jednego i każdy element klasy równoważności muszą być powiązane ze wszystkimi elementami odpowiednich klas równoważności w innych dziedzinach interpretacji. Chodzi o to, że każda klasa równoważności reprezentuje wartość „abstrakcyjną”; w całkowicie abstrakcyjnej interpretacji klasy równoważności są singletonami.

Możemy podać prosty warunek, aby zapewnić, że n-arynowa relacja R indukuje tę strukturę. Zdefiniuj v ~ v 'w domenie V iff istnieje wartość x w innej domenie X (i dowolne wartości ... w innych domenach) taka, że ​​R (..., v, ..., x, ... ) i R (..., v ', ..., x, ...). Definiuje to symetryczne relacje w każdej z domen. Nałożenie lokalnej przechodniości dałoby nam pers w każdej domenie, ale to nie wystarczyłoby, ponieważ chcemy zapewnić przechodniość w różnych interpretacjach. Osiąga to następujący warunek: jeśli v_i ~ v'_i dla wszystkich i, to R (..., v_i, ...) iff R (..., v'_i, ...) Nazywam to „zig- zag kompletność "; w przypadku n = 2 oznacza, że ​​jeśli R (a, c) i R (a ', c') to R (a, c ') iff R (a', c).

Propozycja. Jeśli R i S są zygzakowatymi pełnymi relacjami, to też R x S i R -> S.

Propozycja. Załóżmy, że t i t 'są terminami typu th w kontekście pi, a R jest zygzakowatą kompletną relacją logiczną; wówczas, jeżeli osąd równoważności t = t 'interpretuje się w następujący sposób:

dla wszystkich u_i w V_i [[pi]],
R ^ {pi} (..., u_i, ...) oznacza, że ​​dla wszystkich u, V_i [[t]] u_i ~ V_i [[t ']] u_i

interpretacja ta spełnia zwykłe aksjomaty i reguły logiki równań.

Intuicja polega na tym, że terminy mają być „równoważne” zarówno w ramach jednej interpretacji (V_i), jak i interpretacji; tj. znaczenia t i t 'są w tej samej klasie równoważności indukowanej przez R, niezależnie od zastosowanej interpretacji.

Pytania:

1. Czy ktoś już widział taką strukturę?

2. Jakie są naturalne uogólnienia tych pomysłów na inne zdania i „arbitralne” kategorie semantyczne?

Bob Tennent [email protected]

Nie wiem o dziedzinie semantyki, ale wspomniana koncepcja jest kluczowa w złożoności liczenia.

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

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

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