Un tipo indica qué clase de objeto podemos construir y qué operaciones están permitidas. En la lectura de proposiciones como tipos, demostrar también será construir: una función para una implicación, dos evidencias para una conjunción y un testigo para una existencia. Escribiremos cada entrada y cada salida antes de combinar términos. Hay distintas teorías de tipos; indicaremos cuándo una distinción depende del sistema concreto.
Si necesitas repasar:
1. El contexto dice qué podemos usar y el juicio dice qué hemos construido
Γ⊢t: A se lee: bajo las hipótesis del contexto Γ, t tiene tipo A.
No basta escribir un nombre de variable para tener un término cerrado: una hipótesis es una entrada que se supone disponible.
Primero se comprueba que los tipos y las dependencias tengan sentido; después que el término siga sus reglas. Usaremos notación matemática de funciones, productos y tipos dependientes, no una sintaxis que se prometa idéntica en todos los asistentes.
Una hipótesis no es una construcción sin entradas
Contexto Γ contiene x: A.
Lo disponible
Podemos derivar Γ⊢x: A: la variable declarada proporciona un término bajo esa hipótesis.
Lo que no se hizo
No se ha construido un objeto de A sin contexto. Si A fuera vacío, no existiría ninguna entrada real para suministrar a esa variable.
Resultado cerrado
Sí podemos construir una función que, dada una entrada de A, la devuelva. Su tipo será A→A, sin exigir antes un habitante cerrado de A.
Se conserva la diferencia entre suponer una entrada y producirla.
La identidad existe incluso cuando A es vacío; en ese caso no hay entradas a las que aplicarla.
Aplicar una regla exige que coincidan los tipos
Γ contiene n: N y f: N→Bool, con Bool de dos constructores.
Entrada válida
f(n) tiene tipo Bool porque n tiene el tipo que recibe f.
Salida disponible
El resultado será un booleano, no un natural solo por haber empezado con uno.
Entrada incorrecta
f(true) no está justificada por esos datos: true tiene tipo Bool, y no se ha dado una conversión de Bool a N.
Los tipos controlan qué composiciones están permitidas.
Tener dos nombres de tipos no autoriza a identificarlos aunque se puedan codificar sus valores.
2. Una función introduce una entrada y construye una salida
La primera regla introduce una función y la segunda la elimina mediante aplicación.
Como interpretación lógica, una prueba de A→B transforma cualquier evidencia de A en evidencia de B. No exige disponer previamente de una prueba cerrada de A. La hipótesis queda expresada en la entrada de la función.
La identidad devuelve exactamente lo recibido
Construir A→A.
Suponer entrada
Introducir x: A en el contexto.
Construir salida
El propio x ya tiene tipo A. No hace falta inventar otra evidencia.
Abstraer
Cerrar la entrada produce λx. x: A→A.Al aplicarla a a: A, el resultado es a.
La demostración de A→A no presupone una prueba sin hipótesis de A.
Si se borra λx pero se deja x libre, ya no se ha dado el término cerrado anunciado.
Una segunda entrada puede ignorarse de forma legítima
Construir A→(B→A).
Primera entrada
Tomar a: A.
Segunda entrada
Tomar b: B; el a anterior sigue disponible. Elegir a como salida de tipo A.
Cerrar ambas
λa. λb. a tiene el tipo solicitado. Recibe dos entradas, aunque use solo la primera.
No toda entrada tiene que intervenir en el cálculo de una función.
Para A→B sin una entrada o regla que produzca B no bastaría devolver a, cuyo tipo es A.
3. Un producto necesita dos componentes y permite extraerlas
Para construir A×B se dan a: A y b: B y se forma (a, b). Si p: A×B, sus proyecciones p.1 y p.2 tienen tipos A y B. Las posiciones están tipadas: intercambiarlas cambia el producto de destino.
En la lectura lógica abstracta, el producto representa conjunción. En un sistema como Lean, el producto de datos y la conjunción de proposiciones son construcciones distintas con reglas análogas: no se sustituye literalmente Prod por And en cualquier expresión.
Intercambiar un par conserva los tipos de sus piezas
p: A×B; producir B×A.
Extraer
p.1: A y p.2: B.
Orden nuevo
El producto destino pide primero B y después A. Formar (p.2, p.1).
Función
λp.(p.2, p.1): A×B→B×A.Ninguna componente se convirtió en otra; solo cambió de posición.
Dos intercambios recuperan el par en la igualdad apropiada del sistema.
(p.1, p.1) tendría tipo A×A y no sirve en general para B×A.
Una proyección puede descartar información, pero no inventarla
Entrada (3, true): N×Bool.
Primera proyección
Su primera componente es tres, de tipo N.
Segunda proyección
Su segunda componente es true, de tipo Bool.
Reconstrucción
Con ambas se recupera el par. Con solo el natural tres no se puede saber si el booleano original era true o false.
Introducir el producto requiere más datos que extraer una componente.
El descarte es permitido por estas reglas usuales; no se supone aquí una teoría lineal que exija usar cada entrada exactamente una vez.
4. Una suma marca qué alternativa se ha construido
A+B tiene dos constructores: inl(a) con a: A e inr(b) con b: B. La etiqueta izquierda o derecha distingue las alternativas incluso si A y B son el mismo tipo. Para obtener C de A+B hay que explicar qué hacer en los dos casos.
En la lectura proposicional corresponde a una disyunción con evidencia de una rama. No se obtiene una transformación de A+B a C dando únicamente el caso izquierdo y suponiendo que nunca llegará el derecho.
El mismo número puede entrar por dos ramas distintas
Tipo N+N y número tres.
Izquierda
inl(3) lleva la etiqueta izquierda.
Derecha
inr(3) lleva la etiqueta derecha; no es el mismo constructor aunque el dato numérico coincida.
Eliminar
Definir una función que devuelva cero en la rama izquierda y uno en la derecha distingue ambos términos.
Las marcas son parte de la información del tipo suma.
No se identifica una suma disjunta con una unión que borre la procedencia.
Para llegar a C se necesita un plan para cada rama
Disponemos de f: A→C y g: B→C.
Caso izquierdo
Si la entrada es inl(a), devolver f(a): C.
Caso derecho
Si es inr(b), devolver g(b): C.
Función total
El análisis de casos cubre todos los constructores de A+B.
Así se construye A+B→C.
La eliminación de una disyunción exige las dos transformaciones.
Si falta g, todavía no se ha justificado qué devolver ante una entrada derecha.
5. Negar A es transformar cualquier evidencia de A en una contradicción
El tipo vacío, que escribiremos Empty o 𝟘, no tiene constructores. No es el natural cero. Su regla de eliminación permite construir un término de cualquier tipo a partir de una entrada de Empty: no hay ningún caso constructor que pueda quedar sin resolver.
Si se tienen a: A y h:¬A, la aplicación h(a) produce contradicción. Esto explica qué datos hacen falta para usar una negación.
Una contradicción disponible cierra cualquier objetivo
Contexto a: A y h: A→Empty; objetivo B.
Aplicar
h(a) tiene tipo Empty por la regla de función.
Eliminar vacío
El eliminador de Empty produce un término de B a partir de esa contradicción.
Alcance
No se construyó un habitante de B sin hipótesis. Se mostró que de esas dos hipótesis incompatibles se deriva B.
El principio de explosión usa una contradicción real en el contexto.
Escribir la palabra falso sin una evidencia de Empty no permite esta regla.
De una prueba de A se construye su doble negación
Entrada a: A; objetivo ¬¬A.
Desplegar tipos
¬¬A significa (A→Empty)→Empty.Introducir
Suponer h: A→Empty y aplicar h a la evidencia a.Abstraer
λh. h(a) tiene tipo ¬¬A. Esta dirección es constructiva; no se ha usado tercero excluido.
A→¬¬A tiene una construcción directa.
La dirección ¬¬A→A no se obtiene en general invirtiendo mecánicamente esta función.
6. Un tipo dependiente decide el tipo de salida a partir de la entrada
Una familia B(x) asigna un tipo a cada x: A. El producto dependiente Π(x: A)B(x) contiene funciones que, para cada entrada, entregan una salida del tipo correspondiente.
Ejemplo: Vec(Bool, n) es el tipo de vectores booleanos de longitud n. El índice n forma parte del tipo, no es una etiqueta informal. La cuantificación universal se interpreta mediante una función que entrega evidencia para cualquier entrada.
La longitud prometida cambia con el natural de entrada
Construir ceros: Π(n: N)Vec(Bool, n).
Base
Para cero, devolver el vector vacío de longitud cero.
Paso
Para n+1, colocar false delante del vector ceros(n), obteniendo longitud n+1.
Control
ceros(2) tiene longitud dos y ceros(3) longitud tres. La recursión usa un natural menor y el resultado respeta el índice de cada entrada.
Un único término puede tener tipos de salida que varían con n.
Devolver siempre el vector vacío no cumpliría el tipo para n positivo.
Un universal requiere un argumento arbitrario, no unas muestras
Construir Π(n: N) una prueba de n=n.
Entrada arbitraria
Introducir n: N sin fijar un numeral concreto.
Evidencia
La reflexividad de igualdad proporciona una prueba de n=n para ese n.
Universal
Abstraer n da una función que suministra esa prueba para cualquier natural. No se depende de haber revisado cero, uno y dos.
La entrada arbitraria conserva la generalidad del enunciado.
Para un dominio finito conocido sí podría bastar un análisis exhaustivo de sus constructores.
7. Una existencia constructiva vincula un testigo con su evidencia
En la notación constructiva abstracta, Σ(x: A)B(x) contiene pares (a, b) donde a: A y b: B(a). Al elegir a también elegimos la obligación exacta de la segunda componente. No vale adjuntar evidencia sobre otro testigo sin una igualdad que permita transportarla.
Los sistemas concretos distinguen construcciones. En Lean, una existencia proposicional Exists vive en Prop; Sigma agrupa datos dependientes en Type y Subtype agrupa un dato con una propiedad. Las restricciones de eliminación impiden tratarlos todos como una misma caja de datos.
Elegir un testigo transforma la propiedad en una obligación concreta
En notación matemática, Σ(n: N)(n²=4).
Testigo
Elegir n=2.Calcular obligación
La segunda componente debe probar 2²=4.Ambos lados calculan hasta cuatro y sirve reflexividad.
Par
El par formado por dos y esa evidencia pertenece al tipo dependiente. Si cambiáramos el testigo a tres, pediría 9=4 y la prueba anterior no serviría.
No basta decir que algún n funciona: se da uno y se verifica.
El dibujo usa la lectura abstracta de proposiciones como tipos, no la sintaxis literal de Sigma en Lean.
Extraer la segunda componente conserva la referencia a la primera
p: Σ(n: N)Vec(Bool, n).
Testigo extraído
p.1 es un natural, por ejemplo dos.
Dato dependiente
p.2 tiene tipo Vec(Bool, p.1). Si el primero es dos, su longitud es dos.
Cambio indebido
Sustituir la primera componente por tres y dejar el mismo vector no produce un par del tipo anunciado. Se necesitaría construir un nuevo vector de longitud tres.
Dato y tipo dependiente se mantienen ligados.
Una existencia en Prop no ofrece sin más una función computable que extraiga datos hacia Type; se respetan las reglas del asistente utilizado.
8. Reducir un término calcula; demostrar una igualdad puede requerir más
La reducción beta transforma (λx. t)(a) en t con a sustituido por x, evitando capturar variables libres. Las proyecciones de un par se reducen a sus componentes. La igualdad definicional reconoce expresiones que coinciden mediante las reglas de cálculo del sistema.
Una igualdad proposicional es un tipo con términos de prueba; no toda prueba de igualdad convierte sus lados en expresiones definicionalmente idénticas. Las teorías constructivas puras con normalización controlan sus términos; no se transfiere esa garantía a recursión ilimitada ni a cualquier extensión por axiomas.
Calcular una función y después una proyección
Término (λp. p.2)((3, true)).
Aplicar
Sustituir el par por p produce (3, true).2.
Proyectar
La segunda proyección del par reduce a true.
Tipo
La función original tenía tipo N×Bool→Bool y el resultado es Bool. Cada paso preservó el tipo.
El resultado se obtuvo por cálculo, sin un teorema externo.
La primera proyección daría tres y tendría otro tipo.
Sustituir debe evitar capturar una variable libre
En un contexto con y: A, aplicar (λx. λy. x) a ese y libre; los tipos de entrada se toman iguales para simplificar.
Conflicto de nombres
La y ligada interior tiene el mismo nombre que la entrada libre. Sustituir sin cuidado convertiría una función constante en la identidad.
Renombrar
Renombrar la variable ligada interior como z: λx. λz. x.
Reducir
La aplicación da λz. y, que devuelve la y del contexto para cualquier z. No da λy. y.
Los nombres ligados se pueden cambiar sin alterar el significado.
La notación con ámbitos o índices de variables ayuda a controlar esta obligación.
9. Las identidades y los universos añaden reglas que hay que declarar
Su eliminación permite transportar datos de B(a) a B(b). No cambia un índice porque se parezca al otro: utiliza una igualdad disponible.
Los universos organizan tipos de tipos. En sistemas predicativos habituales, Type u pertenece a un nivel superior, no a sí mismo. Las reglas exactas, la extensionalidad y principios como univalencia dependen de la teoría; no se incorporan sin indicarlo.
Una igualdad permite transportar una longitud
h: n=m y v: Vec(Bool, n).
Situación
v tiene longitud indexada por n. El objetivo pide un vector indexado por m.
Usar h
La eliminación de igualdad transporta v en la familia k↦Vec(Bool, k), obteniendo un término de Vec(Bool, m).
Reflexividad
Si h es la evidencia reflexiva n=n, el transporte calcula hasta el mismo vector en las reglas habituales.
Un cambio de índice necesita cálculo definicional o evidencia de igualdad.
No se afirma que dos naturales distintos sean iguales solo para adaptar la longitud.
Un universo de tipos no es automáticamente uno de sus propios elementos
Trabajar con una jerarquía predicativa Type₀, Type₁,… .
Tipos pequeños
N y Bool pueden vivir en Type₀, y sus términos viven en esos tipos.
Tipo del universo
Type₀ vive en Type₁. La regla no proporciona Type₀: Type₀.
Alcance
La jerarquía controla qué formaciones se permiten. No se deducen de esta explicación todas las propiedades de Prop impredicativo o de otras teorías con reglas diferentes.
Se distingue un término, su tipo y el universo de ese tipo.
Introducir un universo sin restricciones puede alterar la consistencia; las reglas forman parte del sistema elegido.
10. Lo clásico añade principios; lo decidible ya permite elegir casos concretos
Tercero excluido afirma A∨¬A para toda proposición. La lógica constructiva no lo ofrece como regla general sin una construcción que elija una rama. Sí permite demostrarlo para propiedades decidibles mediante un procedimiento que devuelve evidencia de una alternativa.
Agregar principios clásicos puede facilitar pruebas de existencia sin entregar automáticamente un testigo calculable. No significa que toda prueba clásica sea errónea: significa que se declara el sistema y se distingue demostrar una proposición de calcular datos.
La igualdad de booleanos es decidible por sus cuatro casos
Comparar b y c de tipo Bool, con constructores false y true.
Iguales
false con false y true con true dan una prueba de igualdad por reflexividad.
Diferentes
false con true y true con false dan evidencia de desigualdad por disjunción de constructores.
Totalidad
Los cuatro casos cubren todas las entradas. Para cada pareja obtenemos igualdad o su negación de manera constructiva.
Una propiedad concreta puede ser decidible sin tercero excluido general.
No se infiere de cuatro casos de Bool una decisión para toda proposición matemática.
Negar la doble negación no la convierte por sí sola en un dato
Tenemos h:¬¬A y queremos construir a: A.
Qué ofrece h
h recibe una negación de A y devuelve contradicción. No recibe un número ni entrega directamente a: A.
Información adicional
Si disponemos de una decisión A+¬A, analizamos casos: la rama A aporta evidencia; la otra contradice h y permite eliminar vacío.
Frontera general
Sin tal decisión o un principio clásico adicional, esa construcción no da ¬¬A→A para A arbitraria.
Se ve exactamente dónde entra la elección de alternativas.
Las bibliotecas pueden aportar principios clásicos; su uso debe quedar identificado en las dependencias de la prueba.
Ahora lo resolvemos de principio a fin.
EJEMPLO RESUELTO 1
Intercambiar un par
Construye una prueba de A∧B→B∧A.
Interpretación
En la lectura proposicional usamos las reglas de conjunción, análogas a las de un producto.
Entrada
Suponer p: A∧B.
Extraer A
La primera proyección p.1 es evidencia de A.
Extraer B
La segunda proyección p.2 es evidencia de B.
Construir destino
Formar (p.2, p.1), evidencia de B∧A con el orden requerido.
Cerrar
λp.(p.2, p.1) prueba A∧B→B∧A.En un asistente concreto se usan los constructores de conjunción correspondientes.
λp.(p.2,p.1).
La primera componente tiene tipo B y la segunda A.
EJEMPLO RESUELTO 2
Composición
Dados f:A→B y g:B→C, construye A→C.
Datos
f: A→B y g: B→C están disponibles.Entrada
Introducir x: A arbitrario.
Primera aplicación
f(x): B porque coincide el tipo de entrada.
Segunda aplicación
g(f(x)): C porque g recibe precisamente un B.
Abstraer
λx. g(f(x)): A→C es la composición g∘f.Comprobar
El tipo intermedio B coincide en salida y entrada. Invertir las funciones pediría otros tipos y no está justificado en general.
g∘f=λx.g(f(x)).
La salida intermedia B coincide con la entrada de g.
Los símbolos que hemos usado
- a:A
- Juicio: el término a tiene tipo A en el contexto considerado.
- Γ
- Contexto ordenado de variables con tipos e hipótesis disponibles.
- A→B
- Tipo de funciones que reciben un término de A y producen uno de B.
- A×B
- Tipo de pares con primera componente de A y segunda de B.
- λx.t
- Función que, dada una entrada x, devuelve el término t.
- Π(x:A) B(x)
- Tipo de funciones dependientes: para cada x:A producen un elemento de B(x).
- Σ(x:A) B(x)
- Tipo de pares dependientes (a,b) con a:A y b:B(a).
- 0
- Tipo vacío, sin constructores, que representa falsedad en la interpretación elegida.
Ahora te toca a ti.
Tienes cinco ejercicios. Inténtalos; las pistas te ayudan si te atascas.
Practicar este tema →