El equipo LoReL está integrado por miembros del Instituto de Ciencias de la Computación (UBA-CONICET), el Departamento de Computación de la FCEN (Universidad de Buenos Aires), y la Universidad Nacional de Quilmes, con estudiantes de la Universidad Nacional de la Plata y la Universidad Nacional de Rosario.

Esta jornada tiene por objetivo que los estudiantes de licenciatura y doctorado del equipo interactúen entre sí, mostrando los avances y proyectos de sus respectivas tesis.

Abstracts

Cristian Sottile (tesinista @ UNLP) - Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Dos tipos A y B son considerados isomorfos si existen dos funciones f, de A en B, y g, de B en A, tales que g · f es la identidad en A y f · g es la identidad en B. Ejemplos de esto son los tipos A×B y B×A, y A×B ⇒ C y A ⇒ B ⇒ C. Normalmente, en los sistemas formales los tipos isomorfos son considerados diferentes –es decir, no tipan los mismos términos–, y eso presenta algunos inconvenientes desde el punto de vista práctico. Por ejemplo: sean A y B isomorfos, x : A y f : B ⇒ C, la aplicación de f con x requerirá una transformación intermedia explícita sobre x, de A en B; siendo g : A ⇒ B dicha transformación, finalmente la aplicación se escribirá (f · g) x. Si los tipos isomorfos fueran identificados –es decir, tiparan los mismos términos–, x : A y también x : B, por lo tanto podría escribirse f x, sin transformaciones intermedias. En ese sentido fue diseñado System I, un sistema de pruebas basado en el fragmento con ⇒ y ∧ de la lógica intuicionista en el que las proposiciones isomorfas tienen las mismas demostraciones, definiendo para ello un sistema de equivalencias en el cálculo Lambda. Esta tesina propone extender System I agregando polimorfismo. Esto implica agregar ∀ al fragmento lógico y extender los términos, tipos, sistema de tipos y semántica operacional del cálculo asociado, y probar ciertas propiedades de interés como preservación de tipos, además de extender la implementación del intérprete existente de System I.

Federico Lochbaum (tesinista @ UNQ) - Esbozo de un lenguaje funcional-lógico

El objetivo de esta charla es mostrar algunos progresos en el diseño y estudio de la semántica de un lenguaje de programación que combina características funcionales con características lógicas; en particular elección no determinística y unificación. Empezamos ilustrando comportamientos esperados a través de varios ejemplos. Presentaremos una semántica formal tentativa y comentaremos sobre algunos desafíos que se presentan y posibles líneas de trabajo futuro.

Alan Rodas (tesinista @ UNQ) - Implementación de lambda cálculo para matrices de densidad con controles clásicos y probabilísticos

El trabajo de grado consiste en una implementación ejecutable en una computadora tradicional por medio de simulación tanto de λρ y λρ°, extensiones al calculo lambda para computación cuántica que utilizan matrices de densidad, con un control clásico en el primer caso, y con control probabilístico en el segundo. El trabajo busca demostrar la factibilidad de realizar lenguajes de alto nivel a partir de extensiones teóricas al calculo lambda.

Agustín Borgna (tesinista @ UBA) - Simulación del lambda cálculo de matrices densidad en el cálculo de Selinger-Valiron, y viceversa

λρ es un cálculo lambda cuántico con control clásico y datos cuánticos y reducciones probabilísticas que representa estados cuánticos a través de matrices de densidad. Esta formulación alternativa de los postulados cuánticos resulta equivalente al approach clásico, permitiendo además representar estados mixtos. λq es un cálculo similar que utiliza la representación clásica de los estados cuánticos como vectores en un espacio de Hilbert. En esta charla voy a presentar una simulación de λρ en λq y las limitaciones encontradas al realizar la traducción. Luego voy a discutir la traducción para λρ°, una variación de λρ que permite representar la medición con reducciones deterministas y seguir así las trazas mixtas de los programas cuánticos.

Malena Ivnisky (tesinista @ UBA) - Agregando punto fijo a una extensión cuántica de lambda cálculo con matrices de densidad

Al agregar el operador canónico de punto fijo a un lenguaje es necesario que la interpretación de los tipos sea un orden parcial completo (CPO) para que este esté bien definido. Esta tesis busca agregar punto fijo a un cálculo en matrices de densidad, reinterpretando sus términos de forma tal que su dominio resulte un CPO. Para lograrlo se pasa de la interpretación previa en la cual las matrices de densidad tenían su traza acotada por 1 a una interpretación en la cual la cota de la traza depende del tipo del término interpretado. Además se demuestran otras propiedades interesantes que siguen valiendo al realizar esta extensión.

Lucas Romero (tesinista @ UBA) - Normalización fuerte y confluencia en una extensión polimórfica de lambda-rho

λρ y λρ° son cálculos lambda simplemente tipados que utilizan matrices de densidad para representar el estado cuántico de un sistema. Este trabajo apunta a extender ambos cálculos con un sistema de tipado polimórfico a la Curry similar al de System F y contextos de tipado un poco más permisivos. Sobre estas extensiones demostramos propiedades deseables: Subject reduction y normalización fuerte. Además, estudiamos la noción de confluencia para un cálculo con reducciones probabilísticas y presentamos las dificultades y posibles enfoques para lograr la confluencia de λρ y λρ°.

Ignacio Grima (tesinista @ UNR) - Implementando un intérprete de Lambda-S

Lambda-S es una extensión del lambda cálculo de primer orden que unifica dos enfoques para prevención del clonado de qbits en los lambda cálculos cuánticos. Uno es la prohibición de duplicar variables, mientras la otra es el considerar todos los términos lambda como funciones algebraicas lineales. El objetivo de esta tesina es implementar un intérprete de dicho cálculo en Haskell, para lo cual se deberá transformar las relaciones matemáticas de tipado, y reducción de términos, en funciones.

Francisco Noriega (tesinista @ UBA) - Extendiendo el cálculo lambda vectorial con subtipado

Vectorial es un lambda cálculo basado en álgebra lineal, que a través de su sistema de tipos permite describir combinaciones lineales de términos como resultado de la reducción de un programa. Sin embargo, no posee la propiedad clásica de Subject Reduction, sino una versión débil de la misma, y por lo tanto presenta el problema de que al reducir un término, el tipo asociado al mismo puede no ser el mismo para el término reducido.

Este trabajo intenta extender Vectorial con reglas de subtipado para poder recuperar la propiedad clásica de Subject Reduction

En esta charla se presentará brevemente el sistema de tipos original de Vectorial, haciendo énfasis en el teorema de Subject Reduction; y los cambios realizados al sistema de tipos (incluido la adhesión de subtipado).

Juan Pablo Rinaldi (ex tesinista @ UNR) - Demostrando normalización fuerte sobre una extensión cuántica del lambda cálculo

Una de las propiedades fundamentales de la mecánica cuántica es la del no-clonado, la cual indica que es imposible crear una copia idéntica de un estado cuántico desconocido. Los lenguajes funcionales cuánticos pueden diferenciarse dependiendo de cómo se trate dicha propiedad. Por un lado tenemos la familia de lenguajes que utilizan lógica lineal (lenguajes LL) para excluir los términos que duplican estados. Por otro lado tenemos la familia de lenguajes que utilizan propiedades del álgebra lineal (lenguajes AL), los cuales admiten términos que los otros excluyen, pero los interpretan de forma diferente, evitando también el clonado. Los lenguajes AL, al utilizar un sistema de tipos clásicos, son más sencillos que los LL, pero los primeros tienen una desventaja frente a los últimos: no soportan fácilmente el operador de medición, elemento fundamental de la mecánica cuántica. Por este motivo se propuso desarrollar un lenguaje, λS, que posea lo mejor de ambos enfoques: la elegancia de la linealidad algebraica y el soporte para el operador de medición usando lógica lineal. El objetivo de la presente charla es describir la demostración de la propiedad de normalización fuerte sobre dicho lenguaje. Esta propiedad implica que no habrá loops infinitos, y por lo tanto, un programa bien tipado no tiene ejecuciones infinitas.

Pablo Barenbaum (doctorando @ UBA) - Family developments en el cálculo de sustituciones lineales

En esta charla presentamos un resultado conocido como "finite family developments" (FFD) para el cálculo de sustituciones lineales (LSC). Este resultado afirma que toda reducción infinita debe contraer radicales creados a través de interacciones arbitrariamente largas. Para enunciarlo y demostrarlo, usamos una variante del LSC dotada de etiquetas, siguiendo el trabajo hecho por Lévy sobre el cálculo-λ. Mostramos también cómo FFD puede aplicarse satisfactoriamente para estudiar otras propiedades del LSC: reducción optimal, estandarización y normalización de estrategias.

Andrés Viso (doctorando @ UBA) - Bisimulación fuerte para operadores de control

El propósito de este trabajo es identificar programas con operadores de control cuyas semánticas de reducción se correspondan. Esto se logra introduciendo una relación de sigma-equivalencia definida sobre una presentación revisada del Lambda-mu Cálculo de Parigot. Nuestro resultado se construye a partir de tres ingredientes principales: (1) una factorización de la reducción de Lambda-mu en pasos multiplicativos y exponenciales mediante el uso de operadores explícitos en el marco de un nuevo cálculo llamado Lambda-Mu; (2) adaptar la noción de sigma-equivalencia introducida por Laurent al cálculo con operadores de control explícitos; y (3) una adecuada interpretación semántica de los términos del cálculo en las Polarized Proof-Nets de Laurent. El resultado obtenido es una relación de sigma-equivalencia para términos del Lambda-Mu Cálculo que resulta ser una bisimulación fuerte con respecto a la noción de reducción exponencial, al mismo tiempo que preserva la semántica respecto a las PPN.