Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily true that $\lambda x{.}f(x)=\lambda x{.}g(x)$.

I've tried to understand this phenomenon and then it goes something like this: actually, the argument you pass to $\lambda$ is not just $x{.}f(x)$, but it is the entailment $x:A\vdash f(x):P(x)$. Thus different reasons why $f(x):P(x)$ for each $x:A$ give different functions. But I've never seen things like this written down somewhere, so I feel quite uncertain about it.

I'd like to know why $\lambda x{.}f(x)$ is not $\lambda x{.}g(x)$ even if $f(x)=g(x)$. From a type theoretical point of view, but maybe also from a models point of view. If there are models that can easily explain what kind of behavior we can expect from $\lambda$, that would be very helpful.


Edit. I should add that the bit of lambda calculus I have learned is from doing dependent type theory (and more specifically, Martin-Lof's intensional type theory) in Coq. There, the dependent product $$\prod(x:A),\ P(x)$$ is defined for a dependent type $P:A\to\mathsf{Type}$ over a type $A$ by introducing elements $\lambda x{.}f(x)$ for each $x:A\vdash f(x):P(x)$, with for each $f:\prod(x:A),\ P(x)$ and each $a:A$, a term $\mathsf{apply}(f,a):P(a)$. These are then required to satisfy the $\beta$- and $\eta$-conversion rules: $$ \begin{split} \beta.\qquad\qquad & \mathsf{apply}(\lambda x{.}f(x), a)=f(a)\\ \eta.\qquad\qquad & \lambda x{.}\mathsf{apply}(f,x)=f, \end{split} $$ but not rule $\xi$, which is the rule saying that $\lambda x{.}f(x)=\lambda x.g(x)$ whenever $f(x)=g(x)$ for all $x:A$. But I don't know about anything that would break rule $\xi$, hence my question.


Here's a concrete example where I face this problem.

An example of such $f$ and $g$ where this problem bugged me the most comes from proving that the axiom of choice is an equivalence. Suppose that $A$ is a type, that $P$ is a dependent type over $A$ and that $R$ is a dependent type over $P$, i.e. $R:\prod(x:A),\ (P(x)\to\mathsf{Type})$. Then the type theoretical axiom of choice is the function $$ \mathsf{ac}:\prod(x:A)\sum (u:P(x)),\ R(x,u)\to\sum\Big(s:\prod(x:A),\ P(x)\Big)\prod(x:A),\ R(x,s(x)) $$ given by $$ \lambda f.\langle \lambda x.\mathsf{proj_1}f(x),\lambda x.\mathsf{proj_2}f(x)\rangle $$ A candidate inverse would be given by $$ \mathsf{ac{-}inv}:=\lambda w.\lambda x.\langle\mathsf{proj_1}w(x),\mathsf{proj_2}w(x)\rangle. $$ To prove that this is a right inverse you need the $\eta$-conversion at some point, but to prove that it is a left inverse, the identity $$ \lambda x.\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=\lambda x.f(x) $$ is needed at some point. While it is fairly obvious that $\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=f(x)$ for each $x:A$, this is not a step you can make in Coq, because there's no rule $\xi$ there (as far as I know). Even $\eta$ you have to introduce manually and that is only possible using the identity types of Martin-Lof. Mike Shulmann has constructed a way around this issue: there is a proof that the map $\mathsf{ac}$ is indeed an equivalence. I understand this proof, but not the behavior of $\lambda$. What can $\lambda$ do if you don't have $\xi$ that prohibits me from making this step?

share|improve this question
1  
One small suggestion: this question seems like an excellent fit for the theoretical (or maybe non-theoretical?) CS SE sites, cstheory.stackexchange.com and cs.stackexchange.com; you might try migrating this question over there? –  Steven Stadnicki Jun 8 '12 at 16:52
    
@StevenStadnicki I didn't think of the CS SE, but maybe it's a good idea to migrate it. On the other hand, their lambda-calculus tag is not a lot bigger than the one here... –  Egbert Jun 8 '12 at 17:14
    
@StevenStadnicki it's worth pointing out that cstheory.SE is for research-level questions. –  user2468 Aug 6 '12 at 0:20
add comment

1 Answer 1

I’m pretty sure that the $\xi$ rule is implemented in Coq. The doc says somewhere

Let us write E[Γ] ⊢ t ▷ u for the contextual closure of the relation t reduces to u in the environment E and context Γ with one of the previous reduction β, ι, δ or ζ.

The $\xi$ rule is usually not even mentionned because this is a consequence of the contextual closure of definitional equality which is usually assumed.

In your concrete example, the problem does not come from $\xi$ but from the "fairly obvious" fact that $\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=f(x)$. This is called $\eta$-equality for dependent sums, but Coq does not satisfy this definitionally (not even Coq 8.4 which has only $\eta$-equality for functions).

So yes, in Coq you have to prove $\eta$-equality for dependent sums using identity types, but this has nothing to do with $\xi$.

In Agda there is $\eta$-equality for dependent sums (and more generally for records), so probably that these two functions are definitionally inverse to each other in Agda.

share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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