4
votes
Accepted
Is Linear Evaluation Parametric?
Here's an Agda formalization of the non-linear version of your argument, and my comment above:
...
- 921
3
votes
Efficient algorithm/ implementation to compute Transitive Closure of a Rule with respect to a Relationship
I give here an answer for a very specific subcase.
We let $x \in A_1 \times \dots \times A_k$ be written $(x^1,\dots,x^k)$.
When the rule $\sigma$ acts on each $A_i$ independently, in the same way, ...
2
votes
Accepted
Why Reflexive Graphs for Parametricity?
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$ ...
- 1,653
1
vote
What is the relation of parametricity and function extensionality?
Indeed there is a similarity in these two definitions.
Function extensionality that you showed is just a condition that specifies when two functions are equal.
If we talk about logical relations then ...
- 244
Only top scored, non community-wiki answers of a minimum length are eligible