Extraction of structured programs from specification proofs

We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.

Rawls and Health Care

John Rawls’s A Theory of Justice (1971), his first major work articulating his theory of justice as fairness, was immediately recognized as a fundamental contribution to political philosophy in the twentieth century. Working within the tradition established by previous philosophers such as Kant and Locke, Rawls employed the contract theory approach. Taking it to a higher order of abstraction, he sought to determine not what the structure of social organization would be, but what the principles which governed social institutions would be under a hypothetical contracting situation. Rawls uses this contract theory approach to construct a society in which the morally irrelevant contingencies of nature and social arrangements are mitigated by principles of justice which govern the basic institutions of society. A common observation has been that Rawls left out any discussion of health care and how it might fit into his conception of a just society. Several philosophers have articulated expansions of the theory to account for health care. In the chapters that follow I will continue this tradition and consider how justice as fairness might be expanded to account for just health care allocation. In doing so, I hope to answer a particularly strong critique of the theory brought up by Amartya Sen and Martha Nussbaum, and to argue for a broadened conception of health care which takes into account the complex causal relationship between society and human health.

Divisia indexes, money and welfare

We suggest the use of a particular Divisia index for measuring welfare losses due to interest rate wedges and in‡ation. Compared to the existing options in the literature: i) when the demands for the monetary assets are known, closed-form solutions for the welfare measures can be obtained at a relatively lower algebraic cost; ii) less demanding integrability conditions allow for the recovery of welfare measures from a larger class of demand systems and; iii) when the demand speci…cations are not known, using an index number entitles the researcher to rank di¤erent vectors of opportunity costs directly from market observations. We use two examples to illustrate the method.

Trabalho móvel: em trânsito por aeroportos e aviões

Argumenta-se na contemporaneidade que o trabalho adquiriu a possibilidade de ser realizado “a qualquer hora e em qualquer lugar” e que, particularmente, pode ser realizado em movimento, enquanto a pessoa que trabalha desloca-se de um lugar a outro. Este estudo investiga esse último, o trabalho móvel; em especial, aquele que envolve o uso de tecnologias de informação e comunicação e realizado enquanto a pessoa que trabalha desloca-se por meio do sistema de transporte aéreo. Este projeto explora, especificamente, o desempenho de espaço-tempos de trabalho em terminais de aeroportos e em aviões. Para tanto, adota a abordagem teórico-metodológica Teoria Ator-Rede que considera o social um movimento de associações entre elementos heterogêneos e os espaço-tempos, incluindo aqueles de trabalho, efeitos de modos como humanos e não humanos relacionam-se entre si. A estratégia metodológica envolveu uma combinação de observação de campo, auto-observação e entrevistas com pessoas que vivem a experiência do trabalho móvel. A coleta de dados compreendeu: (a) horas de observação de pessoas e situações, em alguns terminais de aeroportos no Brasil e em voos entre a cidade de São Paulo e outras capitais do país, e (b) entrevistas semiestruturadas com pessoas que, com certa frequência, deslocam-se para trabalhar por meio do sistema de transporte aéreo. Como resultado, este estudo contribui para as análises sobre o fenômeno do trabalho móvel, realizado em aeroportos e aviões, e destaca: os atores envolvidos, bem como os agentes que levam esses atores a agir; a quantidade de objetos ativos na manifestação do fenômeno; e as controvérsias envolvidas com o tema. Além disso, aponta elementos empíricos (i) que revelam lugares em que os fenômenos de trabalho móvel se manifestam esporadicamente, de modo disperso, como “bolhas”, e (ii) que se contrapõem à ideia que é possível trabalhar “a qualquer hora e em qualquer lugar”. As contribuições deste estudo ecoam resultados de pesquisas desenvolvidas sobre trabalho móvel, assim como apresentam particularidades, como a metáfora da bolha, amplificações de aspectos pouco presentes nos textos sobre o tema e elementos peculiares do trabalho móvel investigado no espaço-tempo da pesquisa

Sustainable silvopastoral systems: theory and a practical case

Muitas transformações são esperadas por causa das mudanças do clima, especialmente das atividades agrícolas realizadas nos trópicos. Esta tese centra-se em dois aspectos. O primeiro deles é o de reunir o conhecimento de sistemas silvipastoris; este ponto de vista estabelece a importância de solos tropicais e sua gestão adequada de acordo com as normas ambientais e sustentáveis. A segunda parte da tese é a aplicação desses princípios em um caso específico: a fazenda "El Paraíso". O objetivo central ou problema a resolver da segunda parte é propor um projeto para melhorar as atividades de produção de carne e, ao mesmo tempo, ajudar a preservar e melhorar o meio ambiente e especialmente os ecossistemas tropicais. A metodologia utilizada na tese foi buscar e analisar informações sobre o assunto. Depois disso, a investigação experimental e de campo foi realizada para levantar o projeto que combinaria as duas partes da obra. No final, com a informação recolhida uma proposta de projeto foi feita. O objetivo era propor a transformação dos processos de produção na fazenda selecionada. Logo de desenvolver e apresentar o projeto, foram analisadas as possibilidades de implementação do projeto. A conclusão do estudo foi o de apresentar e discutir três cenários possíveis após a implementação. Finalmente, a conclusão geral apresenta as realizações, as oportunidades e possíveis expansões futuras do projeto.

On the construction of explicit exponential based schemes for Stiff SDEs

Trabalho apresentado Numerical Solution of Differential and Differential-Algebraic Equations (NUMDIFF-14), Halle, 7-11 Sep 2015

Phylogenetic structure of Guinea-Bissau ethnic groups for mitochondrial DNA and Y chromosome genetic systems

The maternal and paternal genetic profile of Guineans is markedly sub-Saharan West African, with the majority of lineages belonging to L0-L3 mtDNA sub-clusters and E3a-M2 and E1-M33 Y chromosome haplogroups. Despite the sociocultural differences among Guinea-Bissau ethnic groups,marked by the supposedly strict admixture barriers, their genetic pool remains largely common. Their extant variation coalesces at distinct timeframes, from the initial occupation of the area to later inputs of people. Signs of recent expansion in mtDNA haplogroups L2a-L2c and NRY E3a-M2 suggest population growth in the equatorial western fringe, possibly supported by an early local agricultural centre, and to which the Mandenka and the Balanta people may relate. Non-West African signatures are traceable in less frequent extant haplogroups, fitting well with the linguistic and historical evidence regarding particular ethnic groups: the Papel and Felupe-Djola people retain traces of their putative East African relatives; U6 and M1b among Guinea-Bissau Bak-speakers indicate partial diffusion to Sahel of North African lineages; U5b1b lineages in Fulbe and Papel represent a link to North African Berbers, emphasizing the great importance of post-glacial expansions; exact matches of R1b-P25 and E3b1-M78 with Europeans likely trace back to the times of the slave trade.

Sheaves, local homeomorphisms and local sets as Hilbert locale modules

We give a thorough account of the various equivalent notions for \sheaf" on a locale, namely the separated and complete presheaves, the local home- omorphisms, and the local sets, and to provide a new approach based on quantale modules whereby we see that sheaves can be identi¯ed with certain Hilbert modules in the sense of Paseka. This formulation provides us with an interesting category that has immediate meaningful relations to those of sheaves, local homeomorphisms and local sets. The concept of B-set (local set over the locale B) present in [3] is seen as a simetric idempotent matrix with entries on B, and a map of B-sets as de¯ned in [8] is shown to be also a matrix satisfying some conditions. This gives us useful tools that permit the algebraic manipulation of B-sets. The main result is to show that the existing notions of \sheaf" on a locale B are also equivalent to a new concept what we call a Hilbert module with an Hilbert base. These modules are the projective modules since they are the image of a free module by a idempotent automorphism On the ¯rst chapter, we recall some well known results about partially ordered sets and lattices. On chapter two we introduce the category of Sup-lattices, and the cate- gory of locales, Loc. We describe the adjunction between this category and the category Top of topological spaces whose restriction to spacial locales give us a duality between this category and the category of sober spaces. We ¯nish this chapter with the de¯nitions of module over a quantale and Hilbert Module. Chapter three concerns with various equivalent notions namely: sheaves of sets, local homeomorphisms and local sets (projection matrices with entries on a locale). We ¯nish giving a direct algebraic proof that each local set is isomorphic to a complete local set, whose rows correspond to the singletons. On chapter four we de¯ne B-locale, study open maps and local homeo- morphims. The main new result is on the ¯fth chapter where we de¯ne the Hilbert modules and Hilbert modules with an Hilbert and show this latter concept is equivalent to the previous notions of sheaf over a locale.

Análise do comportamento reológico de pastas de cimento contendo resíduos de pneu para poços de petróleo

The low tenacity presented by the Portland cement pastes used in the oil wells cementation has been motivating several researches with attention focused on alternative materials. Additives have been developed to generate flexible pastes with mechanical resistance capable to support the expansions and retractions of the metallic covering of the wells that submit to the steam injection, technique very used to increase the recovery factor in oil reservoirs with high viscosity. A fresh paste with inadequate rheological behavior may commit the cementation process seriously, involving flaws that affect the performance of the paste substantially in the hardened state. This work proposes the elaboration and the rheological analysis of Portland cement pastes with addition of residues of rubber tire in several proportions, with the aim of minimizing the damages provoked in the hem cementing of these wells. By thermogravimetric analysis, the particles of eraser that go by the sieve of 0,5mm (35 mesh) opening and treated superficially with NaOH solution of 1 mol/L presented appropriate thermal resistance for wells that submit to thermal cyclic. The evaluation of the study based on the results of the rheological analysis of the pastes, complemented by the mechanical analysis, thickening, stability, tenor of free water and filtrate loss, being used as parameter a paste reference, without rubber addition. The results showed satisfactory rheology, passive of few corrections; considerable loss of mechanical resistance (traction and compression), compensated by earnings of tenacity, however with established limits for its application in oil wells; satisfactory stability, free water and thickening time

Simulação de fluxo de fluidos em meios porosos desordenados uma análise de efeito de escala na estimativa da permeabilidade e do coeficiente de arrasto

The present study provides a methodology that gives a predictive character the computer simulations based on detailed models of the geometry of a porous medium. We using the software FLUENT to investigate the flow of a viscous Newtonian fluid through a random fractal medium which simplifies a two-dimensional disordered porous medium representing a petroleum reservoir. This fractal model is formed by obstacles of various sizes, whose size distribution function follows a power law where exponent is defined as the fractal dimension of fractionation Dff of the model characterizing the process of fragmentation these obstacles. They are randomly disposed in a rectangular channel. The modeling process incorporates modern concepts, scaling laws, to analyze the influence of heterogeneity found in the fields of the porosity and of the permeability in such a way as to characterize the medium in terms of their fractal properties. This procedure allows numerically analyze the measurements of permeability k and the drag coefficient Cd proposed relationships, like power law, for these properties on various modeling schemes. The purpose of this research is to study the variability provided by these heterogeneities where the velocity field and other details of viscous fluid dynamics are obtained by solving numerically the continuity and Navier-Stokes equations at pore level and observe how the fractal dimension of fractionation of the model can affect their hydrodynamic properties. This study were considered two classes of models, models with constant porosity, MPC, and models with varying porosity, MPV. The results have allowed us to find numerical relationship between the permeability, drag coefficient and the fractal dimension of fractionation of the medium. Based on these numerical results we have proposed scaling relations and algebraic expressions involving the relevant parameters of the phenomenon. In this study analytical equations were determined for Dff depending on the geometrical parameters of the models. We also found a relation between the permeability and the drag coefficient which is inversely proportional to one another. As for the difference in behavior it is most striking in the classes of models MPV. That is, the fact that the porosity vary in these models is an additional factor that plays a significant role in flow analysis. Finally, the results proved satisfactory and consistent, which demonstrates the effectiveness of the referred methodology for all applications analyzed in this study.

Morfo-anatomia de plântulas e número cromossômico de Cybistax antisyphilitica (Mart.) Mart. (Bignoniaceae)

Plântulas de Cybistax antisyphilitica (ipê-verde), espécie arbórea que ocorre no Estado de São Paulo, Brasil, foram estudadas morfoanatomicamente e citogeneticamente. As plântulas são eudicotiledôneas, fanerocotiledonares e epigéias. Suas sementes apresentam alas hialinas, assimétricas e de textura papirácea. A raiz é axial com tecido epidérmico irregular. O hipocótilo é verde, glabro e apresenta os elementos do xilema em diferenciação. Os cotilédones são verdes, foliáceos, reniformes, com mesofilo heterogêneo, epiderme pilosa e feixes vasculares colaterais. Os eófilos são glabros, peciolados, de filotaxia oposta, dorsiventrais, hipoestomáticos e possuem mesofilo heterogêneo e assimétrico. Não há diferenças anatômicas significativas entre os eófilos e os metáfilos. O sistema vascular do pecíolo dos metáfilos dispõe-se em forma de ferradura. A espécie apresenta número cromossômico mitótico 2n = 40 com comprimento cromossômico geral médio de 1,042 µm ± 0,140 e amplitude variando de 0,58 µm até 1,60 µm.

Uma análise histórico-epistemológica do conceito de grupo

This work aims to analyze the historical and epistemological development of the Group concept related to the theory on advanced mathematical thinking proposed by Dreyfus (1991). Thus it presents pedagogical resources that enable learning and teaching of algebraic structures as well as propose greater meaning of this concept in mathematical graduation programs. This study also proposes an answer to the following question: in what way a teaching approach that is centered in the Theory of Numbers and Theory of Equations is a model for the teaching of the concept of Group? To answer this question a historical reconstruction of the development of this concept is done on relating Lagrange to Cayley. This is done considering Foucault s (2007) knowledge archeology proposal theoretically reinforced by Dreyfus (1991). An exploratory research was performed in Mathematic graduation courses in Universidade Federal do Pará (UFPA) and Universidade Federal do Rio Grande do Norte (UFRN). The research aimed to evaluate the formation of concept images of the students in two algebra courses based on a traditional teaching model. Another experience was realized in algebra at UFPA and it involved historical components (MENDES, 2001a; 2001b; 2006b), the development of multiple representations (DREYFUS, 1991) as well as the formation of concept images (VINNER, 1991). The efficiency of this approach related to the extent of learning was evaluated, aiming to acknowledge the conceptual image established in student s minds. At the end, a classification based on Dreyfus (1991) was done relating the historical periods of the historical and epistemological development of group concepts in the process of representation, generalization, synthesis, and abstraction, proposed here for the teaching of algebra in Mathematics graduation course

Obstáculos superados pelos matemáticos no passado e vivenciados pelos alunos na atualidade : a polêmica multiplicação de números inteiros

In Mathematics literature some records highlight the difficulties encountered in the teaching-learning process of integers. In the past, and for a long time, many mathematicians have experienced and overcome such difficulties, which become epistemological obstacles imposed on the students and teachers nowadays. The present work comprises the results of a research conducted in the city of Natal, Brazil, in the first half of 2010, at a state school and at a federal university. It involved a total of 45 students: 20 middle high, 9 high school and 16 university students. The central aim of this study was to identify, on the one hand, which approach used for the justification of the multiplication between integers is better understood by the students and, on the other hand, the elements present in the justifications which contribute to surmount the epistemological obstacles in the processes of teaching and learning of integers. To that end, we tried to detect to which extent the epistemological obstacles faced by the students in the learning of integers get closer to the difficulties experienced by mathematicians throughout human history. Given the nature of our object of study, we have based the theoretical foundation of our research on works related to the daily life of Mathematics teaching, as well as on theorists who analyze the process of knowledge building. We conceived two research tools with the purpose of apprehending the following information about our subjects: school life; the diagnosis on the knowledge of integers and their operations, particularly the multiplication of two negative integers; the understanding of four different justifications, as elaborated by mathematicians, for the rule of signs in multiplication. Regarding the types of approach used to explain the rule of signs arithmetic, geometric, algebraic and axiomatic , we have identified in the fieldwork that, when multiplying two negative numbers, the students could better understand the arithmetic approach. Our findings indicate that the approach of the rule of signs which is considered by the majority of students to be the easiest one can be used to help understand the notion of unification of the number line, an obstacle widely known nowadays in the process of teaching-learning

Um estudo sobre a aprendizagem de alguns conceitos algébricos e geométricos

The objective of the present work was develop a study about the writing and the algebraic manipulation of symbolical expressions for perimeter and area of some convex polygons, approaching the properties of the operations and equality, extending to the obtaining of the formulas of length and area of the circle, this one starting on the formula of the perimeter and area of the regular hexagon. To do so, a module with teaching activities was elaborated based on constructive teaching. The study consisted of a methodological intervention, done by the researcher, and had as subjects students of the 8th grade of the State School Desembargador Floriano Cavalcanti, located on the city of Natal, Rio Grande do Norte. The methodological intervention was done in three stages: applying of a initial diagnostic evaluation, developing of the teaching module, and applying of the final evaluation based on the Mathematics teaching using Constructivist references. The data collected in the evaluations was presented as descriptive statistics. The results of the final diagnostic evaluation were analyzed in the qualitative point of view, using the criteria established by Richard Skemp s second theory about the comprehension of mathematical concepts. The general results about the data from the evaluations and the applying of the teaching module showed a qualitative difference in the learning of the students who participated of the intervention