New paper: Subject reduction in a Curry-style polymorphic type system with a vectorial structure

(Versión en español más abajo)

New paper submitted, with Pablo Arrighi and Benoît Valiron.

Title: Subject reduction in a Curry-style polymorphic type system with a vectorial structure.

Abstract: The algebraic lambda-calculus [Vau09] and the linear-algebraic lambda-calculus [AD08] extend the lambda-calculus with the possibility of making arbitrary linear combinations of lambda-terms. The two foundational works of [ADC09] and [DCP10] describe type systems for this calculus respectively accounting for scalars and sums. Building on these approaches, we devise a typed algebraic lambda-calculus merging the two approaches while keeping a language featuring local confluence and a weak subject reduction. This gives rise to an original and general type theory where types, in the same way as terms, have a vector space-like structure. The main contribution of this paper is a subject reduction result, a problem renowned to be a delicate matter under the presence of union-like type constructs.

Basically the idea of the paper is to present the several-times announced "vectorial type system": we present here a type system with a non-standard subject reduction. We conclude that, in general, to have subject reduction in a vectorial type system we would need to move to Church-style.

I uploaded the paper to arXiv today, so it will appear next Tuesday. I will put the link here. arXiv:1012.4032.

---

Nuevo paper enviado, con Pablo Arrighi y Benoît Valiron.

Título: Subject reduction (ni idea cómo se dice eso en español) en un sistema de tipos polimórfico à la Curry con una estructura vectorial.

Resumen: El lambda-cálculo algebraico [Vau09] y el lambda-cálculo algebraico-lineal [AD08] extienden el lambda-cálculo con la posibilidad de hacer combinaciones lineales arbitrarias de lambda-términos. Los dos trabajos fundacionales de [ADC09] y [DCP10] describen sistemas de tipos para este cálculo respectivamente teniendo en cuenta escalares y sumas. Construido sobre estos enfoques, elaboramos un lambda-cálculo algebraico fusionando ambos, logrando un lenguaje con confluencia local y una subject reducción débil. Esto da lugar a una teoría de tipos original y general donde los tipos, de la misma manera que los términos, tienen una estructura al estilo de un espacio vectorial. La principal contribución de este paper es el resultado de subject reduction, un problema reconocido como complicado en presencia de construcciones de tipo unión.

Básicamente la idea del paper es presentar el muchas veces anunciado "sistema de tipos vectorial": lo que presentamos aquí es un sistema de tipos con un subject reduction no estándar. Concluímos que, en general, para tener subject reduction in sistemas de tipos vectoriales deberíamos pasarnos a Church-style.

Hoy subí el paper a arXiv, así que aparecerá el próximo martes. Pondré el link aquí. arXiv:1012.4032. Y aquí una explicación más amena del paper.

Slides Types 2010

Como ya había adelantado, la semana pasada estuve en Varsovia participando del workshop Types 2010. Los slides de mis presentaciones están disponibles a través de mi página web: Sums in algebraic lambda-calculi y A vectorial type system (work-in-progress).

Hubo en general muy buenas charlas. En particular, les recomiendo ver los slides de la excelente charla de Henk Barendregt: Lambda calculus with types.

Visita al TypiCal

Los días lunes y martes pasados estuve visitando a Benoît Valiron del proyecto TypiCal en la École Polytechnique de París. Allí dí un seminario (abstract y transparencias aquí) y estuvimos debatiendo con Benoît sobre el trabajo que estoy haciendo.

Fue una muy productiva visita!

Estación de RER donde está la École

Mi hotel estaba a sólo unas cuadras de la torre, así que el martes a la mañana aproveché para ir hasta allí y tomar algunas fotos antes de ir al Laboratorio.

Vectorial, Lógica Lineal y Ortogonalidad

El miércoles y jueves pasados estuve en Lyon, invitado por Barbara Petit del grupo PLUME de la École Normale Supérieure de Lyon. Allí di un seminario sobre los sistemas de tipos que he desarrollado: Scalar, Additive y Vectorial, y algunos de los problemas sobre cómo chequear ortogonalidad entre términos y algunas pistas para resolverlo.

Olivier Laurent se dio cuenta de simplemente ver la presentación, la conexión entre Additive y Intuitionistic Multiplicative Exponential Linear Logic.

Pronto estaré publicando un nuevo paper sobre Additive (con esa conexión a la lógica lineal) y Vectorial. Además, hemos empezado a trabajar juntos con Barbara en el problema de la ortogonalidad, usando subtyping.

Próximos viajes:
Los días 4 y 5 de Mayo voy a París a visitar a Benoît Valiron y Gilles Dowek del proyecto TypiCal, en la École Polytechnique de París, donde daré otro seminario. Luego, el 18 de Mayo estaré en Chambery, donde iremos con mi director, Pablo Arrighi, a participar de una serie de seminarios organizados por Lionel Vaux del grupo LAMA.

System F à la Curry y Grupo de trabajo

Buenas!

Les cuento que ya estoy instaladísimo en Grenoble. Lo que he hecho en estos días es adaptar un sistema de tipos polomórficos (System F à la Curry, ver [1], [3] o [4] para más detalles) al Linear-Algebraic Lambda-Calculus de Arrighi y Dowek [2], además hice una prueba de strong normalization (ver [1] o [3]) para este «Linear-Algebraic System F» y algunos comentarios respecto a que este sistema se corresponde de acuerdo al Isomorfismo de Curry-Howard (ver [4]) con la misma lógica (Lógica Proposicional de Segundo Orden) que el System F original. La idea ahora es empezar a jugar con reglas de tipos más complejas, hacer alguna clase de álgebra de tipos, para obtener alguna lógica un poco más loca. Ya les comentaré cuando tenga algo más armado :)

Este próximo jueves nos juntamos con el grupo de trabajo que estamos más o menos en los mismos temas, en lo que le hemos dado a llamar WHOCAS: «(informal) Workshop on Higer-Order Calculi and Algebraic Structures», seremos sólo 5 personas, ya que es un grupo de trabajo más que un workshop: Lionel Vaux, Benoît Valiron, Gilles Dowek, Pablo Arrighi y yo. La idea es que cada uno dará una pequeña charla de 40 minutos contando en qué está trabajando, así vemos qué colaboraciones pueden salir de allí. Luego del WHOCAS publicaré aquí las transparencias que use.

Referencias
[1] Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and types. Cambridge University Press, 1989.
[2] Pablo Arrighi, Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. Lecture Notes in Computer Science: (RTA'08), 5117:17-31, 2008. (preprint en arXiv:quant-ph/0612199)
[3] Henk Barendregt. Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science. Clarendon Press, Oxford, 1992.
[4] Morten Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. (disponible para bajar en CiteSeer)