8

Makoto Takeyama and I sent the following to data-refinement@etl.go.jp on Jan 5, 1996: Subject: what is a data refinement relation? Dear all: anyone still interested in data refinement? Recently Mak and I have been looking again at an idea we considered many months ago. The motivation is to characterize the logical relations relevant to ...


6

The second paragraph of Plotkin's 1973 Memo on Lambda-definability and Logical Relations says this: "The definition of logical [relation] is derived from a corresponding one of M. Gordon for the typed λ-calculus." This doesn't say explicitly that the term was coined by Gordon. But, given that the memo is titled "Lambda-definability and logical ...


2

In the months since I asked this question, I think I have found a sensible answer. Often, the type of relations considered do not compose. For instance, if your notion of a relation $R : D \to E$ between $\omega$CPOs is an $\omega$-chain complete subset of $|D|\times |E|$, then the relation $R : \omega + 1 \to \mathbb{N}$ between the ordered naturals plus ...


2

I guess the main reason why you could not find anything about this is that it is rarely needed (and can be reduced to the better-known boolean operations, as you noted). Checking language equivalence of two automata is close, but there you don't necessarily want to compute the symmetric difference exactly, just check whether it is empty. One way of ...


Only top voted, non community-wiki answers of a minimum length are eligible