Operational Aspects of Full Reduction in Lambda Calculi

Esta tesis estudia la reducción plena (‘full reduction’ en inglés) en distintos cálculos lambda. 1 En esencia, la reducción plena consiste en evaluar los cuerpos de las funciones en los lenguajes de programación funcional con ligaduras. Se toma el cálculo lambda clásico (i.e., puro y sin tipos) como el sistema formal que modela el paradigma de programación funcional. La reducción plena es una técnica fundamental cuando se considera a los programas como datos, por ejemplo para la optimización de programas mediante evaluación parcial, o cuando algún atributo del programa se representa a su vez por un programa, como el tipo en los demostradores automáticos de teoremas actuales. Muchas semánticas operacionales que realizan reducción plena tienen naturaleza híbrida. Se introduce formalmente la noción de naturaleza híbrida, que constituye el hilo conductor de todo el trabajo. En el cálculo lambda la naturaleza híbrida se manifiesta como una ‘distinción de fase’ en el tratamiento de las abstracciones, ya sean consideradas desde fuera o desde dentro de si mismas. Esta distinción de fase conlleva una estructura en capas en la que una semántica híbrida depende de una o más semánticas subsidiarias. Desde el punto de vista de los lenguajes de programación, la tesis muestra como derivar, mediante técnicas de transformación de programas, implementaciones de semánticas operacionales que reducen plenamente a partir de sus especificaciones. Las técnicas de transformación de programas consisten en transformaciones sintácticas que preservan la equivalencia semántica de los programas. Se ajustan las técnicas de transformación de programas existentes para trabajar con implementaciones de semánticas híbridas. Además, se muestra el impacto que tiene la reducción plena en las implementaciones que utilizan entornos. Los entornos son un ingrediente fundamental en las implementaciones realistas de una máquina abstracta. Desde el punto de vista de los sistemas formales, la tesis desvela una teoría novedosa para el cálculo lambda con paso por valor (‘call-by-value lambda calculus’ en inglés) que es consistente con la reducción plena. Dicha teoría induce una noción de equivalencia observacional que distingue más puntos que las teorías existentes para dicho cálculo. Esta contribución ayuda a establecer una ‘teoría estándar’ en el cálculo lambda con paso por valor que es análoga a la ‘teoría estándar’ del cálculo lambda clásico propugnada por Barendregt. Se presentan resultados de teoría de la demostración, y se sugiere como abordar el estudio de teoría 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.

Hibridación termosolar en centrales convencionales de generación de electricidad (HiTERCON)

El modelo energético actual está marcado por el predominio de los combustibles fósiles y el intento de introducir energías renovables para evolucionar hacia un modelo más sostenible. Entre las distintas alternativas, las plantas híbridas solar-fósil parecen una solución interesante ya que combinan las ventajas de las dos fuentes de energía. Hasta el momento, las líneas de investigación y análisis de plantas híbridas se ha centrado en el acoplamiento de tecnología solar a plantas o ciclos de potencia operativos. Este enfoque, tiene sentido en un marco como el actual, donde las plantas híbridas operativas no disponen de sistema de almacenamiento y donde se intenta reducir los costes, acoplando tecnología solar a ciclos de potencia existentes. Sin embargo, resta generalidad al análisis de la hibridación, imponiendo el diseño de la planta. Resulta interesante por tanto, realizar estudios que analicen la hibridación desde un punto de vista más general y que permitan a la propia planta, optimizar su diseño. Este estudio pretende aportar conocimiento en esta línea, analizando distintas posibilidades de diseño de futuras plantas híbridas operando en modo Fuel saving mode (FSM). Para ello, se ha realizado un estudio general y sistemático de distintas topologías de plantas híbridas, las cuales consideran como ciclo de potencia el ciclo Brayton y el ciclo Rankine. Para aportar la máxima generalidad posible, se han considerado un amplio abanico de condiciones operativas en ambos bloques. Como aporte al resto de estudios, éste estudio analiza la hibridación desde el punto de vista del bloque termosolar lo que indirectamente permite analizar el funcionamiento de la planta en modo híbrido. Para ello, se han identificado dos casos de diseño: 1. Caso A: Diseño de planta híbrida a partir de una planta o bloque convencional 2. Caso B: Diseño de planta híbrida a partir de una tecnología solar determinada La distinción entre casos de diseño, permite por un lado, establecer el potencial de la hibridación en las dos situaciones que se pueden plantear en la práctica estableciendo además, una base comparativa de resultados y por otro lado, identificar las condiciones de funcionamiento óptimas en las que diseñar la planta. Como conclusión principal, el estudio realizado demuestra que las condiciones de funcionamiento que optimizan la planta híbrida pueden diferir dependiendo del caso de diseño que se considere, lo que implica que el funcionamiento de la planta no tiene porqué estar optimizado simultáneamente para sus dos modos de funcionamiento (modo fósil y modo híbrido). Por tanto, se considera que el diseño final de la planta híbrida debería estar en función del tiempo en que la planta opera en cada uno de los modos, es decir, del Solar Capacity Factor (SCF). Además, el estudio realizado identifica dos situaciones concretas para las cuales la hibridación estaría desaconsejada desde un punto de vista energético. Aunque los resultados obtenidos son sólo una primera aproximación del diseño final de la planta híbrida, proporcionan unas directrices a partir de la cuales iniciar su desarrollo. Esto es especialmente interesante de cara a políticas estratégicas, donde en función de los objetivos vigentes o que se puedan plantear, se puede modificar el diseño de la planta en su estructura básica.

Metodología para la caracterización termoeconómica de plantas híbridas de generación de electricidad

Actualmente la metodología empleada para la evaluación termoeconómica de plantas híbridas solares fósiles consta en la determinación de un factor termoeconómico anual Y. Este factor se define en función del tipo de estudio que se desea realizar. Por ejemplo, en estudios energéticos y / o exergéticos ese parámetro característico se corresponde con el rendimiento. En estudios de tipo medio ambiental, el parámetro a calcular son las emisiones de CO2. En un estudio de tipo económico son típicos los costes nivelados de electricidad (LEC), el valor neto actualizado (VAN) o el periodo de retorno (PR). Esto provoca que los resultados obtenidos carezcan de generalidad, haciéndose difícil su comparación bajo una base común. Además son frecuentes situaciones donde un mismo valor del parámetro Y se corresponde con plantas con diferentes características localización, diseño y / o condiciones de operación. Este estudio pretende aportar una metodología para el análisis paramétrico de plantas híbridas solares fósiles (MASF) que cubra las limitaciones existentes. MASF se fundamenta en el cálculo simultáneo de tres factores: Factor de tamaño del bloque solar SSF. Representa el ratio de irradiación incidente sobre el bloque solar que es trasformada en energía térmica. Factor de hibridación cf). Representa el ratio de energía térmica que es debida al recurso solar. Factor termoeconómico Y. Parámetro representativo del enfoque desde el cual se realiza el estudio. MASF ha sido definida en base a un estudio numérico que analiza la variación en las prestaciones anuales de las plantas híbridas solares fósiles ante diferentes valores de sus parámetros constructivos y operativos. Las principales aportaciones de MASF sobre el estado del arte se pueden resumir en: 1. Se ha dotado al proceso de evaluación de plantas híbridas solares fósiles de una metodología general y sistemática. 2. Se han definido dos resoluciones temporales de cálculo: una basada en valores medios anuales (agregada) y otra basada en valores instantáneos (desagregada). 3. Se han establecido criterios que permiten seleccionar que resolución es más recomendable en cada caso. 4. Se han establecido las principales hipótesis que se pueden adoptar para cada resolución. 5. Se ha definido el parámetro SSF hasta ahora no existente en la literatura especializada. 6. La metodología MASF permite discriminar plantas que tienen un mismo valor del factor termoeconómico Y y mismo factor de hibridación cf) en función del factor de tamaño del bloque solar SSF. 7. La metodología MASF permite determinar las prestaciones de la planta ante diferentes condiciones operativas de la planta. Se ha aplicado la metodología MASF a la realización de dos estudios: Diseño de una planta híbrida solar fósil. Se ha analizado como afectan a la viabilidad termoeconómica las diferentes opciones de diseño de un bloque solar en el caso de estudiar la posible hibridación de una planta fósil existente. Diseño de políticas energéticas. Se ha analizado como varía la viabilidad termoeconómica de una planta híbrida solar fósil ante diferentes políticas energéticas (incentivos a la instalación e incentivos a la generación). Este estudio se ha completado con el análisis de dos situaciones actuales: hibridación en España y proyectos subvencionados por el Banco Mundial.

Análisis, diseño e implementación de un SDK híbrido basado en tecnologías web para la integración de clientes contra una plataforma de servicios RESTFul/JSON

En el departamento de Ocio Digital de bq se desarrollan multitud de proyectos con diferentes modelos de negocio y diferentes stack tecnológicos. Para llevar a cabo todos estos proyectos, es necesario tener un ecosistema de desarrollo lo más unificado y centralizado posible. Por eso, en el departamento existe una plataforma genérica de servicios REST sobre la que se apoyan todos los aplicativos desarrollados. Para agilizar y facilitar la integración de los aplicativos con la plataforma de servicios,se desarrolla este SDK (Software Development Kit) basado en JavaScript llamado corbel-js. Este SDK ha de funcionar tanto en aplicaciones web, como en un middleware basado en node.js desarrollado también en la organización, por lo que el SDK se ha desarrollado de forma híbrida, siendo capaz de ejecutarse tanto en en el lado del cliente, como en el lado del servidor. Además, como parte de la filosofía del departamento, el desarrollo del SDK está basado en tecnologías Open Source, usando metodologías ágiles de desarrollo y un sistema de integración continua y revisión de código, garantizando la calidad del mismo. ABSTRACT A lot of different kinds of software projects are developed in the digital department of bq. To easily develop all of these projects, each one with its own business model and technology stack, it is necessary to have an unique software ecosystem. Because of that, in the software department a generic service REST platform has been developed. To support an easy integration of the applications with the service platform of the organization, this SDK(Software Development Kit) has been developed in JavaScript. As the SDK has to run under a web application and under a software middleware based in node.js, also developed in the organization, the SDK is hybrid, being capable of run inside a web client application or inside a node.js application server. As a part of the software philosophy of the department, the development of the SDK is made with a whole open source software stack, using agile software methodologies.

Hybrid wind-diesel power plant valuation and optimization using real option theory and dynamic programming

El sistema de energía eólica-diesel híbrido tiene un gran potencial en la prestación de suministro de energía a comunidades remotas. En comparación con los sistemas tradicionales de diesel, las plantas de energía híbridas ofrecen grandes ventajas tales como el suministro de capacidad de energía extra para "microgrids", reducción de los contaminantes y emisiones de gases de efecto invernadero, y la cobertura del riesgo de aumento inesperado del precio del combustible. El principal objetivo de la presente tesis es proporcionar nuevos conocimientos para la evaluación y optimización de los sistemas de energía híbrido eólico-diesel considerando las incertidumbres. Dado que la energía eólica es una variable estocástica, ésta no puede ser controlada ni predecirse con exactitud. La naturaleza incierta del viento como fuente de energía produce serios problemas tanto para la operación como para la evaluación del valor del sistema de energía eólica-diesel híbrido. Por un lado, la regulación de la potencia inyectada desde las turbinas de viento es una difícil tarea cuando opera el sistema híbrido. Por otro lado, el bene.cio económico de un sistema eólico-diesel híbrido se logra directamente a través de la energía entregada a la red de alimentación de la energía eólica. Consecuentemente, la incertidumbre de los recursos eólicos incrementa la dificultad de estimar los beneficios globales en la etapa de planificación. La principal preocupación del modelo tradicional determinista es no tener en cuenta la incertidumbre futura a la hora de tomar la decisión de operación. Con lo cual, no se prevé las acciones operativas flexibles en respuesta a los escenarios futuros. El análisis del rendimiento y simulación por ordenador en el Proyecto Eólico San Cristóbal demuestra que la incertidumbre sobre la energía eólica, las estrategias de control, almacenamiento de energía, y la curva de potencia de aerogeneradores tienen un impacto significativo sobre el rendimiento del sistema. En la presente tesis, se analiza la relación entre la teoría de valoración de opciones y el proceso de toma de decisiones. La opción real se desarrolla con un modelo y se presenta a través de ejemplos prácticos para evaluar el valor de los sistemas de energía eólica-diesel híbridos. Los resultados muestran que las opciones operacionales pueden aportar un valor adicional para el sistema de energía híbrida, cuando esta flexibilidad operativa se utiliza correctamente. Este marco se puede aplicar en la optimización de la operación a corto plazo teniendo en cuenta la naturaleza dependiente de la trayectoria de la política óptima de despacho, dadas las plausibles futuras realizaciones de la producción de energía eólica. En comparación con los métodos de valoración y optimización existentes, el resultado del caso de estudio numérico muestra que la política de operación resultante del modelo de optimización propuesto presenta una notable actuación en la reducción del con- sumo total de combustible del sistema eólico-diesel. Con el .n de tomar decisiones óptimas, los operadores de plantas de energía y los gestores de éstas no deben centrarse sólo en el resultado directo de cada acción operativa, tampoco deberían tomar decisiones deterministas. La forma correcta es gestionar dinámicamente el sistema de energía teniendo en cuenta el valor futuro condicionado en cada opción frente a la incertidumbre. ABSTRACT Hybrid wind-diesel power systems have a great potential in providing energy supply to remote communities. Compared with the traditional diesel systems, hybrid power plants are providing many advantages such as providing extra energy capacity to the micro-grid, reducing pollution and greenhouse-gas emissions, and hedging the risk of unexpected fuel price increases. This dissertation aims at providing novel insights for assessing and optimizing hybrid wind-diesel power systems considering the related uncertainties. Since wind power can neither be controlled nor accurately predicted, the energy harvested from a wind turbine may be considered a stochastic variable. This uncertain nature of wind energy source results in serious problems for both the operation and value assessment of the hybrid wind-diesel power system. On the one hand, regulating the uncertain power injected from wind turbines is a difficult task when operating the hybrid system. On the other hand, the economic profit of a hybrid wind-diesel system is achieved directly through the energy delivered to the power grid from the wind energy. Therefore, the uncertainty of wind resources has increased the difficulty in estimating the total benefits in the planning stage. The main concern of the traditional deterministic model is that it does not consider the future uncertainty when making the dispatch decision. Thus, it does not provide flexible operational actions in response to the uncertain future scenarios. Performance analysis and computer simulation on the San Cristobal Wind Project demonstrate that the wind power uncertainty, control strategies, energy storage, and the wind turbine power curve have a significant impact on the performance of the system. In this dissertation, the relationship between option pricing theory and decision making process is discussed. A real option model is developed and presented through practical examples for assessing the value of hybrid wind-diesel power systems. Results show that operational options can provide additional value to the hybrid power system when this operational flexibility is correctly utilized. This framework can be applied in optimizing short term dispatch decisions considering the path-dependent nature of the optimal dispatch policy, given the plausible future realizations of the wind power production. Comparing with the existing valuation and optimization methods, result from numerical example shows that the dispatch policy resulting from the proposed optimization model exhibits a remarkable performance in minimizing the total fuel consumption of the wind-diesel system. In order to make optimal decisions, power plant operators and managers should not just focus on the direct outcome of each operational action; neither should they make deterministic decisions. The correct way is to dynamically manage the power system by taking into consideration the conditional future value in each option in response to the uncertainty.