Repository files navigation

Agda es tanto un lenguaje de programación (funcional) como un asistente depruebas (VeasePROOF = PROGRAM - Samuel Mimram. De acuerdo con ladocumentaciónoficial de Agda, Agda es una extensión de la teoría de tipos de Martin-Löf, por lo quesu poder expresivo es adecuado para escribir pruebas y especificaciones deobjetos matemáticos. De esta forma, Agda también es una herramienta para laformalización de las matemáticas. En tanto que para poder aprovechar todo elpoder de Agda como asistente de pruebas y herramienta de formalización dematemáticas se requiere estudiar la teoría de tipos antes mencionada, en estabreve pero concisa introducción no se tocarán los detalle; sin embargoconsidero importante mencionar que, yo como autor, el acercamiento que hetenido con la teoría de tipos de Martin-Löf y Agda ha sido gracias a lateoría homotópica de tipos, de modo que mi forma de pensar sobre lo que sepresentará en este trabajo no podría empatar directamente con la teoría sobrela cual se fundamenta Agda.

Hay mucho que decir sobre la relación entre la lógica, las categorías y lostipos; sin emargo me limitaré a mencionar la correspondenciaCurry-Howard-Lambek por muy encima, y una breve mención de tipos dependientes ysu interpretación tanto lógica como categórica.

EnThe Formulae-As-Types Notion of Construction, un artículo escrito por el lógico Alvin Howard en1980 menicona que Curry sugirió una relación entre los combinadores delcálculo lambda y axiomas de la lógica. En este mismo escrito, Howard formalizalas observaciones hechas por Curry. Por otro lado, a inicios de los 70's elmatemático Joachim Lambek demuestra que las categorías cartesianas cerradas yla lógica combinatoria tipada comparten una teoría ecuacional en común.

La correspondencia es entonces

Es importante señalar que, a diferencia de la teoría de conjuntos, los tiposproducto y función son conceptos primitivos.

La forma de construir términos de un tipo producto coincide con aquella de lateoría de categorías. Dados$a : A$ y$b : B$ podemos construir$(a , b) : A × B$.Hablaremos un poco más sobre cómo "acceder" a los elementos que componen un tipoproducto cuando entremos bien en materia sobre usar a Agda como un asistente deprueba.

Por otro lado, la forma de construir un tipo flecha es mediante un proceso deabstracción. Si tenemos un término, y observamos que podemos abstraer ciertocomportamiento de interés, entonces podemos introducir un tipo flecha queabstrae el comportamiento deseado, de forma análoga a como solemos hacerlo enmatemáticas. Si, por ejemplo, observamos que la sucesión 0, 1, 2, 4, 16, 32, ...presenta un comportamiento cuadrático, podemos abstraer este comportamientoescribiendo una representación simbólica de este en términos de nuestro lenguajematemático:$$f(x) = x^2$$

Para restringir más dicho comportamiento en función de la clase de términos quequeremos considerar en nuestra abstracción, introducimos dominios y codominios.

$$f : ℕ → ℕ$$

de modo que sólo permitimos que$f$ "funcione" con naturales, y garantizamos quetras hacer cualquier cómputo con$f$, el número que nos devuelve es un númeronatural.

De forma análoga, el proceso de abstracción involucrado en la introducciónde un tipo flecha involucra un términot : B, del cual abstraemosx : Ay garantizamos que tras cualquier cómputo realizado con este tipo flechaobtenemos otro término de tipoB. Expresamos esto con la siguientesintaxis:

λx. t:A→B

La teoría de tipos de Martin-Löf permite trabajar con tipos que dependen deotros; es de esta forma que sontipos dependientes. Se introducen los tiposde funciones dependientes, y los tipos coproducto.

El HoTT Book menciona que los elementos (términos) de un tipo Π son funcionescuyo tipo codominio puede variar según el elemento del dominio hacia el cualse aplica la función. En virtud de este comportamiento familiar para aquellaspersonas que han estudiado teoría de conjuntos es que reciben el nombre de Π,pues el producto cartesiano generalizado tiene este mismo comportamiento.

Dado un conjunto$A$, y una familia$B$ indizada por$A$, el producto cartesiano generalizado es$$\prod\limits_{a ∈ A} B(a) = { f: A → \bigcup\limits_{a ∈ A}B(a)\ \vert\ ∀a ∈ A . f(a) ∈ B(a) }$$

En teoría de tipos escribimos: en lugar de∈, pero la sintaxis es prácticamente la misma.Dado un tipoA, y una familiaB:A → Type, podemos construir el tipo de funcionesdependientes

Π(a:A)B(a):Type

Intuitivamente, y en efecto así ocurre, siB es una familia constante, entonces

Π(a:A)B(a)≡ (A→B)

De esta forma, el tipo Π generaliza a los tipos flecha. Estos tipos además permiten elpolimorfismo de funciones. Una función polimorfa es aquella que toma un tipo comoargumento y actúa sobre los elementos de dicho tipo. Esto debería recordarle a usteddel ∀ en la lógica. Una observación pertinente es que los tipos producto se puedenpensar como una versión "no dependiente" en cierto sentido de los tipos Π.

Así como los tipos Π generalizan a los tipos flecha, los tipos Σ generalizan a lostipos producto, en tanto que permiten que el elemento en la "segunda coordenada"dependa del elemento en la "primera coordenada". Obsevese que este comportamientoes el mismo que permite el coproducto de la categoría de conjuntos (la unión disjunta).

Σ(x:A)B(x)

Intuitivamente, y de nuevo es cierto que, si$B$ es constante, entonces$$\right( \sum\limits_{x : A} B \left) ≡ (A × B)$$

Así como el tipo Π se puede identificar con el ∀ en lógica, el tipo Σ se puedeidentificar con el cuantificador ∃. Una observación adicional pertinenterespecto a los tipos Σ es que los tipos + son una versión "no dependiente" encierto sentido de los tipos Σ.

Resumiendo algunos comentarios relevantes a esta pequeña introducción a lateoría de tipos de Martin-Löf, tenemos la siguiente tabla.

El poder expresivo de la teoría de tipos de Martin-Löf (y por extensión la teoríahomotópica de tipos) permite identificar proposiciones matemáticas con tipos, y susdemostraciones con términos de un tipo dado. De esta forma, si ocurre que el tipotiene por lo menos un término, entonces podemos permitir decir que tenemos unademostración de dicha proposición.En HoTT las proposiciones (de la lógica proposicional) corresponden a una claseparticular de tipos, en tanto queen la lógica de primer orden no hay forma de distinguir entre una prueba de otra.Estas tecnicalidades se mencionan con el propósito de incitar a la persona leyendoo escuchando esto a investigar más por su cuenta, puespara propósitos de esta exposición haremos uso del tipoSet de Agda, que renombraremosaType para hacer énfasis en este paradigma de "Proposiciones como tipos".

Iniciamos escribiendo al inicio de todo nuestro archivo con extensión.agda o.lagda.mdlas siguientes cláusulas:

open importData.Productrenaming (_×_ to _∧_)Type=Set

En la primera línea le pedimos a Agda por favor y con mucho cariño que de labiblioteca estándar importe el tipo Product y que además renombre el operador×a∧. En la segunda línea renombramos al tipoSet comoType.

Para pedirle a Agda, de nuevo por favor y con mucho cariño, que nos diga silo que hemos escrito hasta el momento está bien escrito y bien tipadopresionamos la combinaciónC-c C-l en emacs o en vscode con la extensiónagda-mode.Si todo está bien, deberíamos ver colorcitos en el código Agda que escribimos yningún mensaje al fondo de emacs o de vscode.

Ya con nuestro preámbulo listo, empecemos a demostrar pero no sin antes dar el créditocorrespondiente. La gran mayoría de cosas que se expondrán a continuación fueron tomadasde las siguientes fuentes:

• Propositional Logic in Agda - Samuel Mimram
• The HoTT Game
• Agda in a hurry - Martin Escardó
• HoTTEST School Agda Notes - Martin Escardó
• HoTT UF in Agda - Martin Escardó*Proof = Program - Samuel Mimram

Sean$A, B$ proposiciones. Entonces$A ∧ B ⇔ B ∧ A$.

Recordando que bajo nuestro paradigma en uso las proposiciones son tipos,codificamos nuestra proposición como un tipo y, para demostrar la proposiciónbuscamos definir un término bien tipado del tipo de nuestra proposición.

∧-comm: {AB:Type}→A∧B→B∧A∧-comm=？

Como no sabemos ni pío de Agda, le preguntamos a Agda qué opina que deberíaser la definición de nuestro término que, a final de cuentas será nuestraprueba. Esto lo hacemos escribiendo el signo de interrogación despues de el signode igualdad. Si le pedimos a Agda que verifique si nuestro programa está bien tipado,apareceran mensajes en la parte de abajo de emacs/vscode y los símbolos{ }0 endonde habíamos puesto nuestro preciado símbolo de interrogación. Estos símbolossignifican que ahí hay unhueco de meta.Los mensajes leen

?0:A∧B→B∧A

Lo que denotan los símbolos?0 es que nuestra meta0 es la de producir un términodel tipoA ∧ B → B ∧ A. Podemos pedirle a Agda que nos de más información sobre nuestroproblema (Contexto y Meta) al posicionar el cursor en el hueco de metamediante la combinación de teclasC-c C-, en emacs.

Veremos que ahora nos muestra mensajes muy distintos a los anteriores.Nos dice que en nuestra declaración del término que necesitamos debemos asumir queB yA son tipos. Quizás para esta situación no es muy reveladora la informaciónque brinda Agda, pero en otras situaciones brinda información bastante útil.

Podemos pedirle a Agda que nos de más pistas, con base en la naturaleza de lostérminos de los tipos que queremos producir. Para esto, de nuevo con el cursor en el huecode meta, presionamos la combinación de teclasC-c C-r en emacs/vscode para "refinar la meta".

∧-comm: {AB:Type}→A∧B→B∧A∧-comm= λ x→ { }1

Al hacer esto, notamos que agda modifica el hueco y las metas se modifican acordemente.Ahora nuestra meta es producir un término de tipoB ∧ A. Si volvemos a pedirle a Agdael contexto y meta del problema, veremos que ahora tenemos a nuestra disposiciónun términox : A ∧ B, con el cual podemos producir un término de tipoB ∧ A.Si de nuevo le pedimos a Agda que refine la meta, tendremos ahora dos metas nuevas:producir un término de tipoB y otro término de tipoA.

∧-comm: {AB:Type}→A∧B→B∧A∧-comm= λ x→ { }1 , { }2

∧-comm: {AB:Type}→A∧B→B∧A∧-comm= λ x→ {aa}0, {aa}1

De aquí, podemos proceder de al menos tres formas distintas.

• Podemos recordar que en la teoría de tipos de Martin-Löf (MLTT) el tipo productoes una noción primitiva, y por lo tanto Agda debe de implementar de forma "nativa"un eliminador izquierdo y derecho para el tipo producto.

• Podemos probar un lema (redundante bajo la observación anterior)

• Podemos aprovechar las bondades de Agda y su pattern matching para poder construir el términoque queremos en virtud de la sintaxis que tienen los términos del tipo producto.

En tanto que para lo primero habría que irse a la documentación de Agda, y podríamosusar lo tercero para probar el lema de la segunda opción, mejor probamos juntos el lemay las otras opciones se quedan como ejercicio.

En MLTT, los términos del tipo producto se forman según el siguiente juicio:

Γ⊢ a:AΓ⊢ b:B--------------------------[×-intro]Γ⊢ (a , b):A×B

De esta forma, aprovechando el pattern matching de Agda podemos escribir la siguiente demostraciónpara el lema

Sean$A$,$B$ proposiciones. Entonces$A ∧ B ⊃ A$ y$A ∧ B ⊃ B$.

∧-el: {A B: Type}→ A ∧ B→ A∧-el (a , b)= a∧-er: {A B: Type}→ A ∧ B→ B∧-er (a , b)= b

Una observación pertinete es que al refinar y obtener los dos huecos anteriormente,Agda nos está diciendo que utilicemos la regla de introducción del tipo producto, tal y comolo hicimos al probar nuestro lema, para generar el término que deseamos. Entonces el proceso derefinamiento de meta corresponde a aplicar una regla de introducción.

Ya armados con nuestro lema, podemos demostrar lo que queríamos en un inicio.Para "darle" a Agda los términos tenemos dos opciones, que realmente son la misma:

• Escribir sobre el hueco el término y luego presionarC-c C-SPC ó,
• Presionar sobre el huecoC-c C-SPC.

Antes de rellenar ambos huecos, prueba usando la combinaciónC-c C-nen alguno de los huecos, y escribiendo∧-er x o∧-el x. Encontrarás que Agdanormaliza el término que escribiste. Al escribir∧-er x regresaproj₂ x el cuales el resultado de aplicar el eliminador "nativo" del tipo producto sobre el términox.Tras darle a Agda los términos necesarios, terminamos nuestra prueba.

∧-comm: {A B: Type}→ A ∧ B→ B ∧ A∧-comm=λ x→ (∧-er x) , (∧-el x)

En conclusión, el termino∧-comm = λ x → (∧-er x) , (∧-el x) es prueba/testigo de queel tipo∧-comm : {A B : Type} → A ∧ B → B ∧ A no es vacío y por lo tanto es una proposición"verdadera".

Notemos que esta demostración tiene su contraparte categórica.

Y también tiene su contraparte en el cálculo de secuentes.

Sean$A, B$ proposiciones. Entonces$A ⊃ B ⊃ A$

prop1: {A B: Type}→ A→ B→ Aprop1=λ a→ (λ b→ a)

Sean$A, B, C$ proposiciones. Si$A ⊃ B$ y$B ⊃ C$ entonces$A ⊃ C$.

-- Si uno tiene muchas ganas,-- puede escribir la proposición en notación de cálculo de secuentes→-trans: {A B C: Type}→ (A→ B)→ (B→ C)------------→ (A→ C)→-trans f g=λ a→ g (f a)

Sea$A$ una proposición. Entonces$A ⊃ A$.

id: {A: Type}→ A→ Aid=λ a→ a

Sean$A, B$ proposiciones. Si$A ⊃ B$ y$A$, entonces$B$.

→app: {A B: Type}→ (A→ B)→ A----------------[App/Modus Ponens]→ B→app f a= f(a)

Sea$A$ una proposición. Entonces$A ⊃ A ∧ A$.

Δ: {A: Type}→ A-------------→ (A ∧ A)Δ a= id a , id a

Sean$A, B, C$ proposiciones. Entonces$A × B ⊃ C$ si y solo si$A ⊃ B ⊃ C$(Hom(A × B, C) ≅ Hom(A, Cᴮ))

currying: {A B C: Type}→ (A ∧ B→ C)----------------→ A→ B→ Ccurrying=λ f→λ a→λ b→ f (a , b)currying2: {A B C: Type}→ (A→ B→ C)----------------→ (A ∧ B→ C)currying2=λ f→λ ab→ (f (∧-el ab)) (∧-er ab)

Podemos definir el si y solo si.

_⇔_: (A B: Type)→ Type A ⇔ B= (A→ B) ∧ (B→ A)

Sean$A, B, C$ proposiciones. Entonces $A ⊃ (B ∧ C) ⇔ ((A ⊃ B) ∧ (A ⊃ C))

Para probar una doble implicación necesitamos dar una prueba de la ida y una prueba del regreso.Para probar la ida podemos suponer que disponemos de un término del tipo t₁ : (A → (B ∧ C)) ydebemos construir un t₂ : ((A → B) ∧ (A → C)).Para demostrar el regreso, debemos suponer que conamos con un término t₁ : ((A → B) ∧ (A → C))y construir un t₂ : (A → (B ∧ C))

→-dist∧: {A B C: Type}→ (A→ (B ∧ C)) ⇔ ((A→ B) ∧ (A→ C))→-dist∧= (λ t₁→-- ⊃ )                (λ a→ ∧-el (t₁ a)) ,λ a→ ∧-er (t₁ a)) ,λ t₁→-- ⊂ )λ a→ (∧-el t₁) a , (∧-er t₁) a

La disjunción es un tipo inductivo.

-- Cuando se tiene algo de la forma (A B : Type) estamos diciendole a Agda que queremos-- explicitos los tipos. Cuando se tiene algo de la forma {A B : Type} le pedimos a agda-- que infiera los tipos.data_∨_ (A B: Type): Typewhereleft: A→ A ∨ Bright: B→ A ∨ B

Muchas veces, cuando un tipo suma está involucrado, es necesario separar por casos.Esto se aprecia en la definición del tipo ∨, en tanto que un término de dicho tipoen principio puede tener dos formas: dicho término pudo haber sido construidomediante una aplicación deleft, o mediante una aplicación deright. Por consiguiente,debemos tomar en cuenta estos dos casos distintos en nuestras pruebas.

--{ Principio de demostración por casos }--caseof: {A B C: Type}→ (A ∨ B)→ (A→ C)→ (B→ C)----------------[∨-elim]→ C caseof (left a∨b) c₁ c₂= c₁ a∨b-- Caso 1. Ocurre Acaseof (right a∨b) c₁ c₂= c₂ a∨b-- Caso 2. Ocurre B

La disjunción es conmutativa.

∨-comm: {A B: Type}→ A ∨ B→ B ∨ A∨-comm (left a∨b)= right a∨b∨-comm (right a∨b)= left a∨b

La disjunción distribuye sobre la conjunción.

∨-dist∧: {A B C: Type}→ (A ∨ (B ∧ C))-------------------→ (A ∨ B) ∧ (A ∨ C)∨-dist∧ (left a∨[b∧c])= left a∨[b∧c] , left a∨[b∧c] ∨-dist∧ (right a∨[b∧c])= right (∧-el a∨[b∧c]) , right (∧-er a∨[b∧c])

En la lógica proposicional, una proposición falsa es aquella que no se puede demostrar.Por lo tanto, la definimos como tal.

data⊥: Typewhere-- su contraparte es ⊤, el tipo cuyo sólo tiene un término.data⊤: Typewhere⋆: ⊤

Observa que no tiene constructor alguno. Por lo tanto no hay forma de construir un términode ⊥.

Si$A$ es una proposición, entonces$⊥ ⊃ A$.

⊥-e: {A: Type}→ ⊥-------------→ A⊥-e ()

Donde () es una "función vacía".

La negación de una proposición es un operador que recibe una proposicióny nos regresa otra proposición.

¬: Type→ Type¬ T= T→ ⊥

Sean$A, B$ proposiciones. Si$A ⊃ B$ y$¬B$, entonces$¬A$.

¬impl: {A B: Type}→ (A→ B)→ ¬ B-------------→ ¬ A¬impl a→b ¬b a= ¬b(→app a→b a)

Sea$P$ una proposición. Entonces$¬(P ∧ ¬P)$.

no-contr: {P: Type}-----------→ ¬(P ∧ ¬ P)no-contr p∧¬p= ∧-er p∧¬p (∧-el p∧¬p)

Nuestra prueba refleja la siguiente deducción.

 {P:Type}⊢P∧¬P-----------⊢⊥

pero eso es justo lo que nos pide la definición de la negación.

Sea$A$ una proposición. Entonces$A ⊃ ¬(¬ A)$.

¬¬I: {A: Type}→ A-----------→ ¬(¬ A)¬¬I a=λ ¬a→ →app ¬a a

Sean$A, B$ proposiciones. Si$¬A$ y$A$ entonces$B$.

-- Observa que por currying da igual escribir "¬A" y "A" a escribir-- ¬A ⊃ A.¬e: {A B: Type}→ ¬ A→ A--------------→ B¬e ¬a a= ⊥-e (→app ¬a a)

Sean$A, B$ proposiciones. Entonces

• $(¬ A ∧ ¬ B) ⊃ ¬ (A ∨ B)$
• $¬ (A ∨ B) ⊃ (¬ A ∧ ¬ B)$
• $(¬ A ∨ ¬ B) ⊃ ¬ (A ∧ B)$
• $¬ (A ∧ B) ⊃ (¬ A ∨ ¬ B)$

¬∧¬→¬∨: {A B: Type}→ ¬ A ∧ ¬ B-----------→ ¬ (A ∨ B)¬∧¬→¬∨ ¬a∧¬b a∨b= caseof a∨b (∧-el ¬a∧¬b) (∧-er ¬a∧¬b)¬∨→¬∧¬: {A B: Type}→ ¬ (A ∨ B)------------→ ¬ A ∧ ¬ B¬∨→¬∧¬ ¬[a∨b]= (λ a→ →app ¬[a∨b] (left a)) ,λ b→ →app ¬[a∨b] (right b)¬∨¬→¬∧: {A B: Type}→ ¬ A ∨ ¬ B------------→ ¬ (A ∧ B)         ¬∨¬→¬∧ ¬a∨¬b a∧b= caseof ¬a∨¬b                   (λ ¬a→                         →app ¬a (∧-el a∧b))λ ¬b→                        →app ¬b (∧-er a∧b)-- ¬∧→¬∨¬' : {A B : Type}--      → ¬ (A ∧ B)--      ---------------      → (¬ A ∨ ¬ B)-- ¬∧→¬∨¬' ¬a∧b = ?

El marco teórico bajo el cual trabaja Agda está basado en la lógicaintuicionista. En virtud de la equivalencia de implicación$$¬(A ∧ B) ⊃ ¬A ∨ ¬B$$con el lema del tercer excluido:$$A ∨ ¬A ⊃ ⊤$$no podemos terminar de demostrar las equivalencias de De Morgan. Si en verdadqueremos con toda nuestra alma emplear el lema del tercer excluido,podemos introducirlo como un postulado de la siguiente forma:

• README.Case

postulateLEM: {A: Type}→  A ∨ ¬ Alemma1: {A: Type}→ ¬ (¬ (¬ A))→ ¬ Alemma1 ¬[¬¬a] a= →app ¬[¬¬a] (¬¬I a)dnn: {A: Type}→ ¬(¬ A)----------→ Adnn {A} ¬¬a= caseof LEM              (λ a→ a)-- sup Aλ ¬a→ ⊥-e (¬e ¬¬a ¬a)-- sup ¬A

¿Puedes probar la equivalencia de DeMorgan restante con estas herramientasno constructivas?

-- ¬∧→¬∨¬ : {A B : Type}--      → ¬ (A ∧ B)--      ---------------      → ¬ A ∨ ¬ B-- ¬∧→¬∨¬ = ?

En esta sección codificaremos a los números naturales en Agda y demostraremosalgunas propiedades sobre los objetos que vayamos construyendo.

Una familia de tipos es una función que manda términos en tipos.

dataBool: Typewheretrue: Boolfalse: Bool-- D es una familia de tipos indizada por Bool.D: Bool→ TypeD true= BoolD false= ⊥--- Los tipos dependientes nos permiten definir familias de funciones para cada Tipo--- Esto se conoce como polimorfismo-- Observa que esta función recibe como parámetro una familia de tipos (X : Bool → Type)-- "Para todo b : Bool, define cómo se comporta X b".if[_]_then_else_: (X: Bool→ Type)→ (b: Bool)→ X true→ X false→ X b-- si b es true, entonces actúa según la familia en true.if[ X ] true then x else y= x-- si b es false, entonces actúa según la familia en false.if[ X ] false then x else y= y

$$\prod\limits_{b : Bool} D(b)$$

Definimos a los números naturales como untipo inductivo*.

dataℕ: Typewherezero: ℕsuc: ℕ→ ℕ

La definición es inductiva:

• La clausula base :zero es un término de ℕ
• La clausula inductiva : sit : ℕ entoncessuc t : ℕ.

Por conveniencia y eficiencia, le pedimos a Agda que utilice los símbolos con los queestamos familiarizados para denotar a los números naturales en lugar de escribirsuc (suc (suc … (suc zero) … )) para denotar a un número.

{-# BUILTIN NATURAL ℕ #-}

Con la instrucción anterior, Agda se apoya en la implementación de los númerosnaturales con la que viene Haskell.

Ya con otro tipo más interesante, podemos jugar con nuestra función anterior

fam: Bool→ Typefam true= ℕfam false= Boolfun: (b: Bool)→ fam bfun b= if[ fam ] b then6 else false-- Podemos permitir que los tipos que devuelve una función no sean los mismos :D

Ya que estamos un poco más familiarizados con los tipos dependientes codifiquemosel principio de inducción matemática en Agda para números naturales.

Sea$φ$ una propiedad de los números naturales. Si$φ(0)$ y$φ(n) ⊃ φ(n+1)$ entonces$∀ k ∈ ℕ : φ(k)$.

Para codificar una propiedad de los números naturales arbitraria, podemos hacerlocon una familia de tipos indizada sobre ℕ, de modo que{φ : ℕ → Type} jugará el papelde una propiedad sobre ℕ. Luego, necesitamos construir dos términos en virtud de lo quequeremos demostrar: un término para φ(0);φ 0; y un término para φ(n) ⊃ φ(n+1);(n : ℕ) → φ n → φ (suc n); esto se puede leer como "$∀ n ∈ ℕ . (φ(n) ⊃ φ(n+1))$".Nuestra meta entonces es construir un término o testigo de(k : ℕ) → φ n; que se puede leer como "$∀ k ∈ ℕ . φ(k)$".

Nota sobre la notación:agda function-types

ℕ-elim: {φ: ℕ→ Type}→ φ zero→ ((n: ℕ)→ φ n→ φ (suc n))------------------------------→∀ (k: ℕ)→ φ k---- Es lo mismo que sólo escribir (k : ℕ) → φ k pero---- se ve perron jajaja (TODO Borrar esto jaja)---- Sup. que ocurren las dos hipótesis.---- Queremos construir un testigo de la conclusión a partir de estas hip.-- ℕ-elim {φ} φ₀ f = h--   where--    h : (n : ℕ) → φ n--    h n = ?-- hacemos casos sobre n, en tanto que n ∈ ℕ implica que n es zero o es sucesor de alguien.ℕ-elim {φ} φ₀ f= hwhereh:∀ (n: ℕ)→ φ n    h zero= φ₀    h (suc k)= f k HI----- Alternativamente, h (suc k) f k (h k)whereHI: φ k----------- la HI nos da información sobre cómo fue construida laHI = h k        ----------- evidencia de φ hasta k. Recordar que φ: ℕ→ Type es una fam.---- Es recursivo el asunto. Para verificar h (suc k), verfica h k, y---- así te vas hasta h zero, y luego te subes de regreso a h (suc k).-- ℕ-elim {φ} φ₀ f = h--   where--    h : (n : ℕ) → φ n--    h zero = φ₀      --- La evidencia de que φ zero ocurre es una hipótesis.--- La evidencia de que sabemos cómo producir una prueba para suc n está codificada--- en nuestra hipótesis.--- Agda nos pide φ (suc n). Notamos que podemos producir un término de este tipo--- a partir de nuestra hipótesis f. Para aplicar dicha hipótesis necesitamos--- un término de tipo (n₁ : ℕ) → φ n₁--    h (suc n) = f n HI--      where--        HI : φ n--        HI = h n

Una prueba más elegante:

Nat-elim: {φ: ℕ→ Type}→ φ0→ ((k: ℕ)→ φ k→ φ (suc k))--------------------------------→ (n: ℕ)→ φ nNat-elim {φ} φ₀ f zero= φ₀Nat-elim {φ} φ₀ f (suc x)= f x (Nat-elim φ₀ f x)

De acuerdo con Martin Escardó, esta es la única definición recursiva en toda la teoríade tipos de Martin Löf. Cualquier otra llamada recursiva tiene que ser propia de laregla de eliminación del tipo inductivo.

Ahora que ya tenemos nuestro tipo de números naturales y una forma de hacer inducciónsobre estos, utilicemos estas construcciones para demostrar cosas sobre ℕ.

Definimos la suma de forma inductiva.

La suma en ℕ se define como a continuación.

_+_: ℕ→ ℕ→ ℕ-- casos en m en m + n = ?zero + zero= zerozero + suc n= suc nsuc m + zero= suc msuc m + suc n= suc (suc (m + n))_·_: ℕ→ ℕ→ ℕzero · n= zero(suc m) · n= (m · n) + n_≤_: ℕ→ ℕ→ Typezero ≤ y= ⊤suc x ≤ zero= ⊥suc x ≤ suc y= HIwhereHI: Type    HI= x ≤ y

[nat_sum]!(/Users/nicky/Working Directory/Servicio Social/PresentacionAgda/nat_sum_conm.png)

La igualdad entre dos objetos matemáticos generalmente es una proposición.Si los objetos en cuestión satisfacen nuestra definición de igualdad, entoncespodemos dar una prueba de dicha igualdad; la experiencia muestra que esto no siemprees trivial; en otro caso, no podemos dar prueba de este hecho.

Para decidir la igualdad entre dos números naturales, por construcción necesitamosverificar tres casos:

• ambos son cero
• alguno de los dos son cero
• sus sucesores son iguales.

Entonces, dados dos números naturales, siguiendo nuestro paradigma de proposiciones como tipos,definimos el tipo igualdad de dos números naturales.

_≡'_: ℕ→ ℕ→ Typezero ≡' zero= ⊤zero ≡' suc b= ⊥-- el cero no es sucesor de nadiesuc a ≡' zero= ⊥-- no tenemos reflexividad todavia. Mismo caso que el anterior.suc a ≡' suc b= a ≡' b-- si sus sucesores son iguales, entonces inductivamente decidimos.

Existe una forma más general de definir la igualdad para cualesquier tipo, y es medianteel tipo identidad. El razonamiento básico detrás de la definición es la siguiente:

Bajo el paradigma de Tipos como Proposiciones, como ya se discutió antes, tiene sentidopensar en la igualdad como un tipo más. Sin embargo, queremos definir la igualdad paracualquier tipo. ¿Cómo definimos este tipo? La información básica para decidir la igualdadentre dos objetos es la siguiente: necesitamos la clase de objetos con los que estamos lidiando,esto es el tipo de los objetos a comparar, a saberT, y necesitamos dos objetos a comparar,esto es,x : T yy : T. Dada esta información, el tipo igualdadx = y es un tipo quedepende de los términosx yy. Por lo tantox = y debe ser un tipo dependiente.Sip : x = y, entonces es porquep es testigo de la igualdad; en otras palabras,p es una identificación dex y dey. Sip, q : x = y, entonces debemos poder formartambién el tipop = q. De esta forma, podemos emplear a los tipos para decir cosas sobrela igualdad (¿será que dos identificaciones también pueden identificarse entre si?, ¡pensar enhomotopía!). Finalmente, la propiedad fundamental que satisfacen todas las nociones de igualdades una de reflexividad. Se codifica al tipo identidad entonces como un tipo inductivodependiente con un constructor que debe testificar la reflexividad, con el propósito de dotarde estructura inductiva y de tipo con el fin de hacer más rica la discusión sobre la igualdaden la teoría.

Aunque la discusión dada en esta exposición es quizás un poco larga, el tema de igualdades uno muy rico en contenido y discusión dentro de la teoría homotópica de tipos. Se hacela cordial invitación a leer más sobre el tema en las referencias.

-- Dados un tipo T, para cada dos x , y : T-- tenemos un tipo x ≡ y llamado tipo identidad de x a y.data_≡_ {T: Type}: T→ T→ Typewhererefl: (x: T)→ x ≡ x-- x ≡ y es la proposición "x = y según T", y para cada x tenemos una prueba de que x es-- igual a x según T.

Probemos la reflexividad de ≡.

≡ es transitiva y simétrica.

≡-sym:∀ {T: Type} {n m: T}→ n ≡ m-----------→ m ≡ n-- n ≡ m fue construido como `refl n`-- para construir m ≡ n basta entonces hacer lo mismo, en tanto que n ≡ m.-- es decir, tanto m y n están identificados internamente en T.≡-sym (refl n)= refl n≡-trans:∀ {A: Type} {x y z: A}→ x ≡ y→ y ≡ z-------------------------→ x ≡ z-- como x ≡ y, y por hipótesis y ≡ z, entonces x y z deben estar-- también identificados en x ≡ y-- ≡-trans x≡y (refl y) = x≡y≡-trans (refl x) (refl y)= refl x

Regresando a nuestras definiciones de suma, producto y orden; ya conel tipo identidad y los tipos dependientes podemos demostrar propiedades sobreestas operaciones.

• ∀ A B : Type . ∀ f : A → B . ∀ x y : T . x ≡ y ⇒ f x ≡ f y
• ∀ n ∈ ℕ . n + 0 = n
• ∀ n ∈ ℕ . 0 + n = n
• ∀ n, m ∈ ℕ . n + suc m = suc (m + n)

cong:∀ {A B: Type} (f: A→ B) {x y: A}→ x ≡ y--------→ f x ≡ f ycong f (refl x)= refl (f x)zero+n-=-n:∀ (n: ℕ)→ (zero + n) ≡ nzero+n-=-n zero= refl zerozero+n-=-n (suc n)= refl (suc n)n+zero-=-n:∀ (n: ℕ)→ (n + zero) ≡ nn+zero-=-n zero= refl zeron+zero-=-n (suc n)= refl (suc n)-- Doble inducción sobre n y m :D+-suc:∀ (n m: ℕ)→ (suc m + n) ≡ suc (m + n)+-suc zero m= cong suc (≡-sym (n+zero-=-n m))+-suc (suc n) zero= cong suc (cong suc (zero+n-=-n n))+-suc (suc n) (suc m)= cong suc (cong suc HI)whereHI: (suc m + n) ≡ suc (m + n)    HI= +-suc n m

La suma en ℕ es conmutativa.

+-conm:∀ (x y: ℕ)→ (x + y) ≡ (y + x)+-conm zero y= ≡-sym AF4whereAF1: (zero + y) ≡ y    AF1= zero+n-=-n yAF2: (y + zero) ≡ y    AF2= n+zero-=-n yAF3: y ≡ (zero + y)    AF3= ≡-sym AF1AF4: (y + zero) ≡ (zero + y)    AF4= ≡-trans AF2 AF3+-conm (suc x) zero= refl (suc x)+-conm (suc x) (suc y)= cong suc (cong suc HI)whereHI: (x + y) ≡ (y + x)     HI= +-conm x y

x ≤ y ⇔ ∃ k : ℕ . x + k = y

open importAgda.Builtin.Sigma-Σ= Σinfix2 -Σsyntax -Σ A (λ x→ B)= ∃ x ∈ A , B_~_: ℕ→ ℕ→ Typea ~ b= ∃ k ∈ ℕ , (a + k) ≡ b~-es-≤:∀ (a b: ℕ)→ a ≤ b-----------→ a ~ b~-es-≤ zero zero leq1= zero , refl zero-- `zero` es tal que testifica lo que se quiere~-es-≤ zero (suc b) leq1= suc b , refl (suc b)-- `suc b` testifica que `zero + suc b ≡ suc b`~-es-≤ (suc a) (suc b) leq1= k , AF2whereHI: ∃ k ∈ ℕ , (a + k) ≡ b    HI= ~-es-≤ a b leq1k: ℕ    k= fst HIHI': (a + k) ≡ b    HI'= snd HIAF1: (suc a + k) ≡ suc (a + k)    AF1= +-suc k aAF2: (suc a + k) ≡ suc b    AF2= ≡-trans AF1 (cong suc HI')

Mencionar a que aplicación de juicios corresponden las combinaciones de teclas en agdaAgda Docs