Questions tagged [logical-relations]
The logical-relations tag has no usage guidance.
12 questions
3
votes
1
answer
79
views
Is Linear Evaluation Parametric?
Parametric functions satisfy free theorems which state that they take related arguments to related results. This is formalized by the notion of parametric transformation introduced in section 5 of ...
- 93
1
vote
1
answer
80
views
Efficient algorithm/ implementation to compute Transitive Closure of a Rule with respect to a Relationship
(Recalling some) Definitions:
Fix a finite collection of finite sets: $A_1,\ldots,A_k$. Then relationship $R\subseteq A_1 \times A_2 \times \ldots\times A_k$. (Remark: $A_i$'s need not be distinct.)
...
- 111
6
votes
0
answers
120
views
List Functions That Don't Depend on Length
Intuitively, a polymorphic function of type $f : \forall a. [a] \to [a]$ cannot inspect the type of its elements. This intuition can be captured formally using either natural transformations or ...
- 93
4
votes
1
answer
200
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 ...
- 1,187
13
votes
1
answer
420
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 ...
- 1,740
5
votes
0
answers
109
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 ...
- 453
-1
votes
1
answer
2k
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 ...
- 11
7
votes
2
answers
860
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 ...
- 89
16
votes
2
answers
508
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 ...
- 32.9k
16
votes
4
answers
824
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 ...
- 1,092
17
votes
2
answers
1k
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 ...
- 2,717
33
votes
4
answers
4k
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 ...
- 431