4
$\begingroup$

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 note a similarity in the definition of a (binary) logical relation
f1 [A -> B] f2 being:
∀ x1 x2 → x1 [A] x2 -> f1 x1 [B] f2 x2.

What is the relation of logical relations to function extensionality? Is there perhaps a relation to eta-equality?

$\endgroup$
1

1 Answer 1

1
$\begingroup$

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 a relation between two functions of types $A \to B$ does not necessarily have to express equality between two functions. But the equality relation is a possible binary relation between functions. Let us see how we can formulate a logical relation that specifies that two functions (both of type $A \to B$) are equal.

Denote by $A \leftrightarrow B$ the type of relations between values of types $A$ and $B$. The identity relation for the type $A$ is denoted by $[\textrm{id}^A]: A \leftrightarrow A$.

The logical relation for the extensional equality is formulated like this: Two functions are equal when they are in the identity relation for the type $A \to B$. That identity relation is denoted by $[\textrm{id}^{A \to B}]$. Then we can rewrite the Agda definition of the extensional equality in the language of relations like this:

$f_1\, [\textrm{id}^{A \to B}]\, f_2$ means $\forall x_1,\, x_2$ if $ x_1 \,[\textrm{id}^{A}]\, x_2$ then $f_1 (x_1) \,[\textrm{id}^{B}]\, f_2 (x_2)$

Now we can further rewrite this definition via the function-type construction for relations. The function-type construction is defined like this: Given any two relations $[r] : A \leftrightarrow B$ and $[s]:C\leftrightarrow D $, we can define the relation $[r\to s]: (A \to C) \leftrightarrow (B \to D)$ by the formula similar to what you wrote: for any two functions $f: A\to C$ and $g: B\to D$, we have:

$f\, [r\to s]\, g$ means $\forall x:A,\, y:B$, if $ x \,[r]\, y$ then $f(x) \,[s]\, g(y)$

Now if we set $A=B$, $C = D$, $[r] = [\textrm{id}^A]$, and $[s] = [\textrm{id}^C]$, then we will get: $[r \to s] = [\textrm{id}^{A\to C}]$. So, the identity relation on functions is obtained by the function-type construction from identity relations on types A and B. That's all it seems to be.

$\endgroup$
4
  • $\begingroup$ This answer is totally correct, but let me add one additional comment. Parametric models satisfy the identity extension property: if $A[a]$ is a type with a free variable $a$, and $\mathsf{Id}_X$ is the identity relation for $X$, then $[\![ A[a] ]\!] (\mathsf{Id}_X/a) = \mathsf{Id}_{A[X]}$. This forces all parametric models to satisfy the condition above. $\endgroup$ Mar 31, 2023 at 8:28
  • $\begingroup$ @NeelKrishnaswami It is hard for me to follow the notation in your comment. I will revise my answer a bit. I think the main point is that we must show a proof that [A -> B] = id follows from [A] = id and [B] = id, it does not follow automatically. $\endgroup$
    – winitzki
    Mar 31, 2023 at 8:34
  • $\begingroup$ Sorry! I didn't think my commented warranted a whole new answer, but comments make it hard to use rich notation... $\endgroup$ Mar 31, 2023 at 8:36
  • $\begingroup$ @NeelKrishnaswami I have rewritten my answer and introduced new notation. I showed the derivation now. I'm not an expert in programming language theory, and I don't really understand the notation or the substance of what's going on in Reynolds's papers. For example, you said that "parametric models" will satisfy the "identity extension lemma". I think a practical programmer will not need to worry about the details of the models of the programming language. A programmer would never expect the programming language to implement a model that doesn't satisfy the identity extension lemma. $\endgroup$
    – winitzki
    Mar 31, 2023 at 9:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.