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.

Experimental evidence of super-resolution better than lambda/105 with positive refraction

Super-resolution (SR) systems surpassing the Abbe diffraction limit have been theoretically and experimentally demonstrated using a number of different approaches and technologies: using materials with a negative refractive index, utilizing optical super-oscillation, using a resonant metalens, etc. However, recently it has been proved theoretically that in the Maxwell fish-eye lens (MFE), a device made of positive refractive index materials, the same phenomenon takes place. Moreover, using a simpler device equivalent to the MFE called the spherical geodesic waveguide (SGW), an SR of up to λ/3000 was simulated in COMSOL. Until now, only one piece of experimental evidence of SR with positive refraction has been reported (up to λ/5) for an MFE prototype working at microwave frequencies. Here, experimental results are presented for an SGW prototype showing an SR of up to λ/105. The SGW prototype consists of two concentric metallic spheres with an air space in between and two coaxial ports acting as an emitter and a receiver. The prototype has been analyzed in the range 1 GHz to 1.3 GHz.

Heated fiber optic distributed temperature sensing for measuring soil volumetric heat capacity and water content: A dual probe heat-pulse approach

The first feasibility study of using dual-probe heated fiber optics with distributed temperature sensing to measure soil volumetric heat capacity and soil water content is presented. Although results using different combinations of cables demonstrate feasibility, further work is needed to gain accuracy, including a model to account for the finite dimension and the thermal influence of the probes. Implementation of the dual-probe heat-pulse (DPHP) approach for measurement of volumetric heat capacity (C) and water content (θ) with distributed temperature sensing heated fiber optic (FO) systems presents an unprecedented opportunity for environmental monitoring (e.g., simultaneous measurement at thousands of points). We applied uniform heat pulses along a FO cable and monitored the thermal response at adjacent cables. We tested the DPHP method in the laboratory using multiple FO cables at a range of spacings. The amplitude and phase shift in the heat signal with distance was found to be a function of the soil volumetric heat capacity. Estimations of C at a range of moisture contents (θ = 0.09– 0.34 m3 m−3) suggest the feasibility of measurement via responsiveness to the changes in θ, although we observed error with decreasing soil water contents (up to 26% at θ = 0.09 m3 m−3). Optimization will require further models to account for the finite radius and thermal influence of the FO cables. Although the results indicate that the method shows great promise, further study is needed to quantify the effects of soil type, cable spacing, and jacket configurations on accuracy.

Prospectives of monitoring biological activity in a red-legged partridge incubator with a carbon dioxide probe

This study focuses on the relationship between CO2 production and the ultimate hatchability of the incubation. A total amount of 43316 eggs of red-legged partridge (Alectoris rufa) were supervised during five actual incubations: three in 2012 and two in 2013. The CO2 concentration inside the incubator was monitored over a 20-day period, showing sigmoidal growth from ambient level (428 ppm) up to 1700 ppm in the incubation with the highest hatchability. Two sigmoid growth models (logistic and Gompertz) were used to describe the CO2 production by the eggs, with the result that the logistic model was a slightly better fit (r2=0.976 compared to r2=0.9746 for Gompertz). A coefficient of determination of 0.997 between the final CO2 estimation (ppm) using the logistic model and hatchability (%) was found.