lunes, 31 de mayo de 2010

SSA

Alcance de una definición

Muchas optimizaciones y transformaciones de programas requieren saber cuándo se usa o no se usa una variable. El caso paradigmático es la eliminación de código muerto.

a=1
b=2
f(a)

Está claro que la segunda línea no es necesaria ya que "b" no se usa luego en el programa.

La forma de saber si se usa y dónde se usa una variable (o, dualmente, si se define y dónde se define una variable) es mediante un análisis de alcance. El gran problema de un análisis de este tipo es que una misma variable puede estar definida en varios lugares y usarse en varios lugares. Incluso, cuando no hay estructuras de control de flujo.

a=1
b=2
f(a) //Se usa el "a" de la primera línea
a=3 //Ahora redefinimos el "a"
f(b)
b=4
g(a,b)

Renombrado de variables

De esta forma es muy lioso trabajar. Sin embargo, dado que las cadenas de definición-uso son alfa-equivalentes (se puede renombrar la variable con otro nombre no usado en el programa) es posible obtener un renombrado donde cada variable se defina únicamente una vez. En el caso de arriba sería

a1=1
b1=2
f(a1)
a2=3
f(b1)
b2=4
g(a2,b2)

Todo esto funciona bien, hasta que introducimos estructuras de control de flujo.

Supongamos una simple selección.

if(cond) a=1
else a=2
f(a)

Si intento renombrar, me encuentro con un problema: Tengo dos definiciones para un uso.

if(cond) a1=1
else a2=2
f(...) //a1 o a2

Funciones φ

Lo que se hace para solucionar este problema es la introducción de funciones φ. Estas funciones devuelven el valor correspondiente según el lugar desde donde provenga el flujo de control.

if(cond) a1=1
else a2=2
a3 = φ (a1, a2) //Usamos "a1" si venimos de la rama "then" y usamos "a2" si es de la rama "else"
f(a3)

Cuando se usa este sistema se dice que el programa está en forma SSA. En esta forma todas las cadenas de definición-uso (y sus duales de uso-definición) son inmediatas de obtener. Esto simplifica muchísimo esas transformaciones y optimizaciones mencionadas al inicio.

Por otra parte, las funciones φ se utilizan como funciones normales hasta que se quiera salir de la forma SSA. Tanto para convertir un programa en SSA como para salir de esta forma existen ya algorimos muy trillados. Quizás hablemos de ellos algún día ya que usan conceptos muy curiosos como las fronteras de dominio.

viernes, 28 de mayo de 2010

Sustituciones

Ya hablé del álgebra de términos, pero no dije nada de cómo se usaba y para qué servía. En este artículo voy a exponer una de las operaciones sobre esta álgebra: la sustitución.

Definición

Realmente, no debería llamarse sustitución, ya que no es una sustitución de "quito esto y pongo lo otro". Esto es así porque no vamos a cambiar términos por términos sino variables por términos. O sea, una sustitución es una aplicación de las variables en los términos.

[$$ \sigma : V\to T(A,V)
$$]

Lo interesante de esta aplicación es que puede extenderse de forma congruente a todo el álgebra de términos. Para eso introducimos una nueva aplicación extendida

[$$ \bar{\sigma} : T(A,V)\to T(A,V) $$]

Y la definimos para que mantenga la estructura de los términos así:

[$$ \bar{\sigma}(x)=\sigma (x) $$]
[$$ \bar{\sigma}(f(M_1,...,M_n))=f (\bar{\sigma}(M_1),...,\bar{\sigma}(M_n)) $$]

El conjunto de todas las sutituciones en T(A,V) lo escribiremos como S(A,V). Usualmente no se distingue entre la sustitución con y sin barra. En este artículo haremos la distinción para ser formales, pero en otros lugares sólo se usa s.

Dominio y restricción

Llamamos dominio de una sustitución al conjunto de variables que no se sustituyen por ellas mismas.

[$$ dom(\sigma)=\left\{x\in V\mid \sigma(x)=x \right\},\qquad \sigma\in S(A,V) $$]

Cuando el dominio sea infinito, la sustitución se llamará infinita. Generalmente cuando se habla de sustitución, sólo se hace referencia a las sustituciones no infinitas. Nosotros sólo consideraremos las sustituciones no infinitas.

La restricción de una sustitución a un subconjunto (finito) de variables se define así.

[$$ \sigma\mid_W(x)=\left\{\begin{matrix}
\sigma(x) & \Leftarrow x\in W\\
x & \Leftarrow x\not\in W
\end{matrix}\right.\qquad W\subset V
$$]

Para indicar una sustitución lo más sencillo es componer varias sustituciones simples. Una sustitución simple es la que tiene dominio unitario. Representaremos a estas sustituciones así:

[$$ \sigma=\left[ x \mapsto M \right] $$]

Donde

[$$ \sigma(x)=M $$]

Si llamamos "id" a la sustitución identidad, entonces una sustitución arbitraria se representa así:

[$$ id\circ\left[ x_1 \mapsto M_1 \right]\circ\cdots\circ \left[ x_n \mapsto M_n \right] $$]

Donde

[$$ dom(\sigma)=\left\{ x_1,...,x_n\right\} $$]

Edit: Corrección. Una sustitución arbitraria donde todas las variables se renombren. Cuando hay variables comunes entre el dominio y el resultado de la sustitución hay que usar una sustitución simultánea.[$$ \left[ x_1 \mapsto M_1 ,\cdots\circ , x_n \mapsto M_n \right] $$]


Introduciendo la sustitución indefinida

Cuando realizamos un algoritmo muchas veces necesitamos un "valor de error", en el conjunto de sustituciones sobre el álgebra de términos con indefinido se introduce una transformación especial que llamaremos la sustitución indefinida. Su propiedad es que siempre asigna el valor indefinido.

[$$ \omega : T^\Omega(A,V) \to T^\Omega(A,V) $$]
[$$ \omega (M) = \Omega $$]

Al conjunto de sustituciones con sustitución indefinida (sobre el álgebra de términos con indefinido) lo definimos de esta forma:

[$$ S^\omega(A,V)=S(A,V)\cup \left\{ \omega \right\} $$]

Hemos de arreglar un poco las operaciones anteriores de la siguiente forma:

[$$ \bar{\sigma}(\Omega)=\Omega $$]
[$$ \omega\mid_W=\omega $$]

Ahora queda averiguar qué estructura matemática tiene la operación de sustitución sobre el álgebra de términos, pero eso lo dejaré para otro día.


lunes, 24 de mayo de 2010

Descanse en paz, Martin Gardner


En la biblioteca de mi instituto, sitio poco frecuentado, estaba la colección de una extraña revista. ¡Tenía dos títulos! Uno era "Investigación y ciencia" y el otro era "Scientific American". Luego me enteré de que era la traducción de la revista americana y de ahí lo de los dos títulos. Aparte de ser algo torpe de joven, también me picaba la curiosidad de la ciencia. Dentro de la revista, lo más curioso de todo era un apartado que ponía "Juegos Matemáticos". Ni idea de quién lo escribía pero eran cosas muy curiosas.

Años después me enteré de que el escritor de esas columnas era Martin Gardner y, por ese trabajo, se le había otorgado reconocimiento internacional. Además, había escrito muchos libros de matemáticas para gente de la calle (torpes como yo) y tenía hasta legión de seguidores. Uno de esos libros; no escrito por él, pero sí anotado; es el que tiene entre las manos en la foto de arriba: "Alicia en el país de las maravillas" y "A través del espejo" anotados con las curiosidades matemáticas que se esconden en tan conocida obra.

El 22 de mayo murió en Oklahoma, la tierra que le vio nacer. Descanse en paz.

sábado, 22 de mayo de 2010

Las reglas del lambda cálculo

El lambda cálculo consta de varias reglas. He puesto aquí las que he encontrado, pero no pretendo ser exhaustivo. Si alguien conoce alguna regla más, estaría encantado de incluirla en la lista.

La regla beta

El lambda cálculo se basa en una regla fundamental: la regla beta.

Esta regla dice que si quiero calcular f(3) y tengo definida f(x), lo que hay que hacer es sustituir x por 3.

[$$ (\lambda x.e)v \rightarrow \left[ x \mapsto v \right] e $$]

La regla alfa

Sin embargo, esto significa que realmente la x puede ser renombrada y si defino f(x) usando la y, tengo la definición equivalente f(y). Esto es cierto, siempre que no tenga usada la y para otra cosa, claro. En la jerga se dice que la y no es libre. Las variables libres de una expresión se capturan con la función "fv".

[$$ \frac {y\not \in fv(e)}{\lambda x.e \rightarrow \lambda y.\left[ x \mapsto y\right] e} $$]

La regla alfa es realmente una equivalencia porque puedo usarla para cambiar la x por la y (u otra variable) y luego usarla de nuevo para volver a la x. Por esa razón se la suele llamar la alfa-equivalencia.

La alfa-equivalencia ocurre siempre que tenemos variables ligadas y captura, junto a la definición de sustitución, ese hecho.

La regla eta

Los estudiosos del lambda cálculo se dieron cuenta de que había ciertas funciones que no podían reducirse con la regla beta, pero que "obviamente" podían reducirse. Era el caso de funciones como f(x)=g(x). Si son iguales, cambia una por otra sea lo que sea x. Como la reducción beta sólo puede cambiar la x por otra cosa, se imponía una nueva regla que dio en llamarse la regla eta.

[$$ \lambda x. (e x) \to e $$]

Esta simple e inocente regla introduce bastantes problemas cuando introducimos otros elementos que no sean funciones. Tantos problemas que los lenguajes de programación actuales no la implementan. Por ejemplo, si e lanzase una excepción, el antecedente de la regla eta no lo haría, mientras que el consecuente sí.

La regla delta

Hemos hablado de lanzar excepciones, pero ¿cómo introducimos esos nuevos valores en el sistema? Las reglas vistas hasta ahora sólo pueden actuar sobre funciones anónimas. Por esa razón se introducen reglas a la carta. Todas estas reglas se agrupan en una única regla, la regla delta, que hace de puente entre las definiciones de los elementos a gusto de usuario y el lambda cálculo.

[$$ \frac{e \rightarrow_\delta e'}{e \rightarrow e'} $$]

La hipótesis de la regla delta es que una expresión e puede reducirse de forma externa a otra expresión e'. En este caso, una expresión e se reduce en el lambda cálculo a la expresión e'.

La regla mu

Finalmente puede ocurrir que queramos introducir valores predefinidos para ciertas variables en nuestra computación. Se incluye entonces un enterno global y se añade la regla mu para poder usar esos valores definidos.

[$$
\frac{x\in dom(\Gamma),\: \Gamma(x)=e}{x\rightarrow e}
$$]

Esta regla sólo se puede usar si la variable no está ligada

jueves, 20 de mayo de 2010

Tipos intersección

¿Qué son?

Supongamos que tenemos una función con el siguiente tipo

[$$ f: A \rightarrow B \rightarrow C $$]

¿Cuál es el tipo de esta nueva función?

[$$ \lambda x. f x x $$]

Esta claro que la x tendrá que ser de tipo A y de tipo B. Si tuviéramos subtipos, y asumiendo que el tipo de x es X, diríamos

[$$ X\le A,\quad X\le B $$]

Sería tarea del motor de inferencia buscar el tipo adecuado. Por otra parte, podríamos introducir una solución tramposa. Inventarnos el tipo

[$$ X=A\cap B $$]

con las  propiedades

[$$ T\cap S \le T $$]
[$$
T\cap S \le S $$]

Ni que decir tiene que esto recuerda mucho al concepto de intersección de conjuntos, de ahí el nombre.

El sistema de Coppo-Dezani

Si introducimos las reglas usuales de una intersección (es decir, las de un ínfimo) obtenemos el sistema de Coppo-Dezani (sistema CD). Este sistema tiene unas cualidades muy interesantes.

  • Cumple la reducción de sujeto. Es lo mínimo que se puede pedir a un sistema de tipos para una estrategia de evaluación por nombre: que si evaluamos en un paso nuestra expresión (sea el redex que sea), el tipo siga siendo el mismo.
  • Los términos tipables son los términos fuertemente normalizables. O sea, que sólo podremos darle un tipo a los términos cuya evaluación acabe.
  • Las formas normales son tipables ya que no tienen más pasos de evaluación.
  • Cumple la expansión de sujeto. Esto es interesante. Si damos un paso de evaluación marcha atrás, el tipo también se mantiene.
  • Estas propiedades nos llevan a la gran característica definitoria del sistema CD: Un término es tipable si y sólo si su evaluación acaba sea cual sea la estrategia de evaluación (es fuertemente normalizable).

Esta última propiedad no es buena. Y no lo es porque significa que no podemos darle un tipo a expresiones de la forma

[$$ K x y = x $$]
[$$ K\; 3\;((\lambda z. z z)(\lambda z. z z)) $$]

La función K (el combinador K) descarta su segundo parámetro, por lo que el término debería tener tipo entero (el resultado es 3). Sin embargo, no es tipable porque el segundo argumento nunca termina su evaluación. Este término no es fuertemente normalizable, es sólo normalizable de cabeza.

El sistema de Coppo-Dezani-Venneri

La solución es añadir una constante ? que significa "cualquier cosa". Sería vista como la intersección nula o como el elemento neutro de la intersección.

[$$ \omega \cap X = X $$]
[$$ X \cap \omega = X $$]

Al añadir las reglas apropiadas para introducir esta constante, los autores del sistema CDV se vieron forzados a separar los tipos en dos niveles. El nivel de tipo simple y el nivel de intersección (o secuencia) de tipos.

[$$ \tau ::= X\;\mid\;\omega\;\mid\;\sigma \rightarrow \tau $$]
[$$ \sigma ::= \tau_1 \cap \cdots \cap \tau_n\qquad (n>0) $$]

Con este sistema, las propiedad principal es que se puede asignar un tipo a los términos con forma normal de cabeza.

El sistema de Barendregt-Coppo-Dezani

El problema de los tipos restringidos del sistema CDV se soluciona introduciendo una relación de subtipo. Esto es así porque en posición covariante las intersecciones distribuyen.

[$$ A\rightarrow (B\cap C)=(A\rightarrow B)\cap(A\rightarrow C) $$]

Introduciendo una relación de subtipo que sea un preorden se puede derivar una clase de equivalencia y trabajar con el orden parcial generado en el conjunto cociente.

Este sistema es bastante más complejo. La relación de subtipo tiene hasta ocho reglas. La relación de tipado tiene seis reglas.

El sistema BCD tiene la misma potencia que el CDV. Sin embargo tiene un gran fallo: existen varias formas de demostrar que una expresión tiene un tipo. Las reglas no son dirigidas sintácticamente.

A pesar de todo esto, el sistema BCD es el más conocido y usado de los sistemas de tipos intersección.

lunes, 17 de mayo de 2010

Lo que nunca me enseñaron: El álgebra de términos

Cuando me enseñaron la lógica de primer orden, empezaron con las definiciones de alfabeto, término, sustitución, igualdad, unificación, etc. Realmente antes habíamos visto los términos, las gramáticas, autómatas y demás, pero nunca desde el punto de vista algebraico.

En un caso era demasiado complejo y en otro demasiado general. Aquí explico lo que es el álgebra de términos de la manera más simple y sencilla posible. A partir de estas definiciones se pueden explorar otras estructuras y operaciones matemáticas con un buen fundamento.

El alfabeto

Supongamos que tenemos un alfabeto de símbolos (que llamaremos funtores) de forma que cada funtor tenga una aridad.

[$$ A=(F,a) $$]
[$$ a:F \rightarrow \mathbb{N} $$]

Este alfabeto no podrá ser vacío ni no numerable.

[$$ 0<\left| F \right| \le \aleph_0 $$]

Cuando la aridad de un funtor es cero, se denomina entonces constante.

Nota: Los símbolos de los paréntesis y las comas están reservados y no podrán formar parte de nuestro alfabeto. Estos símbolos son los que se usan para construir los términos.

Nota: Usaremos las letras del inicio del alfabeto para las constantes (a,b,c) y del medio para los funtores (f,g,h).

Los términos

Llamamos variables a otros símbolos tomados de un conjunto infinito y numerable.

[$$ \left| V \right| = \aleph_0 $$]

Nota: Usaremos las letras del final del alfabeto para las variables.

[$$ \left\{ x,y,z\right\} \subset V $$]

El conjunto de términos de primer orden se define como el menor conjunto[$$ T(A,V) $$]

tal que

[$$ V\subset T(A,V) $$]

y

[$$ M_1,...,M_n \in T(A,V), f\in F \Rightarrow f(M_1,...,M_n) \in T(A,V) $$]

Por ejemplo, si nuestro alfabeto fuera a,b,+ con a y b constantes y con + de aridad dos, algunos términos serían.

  • a()
  • b()
  • +(a(),a())
  • +(a(),b())
  • +(x,b())
  • x

En muchos casos se permite la licencia de omitir los paréntesis vacíos y usar otras notaciones como la infija o la circunfija. Los ejemplos de arriba serían entonces:

  • a
  • b
  • a+a
  • a+b
  • x+b
  • x

Términos con indefinido

Muchas veces es útil añadir un valor indefinido para denotar un error o algún valor excepcional. En estos casos se define

[$$ T^\Omega(A,V)=T(A,V)\cup \left\{ \Omega \right\} $$]

Obviamente, el valor indefinido no debe estar ni entre los funtores ni entre las variables.

[$$ \Omega \not \in F $$]
[$$ \Omega \not \in V $$]

Igualdad de términos

Dos términos son iguales si lo son símbolo a símbolo. Esta relación se puede definir recursivamente sobre la estructura de los términos:

[$$ x = x $$]
[$$ \frac{M_1=M'_1,...,M_n=M'_n}{f (M_1,...,M_n) = f (M'_1,...,M'_n)} $$]



miércoles, 12 de mayo de 2010

Excepciones o asertos

Existen varios niveles de errores cuando se ejecuta un programa o parte de un programa.

En principio, el error puede ser un resultado correcto del mismo. En este caso más que un error es un resultado especial. Generalmente hay que atender a este resultado inmediatamente cuando se produce ya que es lo que le hemos pedido a la subrutina y lo que ésta nos devuelve. A esta técnica se la denomina código de error.

También puede ser que no sea un resultado correcto. Esto tiene dos consecuencias. En primer lugar toda la zona en la que se ha producido el error y que estaba trabajando para obtener ese resultado ha hecho un trabajo en balde. En segundo lugar, no tenemos que atender al resultado inmediatamente porque toda la zona ha quedado invalidada. Lo que tenemos es una excepción que será manejada después, cuando salgamos de la zona que estaba calculando ese resultado.

Finalmente, ocurre que es el propio estado del programa lo que es inválido. Los invariantes no se cumplen, las precondiciones fallan o ha ocurrido algo inesperado e irrecuperable. Obviamente esto no debe suceder nunca. En este caso hemos de usar asertos. Los asertos sólo se usan en depuración, así que si fallan en la versión de producción probablemente nuestro programa deje de funcionar.

Entonces, el algoritmo para decidir si usamos excepciones o asertos es el siguiente:

  1. ¿Si el hecho ocurre, puedo solucionarlo? Si la respuesta es NO, es un aserto.
  2. ¿Si el hecho ocurre, es parte del resultado? Si la respuesta es NO, es una excepción. (Se puede comprobar esto pensando ¿voy a solucionar el hecho más adelante?)
  3. En otro caso, es un resultado correcto del procedimiento o código de error.

jueves, 6 de mayo de 2010

Las guerras del RIA

Hace poco saltó la noticia de que Apple prohibía cualquier cosa que no estuviera hecha con C/C++, objective C o JavaScript en sus iPhone e iPad. El enfado ha sido monumental en muchos sitios, llamando a la nueva licencia, por ejemplo, la iNazi.

Uno de los grandes perjudicados ha sido Adobe, cuyo sistema RIA (Flash) no podrá ser portado. Teniendo en cuenta que esta portabilidad ha sido uno de los buques insignia de Adobe en este campo, le ha hecho mucho daño. El resultado ha sido una demanda por monopolio contra Apple.

A todo esto, el ganador podría ser el nuevo estándar HTML 5 que incluye bastantes características nuevas orientadas a RIA. Desarrollado por el W3C, es un estándar libre y, además, está siendo apoyado por Apple.

¿Me parece a mí o las tecnologías libres han encontrado una nueva utilidad: ser usadas como armas arrojadizas contra la competencia?

domingo, 2 de mayo de 2010

Nunca es tarde para una (buena) compilación

Compilación estática y compilación dinámica

La compilación usual es la compilación estática. En la compilación estática analizamos el código fuente y generamos un código ejecutable en la plataforma de destino que queramos. Es lo que se denomina código nativo o código máquina.

Generalmente este tipo de compilación es muy rígida porque necesitamos saberlo todo antes de producir el ejecutable nativo. Una primera solución a este problema es separar el código nativo en bloques distintos que cargamos cuando vayamos a ejecutar. A esto se le denomina biblioteca dinámica.

Pero podemos hacerlo mejor. Podríamos no generar un código nativo, sino separar el compilador en dos partes. La primera genera un código incompleto llamado código intermedio o bytecode y la segunda termina de compilar ese código incompleto al código nativo más tarde. Cuando vayamos a ejecutar.

Esto es la compilación dinámica que fue introducida por David Ungar en el lenguaje Self. Este tipo de traducciones de un código binario a otro código binario se llaman traducciones binarias. Son usuales en los emuladores y máquinas virtuales.

La compilación dinámica más simple es la adelantada en el tiempo (AOT en sus siglas en inglés). En este caso compilamos todo el código intermedio a código nativo en cuanto tenemos que ejecutar el programa. Esto hace que sea lento arrancar el programa pero, una vez funcionando, vaya rápido.

¡Justo a tiempo!

Otra opción es compilar más tarde. ¿Cómo vamos a compilar después de cargar el código? Muy sencillo: compilamos conforme vayamos ejecutando. Empezamos a ejecutar una sección del código (función o incluso un bloque de una función). Si está compilado lo ejecutamos y si no, lo compilamos y ejecutamos. De esta manera el arranque es más rápido que en AOT porque sólo compilamos lo que necesitamos para arrancar y no todo el programa.

Esta compilación es la compilación justo a tiemo (JIT en sus siglas inglesas) y es la más usada con diferencia. De hecho, se puede hasta hacer más rápida aún. La técnica es muy sencilla. Introducimos junto al compilador un intérprete. Cuando nos encontramos un trozo de código sin compilar pasamos el intérprete y recogemos estadísticas de uso de ese trozo de código.

Cuando la estadística nos indica que es un trozo de código muy usado, compilamos. Si no es muy usado lo dejamos sin compilar y lo interpretamos. De esta manera se mejoran incluso los tiempos de arranque ya que suelen ser secciones de código que usan mucho las entradas/salidas a disco y compilar no sirve para acelerarlas. Véase la Ley de Amdhal.

Finalmente podemos hacer que el propio usuario o el propio programa decida cuándo compilar y cuándo no. Incluso, compilar desde código fuente y no desde código intermedio. En este caso hay que meter todo el compilador (y no solo la parte de traducción binaria) en el sistema de ejecución. Esto es lo que se llama la compilación incremental.

Pero no todo acaba aquí: Cuando el programa ya está compilado ¡podemos recompilarlo! Esta técnica es la recompilación dinámica (dynarec o DRC en inglés). La recompilación vuelve a optimizar el código ya que una vez que tenemos el programa entero se dispone de más información que cuando se está compilando.