Operational Aspects of Full Reduction in Lambda Calculi

Esta tesis estudia la reduccion plena (‘full reduction’ en ingles) en distintos calculos lambda. 1 En esencia, la reduccion plena consiste en evaluar los cuerpos de las funciones en los lenguajes de programacion funcional con ligaduras. Se toma el calculo lambda clasico (i.e., puro y sin tipos) como el sistema formal que modela el paradigma de programacion funcional. La reduccion plena es una tecnica fundamental cuando se considera a los programas como datos, por ejemplo para la optimizacion de programas mediante evaluacion parcial, o cuando algun atributo del programa se representa a su vez por un programa, como el tipo en los demostradores automaticos de teoremas actuales. Muchas semanticas operacionales que realizan reduccion plena tienen naturaleza hibrida. Se introduce formalmente la nocion de naturaleza hibrida, que constituye el hilo conductor de todo el trabajo. En el calculo lambda la naturaleza hibrida se manifiesta como una ‘distincion de fase’ en el tratamiento de las abstracciones, ya sean consideradas desde fuera o desde dentro de si mismas. Esta distincion de fase conlleva una estructura en capas en la que una semantica hibrida depende de una o mas semanticas subsidiarias. Desde el punto de vista de los lenguajes de programacion, la tesis muestra como derivar, mediante tecnicas de transformacion de programas, implementaciones de semanticas operacionales que reducen plenamente a partir de sus especificaciones. Las tecnicas de transformacion de programas consisten en transformaciones sintacticas que preservan la equivalencia semantica de los programas. Se ajustan las tecnicas de transformacion de programas existentes para trabajar con implementaciones de semanticas hibridas. Ademas, se muestra el impacto que tiene la reduccion plena en las implementaciones que utilizan entornos. Los entornos son un ingrediente fundamental en las implementaciones realistas de una maquina abstracta. Desde el punto de vista de los sistemas formales, la tesis desvela una teoria novedosa para el calculo lambda con paso por valor (‘call-by-value lambda calculus’ en ingles) que es consistente con la reduccion plena. Dicha teoria induce una nocion de equivalencia observacional que distingue mas puntos que las teorias existentes para dicho calculo. Esta contribucion ayuda a establecer una ‘teoria estandar’ en el calculo lambda con paso por valor que es analoga a la ‘teoria estandar’ del calculo lambda clasico propugnada por Barendregt. Se presentan resultados de teoria de la demostracion, y se sugiere como abordar el estudio de teoria de modelos. ABSTRACT This thesis studies full reduction in lambda calculi. In a nutshell, full reduction consists in evaluating the body of the functions in a functional programming language with binders. The classical (i.e., pure untyped) lambda calculus is set as the formal system that models the functional paradigm. Full reduction is a prominent technique when programs are treated as data objects, for instance when performing optimisations by partial evaluation, or when some attribute of the program is represented by a program itself, like the type in modern proof assistants. A notable feature of many full-reducing operational semantics is its hybrid nature, which is introduced and which constitutes the guiding theme of the thesis. In the lambda calculus, the hybrid nature amounts to a ‘phase distinction’ in the treatment of abstractions when considered either from outside or from inside themselves. This distinction entails a layered structure in which a hybrid semantics depends on one or more subsidiary semantics. From a programming languages standpoint, the thesis shows how to derive implementations of full-reducing operational semantics from their specifications, by using program transformations techniques. The program transformation techniques are syntactical transformations which preserve the semantic equivalence of programs. The existing program transformation techniques are adjusted to work with implementations of hybrid semantics. The thesis also shows how full reduction impacts the implementations that use the environment technique. The environment technique is a key ingredient of real-world implementations of abstract machines which helps to circumvent the issue with binders. From a formal systems standpoint, the thesis discloses a novel consistent theory for the call-by-value variant of the lambda calculus which accounts for full reduction. This novel theory entails a notion of observational equivalence which distinguishes more points than other existing theories for the call-by-value lambda calculus. This contribution helps to establish a ‘standard theory’ in that calculus which constitutes the analogous of the ‘standard theory’ advocated by Barendregt in the classical lambda calculus. Some prooftheoretical results are presented, and insights on the model-theoretical study are given.