Questions tagged [logical-relations]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
1 answer

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 ...
vigenary's user avatar
1 vote
1 answer

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.) ...
Inspired_Blue's user avatar
6 votes
0 answers

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 ...
vigenary's user avatar
4 votes
1 answer

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 ...
Łukasz Lew's user avatar
  • 1,177
11 votes
1 answer

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 ...
Max New's user avatar
  • 1,653
5 votes
0 answers

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 ...
Andrew Bacon's user avatar
-1 votes
1 answer

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 ...
Xpl0's user avatar
  • 11
7 votes
2 answers

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 ...
user13264's user avatar
15 votes
2 answers

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 ...
Neel Krishnaswami's user avatar
16 votes
4 answers

Unary parametricity vs. binary parametricity

I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( In this paper, they internalize unary ...
Christopher Monsanto's user avatar
17 votes
2 answers

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 ...
Ohad Kammar's user avatar
  • 2,667
32 votes
4 answers

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 ...
Hongjin Liang's user avatar