No description available.

A cornerstone of theoretical computer science is the Curry-Howard correspondence where formulas are types, proofs are programs, and proof normalization is computation. In this framework we introduce the atomic λμ-calculus, an interpretation of a classical deep inference proof system. It is based on two extensions of the λ-calculus, the λμ-calculus and the atomic λ-calculus. The former interprets classical logic, featuring continuation-like constructs, while the latter interprets intuitionistic deep inference, featuring explicit sharing operators. The main property of the atomic λ-calculus is reduction on individual constructors, derived from atomicity in deep inference. We thus work on open deduction, a deep inference formalism, allowing composition with connectives and with derivations, and using the medial rule to obtain atomicity. One challenge is to find a suitable formulation for deriving a computational interpretation of classical natural deduction. A second design challenge leads us to work on a variant of the λμ-calculus, the ΛμS-calculus, adding streams and dropping names. We show that our calculus has preservation of strong normalization (PSN), confluence, fully-lazy sharing, and subject reduction in the typed case. There are two challenges with PSN. First, we need to show that sharing reductions strongly normalize, underlining that only β, μ-reductions create divergence. Our proof is new and follows a graphical approach to terms close to the idea of sharing. Second, infinite reductions of the atomic calculus can appear in weakenings, creating infinite atomic paths corresponding to finite ΛμS-paths. Our solution is to separate the proof into two parts, isolating the problem of sharing from that of weakening. We first translate into anintermediate weakening calculus, which unfolds shared terms while keeping weakened ones, and preserves infinite reductions. We then design a reduction strategy preventing infinite paths from falling into weakenings.

The main focus of this PhD thesis is the study of microstructures and geometric patterns in materials, in the framework of the Calculus of Variations. My PhD research, carried out in collaboration with my supervisor Mariapia Palombaro and Marcello Ponsiglione, led to the production of three papers [21, 22, 23]. Papers [21, 22] have already been published, while [23] is currently in preparation. This thesis is divided into two main parts. In the first part we present the results obtained in [22, 23]. In these two works geometric patterns have to be understood as patterns of dislocations in crystals. The second part is devoted to [21], where suitable microgeometries are needed as a mean to produce gradients that display critical integrability properties.

Orientador: Roberto Ribeiro Baldino / Banca: Miriam Godoy Penteado / Banca: Márcia Maria Fusaro Pinto / Resumo: O presente estudo trata de uma pesquisa na área de ensino e aprendizagem de Cálculo. Foi realizado um experimento de ensino com um grupo de alunos da graduação em Física, da UNESP de Rio Claro, que estavam cursando a disciplina de Cálculo pela abordagem tradicional do conceito de limite. Durante seis encontros, tópicos de Cálculo foram trabalhados segundo a abordagem infinitesimal, com o auxílio da ferramenta zoom do software Corel Draw. As concepções espontâneas infinitesimais dos alunos foram legitimadas e, a partir delas, o estudo nessa nova abordagem foi desenvolvido. As relações entre as concepções evocadas pelos alunos e suas impressões sobre o trabalho realizado são analisadas aqui. Os alunos apresentaram um novo conhecimento que consiste em um amálgama entre os conceitos de limite e infinitésimo, indicando a superação do obstáculo infinitesimal presente nos cursos de Cálculo para alunos de Física, cujo objetivo é trabalhar com as concepções espontâneas dos alunos e com os conceitos, de modo a aplicá-los em diversas áreas do conhecimento, sem formalizá-los. / Abstract: This study is a research on learning and teaching of Calculus. A teaching experiment was realized with a group of physics students who were attending a Calculus course according to the traditional approach of limits at UNESP, Rio Claro. During six meetings, topics of Calculus were worked according to the infinitesimal approach, with the support of the Corel Draw zoom. First the students’ spontaneous conceptions on infinitesimals were legitimized and then the study in this new approach was developed. The relations between students’ evoked conceptions and their impressions about the work done in the meetings are analyzed. The students presented a new knowledge consisting in an amalgam of limit and infinitesimal number concepts, indicating the overcoming of the infinitesimal obstacle that emerges in Calculus courses for physics students, where students’ spontaneous conceptions are taken up and mathematical concepts are developed informally, aiming at their application to various areas of knowledge. / Mestre

This thesis investigates various formal systems for reasoning about partial functions or partial elements, with particular emphasis on lambda calculi for partial functions. Beeson's (intuitionistic) logic of partial terms (LPT) is taken as the basic formal system and some of its metamathematical properties are established (for later application). Three different flavours of Scott's logic of partial elements (LPE) are considered and it is shown that they are conservative extensions of LPT. This result, we argue, corroborates the choice of LPT as the basic formal system. Variants of LPT are introduced for reasoning about partial terms with a restriction operator ↾, monotonic partial functions (monLPT), lambda-terms λ_p-calculus) and λY-terms λ_pμY-calculus). The expressive powers of some (in)equational fragments are compared in LPT and its variants. Two equational formal systems are related to some of the logics above: Obtulowicz's p-equational logic is related to LPT+↾ and Plotkin's λ_v-calculus is related to one flavour of LPE. The deductive powers of LPT and its variants are compared, using various techniques (among them logical relations). The main conclusion drawn from this comparison is that there are four different lambda calculi for partial functions: intuitionistic or classical, partial or monotonic partial functions. An (in)equational presentation of the intuitionistic lambda calculus for (monotonic) partial functions is given as an extension of p-equational logic. We conjecture that there is no equational presentation of the classical λ_p-calculus. Via a special kind of diamond property, the (in)equational formal system is characterized in terms of β-reduction for partial functions and some decidability problems are solved.

No description available.

The main goal of the study was to investigate high school advanced placement calculus teachers' subject matter and pedagogical perceptions by examining the following questions: What are the teachers' perceptions of the concept of limit, the role of limits, and the teaching of limits in calculus? Additionally, the sampling technique used shed some light on the question: Are these teachers' perceptions associated with their participation in a calculus reform project focused on staff development? A multi-case study approach involving detailed examination of six teachers (three had participated in a calculus reform project and three had not participated in any calculus reform project) was used. The data collected and analyzed included questionnaires, interviews, observational fieldnotes, videotapes of classroom instruction, journals, and written instructional documents. Upon completion of the data collection and analysis, detailed teacher profiles were created with respect to the questions above. The results of this study were then generated by searching for similarities and differences across the entire sample as well as comparing and contrasting the group of project teachers and the independent teachers. The teachers in this study perceived calculus as a linearly ordered set of topics in which the concept of limit formed the backbone for appreciating and understanding all other calculus topics. The teachers felt the intuitive understanding of limits was essential to further understanding of calculus. Nevertheless, little classtime was devoted to developing an intuitive understanding. Furthermore, little emphasis was given to drawing connections between limits and subsequent calculus topics. The independent teachers devoted considerable time to discussing formal epsilon-delta definition and arguments. The complex relationship between teachers' perceptions and classroom practice appeared to be affected by the significant influence of the teachers' goals of preparing students for the advanced placement exam and college calculus and the authority given to the calculus textbook. Differences between the group of independent teachers and the group of project teachers were found related to the following factors: (a) commitment to the textbook, (b) planning, (c) use of multiple representations, (d) attitude toward graphing technology, (e) classroom atmosphere, (f) examinations, (g) appropriate level of mathematical rigor needed for teaching calculus, and (h) the stability of perceptions. These factors, however, were not fully attributed to participation in the calculus reform project. / Graduation date: 1995

Dissertation (Ph.D. in Operations Research)--Naval Postgraduate School, September 1990. / Dissertation supervisor: Bradley, Gordon H. "September 1990." Description based on title screen viewed on December 17, 2009. DTIC Descriptor(s): Mathematical models, sizes (dimensions), validation, models, programming languages, drug addiction, algebra, mathematical programming, language, junctions, calculus, homogeneity, integrated systems, mathematical logic. DTIC Identifier(s): Programming languages, mathematical models, calculus, linear programming. Author(s) subject terms: Data types, integrated modeling, linear programming, model validation, mathematical programming software, special purpose languages. Includes bibliographical references (p. 129-132). Also available in print.

Thesis (M. Phil.)--University of Hong Kong, 1973. / Typewritten.

There exist well-known varieties of implication, such as strict, intuitionist, three-valued and rigorous, which are non-classical in the sense of being more restrictive than material implication. But there exists also a type of implication, intuitively plausible, which is nonclassical not only in being more restrictive, but in satisfying certain theses which are classically false. These theses are exceedingly venerable, dating back to Aristotle and Boethius, but, despite their plausibility, have been generally rejected by logicians since. It has not been noticed, however, that in Sextus Empiricus reference is made to a species of Stoic implication which fits them perfectly. In this work formal recognition is given to this species of implication, known as connexive implication. It is shown that none of the well-known systems of prepositional logic is connexive, and a new system is accordingly constructed. A proof of consistency is given, and a number of problems posed for further investigation.