Introducci´on a la programaci´on Introducci´on al entorno Haskell ´ Taller de Algebra I Primer cuatrimestre de 2015 ´ Taller de Algebra I ´ ¿De qu´e se trata el taller de Algebra I? 1 2 3 Dar una introducci´ on a la computaci´ on y a la programaci´ on, apta tanto para estudiantes de computaci´ on como para estudiantes de matem´ atica. Implementar los algoritmos que se ven en las clases te´ oricas y pr´ acticas... ... usando programaci´ on funcional. Clases te´ orico-pr´acticas todas las semanas del cuatrimestre, dictadas en el laboratorio de computaci´ on. Aproximadamente dos horas de clase y una para consultas. R´egimen de cursada y evaluaci´on R´egimen de evaluaci´ on: Un trabajo pr´ actico en grupos de exactamente tres personas. Debe aprobarse y luego defenderse mediante un coloquio que se aprueba individualmente. Un conjunto de ejercicios individuales que se deben presentar. Son los marcados con asteriscos del final de cada clase. Deber´ an poder comprender y contestar preguntas sobre su resoluci´ on. En caso de no aprobar en alguna de las instancias: Si el trabajo pr´ actico no est´ a aprobado: u ´nica reentrega del trabajo de manera grupal. Si la defensa del trabajo y/o de los ejercicios no est´ a aprobada: hay un u ´nico recuperatorio de los coloquios. No es necesario aprobar para anotarse en las materias correlativas. ´ S´ı es necesario aprobar para rendir el final de Algebra I. ¿Qu´e hacemos en computaci´on? Resolvemos problemas... ¿pero c´ omo? Para resolver un problema 1 2 3 Identificar el problema a resolver. Pensar una soluci´ on con ciertas caracter´ısticas (algoritmo) que sirva para resolverlo. Implementar un programa que respete ese algoritmo. Los programas pueden ser vistos como descripciones ejecutables de la soluci´on de un problema. Ejecutables por... Una computadora es una m´aquina que procesa informaci´on autom´aticamente de acuerdo con un programa almacenado. Claude Bellavoine, ¿Qu´ e es una computadora? Editorial El Ateneo, 1969. Paradigmas de lenguajes de programaci´on ¿C´omo es un lenguaje de programaci´ on? ¿C´ omo se le dice a una computadora lo que tiene que hacer? Paradigma: Definici´ on del modo en el que se especifica el c´omputo (que luego es implementado a trav´es de programas). Representa una “toma de posici´ on” ante la pregunta: ¿c´omo se le dice a la computadora lo que tiene que hacer?. Todo lenguaje de programaci´ on utiliza herramientas de uno o m´as paradigmas. Lenguajes representativos: Paradigma de programaci´ on imperativa: C, Basic, Ada, Clu, . . . Paradigma de programaci´ on en objetos: Smalltalk, Ruby, . . . Paradigma de programaci´ on orientada a objetos: C++, C#, Java, Python, ... Paradigma de programaci´ on en l´ ogica: Prolog, Oz,. . . Paradigma de programaci´ on funcional: LISP, F#, Haskell, Erlang, Clojure, Scala, . . . Haskell: programaci´on funcional Haskell B. Curry (1900–1982) Existen muchos otros lenguajes de programaci´ on y otros paradigmas de lenguajes de programaci´ on, cada uno adaptado a diferentes situaciones. ¿Por qu´e la computaci´on es u´til para un matem´atico? La computaci´ on comenz´ o como una rama de la matem´atica, como una forma de entender (entre otras cosas) si todos los problemas son resolubles. Estas computadoras eran ideales. Con el tiempo, las computadoras se volvieron reales. Y cambiaron el panorama, la forma de hacer matem´atica. Permiten hacer cuentas que llevar´ıan a˜ nos de manera manual probar conjeturas chequar todos los casos en un teorema probar que un teorema est´a bien demostrado y m´as Veamos un ejemplo: los cuatro colores ¿Cu´antos colores hacen falta para colorear un mapa de tal manera que dos regiones lim´ıtrofes tengan distintos colores? Ejemplo: el mapa del mundo y sus pa´ıses se puede colorear con 4 colores. En 1852, Francis Guthrie le pregunt´ o a su hermano matem´atico si 4 colores alcanzar´ıan para cualquier mapa. Ni el hermano de Guthrie, ni su profesor (Augustus de Morgan) ni otros matem´aticos de la poca pudieron demostrar que fuese as´ı (ni encontrar un contraejemplo). Cuatro colores En 1879, Alfred Kempe public´ o un trabajo donde demostr´o que era cierto, que 4 colores bastaban para cualquier mapa. o que la demostraci´ on de Kempe estaba mal. En 1890, Percy Heawood prob´ En 1977, Appel y Haken demostraron que era cierto, que 4 colores bastaban para cualquier mapa. Pero la demostraci´ on de Appel y Haken dividi´ o a la comunidad matem´atica. El problema: Se reduc´ıan a mano todos los mapas a unos 10.000. Chequear que estos eran todos los casos posibles no es sencillo. Adem´as, en la verificaci´ on de estos casos, se encontraron varios errores (que fueron corregidos). Por u ´ltimo, Appel y Haken probaron que en estos casos 4 colores bastaban usando una computadora. ¿Por qu´e creerle a una computadora? Un programa, dec´ıan los cr´ıticos de la computaci´ on entre los matem´aticos, puede fallar (algo que se testea corriendo el mismo programa en distintas m´aquinas), y mucho m´as importante: estar mal hecho (tener bugs). En 2004, Georges Gonthier demostr´ o formalmente el teorema de los cuatro colores. Lo hizo con una computadora (no los 10.000 casos sino todo el teorema) pero escribiendo la demostraci´ on en un lenguaje que sirve para verificar demostraciones: Coq. Observaci´ on: Coq no es el u ´nico lenguaje desarrollado para verificar demostraciones. En el paper http://www.cs.ru.nl/˜freek/comparison/comparison.pdf √ se muestran programas que prueban que 2 es irracional en 17 lenguajes distintos. Ahora un ejemplo posta: la conjetura de Kepler Veamos ahora otro teorema, m´as antiguo, m´as interesante y aun m´as dif´ıcil. Caso f´ acil: dimensi´ on 2. ¿C´ omo se ponen c´ırculos del mismo tama˜ no en el plano de manera de desperdiciar la menor superficie posible? En la disposici´ on de la izquierda, la superficie desperdiciada es mayor que en la de la derecha. Se puede probar que el empaquetamiento hexagonal es la mejor disposici´on (de las infinitas posibles). conjetura de Kepler Caso dif´ıcil: dimensi´ on 3. ¿C´ omo ubicar esferas del mismo radio en el espacio de manera que el volumen desperdiciado sea el menor posible? Las esferas van centradas en los puntos rosas y turquesas. La prueba En 1611, Johannes Kepler public´ o “Strena Seu de Nive Sexangula” (copo de nieve de 6 puntas), donde afirm´ o sin demostrarlo que estas dos formas son las mejores. Esta afirmaci´ on se hizo conocida como la conjetura de Kepler. Despu´es de algunas pruebas falsas por diversos matem´aticos, Tom Hales anunci´o en 1998 que junto con su alumno Samuel Ferguson hab´ıan demostrado la conjetura. La prueba estaba esparcida en 6 papers, con un total de 250 p´aginas m´as 3Gb de programas y archivos que eran necesarios para testear decenas de miles de casos. Hales envi´ o el resultado final a la revista Annals of Math. Un grupo de 12 r´eferis intent´o chequear la validez de la prueba durante a˜ nos. Finalmente, desistieron. Se public´ o en la revista en 2003, con un comentario que dec´ıa que los r´eferis estaban 99% seguros de la correctitud de la demostraci´ on. Flyspeck Hales, no muy convencido, lanz´ o un proyecto ambicioso: demostrar la conjetura de Kepler formalmente. Us´ o para esto dos lenguajes de verificaci´on de pruebas: HOL Light e Isabelle. La demostraci´ on se encuentra explicada en http://arxiv.org/pdf/1501.02155.pdf (enero de 2015, 21 p´aginas). El enunciado en HOL Light es: |- the_kepler_conjecture <=> (!V. packing V ==> (?c. !r. &1 <= r ==> &(CARD(V INTER ball(vec 0,r))) <= pi * r pow 3 / sqrt(&18) + c * r pow 2)) Prueba autom´atica de teoremas Es posible escribir un algoritmo que permite probar mec´anicamente teoremas? M´as precisamente, dar un algoritmo general que dada una f´ormula de la l´ogica de primer orden indique si la misma es un teorema o no. Entscheidungsproblem (problema de decisi´ on) formulado por David Hilbert en 1928. Problema de decisi´on Dados: un conjunto S de datos de alg´ un tipo (por ejemplo, formulas de la l´ogica de primer orden), y una propiedad P de los elementos de S El problema de decisi´ on asociado es dar un algoritmo que termina y devuelve verdadero o falso para cada elemento s ∈ S, y retorna verdadero si y s´ olo si s tiene la propiedad P. Un problema es decidible si existe tal algoritmo Decidibilidad de Entscheidungsproblem Se intent´ o encontrar sin ´exito la soluci´ on al Entscheidungsproblem Luego la pregunta fue si se puede probar que tal algoritmo no existe Independientemente Turing y Church en 1936/7 mostraron que este problema es indecidible (no tiene soluci´ on) Dieron una definici´ on precisa de algoritmos o las M´ aquinas de Turing y prob´ o que el problema de la parada Turing desarroll´ es no decidible Church desarroll´ o el c´ aculo lambda y mostr´ o que no existe algoritmo que pueda decidir si dos funciones son equivalentes Estos enfoques son equivalentes y capturan la noci´ on de los problemas que son computables Recursos para el Taller Interprete de Haskell GHCI (The Glasgow Haskell Compiler Interactive environment) Ubuntu? sudo apt-get install ghc Mac? brew install haskell-platform Windows? (buu) http://www.haskell.org/ghc/download Editores de Texto Ubuntu? Sublime, Gedit, vim, etc. Mac? Sublime, Texmate, Atom, vim etc. Windows? Sublime, Atom, Notepad++, etc. Trabajen comodos!! M´as Recursos C´omo compartir C´odigo 1 Email (no) 2 Dropbox (puede ser) 3 Google Docs (mejor) 4 svn (se hizo la luz) 5 git (vamoo los pibe) Comandos u´tiles para consolas Qu´ e es una consola??? cd ls (dir en windows) cp, mv, rm (copy, move, del en windows) pwd Ejercicio del d´ıa 1 Crear un archivo de texto con el siguiente contenido: suma x y = x - y 2 Guardarlo con el nombre ejemplo.hs en alguna carpeta (no se olviden la ubicaci´on) 3 Abrir GHCI (ghci desde la consola o ejecutando el programa en windows) 4 Cargar el archivo: :l <ruta del archivo> 5 Ejecutar lo siguiente: 6 Corregir y guardar la funci´ on en el archivo para que efectivamente sea la suma (sin cerrar la consola de GHCI) 7 Recargar el programa: 8 Ejecutar suma 2 3 y ver que de 5 :) 9 Aplaudir al docente suma 2 3 :r
© Copyright 2024 ExpyDoc