A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions

In this article we study subsystems SIDᵥ of the theory ID₁ in which fixed point induction is restricted to properly stratified formulas.

Stationary Markovian Equilibrium in Overlapping Generation Models with Stochastic Nonclassical Production

This paper provides new sufficient conditions for the existence, computation via successive approximations, and stability of Markovian equilibrium decision processes for a large class of OLG models with stochastic nonclassical production. Our notion of stability is existence of stationary Markovian equilibrium. With a nonclassical production, our economies encompass a large class of OLG models with public policy, valued fiat money, production externalities, and Markov shocks to production. Our approach combines aspects of both topological and order theoretic fixed point theory, and provides the basis of globally stable numerical iteration procedures for computing extremal Markovian equilibrium objects. In addition to new theoretical results on existence and computation, we provide some monotone comparative statics results on the space of economies.

Seagrass and associated benthic community data derived from field surveys at Low Isles, Great Barrier Reef, conducted July-August, 1997

The distribution of seagrass and associated benthic communities on the reef and lagoon of Low Isles, Great Barrier Reef, was mapped between the 29 July and 29 August 1997. For this survey, observers walked or free-dived at survey points positioned approximately 50 m apart along a series of transects. Visual estimates of above-ground seagrass biomass and % cover of each benthos and substrate type were recorded at each survey point. A differential handheld global positioning system (GPS) was used to locate each survey point (accuracy ±3m). A total of 349 benthic survey points were examined. To assist with mapping meadow/habitat type boundaries, an additional 177 field points were assessed and a georeferenced 1:12,000 aerial photograph (26th August 1997) was used as a secondary source of information. Bathymetric data (elevation below Mean Sea Level) measured at each point assessed and from Ellison (1997) supplemented information used to determine boundaries, particularly in the subtidal lagoon. 127.8 ±29.6 hectares was mapped. Seagrass and associated benthic community data was derived by haphazardly placing 3 quadrats (0.25m**2) at each survey point. Seagrass above ground biomass (standing crop, grams dry weight (g DW m**-2)) was determined within each quadrat using a non-destructive visual estimates of biomass technique and the seagrass species present identified. In addition, the cover of all benthos was measured within each of the 3 quadrats using a systematic 5 point method. For each quadrat, frequency of occurrence for each benthic category was converted to a percentage of the total number of points (5 per quadrat). Data are presented as the average of the 3 quadrats at each point. Polygons of discrete seagrass meadow/habitat type boundaries were created using the on-screen digitising functions of ArcGIS (ESRI Inc.), differentiated on the basis of colour, texture, and the geomorphic and geographical context. The resulting seagrass and benthic cover data of each survey point and for each seagrass meadow/habitat type was linked to GPS coordinates, saved as an ArcMap point and polygon shapefile, respectively, and projected to Universal Transverse Mercator WGS84 Zone 55 South.

DISPRO datasets for validation of coastal hydrodynamic models

Appropriate field data are required to check the reliability of hydrodynamic models simulating the dispersion of soluble substances in the marine environment. This study deals with the collection of physical measurements and soluble tracer data intended specifically for this kind of validation. The intensity of currents as well as the complexity of topography and tides around the Cap de La Hague in the center of the English Channel makes it one of the most difficult areas to represent in terms of hydrodynamics and dispersion. Controlled releases of tritium - in the form of HTO - are carried out in this area by the AREVA-NC plant, providing an excellent soluble tracer. A total of 14 493 measurements were acquired to track dispersion in the hours and days following a release. These data, supplementing previously gathered data and physical measurements (bathymetry, water-surface levels, Eulerian and Lagrangian current studies) allow us to test dispersion models from the hour following release to periods of several years which are not accessible with dye experiments. The dispersion characteristics are described and methods are proposed for comparing models against measurements. An application is proposed for a 2 dimensions high-resolution numerical model. It shows how an extensive dataset can be used to build, calibrate and validate several aspects of the model in a highly dynamic and macrotidal area: tidal cycle timing, tidal amplitude, fixed-point current data, hodographs. This study presents results concerning the model's ability to reproduce residual Lagrangian currents, along with a comparison between simulation and high-frequency measurements of tracer dispersion. Physical and tracer data are available from the SISMER database of IFREMER (www.ifremer.fr/sismer/catal). This tool for validation of models in macro-tidal seas is intended to be an open and evolving resource, which could provide a benchmark for dispersion model validation.

(Table) Density and biomass of phytoplankton in Vostok Bay in August and September 2010

The natural phytoplankton was monitored by means of fluorimetric equipment in Vostok Bay of the Sea of Japan. A gradual increase in the microalgae abundance was revealed in the course of the main water current, which enters the bay and leaves it. The continuous registration of chlorophyll fluorescence at a fixed point in the bay indicates the significant microscale variation of the abundance and functional state of the phytoplankton.

Medidas autosemejantes en el plano, momentos y matrices de Hessenberg

La tesis MEDIDAS AUTOSEMEJANTES EN EL PLANO, MOMENTOS Y MATRICES DE HESSENBERG se enmarca entre las áreas de la teoría geométrica de la medida, la teoría de polinomios ortogonales y la teoría de operadores. La memoria aborda el estudio de medidas con soporte acotado en el plano complejo vistas con la óptica de las matrices infinitas de momentos y de Hessenberg asociadas a estas medidas que en la teoría de los polinomios ortogonales las representan. En particular se centra en el estudio de las medidas autosemejantes que son las medidas de equilibrio definidas por un sistema de funciones iteradas (SFI). Los conjuntos autosemejantes son conjuntos que tienen la propiedad geométrica de descomponerse en unión de piezas semejantes al conjunto total. Estas piezas pueden solaparse o no, cuando el solapamiento es pequeño la teoría de Hutchinson [Hut81] funciona bien, pero cuando no existen restricciones falla. El problema del solapamiento consiste en controlar la medida de este solapamiento. Un ejemplo de la complejidad de este problema se plantea con las convoluciones infinitas de distribuciones de Bernoulli, que han resultado ser un ejemplo de medidas autosemejantes en el caso real. En 1935 Jessen y A. Wintner [JW35] ya se planteaba este problema, lejos de ser sencillo ha sido estudiado durante más de setenta y cinco años y siguen sin resolverse las principales cuestiones planteadas ya por A. Garsia [Gar62] en 1962. El interés que ha despertado este problema así como la complejidad del mismo está demostrado por las numerosas publicaciones que abordan cuestiones relacionadas con este problema ver por ejemplo [JW35], [Erd39], [PS96], [Ma00], [Ma96], [Sol98], [Mat95], [PS96], [Sim05],[JKS07] [JKS11]. En el primer capítulo comenzamos introduciendo con detalle las medidas autosemejante en el plano complejo y los sistemas de funciones iteradas, así como los conceptos de la teoría de la medida necesarios para describirlos. A continuación se introducen las herramientas necesarias de teoría de polinomios ortogonales, matrices infinitas y operadores que se van a usar. En el segundo y tercer capítulo trasladamos las propiedades geométricas de las medidas autosemejantes a las matrices de momentos y de Hessenberg, respectivamente. A partir de estos resultados se describen algoritmos para calcular estas matrices a partir del SFI correspondiente. Concretamente, se obtienen fórmulas explícitas y algoritmos de aproximación para los momentos y matrices de momentos de medidas fractales, a partir de un teorema del punto fijo para las matrices. Además utilizando técnicas de la teoría de operadores, se han extendido al plano complejo los resultados que G. Mantica [Ma00, Ma96] obtenía en el caso real. Este resultado es la base para definir un algoritmo estable de aproximación de la matriz de Hessenberg asociada a una medida fractal u obtener secciones finitas exactas de matrices Hessenberg asociadas a una suma de medidas. En el último capítulo, se consideran medidas, μ, más generales y se estudia el comportamiento asintótico de los autovalores de una matriz hermitiana de momentos y su impacto en las propiedades de la medida asociada. En el resultado central se demuestra que si los polinomios asociados son densos en L2(μ) entonces necesariamente el autovalor mínimo de las secciones finitas de la matriz de momentos de la medida tiende a cero. ABSTRACT The Thesis work “Self-similar Measures on the Plane, Moments and Hessenberg Matrices” is framed among the geometric measure theory, orthogonal polynomials and operator theory. The work studies measures with compact support on the complex plane from the point of view of the associated infinite moments and Hessenberg matrices representing them in the theory of orthogonal polynomials. More precisely, it concentrates on the study of the self-similar measures that are equilibrium measures in a iterated functions system. Self-similar sets have the geometric property of being decomposable in a union of similar pieces to the complete set. These pieces can overlap. If the overlapping is small, Hutchinson’s theory [Hut81] works well, however, when it has no restrictions, the theory does not hold. The overlapping problem consists in controlling the measure of the overlap. The complexity of this problem is exemplified in the infinite convolutions of Bernoulli’s distributions, that are an example of self-similar measures in the real case. As early as 1935 [JW35], Jessen and Wintner posed this problem, that far from being simple, has been studied during more than 75 years. The main cuestiones posed by Garsia in 1962 [Gar62] remain unsolved. The interest in this problem, together with its complexity, is demonstrated by the number of publications that over the years have dealt with it. See, for example, [JW35], [Erd39], [PS96], [Ma00], [Ma96], [Sol98], [Mat95], [PS96], [Sim05], [JKS07] [JKS11]. In the first chapter, we will start with a detailed introduction to the self-similar measurements in the complex plane and to the iterated functions systems, also including the concepts of measure theory needed to describe them. Next, we introduce the necessary tools from orthogonal polynomials, infinite matrices and operators. In the second and third chapter we will translate the geometric properties of selfsimilar measures to the moments and Hessenberg matrices. From these results, we will describe algorithms to calculate these matrices from the corresponding iterated functions systems. To be precise, we obtain explicit formulas and approximation algorithms for the moments and moment matrices of fractal measures from a new fixed point theorem for matrices. Moreover, using techniques from operator theory, we extend to the complex plane the real case results obtained by Mantica [Ma00, Ma96]. This result is the base to define a stable algorithm that approximates the Hessenberg matrix associated to a fractal measure and obtains exact finite sections of Hessenberg matrices associated to a sum of measurements. In the last chapter, we consider more general measures, μ, and study the asymptotic behaviour of the eigenvalues of a hermitian matrix of moments, together with its impact on the properties of the associated measure. In the main result we demonstrate that, if the associated polynomials are dense in L2(μ), then necessarily follows that the minimum eigenvalue of the finite sections of the moments matrix goes to zero.

Reduced certificates for abstraction-carrying code

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixedpoint) abstraction to the code consumer is that its validity is checked in a single pass of an abstract interpretation-based checker. A main challenge is to reduce the size of certificates as much as possible while at the same time not increasing checking time. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. We also provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. The experimental results within the CiaoPP system show that our proposal is able to greatly reduce the size of certificates in practice.

On abstraction-carrying code and certificate-size reduction

Abstraction-Carrying Code (ACC) is a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certificate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible, while at the same time not increasing checking time. Intuitively, we only include in the certificate the information which the checker is unable to reproduce without iterating. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we show how to instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker.

Generation of reduced certificates in abstraction-carrying code

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixedpoint) abstraction to the code consumer is that its validity is checked in a single pass of an abstract interpretation-based checker. A main challenge is to reduce the size of certificates as much as possible while at the same time not increasing checking time. In this paper, we first introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we then instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker.

Reduced certificates for abstraction-carrying code

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certifícate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify information which can be reconstructed by the single-pass checker. Finally, we study what the effects of reduced certificates are on the correctness and completeness of the checking process. We provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. Our ideas are illustrated through a running example, implemented in the context of constraint logic programs, which shows that our approach improves state-of-the-art techniques for reducing the size of certificates.

A non-perturbative renormalization group study of the stochastic NavierStokes equation

We study the renormalization group flow of the average action of the stochastic Navier-Stokes equation with power-law forcing. Using Galilean invariance, we introduce a nonperturbative approximation adapted to the zero-frequency sector of the theory in the parametric range of the Hölder exponent 4−2 ɛ of the forcing where real-space local interactions are relevant. In any spatial dimension d, we observe the convergence of the resulting renormalization group flow to a unique fixed point which yields a kinetic energy spectrum scaling in agreement with canonical dimension analysis. Kolmogorov's −5/3 law is, thus, recovered for ɛ=2 as also predicted by perturbative renormalization. At variance with the perturbative prediction, the −5/3 law emerges in the presence of a saturation in the ɛ dependence of the scaling dimension of the eddy diffusivity at ɛ=3/2 when, according to perturbative renormalization, the velocity field becomes infrared relevant.

Floating car data augmentation based on infrastructure sensors and neural networks

The development of new-generation intelligent vehicle technologies will lead to a better level of road safety and CO2 emission reductions. However, the weak point of all these systems is their need for comprehensive and reliable data. For traffic data acquisition, two sources are currently available: 1) infrastructure sensors and 2) floating vehicles. The former consists of a set of fixed point detectors installed in the roads, and the latter consists of the use of mobile probe vehicles as mobile sensors. However, both systems still have some deficiencies. The infrastructure sensors retrieve information fromstatic points of the road, which are spaced, in some cases, kilometers apart. This means that the picture of the actual traffic situation is not a real one. This deficiency is corrected by floating cars, which retrieve dynamic information on the traffic situation. Unfortunately, the number of floating data vehicles currently available is too small and insufficient to give a complete picture of the road traffic. In this paper, we present a floating car data (FCD) augmentation system that combines information fromfloating data vehicles and infrastructure sensors, and that, by using neural networks, is capable of incrementing the amount of FCD with virtual information. This system has been implemented and tested on actual roads, and the results show little difference between the data supplied by the floating vehicles and the virtual vehicles.

A generic, hard transition to chaos

A hard-in-amplitude transition to chaos in a class of dissipative flows of broad applicability is presented. For positive values of a parameter F, no matter how small, a fully developed chaotic attractor exists within some domain of additional parameters, whereas no chaotic behavior exists for F < 0. As F is made positive, an unstable fixed point reaches an invariant plane to enter a phase half-space of physical solutions; the ghosts of a line of fixed points and a rich heteroclinic structure existing at F = 0 make the limits t --* +oc, F ~ +0 non-commuting, and allow an exact description of the chaotic flow. The formal structure of flows that exhibit the transition is determined. A subclass of such flows (coupled oscillators in near-resonance at any 2 : q frequency ratio, with F representing linear excitation of the first oscillator) is fully analysed

Damping models in the truncated derivative nonlinear Schrödinger equation

Four-dimensional flow in the phase space of three amplitudes of circularly polarized Alfven waves and one relative phase, resulting from a resonant three-wave truncation of the derivative nonlinear Schrödinger equation, has been analyzed; wave 1 is linearly unstable with growth rate , and waves 2 and 3 are stable with damping 2 and 3, respectively. The dependence of gross dynamical features on the damping model as characterized by the relation between damping and wave-vector ratios, 2 /3, k2 /k3, and the polarization of the waves, is discussed; two damping models, Landau k and resistive k2, are studied in depth. Very complex dynamics, such as multiple blue sky catastrophes and chaotic attractors arising from Feigenbaum sequences, and explosive bifurcations involving Intermittency-I chaos, are shown to be associated with the existence and loss of stability of certain fixed point P of the flow. Independently of the damping model, P may only exist as against flow contraction just requiring.In the case of right-hand RH polarization, point P may exist for all models other than Landau damping; for the resistive model, P may exist for RH polarization only if 2+3/2.

Non-periodic driving of coupled oscillators:a spherical swing

Nonlinearly coupled, damped oscillators at 1:1 frequency ratio, one oscillator being driven coherently for efficient excitation, are exemplified by a spherical swing with some phase-mismatch between drive and response. For certain damping range, excitation is found to succeed if it lags behind, but to produce a chaotic attractor if it leads the response. Although a period-doubhng sequence, for damping increasing, leads to the attractor, this is actually born as a hard (as regards amplitude) bifurcation at a zero growth-rate parametric line; as damping decreases, an unstable fixed point crosses an invariant plane to enter as saddle-focus a phase-space domain of physical solutions. A second hard bifurcation occurs at the zero mismatch line, the saddle-focus leaving that domain. Times on the attractor diverge when approaching either fine, leading to exactly one-dimensional and noninvertible limit maps, which are analytically determined.