Semana de descanso y lectura

La semana pasada me desaparecí del planeta (o al menos de la porción digital del mismo) desde el Martes hasta el Sábado. Estuve toda una semanita playando en Puerto La Cruz. :D La verdad, hacía falta un pequeño escape de la rutina para recuperar energía y motivación, más con todo el trabajón que he tenido últimamente, jeje.

No creo que sea tan comodo, pero ¡palantemarik! XD

Fue una semana apartado, más que todo en un hotel con la piscina y eso. Pero además pude hacer algo que no suelo hacer muy a menudo: ¡dormir! XD Siesta tras siesta tras siesta (sé que suena a gente vieja lo de dormir, pero estoy seguro que cualquier computista me entiende, jajaja). Además, tuve la oportunidad de leer un par de libros: uno de literatura y uno técnico.

El libro de literatura que leí fue nada menos que el primero de la trilogía en cinco partes de "The Hitchhikers Guide To The Galaxy" de Douglas Adams. ¡Excelente libro! (y seeeh, debí haberlo leído hace tiempo pero no había tenido realmente la oportunidad hasta ahora.) Lo leí en inglés - como se debe ya que es su lengua original - aunque su inglés es complicado. Sin embargo dibuja escenas bastante detalladas y absurdamente cómicas. ¡Mil veces mejor que la película aquella que ni a los talones le llega! Aunque es gracioso como se le quedan algunos adjetivos pegados al autor como "mind-bogglingly" (viejo, existen otros adjetivos, jajaja), pero estuvo excepcionalmente bueno. Ahora me toca seguir y leer los libros que le suceden. :)

El libro técnico que leí fue "Basic Category Theory for Computer Scientists" de Benjamin Pierce. En realidad fue una relectura, ya que lo había leído ya en otras ocasiones. Pero fue muy valioso releerlo con la aumentada formación formal que tengo ahora y comprendí muchas cosas que no había captado del todo las otras veces. ¡Es una excelente referencia! Recomendado para cualquier computista.

Además, leí una buena parte del "Programming Challenges" de Steven Skiena y Miguel Revilla. Sin embargo, es un enfoque un tanto básico y la lectura se hace tediosa rápidamente. No sé si lo recomendaría para un principiante, pero al menos los problemas propuestos son buenos retos para alguien que esté empezando en esto de los maratones de programación. También comencé a leer un poco del libro de "Homotopy Type Theory" que había dejado en espera. El tipo de escritura de ese libro no es muy clara en ocasiones, pero es comprensible ya que es un compendio de diversos trabajos y diversos autores. Sin embargo, lo que plantean es sumamente interesante y continúo leyéndolo a ver que cosas se pueden utilizar para hacer una mejor computación. :)

Y bueno, no puede faltar la gordura épica durante la semana. Nada más gordito que bufé de desayuno incluido, jajaja. Y en la noche salíamos a comer cada cosa mejor que la otra. Desde parrilla, hasta hamburguesas gourmet y shawarmas callejeros. ¡Todo épicamente bueno!

Y bueno, esto es lo que he de compartir en este momento, jeje. Una semana relax. ¡Hacía falta! Y ahora a volver a la rutina, que hay papers que sacar. XD ¡Hasta una próxima entrada!

Un Libro al Més: Febrero

¡De vuelta a las nubes! :) Como les mencioné en un post anterior, uno de mis objetivos personales del 2014 es leer un buen libro al mes (lo cual no es tan fácil como parece, jajaja). Con una gran serie de responsabilidades en la universidad y muchas cosas en la mente, no había tenido la oportunidad de continuar con esta meta. Sin embargo, lo intentaré nuevamente.

Para el mes de Febrero decidí retomar un libro pequeño, pero violento y poderoso:

Basic Category Theory for Computer Scientists

de Benjamin Pierce

(publicado en 1991, como parte de la serie "Foundations of Computing" de MIT Press)

Ya hace tiempo había comenzado a leerlo, pero nunca tuve la oportunidad de terminarlo. ¡Y es excelente! Aunque no es una lectura ligera, definitivamente, jajaja. Este libro ofrece una introducción a un tema sumamente abstracto, pero de mucha utilidad práctica (especialmente en Computación): La Teoría de Categorías.

En sus principios esta teoría fue menospreciada por ser "demasiado abstracta". De hecho, se le conocía comúnmente por el nombre de "Generalized Abstract Nonsense", lo cual me parece genialmente apropiado, jajaja. Sin embargo, avances en ciencias de la computación han abierto nuevas perspectivas y necesidades para entender la matemática detrás de lo que hacemos. Eventualmente la Teoría de Categorías se hizo notar, pues introdujo muchísimas propiedades interesantes que han sido aplicadas en muchas áreas ya. En particular, son el secreto detrás de la creación de los Monads en los lenguajes funcionales (y posteriormente de los Arrows, que actualmente implementa Haskell).

En resumidas cuentas, la teoría de categorías se define como una colección de objetos y una colección de flechas, que relacionan estos objetos entre si (algo así como una noción generalizada de un grafo). Estas colecciones no son necesariamente conjuntos, aunque los mismos brindan una buena intuición para la teoría que se presenta. La intención de la teoría es descubrir propiedades comunes, de la forma más general posible, usando estas flechas como base para las construcciones involucradas (en vez de los elementos de la colección de objetos, como se esperaría en Teoría de Conjuntos). Finalmente, una categoría puede verse como una generalización de conjuntos junto con todas funciones totales entre ellos. ¡Esta belleza de teoría engloba a todos los objetos con un comportamiento similar a este! Por poner algunos ejemplos:

• Objetos: Conjuntos. Flechas: Funciones totales.
• Objetos: Monoides. Flechas: Homomorfismos.
• Objetos: Grupos. Flechas: Homomorfismos.
• Objetos: Flechas. Flechas: Transformaciones naturales (wait... what?)

La lista continúa... ¡pero hay más! La teoría es tan general que permite agrupar Ω-álgebras arbitrarias, incluso con condiciones E sobre los operadores que incluyen (llamadas (Ω, E)-álgebras). Los monoides, grupos, álgebras booleanas, álgebras de términos, etc., son todos casos especiales de éstas últimas. ¡Incluso hay una categoría para espacios topológicos! Aquí las flechas serían las funciones continuas. Ya la topología generaliza la matemática a niveles extraordinarios. ¡Las categorías, como si nada, son una generalización aún mayor (la topología es sólo un caso especial de estas últimas)! ¿Verdad que se ve un poco más lo de "Generalized Abstract Nonsense"? Jajaja. Aunque la verdad es que me encanta que sea tan abstracto y potencialmente aplicable a tantas estructuras diferentes.

Definitivamente este libro es uno que te puede tener con el ceño fruncido por unos buenos 15 minutos entendiendo lo que dice solamente media página pero, al entender finalmente, la gratificación es enorme. ¡Perfecto para expandir la mente! Lo recomiendo 100% si les gusta la matemática y las cosas abstractas locas. (We are few, but we are proud. XD)

Y bueno, con eso los dejo hasta una próxima entrada. ¡Que la fuerza de los functores los acompañe! :D

Ni tan universal... Lo correcto vs. Lo conveniente

Hoy quiero compartir con ustedes tan solo un párrafo de un libro que he estado leyendo este mes. Como les comenté en ( http://bulda-e-blog.blogspot.com/2014/01/un-libro-al-mes-enero.html ), estoy leyendo "Predicate Calculus and Program Semantics" de Dijkstra y Scholten (1990). El libro es entretenido y bastante ligero (exceptuando el capítulo 5 donde se ponen un poco intensos con la introducción de la cuantificación universal, de la cuál justamente quería hablar).

Dijkstra y Scholten presentan en ese libro una manera inusual de llevar demostraciones lógicas, centrada en la equivalencia en vez de la implicación. Esto acorta considerablemente muchas pruebas y permite exponer propiedades algebráicas que de lo contrario serían difíciles de enunciar. Sin embargo, el costo es convertir la demostración en un cálculo más que en verdadera lógica. La lógica es el estudio de los procesos de razonamiento correctos. ¡Razonamiento humano!. Los razonamientos humanos rara vez se basan en equivalencias y propiedades matemáticas, sino más bien en deducciones realizadas a partir de hechos o suposiciones conocidas.

Desde Aristóteles y sus silogismos, la lógica se ha formalizado de manera que permita deducciones estructuradas y precisas. La lógica simbólica, como la conocemos hoy, de hecho no fue presentada hasta tiempos modernos con Boole y más importantemente con Frege. La lógica que se presenta en el libro parte completamente de lo tradicional y presenta la lógica como una conveniencia, una herramienta y no tanto como objeto de estudio en si. Es otra visión, no necesariamente incorrecta. Eso... hasta que llegas a uno de los últimos párrafos del capítulo 5, el cual les comparto a continuación:

"As the reader will have noticed, we hardly stressed this connection between universal quantification and conjunction. It is not only that we dislike the ominous three dots and that it only works for finite ranges, though -thanks to trading- the range is less a property of the quantified expression and more of a way it has been written down. Our greatest objection is that the analogy sneakily suggests that quantification only provides an (in this case badly needed!) shorthand for 'infinite expressions'. But that metaphor evokes more questions than it answers, and, even worse, questions that we propose to deal with by not raising them, since we don't seem to need the answers. We prefer to view (∀ x :: f.x) as a very finite expression in the one variable f."

Spock does not approve...

Puse en negrita las partes en donde creo que Dijkstra y Scholten están razonando fuera del recipiente. Después de un capítulo completo introduciendo la cuantificación universal como un ente separado, que casualmente se comporta como la generalización de la conjunción, vienen y sueltan esa bomba. ¿Por qué están restringiendo la potencia de los cuantificadores a rangos finitos? Esa es una restricción realmente grave. Para empezar expresiones como (∀ n : n > 10 : n > 9), que se leería como "Toda n mayor que 10, es a su vez mayor que 9", estarían ahora mal formadas ya que su rango es infinito. Además, priva al cuantificador de su naturaleza universal y su poder expresivo. Esta suposición, en mi opinión, casi haría completamente inútil a la lógica de predicados (ni hablar si se incluyen lógicas de órdenes superiores).

La justificación evidente y pertinente es que el libro no está dirigido a lógicos, ni matemáticos, sino a computistas. En computación, las estructuras no solo son discretas, sino que son finitas (limitadas por la memoria de la computadora que se use), por lo tanto no hace falta tomar consideraciones hacia el infinito. Es un argumento sólido, pero completamente errado (en mi opinión). No se puede consolidar una teoría únicamente basada en convenciencia. Es como si los diseñadores de lenguajes de programación basaran sus decisiones en que cosas son más fáciles de implementar o no, en vez de las facilidades que se ofrecerían al potencial futuro programador. Siempre se pueden hacer compromisos, pero una restricción tan grave no se justifica. Por ejemplo, muchas de las cosas importantes en computación usan inducción para demostrar ciertas propiedades.

Axioma de Inducción: P.0 ∧ (∀ n : n e N ∧ P.n : P.(n+1)) ⇒ (∀ n : n e N : P.n)

Nótese que el predicado P podría estar cuantificado universalmente también, pero no lo puse para no pasar a lógica de segundo orden y sobrecomplicar el punto. Si la cuantificación universal se restringe a expresiones finitas, el mismísimo axioma de inducción estaría mal formado y por ende no podría utilizarse de forma general, jajaja. Debo decir que no me convence en lo absoluto el argumento de ellos, aún con lo útil que ha resultado la lógica que ellos proponen (que casualmente, es la que estudiamos en el curso de Lógica Simbólica en la USB), no deberían estar suponiendo restricciones tan fuertes tan a la ligera. En especial esta frase: "questions that we propose to deal with by not raising them", me parece totalmente fuera de lugar. La manera de resolver problemas no es escondiendo la cabeza e ignorándolos totalmente, creo yo.

Y bueno, esto era lo que quería compartir por ahora. Creo que es el post más gallo y TL;DR en este blog hasta el momento, jajjaa. ¡Gracias por leer (si llegaron hasta acá)! XD Creo que éste es un buen ejemplo de como hasta las personas más brillantes e influyentes, aún pueden caer en la tentación de ponerse un tapaojos temporal, comprarse un periquito mascota y no hacer las cosas de la mejor manera. Creo que es importante poder tener el buen criterio de atrapar estos parches y ser capaces de decidir y razonar si los argumentos presentados son convincentes o no. En este caso creo que no y sé de quienes creen que si es suficiente (y en particular uno de ellos es la persona más brillante que conozco), pero para mi no lo es, jeje. Espero no espantarlos demasiado de esta locura bulda.e.bienística y hasta una próxima entrada. Bytes! :D

Un Libro al Mes: Enero

En el pasado post ( http://bulda-e-blog.blogspot.com/2013/12/graciabale-2013-palante-marik-2014.html ), último del 2013, una de las cosas que me propuse fue leer al menos un buen libro al mes. Así, puedo aprovechar las maravillas que recién he redescubierto en la biblioteca de la USB y que no puedo seguir ignorando así (must learn new things! XD).

El libro que me propongo leer para Enero está íntimamente relacionado con mi trabajo de maestría, como un antecedente de suma importancia. Como para no salir del tema (dado que pronto sería la defensa) y ahondar más en lo que considero un libro bastante interesante y divertido de leer, me propongo leer entonces:

"Predicate Calculus and Program Semantics"

de Edsger Dijkstra y Carl Scholten

(publicado en 1990, por la editorial Springer-Verlag)

Ya he leído dos o tres capítulos del libro y está sumamente bien escrito, fácil de entender e interesante. Además, la clásica arrogancia de Dijkstra hace que algunos párrafos hasta den un poco de risa, jajaja. Después de todo, Alan Kay decía: "Arrogance in Computer Science is measured in nano-Dijkstras". No puede constarme que así sea, pero aún así la cita es épica. XD

Una vez termine de leerlo posiblemente escriba otro post con lo que más me gustó, lo que no y lo que considero lo más importante/divertido/interesante del libro. Por ahora, les cuento que muy a grandes rasgos el libro trata de explicar un cálculo (reglas de manipulación) aplicado a programas y especificaciones para los mismos, introduciendo con este objetivo los transformadores de predicados (concentrándose principalmente en la precondición más débil). Para esto, se propone una manera ecuacional de tratar con la lógica de predicados que ellos mismos describen como lo suficientemente formal como para que no haya confusiones, pero sin llegar al punto de que las manipulaciones sean ilegibles y antintuitivas.

Nota aparte, es gracioso como muchos nombres famosos de las ciencias de la computación son reconocidos por trabajos que quizá no fueron los más relevantes que tuvieron (al menos en mi opinión). Dijkstra es mayormente conocido por su algoritmo para hallar caminos de costo mínimo, en grafos sin arcos de costo negativo, en O(n.log(n)). Sin embargo, su mayor contribución es posiblemente aquella de los transformadores de predicados para razonar sobre programas (y muchas otras cosas más). Igualmente, Tony Hoare es conocido por su algoritmo de ordenamiento de arreglos: Quicksort. En mi opinión, su definición de tripletas de programas y especificaciones en conjunto con las relgas de manipulación de las mismas es mucho más relevante. Aunque bueno, ese pudiera ser el "formal methods geek" en mi hablando simplemente, jajaja. :P

Bueno, con esto los dejo por ahora. ¡Es el primer post de muchos en el 2014! Y todo el que quiera sigue bienvenido de compartir la bulda.e.locura si les parece interesante, jeje. Hasta la próxima. Bytes! :D