de execute/2 son execute(st(fr(count, 0, [], [N, 0]), []), Sf) y execute(st(fr(count, 1, [0], [N, 0]), []), Sf). Usando Enum, el silbato se activa en este punto y el desplegado tiene que parar. Esto provoca que este último átomo sea generalizado en el control global produciéndose execute(st(fr(count, X, Y, [N, 0]), []), Sf). Es- to no es aceptable en el caso de la especialización de nuestro intérprete, pues se pierde la pista de la siguiente instrucción a ser ejecutada—lo que provoca que no se pueda eliminar la capa de interpretación—y de hecho, en la mayoŕıa de casos provoca que el programa residual obtenido contenga prácticamente el intérprete por completo. Incrementando la Precisión: Śımbolos Estáticos del Programa Una manera sintáctica de mejorar la precisión asegurando al mismo tiempo terminación, propuesta en [61], consiste en considerar dos conjun- tos de śımbolos: uno con aquellos que aparecen expĺıcitamente en el pro- grama y el objetivo, y otro con el conjunto infinito de śımbolos que el programa puede generar potencialmente. Denotaremos esta relación co- mo E∗ S. Al comparar dos términos, nos quedamos con los śımbolos que pertenezcan al conjunto finito y filtramos el resto. Bajo esta relación, el átomo execute(st(fr(count, 1, [0], [N, 0]), []), Sf) no subsume al átomo execute(st(fr(count, 0, [], [N, 0]), []), Sf), pues los números 0 y 1 son śımbo- los estáticos diferentes del programa. Por tanto, en este caso, el evaluador parcial no se ve obligado a generalizarlos preservándose aśı el valor del PC. Desafortunadamente, la relación E∗ S resulta no comportarse tampoco de forma óptima en nuestro caso, pues execute(st(fr(count, 2, [], [N, 1]), []), Sf) no subsume a execute( st(fr(count, 2, [], [N, 0]), []), Sf). Esto significa que el proceso de desplegado continua con una segunda iteración del bucle. Aun- que está garantizado que el proceso termina, se desplegarán tantas iteracio- nes del bucle como distintas constantes numéricas consecutivas aparezcan en el programa, en este caso 8. No será posible por tanto obtener la de- compilación óptima que aparece en la parte de abajo de la Figura 2.6. Para obtener dicha decompilación, es necesario que el evaluador parcial generalice el contador del bucle lo antes posible, es decir, que el átomo execute(st(fr(count, 2, [], [N, 1]), []), Sf) subsuma a execute(st(fr(count, 2, [], [N, 0]), []), Sf). Intuitivamente, la razón por la que esta relación no se comporta de forma óptima es porque ésta no es capaz de distinguir entre los distintos argumentos y los trata todos por igual. En resumen, este ejemplo sugiere que es necesario tener una relación de subsunción que sea capaz de tener información de contexto en cuenta: en particular, dicha relación dependien- te del contexto, debeŕıa tratar de forma diferente el valor del PC y el valor de la variable del contador. 2.3.3. Subsunción Homeomórfica basada en Tipos En presencia de signaturas infinitas, existe un método general para de- finir relaciones de subsunción homeomórfica; en [61] se define la subsunción homeomórfica extendida basada en resultados previos de Kruskal [58] y Dershowitz [38]. Esta solución define una familia de relaciones de subsun- ción, donde una relación subsidiaria de orden, definida sobre los śımbolos de función del programa, juega un papel esencial. No obstante, veremos que ésta no resuelve realmente el problema en la práctica, pues no propone ningún mecanismo automático para encontrar la relación “correcta” entre los śımbolos de función. Esta tesis propone la subsunción homeomórfica basada en tipos, “type- based homeomorphic embedding” (TbHEm), una relación que mejora el HEm original haciendo uso de información adicional proporcionada en for- ma de tipos. Veremos como este enfoque puede verse como una forma de generar instancias concretas de la relación de HEm extendida como defi- nió Leuschel, incluyendo la posibilidad de tener en cuenta la semántica del programa. Los tipos requeridos para guiar al TbHEm pueden darse manual- mente o, lo que es más interesante, pueden inferirse automáticamente por análisis de programas, como discutimos en el Art́ıculo 3. La observación principal en al que se basa el TbHEm es que, incluso aunque una expresión este definida sobre una signatura infinita, es posible que sólo tome un conjunto finito de valores sobre el dominio correspondien- te para cada computación. Para realizar dicha distinción, nuestra relación se define sobre tipos, los cuales se estructuran en una partición finita (po- siblemente vaćıa) y una partición infinita (también posiblemente vaćıa). Intuitivamente, el TbHEm permite expandir secuencias mientras, al com- parar subtérminos de un tipo infinito, los valores concretos que aparecen en la expresión se mantengan en la partición finita del tipo correspondiente. Utilizando el TbHEm para controlar la EP del intérprete de byte- code En el caso de nuestro intérprete de bytecode, el argumento del PC se puede definir por un tipo estructurado de forma que el intervalo acotado en el cual éste se mueve constituye su partición finita, y el resto de los números enteros forma su parte de infinita. De esta manera, el TbHEm no generalizará el PC mientras su valor permanezca dentro del intervalo acotado. Para inferir este tipo, utilizaremos técnicas de análisis existentes, en particular, usaremos el análisis de tipos buenos (“well-typings”) descrito por Bruynooghe et al. [20]1. Éste infiere el siguiente tipo τPC para el contador de programa del intérprete de la Figura 2.3, teniendo en cuenta el programa bytecode de la Figura 2.4: τPC --> -4; 0; 1; 2; 3; 4; 5; 6; 7; 8; num Se puede interpretar que el tipo τPC consiste en una partición fini- ta (las constantes numéricas) y una partición infinita (el resto de los números distintos de las constantes). Es decir, el tipo se puede inter- pretar como τPC → F ; I donde la partición F es {−4, 0, 1, 2, . . . , 8} y I = num ". Usando esta regla de tipo, el TbHEm asegura que el contador de programa nunca será abstráıdo durante la EP, mien- tras su valor se mantenga en el rango esperado (las constantes numéri- cas). El átomo execute(st(fr(count, 1, [0], [N, 0]), []), Sf) no subsume a 1Disponible on-line en http://saft.ruc.dk/Tattoo/ execute(st(fr(count, 0, [], [N, 0]), []), Sf) usando esta definición de tipo, por tanto, la derivación puede avanzar. Esto evita la necesidad de generalizar el PC lo que provocaŕıa que no pudiésemos obtener una especialización efec- tiva. La derivación bien terminará, o bien el valor del PC se repetirá por algún salto hacia atrás en el código (bucle). En este caso, el TbHEm, tam- bien escrito ET , detectará el átomo correspondiente como peligroso, por ejemplo, execute(st(fr(count, 2, [], [N, 0]), []), Sf) ET execute(st(fr(count, 2, [], [N, 1]), []), Sf), como vemos en la Figura 2.6. El programa decompilado que obtenemos usando los tipos inferidos en combinación con el TbHEm se muestra en la parte baja de la Figura 2.6. Se puede observar que esta decompilación es óptima2 en el sentido de que la capa de interpretación se ha eliminado totalmente o no aparece código residual superfluo. Aparte de la inferencia de “well-typings” que hemos visto, en el Art́ıcu- lo 3 se bosqueja como utilizar