Secondary nontwist phenomena in area-preserving maps

Phenomena as reconnection scenarios, periodic-orbit collisions, and primary shearless tori have been recognized as features of nontwist maps. Recently, these phenomena and secondary shearless tori were analytically predicted for generic maps in the neighborhood of the tripling bifurcation of an elliptic fixed point. In this paper, we apply a numerical procedure to find internal rotation number profiles that highlight the creation of periodic orbits within islands of stability by a saddle-center bifurcation that emerges out a secondary shearless torus. In addition to the analytical predictions, our numerical procedure applied to the twist and nontwist standard maps reveals that the atypical secondary shearless torus occurs not only near a tripling bifurcation of the fixed point but also near a quadrupling bifurcation. (C) 2012 American Institute of Physics. [http://dx.doi.org/10.1063/1.4750040]

Nontwist symplectic maps in tokamaks

We review symplectic nontwist maps that we have introduced to describe Lagrangian transport properties in magnetically confined plasmas in tokamaks. These nontwist maps are suitable to describe the formation and destruction of transport barriers in the shearless region (i.e., near the curve where the twist condition does not hold). The maps can be used to investigate two kinds of problems in plasmas with non-monotonic field profiles: the first is the chaotic magnetic field line transport in plasmas with external resonant perturbations. The second problem is the chaotic particle drift motion caused by electrostatic drift waves. The presented analytical maps, derived from plasma models with equilibrium field profiles and control parameters that are commonly measured in plasma discharges, can be used to investigate long-term transport properties. (C) 2011 Elsevier B.V. All rights reserved.

Flow Visualization with Quantified Spatial and Temporal Errors Using Edge Maps

Robust analysis of vector fields has been established as an important tool for deriving insights from the complex systems these fields model. Traditional analysis and visualization techniques rely primarily on computing streamlines through numerical integration. The inherent numerical errors of such approaches are usually ignored, leading to inconsistencies that cause unreliable visualizations and can ultimately prevent in-depth analysis. We propose a new representation for vector fields on surfaces that replaces numerical integration through triangles with maps from the triangle boundaries to themselves. This representation, called edge maps, permits a concise description of flow behaviors and is equivalent to computing all possible streamlines at a user defined error threshold. Independent of this error streamlines computed using edge maps are guaranteed to be consistent up to floating point precision, enabling the stable extraction of features such as the topological skeleton. Furthermore, our representation explicitly stores spatial and temporal errors which we use to produce more informative visualizations. This work describes the construction of edge maps, the error quantification, and a refinement procedure to adhere to a user defined error bound. Finally, we introduce new visualizations using the additional information provided by edge maps to indicate the uncertainty involved in computing streamlines and topological structures.

COMPARISON MEASURES OF MAPS GENERATED BY GEOSTATISTICAL METHODS

This study uses several measures derived from the error matrix for comparing two thematic maps generated with the same sample set. The reference map was generated with all the sample elements and the map set as the model was generated without the two points detected as influential by the analysis of local influence diagnostics. The data analyzed refer to the wheat productivity in an agricultural area of 13.55 ha considering a sampling grid of 50 x 50 m comprising 50 georeferenced sample elements. The comparison measures derived from the error matrix indicated that despite some similarity on the maps, they are different. The difference between the estimated production by the reference map and the actual production was of 350 kilograms. The same difference calculated with the mode map was of 50 kilograms, indicating that the study of influential points is of fundamental importance to obtain a more reliable estimative and use of measures obtained from the error matrix is a good option to make comparisons between thematic maps.

Axioms for the coincidence index of maps between manifolds of the same dimension

We study the coincidence theory of maps between two manifolds of the same dimension from an axiomatic viewpoint. First we look at coincidences of maps between manifolds where one of the maps is orientation true, and give a set of axioms such that characterizes the local index (which is an integer valued function). Then we consider coincidence theory for arbitrary pairs of maps between two manifolds. Similarly we provide a set of axioms which characterize the local index, which in this case is a function with values in Z circle plus Z(2). We also show in each setting that the group of values for the index (either Z or Z circle plus Z(2)) is determined by the axioms. Finally, for the general case of coincidence theory for arbitrary pairs of maps between two manifolds we provide a set of axioms which characterize the local Reidemeister trace which is an element of an abelian group which depends on the pair of functions. These results extend known results for coincidences between orientable differentiable manifolds. (C) 2012 Elsevier B.V. All rights reserved.

Polar foliations and isoparametric maps

A singular Riemannian foliation F on a complete Riemannian manifold M is called a polar foliation if, for each regular point p, there is an immersed submanifold Sigma, called section, that passes through p and that meets all the leaves and always perpendicularly. A typical example of a polar foliation is the partition of M into the orbits of a polar action, i.e., an isometric action with sections. In this article we prove that the leaves of H : M -> Sigma, coincide with the level sets of a smooth map H: M -> Sigma, if M is simply connected. In particular, the orbits of a polar action on a simply connected space are level sets of an isoparametric map. This result extends previous results due to the author and Gorodski, Heintze, Liu and Olmos, Carter and West, and Terng.

Chains of Infinite Order, Chains with Memory of Variable Length, and Maps of the Interval

We show how to construct a topological Markov map of the interval whose invariant probability measure is the stationary law of a given stochastic chain of infinite order. In particular we characterize the maps corresponding to stochastic chains with memory of variable length. The problem treated here is the converse of the classical construction of the Gibbs formalism for Markov expanding maps of the interval.

Growth hormone pharmacogenetics: the interactive effect of a microsatellite in the IGF1 promoter region with the GHR-exon 3 and-202 A/C IGFBP3 variants on treatment outcomes of children with severe GH deficiency

Insulin-like growth factor type 1 (IGF1) is a mediator of growth hormone (GH) action, and therefore, IGF1 is a candidate gene for recombinant human GH (rhGH) pharmacogenetics. Lower serum IGF1 levels were found in adults homozygous for 19 cytosine-adenosine (CA) repeats in the IGF1 promoter. The aim of this study was to evaluate the influence of (CA)n IGF1 polymorphism, alone or in combination with GH receptor (GHR)-exon 3 and -202 A/C insulin-like growth factor binding protein-3 (IGFBP3) polymorphisms, on the growth response to rhGH therapy in GH-deficient (GHD) patients. Eighty-four severe GHD patients were genotyped for (CA) n IGF1, -202 A/C IGFBP3 and GHR-exon 3 polymorphisms. Multiple linear regressions were performed to estimate the effect of each genotype, after adjustment for other influential factors. We assessed the influence of genotypes on the first year growth velocity (1st y GV) (n = 84) and adult height standard deviation score (SDS) adjusted for target-height SDS (AH-TH SDS) after rhGH therapy (n = 37). Homozygosity for the IGF1 19CA repeat allele was negatively correlated with 1st y GV (P = 0.03) and AH-TH SDS (P = 0.002) in multiple linear regression analysis. In conjunction with clinical factors, IGF1 and IGFBP3 genotypes explain 29% of the 1st y GV variability, whereas IGF1 and GHR polymorphisms explain 59% of final height-target-height SDS variability. We conclude that homozygosity for IGF1 (CA) 19 allele is associated with less favorable short-and long-term growth outcomes after rhGH treatment in patients with severe GHD. Furthermore, this polymorphism exhibits a non-additive interaction with -202 A/C IGFBP3 genotype on the 1st y GV and with GHR-exon 3 genotype on adult height. The Pharmacogenomics Journal (2012) 12, 439-445; doi:10.1038/tpj.2011.13; published online 5 April 2011

The Interactive Effect of GHR-Exon 3 and -202 A/C IGFBP3 Polymorphisms on rhGH Responsiveness and Treatment Outcomes in Patients with Turner Syndrome

Context: There is great interindividual variability in the response to recombinant human (rh) GH therapy in patients with Turner syndrome (TS). Ascertaining genetic factors can improve the accuracy of growth response predictions. Objective: The objective of the study was to assess the individual and combined influence of GHR-exon 3 and -202 A/C IGFBP3 polymorphisms on the short-and long-term outcomes of rhGH therapy in patients with TS. Design and Patients: GHR-exon 3 and -202 A/C IGFBP3 genotyping (rs2854744) was correlated with height data of 112 patients with TS who remained prepubertal during the first year of rhGH therapy and 65 patients who reached adult height after 5 +/- 2.5 yr of rhGH treatment. Main Outcome Measures: First-year growth velocity and adult height were measured. Results: Patients carrying at least one GHR-d3 or -202 A-IGFBP3 allele presented higher mean first-year growth velocity and achieved taller adult heights than those homozygous for GHR-fl or -202 C-IGFBP3 alleles, respectively. The combined analysis of GHR-exon 3 and -202 A/C IGFBP3 genotypes showed a clear nonadditive epistatic influence on adult height of patients with TS treated with rhGH (GHR-exon 3 alone, R-2 = 0.27; -202 A/C IGFBP3, R-2 = 0.24; the combined genotypes, R-2 = 0.37 at multiple linear regression). Together with clinical factors, these genotypes accounted for 61% of the variability in adult height of patients with TS after rhGH therapy. Conclusion: Homozygosity for the GHR-exon3 full-length allele and/or the -202C-IGFBP3 allele are associated with less favorable short-and long-term growth outcomes after rhGH treatment in patients with TS. (J Clin Endocrinol Metab 97: E671-E677, 2012)

Wecken type problems for self-maps of the Klein bottle

We consider various problems regarding roots and coincidence points for maps into the Klein bottle . The root problem where the target is and the domain is a compact surface with non-positive Euler characteristic is studied. Results similar to those when the target is the torus are obtained. The Wecken property for coincidences from to is established, and we also obtain the following 1-parameter result. Families which are coincidence free but any homotopy between and , , creates a coincidence with . This is done for any pair of maps such that the Nielsen coincidence number is zero. Finally, we exhibit one such family where is the constant map and if we allow for homotopies of , then we can find a coincidence free pair of homotopies.

Comparison measures of maps generated by geostatistical methods

This study uses several measures derived from the error matrix for comparing two thematic maps generated with the same sample set. The reference map was generated with all the sample elements and the map set as the model was generated without the two points detected as influential by the analysis of local influence diagnostics. The data analyzed refer to the wheat productivity in an agricultural area of 13.55 ha considering a sampling grid of 50 x 50 m comprising 50 georeferenced sample elements. The comparison measures derived from the error matrix indicated that despite some similarity on the maps, they are different. The difference between the estimated production by the reference map and the actual production was of 350 kilograms. The same difference calculated with the mode map was of 50 kilograms, indicating that the study of influential points is of fundamental importance to obtain a more reliable estimative and use of measures obtained from the error matrix is a good option to make comparisons between thematic maps.

Digital library of historical cartography: open access to cultural heritage and public good

This paper describes the integration of information between Digital Library of Historical Cartography and Bibliographical Database (DEDALUS), both of the University of São Paulo (USP), to guarantee open, public access by Internet to the maps in the collection and make them available to users everywhere. This digital library was designed by Historical Cartography Studies Laboratory team (LECH/USP), and provides maps images on the Web, of high resolution, as well as such information on these maps as technical-scientific data (projection, scale, coordinates), printing techniques and material support that have made their circulation and cultural consumption possible. The Digital Library of Historical Cartography is accessible not only to the historical cartography researchers, but also to students and the general public. Beyond being a source of information about maps, the Digital Library of Historical Cartography seeks to be interactive, exchanging information and seeking dialogue with different branches of knowledge

Interactive application in spanish sign language for a public transport environment

[ES] En este trabajo se presenta el diseño de una herramienta multimedia que traduce a la lengua de signos españolas los mensajes de avisos que puede proporcionar un sistema de megafonía. El objetivo del trabajo es proporcionar una herramienta que mejore la inclusión social de las personas con discapacidades auditivas. Con este propósito, se han seleccionado el entorno y los mensajes de audio habituales en un aeropuerto para desarrollar este proyecto piloto. Por último, los audios se han traducido a lengua de signos españolas sintetizando un avatar usando la técnica de animación de rotoscopía a partir de la grabación en vídeo de un traductor. Los resultados finales han sido evaluados por personas sordas.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.