Hay algo en el cálculo lambda que me deja perplejo. Supongamos que tenemos $x:A\vdash f(x):P(x)$ $x:A\vdash g(x):P(x)$ para algunos dependiente del tipo de $P$ más de un tipo de $A$. Entonces, no es necesariamente cierto que $\lambda x{.}f(x)=\lambda x{.}g(x)$.
He tratado de entender este fenómeno y, a continuación, que es algo como esto: en realidad, el argumento que se pasa a $\lambda$ no es sólo $x{.}f(x)$, pero es la vinculación a la $x:A\vdash f(x):P(x)$. Por lo tanto, distintas razones por las $f(x):P(x)$ por cada $x:A$ dar diferentes funciones. Pero nunca he visto cosas como esta escrito en alguna parte, así que me siento bastante seguro acerca de.
Me gustaría saber por qué $\lambda x{.}f(x)$ no $\lambda x{.}g(x)$ incluso si $f(x)=g(x)$. A partir de un tipo de punto de vista teórico, pero tal vez también de un modelos de punto de vista. Si hay modelos que pueden explicar fácilmente qué tipo de comportamiento que podemos esperar de $\lambda$, que sería muy útil.
Edit. Debo añadir que el bit de cálculo lambda, que he aprendido de hacer dependiente el tipo de teoría (y más específicamente, Martin-Lof intensional tipo de teoría) en Coq. Allí, el producto que dependen de la $$\prod(x:A),\ P(x)$$ is defined for a dependent type $P:A\to\mathsf{Tipo}$ over a type $$ by introducing elements $\lambda x{.}f(x)$ for each $x:A\vdash f(x):P(x)$, with for each $f:\prod(x:),\ P(x)$ and each $a:A$, a term $\mathsf{aplica}(f,a):P(a)$. These are then required to satisfy the $\beta$- and $\eta$-reglas de conversión: $$ \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} $$ pero no de la regla de $\xi$, que es la regla que dice que $\lambda x{.}f(x)=\lambda x.g(x)$ siempre $f(x)=g(x)$ todos los $x:A$. Pero yo no sé acerca de cualquier cosa que rompa la regla de $\xi$, de ahí mi pregunta.
He aquí un ejemplo concreto donde me enfrento a este problema.
Un ejemplo de este tipo de $f$ $g$ donde este problema me fastidiaron la mayoría viene de demostrar que el axioma de elección es una equivalencia. Supongamos que $A$ es un tipo, que $P$ es dependiente del tipo de más de $A$ y $R$ es dependiente del tipo de más de $P$, es decir,$R:\prod(x:A),\ (P(x)\to\mathsf{Type})$. A continuación, el tipo teórico axioma de elección es la función $$ \mathsf{ac}:\prod(x:)\sum (u:P(x)),\ R(x,u)\a\sum\Big(s:\prod(x:),\ P(x)\Big)\prod(x:),\ R(x,s(x)) $$ dada por $$ \lambda f.\langle \lambda x.\mathsf{proj_1}f(x),\lambda x.\mathsf{proj_2}f(x)\rangle $$ Un candidato a la inversa sería dada por $$ \mathsf{ac{-}inv}:=\lambda w.\lambda x.\langle\mathsf{proj_1}w(x),\mathsf{proj_2}w(x)\rangle. $$ Para demostrar que esto es un derecho inversa usted necesita el $\eta$-conversión en algún momento, pero para demostrar que está a la izquierda inversa, la identidad $$ \lambda x.\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=\lambda x.f(x) $$ es necesario en algún momento. Aunque es bastante obvio que $\langle\mathsf{proj_1}f(x),\mathsf{proj_2}f(x)\rangle=f(x)$ por cada $x:A$, este no es un paso que usted puede hacer en Coq, porque no hay ninguna regla $\xi$ no (que yo sepa). Incluso $\eta$ tienes que introducir manualmente y que sólo es posible mediante el uso de la identidad de tipos de Martín-Lof. Mike Shulmann ha construido una forma de evitar este problema: hay una prueba de que el mapa de $\mathsf{ac}$ es de hecho una equivalencia. Entiendo que esta prueba, pero no el comportamiento de $\lambda$. ¿Qué puede $\lambda$ hacer si usted no tiene $\xi$ que prohíbe a mí de hacer este paso?
