Questions tagged [logical-relations]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
2
votes
0answers
70 views

What is the relation of parametricity and function extensionality?

In Agda function extensionality can be defined like this: funExt = {A : Set} {B : Set} {f1 f2 : A → B} → (∀ x1 x2 → x1 ≡ x2 -> f1 x1 ≡ f2 x2) → f1 ≡ f2 One may ...
11
votes
1answer
304 views

Why Reflexive Graphs for Parametricity?

Looking at models of parametric polymorphism, I am curious why are reflexive graph categories are used? In particular, why do they not include relational composition? In looking at the models, they ...
5
votes
0answers
85 views

Characterisation of the BCIW definable functions

Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.) I ...
-1
votes
1answer
1k views

How to XOR automata? [closed]

Say we have 3 DFAs. We know how to OR, AND, or NOT them. But how does one XOR them? There is not one single mention of this online. x XOR y XOR z = ((x|y)(~x|y)|z) (~((x|y)(~x|y))|z). This is way too ...
7
votes
2answers
816 views

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which ...
15
votes
2answers
393 views

Uses of quasi-PERs/difunctional relations/zig-zag relations?

Given sets $A$ and $B$, a difunctional relation $(\sim) \subseteq A \times B$ between them is defined to be a relation satisfying the following property: If $a \sim b$ and $a' \sim b'$ and $a \sim ...
15
votes
4answers
629 views

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( https://dl.acm.org/citation.cfm?id=2359499). In this paper, they internalize unary ...
16
votes
2answers
926 views

What is the origin of logical relations?

I actually have two questions: Who first used logical relations to relate semantics? I traced them back to Reynold's "On the Relation Between Direct and Continuation Semantics", but I can't claim to ...
31
votes
4answers
3k views

What are the differences between logical relations and simulations?

I'm a beginner working on methods proving program equivalence. I've read a few papers about defining logical relations or simulations to prove two programs are equivalent. But I am quite confused ...