Introducción a la programación Introducción al entorno Haskell

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

Download Report