Derivación deductiva de programas funcionales con patrones

Una de las dificultades principales en el desarrollo de software es la ausencia de un marco conceptual adecuado para su estudio. Una propuesta la constituye el modelo transformativo, que entiende el desarrollo de software como un proceso iterativo de transformación de especificaciones: se parte de una especificación inicial que va transformándose sucesivamente hasta obtener una especificación final que se toma como programa. Este modelo básico puede llevarse a la práctica de varias maneras. En concreto, la aproximación deductiva toma una sentencia lógica como especificación inicial y su proceso transformador consiste en la demostración de la sentencia; como producto secundario de la demostración se deriva un programa que satisface la especificación inicial. La tesis desarrolla un método deductivo para la derivación de programas funcionales con patrones, escritos en un lenguaje similar a Hope. El método utiliza una lógica multigénero, cuya relación con el lenguaje de programación es estudiada. También se identifican los esquemas de demostración necesarios para la derivación de funciones con patrones, basados en la demostración independiente de varias subsentencias. Cada subsentencia proporciona una subespecificación de una ecuación del futuro programa a derivar. Nuestro método deductivo está inspirado en uno previo de Zohar Manna y Richard Waldinger, conocido como el cuadro deductivo, que deriva programas en un lenguaje similar a Lisp. El nuevo método es una modificación del cuadro de estos autores, que incorpora géneros y permite demostrar una especificación mediante varios cuadros. Cada cuadro demuestra una subespecificación y por tanto deriva una ecuación del programa. Se prevén mecanismos para que los programas derivados puedan contener definiciones locales con patrones y variables anónimas y sinónimas y para que las funciones auxiliares derivadas no usen variables de las funciones principales. La tesis se completa con varios ejemplos de aplicación, un mecanismo que independentiza el método del lenguaje de programación y un prototipo de entorno interactivo de derivación deductiva. Categorías y descriptores de materia CR D.l.l [Técnicas de programación]: Programación funcional; D.2.10 [Ingeniería de software]: Diseño - métodos; F.3.1 [Lógica y significado de los programas]: Especificación, verificación y razonamiento sobre programas - lógica de programas; F.3.3 [Lógica y significado de los programas]: Estudios de construcciones de programas - construcciones funcionales; esquemas de programa y de recursion; 1.2.2 [Inteligencia artificial]: Programación automática - síntesis de programas; 1.2.3 [Inteligencia artificial]: Deducción y demostración de teoremas]: extracción de respuesta/razón; inducción matemática. Términos generales Programación funcional, síntesis de programas, demostración de teoremas. Otras palabras claves y expresiones Funciones con patrones, cuadro deductivo, especificación parcial, inducción estructural, teorema de descomposición.---ABSTRACT---One of the main difficulties in software development is the lack of an adequate conceptual framework of study. The transformational model is one such proposal that conceives software development as an iterative process of specifications transformation: an initial specification is developed and successively transformed until a final specification is obtained and taken as a program. This basic model can be implemented in several ways. The deductive approach takes a logical sentence as the initial specification and its proof constitutes the transformational process; as a byproduct of the proof, a program which satisfies the initial specification is derived. In the thesis, a deductive method for the derivation of Hope-like functional programs with patterns is developed. The method uses a many-sorted logic, whose relation to the programming language is studied. Also the proof schemes necessary for the derivation of functional programs with patterns, based on the independent proof of several subsentences, are identified. Each subsentence provides a subspecification of one equation of the future program to be derived. Our deductive method is inspired on a previous one by Zohar Manna and Richard Waldinger, known as the deductive tableau, which derives Lisp-like programs. The new method incorporates sorts in the tableau and allows to prove a sentence with several tableaux. Each tableau proves a subspecification and therefore derives an equation of the program. Mechanisms are included to allow the derived programs to contain local definitions with patterns and anonymous and synonymous variables; also, the derived auxiliary functions cannot reference parameters of their main functions. The thesis is completed with several application examples, i mechanism to make the method independent from the programming language and an interactive environment prototype for deductive derivation. CR categories and subject descriptors D.l.l [Programming techniques]: Functional programming; D.2.10 [Software engineering]: Design - methodologies; F.3.1 [Logics and meanings of programa]: Specifying and verifying and reasoning about programs - logics of programs; F.3.3 [Logics and meanings of programs]: Studies of program constructs - functional constructs; program and recursion schemes; 1.2.2 [Artificial intelligence]: Automatic programming - program synthesis; 1.2.3 [Artificial intelligence]: Deduction and theorem proving - answer/reason extraction; mathematical induction. General tenas Functional programming, program synthesis, theorem proving. Additional key words and phrases Functions with patterns, deductive tableau, structural induction, partial specification, descomposition theorem.

Types of Listeria monocytogenes predicted by the positions of EcoRI cleavage sites relative to ribosomal RNA sequences.

By using taxonomic characters derived from EcoRI restriction endonuclease digestion of genomic DNA and hybridization with a labeled rRNA operon from Escherichia coli, a polymorphic structure of Listeria monocytogenes, characterized by fragments with different frequencies of occurrence, was observed. This structure was expanded by creating predicted patterns through a recursive process of observation, expectation, prediction, and assessment of completeness. This process was applied, in turn, to normalized strain patterns, fragment bands, and positions of EcoRI recognition sites relative to rRNA regions. Analysis of 1346 strains provided observed patterns, fragment sizes, and their frequencies of occurrence in the patterns. Fragment size statistics led to the creation of unobserved combinations of bands, predicted pattern types. The observed fragment bands revealed positions of EcoRI sites relative to rRNA sequences. Each EcoRI site had a frequency of occurrence, and unobserved fragment sizes were postulated on the basis of knowing the restriction site locations. The result of the recursion process applied to the components of the strain data was an extended classification with observed and predicted members.

Contemplative Education CenterStage: Training the Mindful Performer

In the late 20th century and early 21st century, contemplative education/studies courses, concentrations, and initiatives have emerged in the academy. Although there has been significant discussion of postsecondary courses and programs that have integrated contemplative views and practices in the literature, there have been few studies of contemplative curricula and pedagogy in higher education. Additionally, there have been even fewer inquiries of the influence of contemplative education on performing arts training within conservatories and college and university departments. The aim of this qualitative study was two-fold: (1) to describe, interpret, and appraise the impact of contemplative education on the curricula of an interdisciplinary conservatory level performing arts program, MFA Contemporary Performance, at Naropa University; and (2) to disclose, compare, and analyze MFA student perceptions of the influence of contemplative education on their professional and personal development. The following questions guided this study: (1) How do faculty and students characterize contemplative education within the MFA in Theater: Contemporary Performance Program? (2) How does contemplative education impact the intended and operational curricula of courses within the MFA Contemporary Performance Program? (3) How do graduate students perceive the effects of contemplative education, offered by the MFA Contemporary Performance Program, on the development of their communication abilities, presence-in-performance, sociolinguistic perspectives, and aesthetic perspectives? Based on the research methodology of educational criticism and connoisseurship, this investigation provides a vivid description and interpretation of the intended and operational curricula of three core courses within the MFA program. These curricula were examined through five dimensions: intentional, curricular, pedagogical, structural, and evaluative. In order to shape our understanding of the contemplative and performative nature of the curricula, the significant and subtle qualities of the courses were further captured by preparation, context-building, reflective, showing, and closing conventions. Since the courses were grounded in postmodern view, they were evaluated according to Doll's criteria of richness, recursion, relations, and rigor for the evaluation of postmodern curricula. MFA first- and second-year students primarily characterized contemplative education as body/mind training for performance and personal development, sitting meditation, and cultivation of mindfulness and awareness. Student perceptions of the impact of contemplative education on the development of their communication abilities, presence-in-performance, sociolinguistic perspectives, and aesthetic perspectives, throughout the course of their two-year training, are presented in a dimensional analysis. The research reveals eight different themes that intersect the three core curricula and interviews with MFA students and faculty. These thematics include inclusivity, nowness, silence, improvisation, goodness, heart, training, and space. The beginning letter of each theme combines to form the acronym, insights. The framework of insights connects and illuminates the most potent aspects of MFA Contemporary Performance values and training.

A recursively defined ordering for proving termination of term rewriting systems /

NSF MCS 77-22830."

The recursive nature of descriptions : a fixed point /

"UIUC-ENG-R-75-2539."

Perspectivas e metodologias de pesquisa da Comunicação Social no contexto da internet com o Big Data e da especialização Data Scientist

O trabalho desenvolvido analisa a Comunicação Social no contexto da internet e delineia novas metodologias de estudo para a área na filtragem de significados no âmbito científico dos fluxos de informação das redes sociais, mídias de notícias ou qualquer outro dispositivo que permita armazenamento e acesso a informação estruturada e não estruturada. No intento de uma reflexão sobre os caminhos, que estes fluxos de informação se desenvolvem e principalmente no volume produzido, o projeto dimensiona os campos de significados que tal relação se configura nas teorias e práticas de pesquisa. O objetivo geral deste trabalho é contextualizar a área da Comunicação Social dentro de uma realidade mutável e dinâmica que é o ambiente da internet e fazer paralelos perante as aplicações já sucedidas por outras áreas. Com o método de estudo de caso foram analisados três casos sob duas chaves conceituais a Web Sphere Analysis e a Web Science refletindo os sistemas de informação contrapostos no quesito discursivo e estrutural. Assim se busca observar qual ganho a Comunicação Social tem no modo de visualizar seus objetos de estudo no ambiente das internet por essas perspectivas. O resultado da pesquisa mostra que é um desafio para o pesquisador da Comunicação Social buscar novas aprendizagens, mas a retroalimentação de informação no ambiente colaborativo que a internet apresenta é um caminho fértil para pesquisa, pois a modelagem de dados ganha corpus analítico quando o conjunto de ferramentas promovido e impulsionado pela tecnologia permite isolar conteúdos e possibilita aprofundamento dos significados e suas relações.

Advanced perturbation technique for digital backward propagation in WDM systems

An improved digital backward propagation (DBP) is proposed to compensate inter-nonlinear effects and dispersion jointly in WDM systems based on an advanced perturbation technique (APT). A non-iterative weighted concept is presented to replace the iterative in analytical recursion expression, which can dramatically simplify the complexity and improve accuracy compared to the traditional perturbation technique (TPT). Furthermore, an analytical recursion expression of the output after backward propagation is obtained initially. Numerical simulations are executed for various parameters of the transmission system. The results indicate that the advanced perturbation technique will relax the step size requirements and reduce the oversampling factor when launch power is higher than -2 dBm. We estimate this technique will reduce computational complexity by a factor of around seven with respect to the conventional DBP. © 2013 Optical Society of America.

On the Transformations of Symplectic Expansions and the Respective Bäcklund Transformation for the KDV Equation

2000 Mathematics Subject Classification: Primary: 34B40; secondary: 35Q51, 35Q53

Въвеждане на рекурсията чрез абстракция и редици от задачи

Pavel Azalov - Recursion is a powerful technique for producing simple algorithms. It is a main topics in almost every introductory programming course. However, educators often refer to difficulties in learning recursion, and suggest methods for teaching recursion. This paper offers a possible solutions to the problem by (1) expressing the recursive definitions through base operations, which have been predefined as a set of base functions and (2) practising recursion by solving sequences of problems. The base operations are specific for each sequence of problems, resulting in a smooth transitions from recursive definitions to recursive functions. Base functions hide the particularities of the concrete programming language and allows the students to focus solely on the formulation of recursive definitions.

Mixed Negative Binomial Distribution by Weighted Gamma Mixing Distribution

Павел Т. Стойнов - В тази работа се разглежда отрицателно биномното разпределение, известно още като разпределение на Пойа. Предполагаме, че смесващото разпределение е претеглено гама разпределение. Изведени са вероятностите в някои частни случаи. Дадени са рекурентните формули на Панжер.

On the Poisson Process of Order k Space

2010 Mathematics Subject Classification: 60E05, 62P05.

An innovative approach to teaching structural induction for computer science

Proofs by induction are central to many computer science areas such as data structures, theory of computation, programming languages, program efficiency-time complexity, and program correctness. Proofs by induction can also improve students’ understanding and performance of computer science concepts such as programming languages, algorithm design, and recursion, as well as serve as a medium for teaching them. Even though students are exposed to proofs by induction in many courses of their curricula, they still have difficulties understanding and performing them. This impacts the whole course of their studies, since proofs by induction are omnipresent in computer science. Specifically, students do not gain conceptual understanding of induction early in the curriculum and as a result, they have difficulties applying it to more advanced areas later on in their studies. The goal of my dissertation is twofold: (1) identifying sources of computer science students’ difficulties with proofs by induction, and (2) developing a new approach to teaching proofs by induction by way of an interactive and multimodal electronic book (e-book). For the first goal, I undertook a study to identify possible sources of computer science students’ difficulties with proofs by induction. Its results suggest that there is a close correlation between students’ understanding of inductive definitions and their understanding and performance of proofs by induction. For designing and developing my e-book, I took into consideration the results of my study, as well as the drawbacks of the current methodologies of teaching proofs by induction for computer science. I designed my e-book to be used as a standalone and complete educational environment. I also conducted a study on the effectiveness of my e-book in the classroom. The results of my study suggest that, unlike the current methodologies of teaching proofs by induction for computer science, my e-book helped students overcome many of their difficulties and gain conceptual understanding of proofs induction.

An Innovative Approach to Teaching Structural Induction for Computer Science

Proofs by induction are central to many computer science areas such as data structures, theory of computation, programming languages, program efficiency-time complexity, and program correctness. Proofs by induction can also improve students’ understanding of and performance with computer science concepts such as programming languages, algorithm design, and recursion, as well as serve as a medium for teaching them. Even though students are exposed to proofs by induction in many courses of their curricula, they still have difficulties understanding and performing them. This impacts the whole course of their studies, since proofs by induction are omnipresent in computer science. Specifically, students do not gain conceptual understanding of induction early in the curriculum and as a result, they have difficulties applying it to more advanced areas later on in their studies. The goal of my dissertation is twofold: 1. identifying sources of computer science students’ difficulties with proofs by induction, and 2. developing a new approach to teaching proofs by induction by way of an interactive and multimodal electronic book (e-book). For the first goal, I undertook a study to identify possible sources of computer science students’ difficulties with proofs by induction. Its results suggest that there is a close correlation between students’ understanding of inductive definitions and their understanding and performance of proofs by induction. For designing and developing my e-book, I took into consideration the results of my study, as well as the drawbacks of the current methodologies of teaching proofs by induction for computer science. I designed my e-book to be used as a standalone and complete educational environment. I also conducted a study on the effectiveness of my e-book in the classroom. The results of my study suggest that, unlike the current methodologies of teaching proofs by induction for computer science, my e-book helped students overcome many of their difficulties and gain conceptual understanding of proofs induction.

Conteúdos de matemática do ensino médio com abordagem de raciocínio recursivo e questões do ENEM e OBMEP

In this work, we have the purpose of reminding the math teacher of High School the recursive process so that he/she can use this tool to introduce contents, using recursion as an alternative to the teaching of mathematics. For this, we used questions taken from the Exame Nacional do Ensino M´edio (ENEM) [National Examination of High School] and from the Olimp´ıada Brasileira de Matem´atica das Escolas P´ublicas (OBMEP) [Brazilian Mathematics Olympiad of Public Schools], in addition to present some contents of mathematics that are defined by recursion. In this dissertation, we also showed some activities that involved the recursive reasoning and were applied in a 3rd grade class of high school in a public school in Natal / RN.

The stochastic geometric machine model

This paper introduces the stochastic version of the Geometric Machine Model for the modelling of sequential, alternative, parallel (synchronous) and nondeterministic computations with stochastic numbers stored in a (possibly infinite) shared memory. The programming language L(D! 1), induced by the Coherence Space of Processes D! 1, can be applied to sequential and parallel products in order to provide recursive definitions for such processes, together with a domain-theoretic semantics of the Stochastic Arithmetic. We analyze both the spacial (ordinal) recursion, related to spacial modelling of the stochastic memory, and the temporal (structural) recursion, given by the inclusion relation modelling partial objects in the ordered structure of process construction.