06/12/2019, 08:40:05 pm *
Bienvenido(a), Visitante. Por favor, ingresa o regístrate.

Ingresar con nombre de usuario, contraseña y duración de la sesión
Noticias: Renovado el procedimiento de inserción de archivos GEOGEBRA en los mensajes.
 
 
Páginas: [1]   Ir Abajo
  Imprimir  
Autor Tema: El juego de los números naturales: demostraciones asistidas con Lean  (Leído 170 veces)
0 Usuarios y 1 Visitante están viendo este tema.
geómetracat
Moderador Global
Pleno*
*

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 801



Ver Perfil
« : 07/11/2019, 01:59:20 pm »

Hola,

Hace tiempo le prometí a manooooh hacer un hilo hablando un poco sobre demostraciones asistidas por ordenador. Últimamente estoy bastante mal de tiempo, así que no me he podido mirar todo lo que hubiera querido estas cosas,
Pero a cambio, traigo algo mucho mejor que lo que hubiera podido escribir: un enlace al "natural number game":
http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/.
Esto es esencialmente un tutorial del lenguaje de programación Lean, estructurado en forma de juego. El objetivo es, comenzando con los axiomas de Peano de los números naturales, demostrar teoremas básicos para la suma, multiplicación, potencia y desigualdades de naturales (por ejemplo, que la suma y el producto de naturales son asociativas y conmutativas, etc). Esto no es muy distinto de lo que uno puede encontrar en un libro de lógica, pero es instructivo (y divertido) demostrar estas cosas usando un lenguaje de programación.

Este juego se enmarca en el llamado proyecto Xena (https://xenaproject.wordpress.com/), dirigido por Kevin Buzzard del Imperial College, que se dedica a formalizar matemáticas en Lean. La formalización de matemáticas es un campo que últimamente parece estar en auge, y donde se han conseguido recientemente cosas bastante impresionantes (por ejemplo, una formalización del forcing y la prueba de la independencia de la hipótesis del continuo).

El juego todavía no está en su versión final. Dentro de unos días o semanas probablemente habrá bastantes más "pantallas", incluyendo "mundos" sobre funciones y lógica proposicional (cuidado: estos lenguajes de programación no están basados en lógica proposicional o de primer orden sino en teorías de tipos dependientes, lo que hace que algunas cosas sean un poco raras si solamente se está acostumbrado a la lógica "usual"). Pero con lo que hay de momento se puede tener una idea de cómo funcionan estas cosas.

Espero que os guste tanto como me ha gustado a mí.
En línea

La ecuación más bonita de las matemáticas: [texx]d^2=0[/texx]
Masacroso
Pleno*
*****

Karma: +2/-0
Desconectado Desconectado

España España

Mensajes: 1.664


Ver Perfil
« Respuesta #1 : 07/11/2019, 02:25:04 pm »

Sumamente interesante, le echo un vistazo, gracias por compartir. Yo de lo poco que conozco de demostraciones por ordenador es el método WZ.

Wilf, uno de sus creadores, habla de él en sus libros A=B o generatingfunctionology. Es bastante sencillo de utilizar (para una computadora, claro) para demostrar identidades combinatorias.
En línea
manooooh
Pleno*
*****

Karma: +1/-0
Desconectado Desconectado

Sexo: Masculino
Argentina Argentina

Mensajes: 2.433


Ver Perfil
« Respuesta #2 : 10/11/2019, 05:03:48 pm »

Hola

Hace tiempo le prometí a manooooh hacer un hilo hablando un poco sobre demostraciones asistidas por ordenador. Últimamente estoy bastante mal de tiempo, así que no me he podido mirar todo lo que hubiera querido estas cosas,
Pero a cambio, traigo algo mucho mejor que lo que hubiera podido escribir: un enlace al "natural number game":
http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/.
Esto es esencialmente un tutorial del lenguaje de programación Lean, estructurado en forma de juego. El objetivo es, comenzando con los axiomas de Peano de los números naturales, demostrar teoremas básicos para la suma, multiplicación, potencia y desigualdades de naturales (por ejemplo, que la suma y el producto de naturales son asociativas y conmutativas, etc). Esto no es muy distinto de lo que uno puede encontrar en un libro de lógica, pero es instructivo (y divertido) demostrar estas cosas usando un lenguaje de programación.

Este juego se enmarca en el llamado proyecto Xena (https://xenaproject.wordpress.com/), dirigido por Kevin Buzzard del Imperial College, que se dedica a formalizar matemáticas en Lean. La formalización de matemáticas es un campo que últimamente parece estar en auge, y donde se han conseguido recientemente cosas bastante impresionantes (por ejemplo, una formalización del forcing y la prueba de la independencia de la hipótesis del continuo).

El juego todavía no está en su versión final. Dentro de unos días o semanas probablemente habrá bastantes más "pantallas", incluyendo "mundos" sobre funciones y lógica proposicional (cuidado: estos lenguajes de programación no están basados en lógica proposicional o de primer orden sino en teorías de tipos dependientes, lo que hace que algunas cosas sean un poco raras si solamente se está acostumbrado a la lógica "usual"). Pero con lo que hay de momento se puede tener una idea de cómo funcionan estas cosas.

Espero que os guste tanto como me ha gustado a mí.

¡¡Qué buena noticia!! Ya lo estuve probando y me ha parecido muy interesante.

Sólo una vez me olvidé de la maldita coma :risa: pero el error me ayudó a comprender a leer el panel de demostración que tiene la página. Hay que prestar atención, y eso es importante porque es clave para manejar casi cualquier lenguaje de programación.

Ahora me pregunto, ¿qué son las "teorías de tipos dependientes"?

Tengo conocimiento de que C es un lenguaje tipado, pero por ejemplo Haskell no lo es. Es decir unos necesitan declarar sus variables de algún tipo y otros directamente lo infieren con el tipo de dato que nosotros le asignemos. Pero ahora la palabra "dependiente" me complica las definiciones porque cuando en Lean se lee a b c : mynat estamos declarando tres variables de tipo natural -- por ende es un lenguaje tipado.

Por lo demás, es práctica, aprender a demostrar con lenguaje Lean, que se aproxima bastante a lo que un matemático hace. ¡Me gustó!

Gracias por compartirlo geómetracat.

Saludos
En línea
geómetracat
Moderador Global
Pleno*
*

Karma: +0/-0
Desconectado Desconectado

Sexo: Masculino
España España

Mensajes: 801



Ver Perfil
« Respuesta #3 : 12/11/2019, 11:32:25 am »

Sumamente interesante, le echo un vistazo, gracias por compartir. Yo de lo poco que conozco de demostraciones por ordenador es el método WZ.

Wilf, uno de sus creadores, habla de él en sus libros A=B o generatingfunctionology. Es bastante sencillo de utilizar (para una computadora, claro) para demostrar identidades combinatorias.

Me ha resultado muy interesante el comentario, no conocía el método WZ. Aunque diría que el enfoque es algo distinto. Aquí lo que se pretende principalmente es tener una especie de "base de datos" de todas las demostraciones, formalizadas en un lenguaje de manera que sea fácil verificar que son correctas. Esto viene porque algunos matemáticos tenían preocupaciones sobre los errores que se cuelan en muchos papers (incluso publicados en revistas de alto impacto) y de los que nadie se da cuenta hasta años más tarde (o quizás nunca).
Un caso muy famoso es el de Vladimir Voevodsky, que fue un matemático de altísimo nivel (ganador de la medalla Fields) que hizo trabajos muy importantes sobre teoría de homotopía aplicada a geometría algebraica. Pues bien, en uno de sus papers (muy difundido y leído por los expertos del campo) había un error en un lema técnico que se le escapó a todo el mundo, y solamente fue detectado años después por el propio Voevodsky cuando los resultados del paper ya habían sido ampliamente citados y usados en otros trabajos. Por suerte se pudo arreglar, pero esto llevó a Voevodsky a empezar a preocuparse por temas de verificación formal de demostraciones y a crear (junto con otra gente) el campo de la "homotopy type theory", que está muy relacionado con estas cosas.

Ahora me pregunto, ¿qué son las "teorías de tipos dependientes"?

Tengo conocimiento de que C es un lenguaje tipado, pero por ejemplo Haskell no lo es. Es decir unos necesitan declarar sus variables de algún tipo y otros directamente lo infieren con el tipo de dato que nosotros le asignemos. Pero ahora la palabra "dependiente" me complica las definiciones porque cuando en Lean se lee a b c : mynat estamos declarando tres variables de tipo natural -- por ende es un lenguaje tipado.

Haskell sí que es un lenguaje tipado. De hecho, como buen representante de los lenguajes de programación funcional, es un lenguaje donde los tipos son realmente importantes. En primera aproximación al menos, puedes considerar Haskell como una implementación del cálculo lambda tipado, que es una versión más débil de las teorías de tipos dependientes. Así que en realidad Lean y todos estos lenguajes se parecen bastante más a Haskell de lo que se parecen a C (que es tipado, pero es un lenguaje imperativo, no funcional).

Las teorías de tipos se pueden pensar de muchas maneras distintas. Puedes pensar en ellas como en un lenguaje de programación abstracta, o también desde el punto de vista lógico, como una fundamentación de la matemática distinta a la usual de lógica de primer orden + teoría de conjuntos.
De hecho, la primera "teoría de conjuntos formal" (la de los Principia Mathematica de Russell y Whitehead) era una teoría de tipos. Para describir la diferencia con la axiomática usual, fíjate que normalmente las matemáticas se construyen en dos "capas": una primera capa que es lógica de primer orden, y sobre esta capa se definen teorías axiomáticas, en particular los axiomas de ZFC. En las teorías de tipos en cambio, solamente tienes una "capa": todo son tipos. Puedes pensar en primera aproximación un tipo como un conjunto (por ejemplo, el tipo de los números naturales, el tipo de los números complejos, el tipo vacío, ...) y sus "elementos" se llaman términos, y la "relación de pertenencia" se denota por dos puntos. Así por ejemplo, [texx]0:Nat[/texx] quiere decir que [texx]0[/texx] es un término del tipo [texx]Nat[/texx]. A diferencia de ZFC, donde todo es un conjunto, aquí hay una distinción importante entre términos y tipos. Un término en general no es un tipo (aunque a veces puede serlo). Por otro lado, tienes una serie de operaciones que puedes realizar con tipos (por ejemplo, la "unión" de dos tipos) y una serie de constructores que te permiten construir términos de estos tipos compuestos a partir de términos de sus componentes (por ejemplo, si [texx]a:A[/texx], y [texx]B[/texx] es otro tipo, puedes definir el tipo "unión" [texx]A+B[/texx] y tienes un constructor [texx]l[/texx] que te permite decir [texx]l(a):A+B[/texx]; cuidado porque a diferencia de en conjuntos decir [texx]a:A+B[/texx] no tiene ningún sentido: un término no puede tener dos tipos distintos).

Hay muchas relaciones entre teoría de tipos, lógica y computación (y también teoría de categorías). Es un tema fascinante, pero muy largo de explicar aquí. Solamente diré que puedes interpretar los tipos como proposiciones (de lógica proposicional, digamos) y sus términos como demostraciones formales de esa proposición. Esto se conoce como "correspondencia de Curry-Howard".

Las teorías de tipos dependientes son aquellas en los que un tipo puede depender de otros tipos. Esto hace que las teorías de tipos dependientes se parezcan más a la lógica de primer orden (tienes análogos para tipos del cuantificador existencial y universal) y por supuesto son mucho más potentes que las teorías de tipos simples.

En fin, espero que esto dé al menos una muy ligera idea de qué va esto de las teorías de tipos y de las diferencias con la lógica usual. Si quieres preguntar algo más o quieres una descripción más concreta de algo, pregunta.




En línea

La ecuación más bonita de las matemáticas: [texx]d^2=0[/texx]
Masacroso
Pleno*
*****

Karma: +2/-0
Desconectado Desconectado

España España

Mensajes: 1.664


Ver Perfil
« Respuesta #4 : 12/11/2019, 11:45:25 am »

Sumamente interesante todo lo que cuentas geómetracat, lástima de disponer sólo de una vida para tantas cosas interesantes que hay.
En línea
manooooh
Pleno*
*****

Karma: +1/-0
Desconectado Desconectado

Sexo: Masculino
Argentina Argentina

Mensajes: 2.433


Ver Perfil
« Respuesta #5 : 12/11/2019, 09:45:33 pm »

Hola

Me ha resultado muy interesante el comentario, no conocía el método WZ. Aunque diría que el enfoque es algo distinto. Aquí lo que se pretende principalmente es tener una especie de "base de datos" de todas las demostraciones, formalizadas en un lenguaje de manera que sea fácil verificar que son correctas. Esto viene porque algunos matemáticos tenían preocupaciones sobre los errores que se cuelan en muchos papers (incluso publicados en revistas de alto impacto) y de los que nadie se da cuenta hasta años más tarde (o quizás nunca).
Un caso muy famoso es el de Vladimir Voevodsky, que fue un matemático de altísimo nivel (ganador de la medalla Fields) que hizo trabajos muy importantes sobre teoría de homotopía aplicada a geometría algebraica. Pues bien, en uno de sus papers (muy difundido y leído por los expertos del campo) había un error en un lema técnico que se le escapó a todo el mundo, y solamente fue detectado años después por el propio Voevodsky cuando los resultados del paper ya habían sido ampliamente citados y usados en otros trabajos. Por suerte se pudo arreglar, pero esto llevó a Voevodsky a empezar a preocuparse por temas de verificación formal de demostraciones y a crear (junto con otra gente) el campo de la "homotopy type theory", que está muy relacionado con estas cosas.

Concuerdo totalmente. De hecho es justo lo que había pensado en su momento y me refrescaste: Tener una especie de DB en donde se alojen todas las demostraciones formales, con el hecho de no repetir lógica y así partir de algunos axiomas y demostrar toda la matemátca que conocemos sin repetir hipótesis (o las menos posible). Armar como una especie de "Mamushkas".

Haskell sí que es un lenguaje tipado. (...)

:sorprendido:. Fui a Wikipedia y tenés razón.

Pero cuando vi Haskell (a principio de año que luego dejé por el trabajo) me hicieron crear sentencias como


esMayor edad = edad > 18

tieneEdadLaboralActiva edad = edad > 18 && edad < 30

estimacionPolicial acto = length (maximum acto) * 1000

consecuencia "campeonato" = "banderazo"
consecuencia "despidos" = "piquete"
consecuencia "Dia de la Memoria" = "banderazo"

moverArriba (x,columna) = (x,columna++"hundido")

pasaronCosas quePaso = (consecuencia,quePaso,estimacionPolicial)


y todas ellas no tienen ningún tipo de dato definido previamente (por ejemplo no dice bool esMayor edad = edad > 18). Haskell lo interpreta sólo. Por eso pensé que era un lenguaje no tipado.

(...) De hecho, como buen representante de los lenguajes de programación funcional, es un lenguaje donde los tipos son realmente importantes. En primera aproximación al menos, puedes considerar Haskell como una implementación del cálculo lambda tipado, que es una versión más débil de las teorías de tipos dependientes. Así que en realidad Lean y todos estos lenguajes se parecen bastante más a Haskell de lo que se parecen a C (que es tipado, pero es un lenguaje imperativo, no funcional).

Las teorías de tipos se pueden pensar de muchas maneras distintas. Puedes pensar en ellas como en un lenguaje de programación abstracta, o también desde el punto de vista lógico, como una fundamentación de la matemática distinta a la usual de lógica de primer orden + teoría de conjuntos.
De hecho, la primera "teoría de conjuntos formal" (la de los Principia Mathematica de Russell y Whitehead) era una teoría de tipos. Para describir la diferencia con la axiomática usual, fíjate que normalmente las matemáticas se construyen en dos "capas": una primera capa que es lógica de primer orden, y sobre esta capa se definen teorías axiomáticas, en particular los axiomas de ZFC. En las teorías de tipos en cambio, solamente tienes una "capa": todo son tipos. Puedes pensar en primera aproximación un tipo como un conjunto (por ejemplo, el tipo de los números naturales, el tipo de los números complejos, el tipo vacío, ...) y sus "elementos" se llaman términos, y la "relación de pertenencia" se denota por dos puntos. Así por ejemplo, [texx]0:Nat[/texx] quiere decir que [texx]0[/texx] es un término del tipo [texx]Nat[/texx]. A diferencia de ZFC, donde todo es un conjunto, aquí hay una distinción importante entre términos y tipos. Un término en general no es un tipo (aunque a veces puede serlo). Por otro lado, tienes una serie de operaciones que puedes realizar con tipos (por ejemplo, la "unión" de dos tipos) y una serie de constructores que te permiten construir términos de estos tipos compuestos a partir de términos de sus componentes (por ejemplo, si [texx]a:A[/texx], y [texx]B[/texx] es otro tipo, puedes definir el tipo "unión" [texx]A+B[/texx] y tienes un constructor [texx]l[/texx] que te permite decir [texx]l(a):A+B[/texx]; cuidado porque a diferencia de en conjuntos decir [texx]a:A+B[/texx] no tiene ningún sentido: un término no puede tener dos tipos distintos).

Hay muchas relaciones entre teoría de tipos, lógica y computación (y también teoría de categorías). Es un tema fascinante, pero muy largo de explicar aquí. Solamente diré que puedes interpretar los tipos como proposiciones (de lógica proposicional, digamos) y sus términos como demostraciones formales de esa proposición. Esto se conoce como "correspondencia de Curry-Howard".

Las teorías de tipos dependientes son aquellas en los que un tipo puede depender de otros tipos. Esto hace que las teorías de tipos dependientes se parezcan más a la lógica de primer orden (tienes análogos para tipos del cuantificador existencial y universal) y por supuesto son mucho más potentes que las teorías de tipos simples.

En fin, espero que esto dé al menos una muy ligera idea de qué va esto de las teorías de tipos y de las diferencias con la lógica usual. Si quieres preguntar algo más o quieres una descripción más concreta de algo, pregunta.

No puedo seguirte mucho pero creo que lo explicaste de forma muy clara Aplauso.

Vamos, que [texx]0\in\Bbb{N}[/texx] es lo mismo que 0 : Nat; "se parecen demasiado", como si yo dijese [texx]S\to b+bS[/texx] que en notación BNF se escribe [texx]\langle S\rangle ::=b\mid b\ \langle S\rangle[/texx]. Quizás sean ejemplos muy simples y por eso se "vean muy parecidos entre sí" pero en el fondo es como decís: son cosas muy distintas.

Para el resto de la cita: ¿El constructor vendría a ser como algo auxiliar, algo que nos permite hacer otras cosas? Lo asemejo a una demostración matemática "clásica", en donde en la prueba se definen funciones auxiliares, variables auxiliares, y luego esas cosas auxiliares se reemplazan para dar lugar a la prueba en sí. Pero puedo estar equivocado.

Saludos
En línea
Páginas: [1]   Ir Arriba
  Imprimir  
 
Ir a:  

Impulsado por MySQL Impulsado por PHP Powered by SMF 1.1.4 | SMF © 2006, Simple Machines LLC XHTML 1.0 válido! CSS válido!