Cómo introducir el tipo de la teoría a la recién llegada

Question

Quiero introducir (dependiente) tipo de la teoría a algunos amigos que tienen antecedentes en la lógica matemática y teoría de conjuntos. Para hacer esta introducción fácil que me gustaría dar una presentación informal que describe los tipos de colección y términos como elementos de los tipos.

Mi plan era presentar el tipo de sistemas como sistemas algebraicos donde los tipos son las clases, los constructores y los separadores son operaciones entre estas clases y $\beta$ $\eta$- reducción son ecuaciones que estas álgebras están obligados a satisfacer.

Por desgracia estoy frente al siguiente problema: no puedo encontrar una manera para describir a $\lambda$-abstracción (el constructor de tipos de función) en este marco algebraico. La razón es que la regla de inferencia que describen $\lambda$-abstracción, es en la forma $$\begin{array}{c} \Gamma, x \colon A \vdash y : B \\ \hline \Gamma \vdash \lambda x \colon A. y \colon A \to B\end{array}$$ que utiliza términos con no vacío contexto de $\Gamma, x \colon A \vdash y \colon B$.

El problema radica en cómo (intuitivamente) interpretar los términos con los que no emtpy contexto en este marco algebraico: términos constantes, es decir, términos con vacío contexto, puede ser interpretado de forma muy natural, como los elementos de los tipos.

Así que la pregunta es:

Lo que podría ser una interpretación intuitiva de los términos con los que no vacía en un contexto algebraico marco como el descrito anteriormente?

Answer 1

Algunas de las observaciones se señaló al inicio:

1. Tipo de teoría debe ser pensado como un general de la teoría matemática de las construcciones: cómo los objetos matemáticos se construyen, ¿cuáles son los diferentes tipos de construcciones (funciones pares, inductivo construcciones, co-inductivo de construcciones, etc.), lo ecuacional leyes que cumplir, y cómo pueden ser generalmente handeled. Por lo tanto, podemos esperar una manera sistemática de la introducción de nuevos tipos de construcciones. En efecto, como vamos a ver cada nueva forma de construcción de tipos sigue el mismo camino: las reglas de formación, la introducción de las reglas, la eliminación de las reglas, la congruencia de las reglas, y las ecuaciones que explican cómo la introducción y eliminaciones de encajar.

2. Clásicos de la matemática se apoya en dos pilares: la lógica de primer orden y la teoría de conjuntos. La teoría de conjuntos es formulado utilizando la lógica de primer orden. En contraste, el tipo de teoría se encuentra en sus propios. No hay ninguna lógica bajo tipo de teoría. De hecho, podemos ver el tipo de teoría común, la unificación de la lógica y teoría de conjuntos: ciertos tipos son como proposiciones lógicas, algunos tipos son como los conjuntos, y también hay tipos que son como nada que haya visto antes.

3. Porque no hay lógica, sólo un formalismo para la construcción de cosas, uno tiene que acostumbrarse a una nueva forma de hablar y de pensar. En el tipo de teoría es imposible decir o pensar "$P$ es cierto", porque el único mecanismo disponible es la construcción de un elemento de un tipo. Desde $P$ es una (especie de) tipo, deberíamos decir "construimos un elemento $e$ tipo $P$". (En la lógica de primer orden el elemento $e$ correspondería a una prueba de $P$.)

4. Por lo tanto, ya que en el tipo de teoría es imposible afirmar que una proposición $P$ mantiene sin llegar a dar una prueba de $e$ de la misma, las pruebas son inevitables. O para ponerlo de otro modo, las pruebas son "ciudadanos de primera categoría", ya que son sólo elementos de ciertos tipos. La situación ordinario de matemáticas es muy diferente: aunque las pruebas son fundamentales para las matemáticas, nadie se ha considerado el conjunto de todas las pruebas de una proposición $P$, ni nada de eso.

Answer 2

Después de haber pasado algún tiempo pensando acerca de este problema y aclaró que el problema en la pregunta que me he dado cuenta de que la solución al problema (esta solución vino a mi mente después de pensar a la semántica del tipo de la teoría de categorías):

Si uno interpreta términos vacíos contexto como elementos de las colecciones/entonces, los tipos de términos con los que no vacía contexto puede ser, naturalmente, interpretado como la cooperación entre los tipos. En detalles: uno puede reguard un contexto de $\Gamma \equiv x_1 \colon A_1, x_2 \colon A_2 \dots x_n \colon A_n$ como una especie de producto cartesiano (que no debe confundirse con el tipo de producto, que viene equipado de proyecciones [eliminadores]), luego de un plazo $\Gamma \vdash t \colon T$ puede ser interpretado como una operación que asocia a cada $n$-tupla de elementos $a_1 \in A_1, \dots , a_n \in A_n$ elemento $t(a_1,\dots,a_n) \in T$ (o $T(a_1,\dots,a_n)$ en el caso de los tipos de dependientes).

Con esta interpretación en cuenta el $\lambda$-abstracción se convierte en una orden superior operador que lleva a las operaciones de la forma $\Gamma, x \colon A \vdash t \colon B$ en las operaciones de la forma $\Gamma \vdash \lambda x \colon A. t \colon A \to B$.

Por supuesto, uno tiene que tener en mente la distinción entre un plazo en el contexto de $x \colon A \vdash t \colon B$ (que en esta interpretación sería una operación entre los tipos de $A$$B$) y el plazo $\vdash\lambda x \colon A. t \colon A \to B$ que es una constante.

Desde una perspectiva de programación el plazo $x \colon A \vdash t \colon B$ es una función de la toma como entrada un valor de tipo $A$ y devolver un valor de tipo $B$, mientras que el término $\lambda x \colon A. t \colon A \to B$ es un valor del tipo $A \to B$ que representan la función de $t$ internamente para el lenguaje de programación (es el código de la función $t$).