We devise imperative programming languages for verified real number computation where real numbers are provided as abstract data types such that the users of the languages can express real number computation by considering real numbers as abstract mathematical entities. Unlike other common approaches toward real number computation, based on an algebraic model that lacks implementability or transcendental computation, or finite-precision approximation such as using double precision computation that lacks a formal foundation, our languages are devised based (...) on computable analysis, a foundation of rigorous computation over continuous data. Consequently, the users of the language can easily program real number computation and reason about the behaviours of their programs, relying on their mathematical knowledge of real numbers without worrying about artificial roundoff errors. As the languages are imperative, we adopt precondition–postcondition-style program specification and Hoare-style program verification methodologies. Consequently, the users of the language can easily program a computation over real numbers, specify the expected behaviour of the program, including termination, and prove the correctness of the specification. Furthermore, we suggest extending the languages with other interesting continuous data, such as matrices, continuous real functions, et cetera.Abstract taken directly from the thesis.E-mail: [email protected]: https://sewonpark.com/thesis. (shrink)

In this paper we specialize the notion of abstract computational procedure previously introduced for intensionally presented structures to those which are extensionally given. This is provided by a form of generalized recursion theory which uses schemata for explicit definition, conditional definition and least fixed point recursion in functional of type level 2 over any appropriate structure. It is applied here to the case of potentially infinite streams as an abstract data type.

As we move our social institutions from paper and ink based operations to the electronic medium, we invisibly create a type of surveillance society, a panopticon society. It is not the traditional surveillance society in which government officials follow citizens around because they are concerned about threats to the political order. Instead it is piecemeal surveillance by public and private organizations. Piecemeal though it is, It creates the potential for the old kind of surveillance on an even grander scale. The (...) panopticon is the prison environment described by Foucault in which prison cells are arranged in a large circle with the side facing the inside of the circle open to view. The guard tower is placed in the middle of the circle so that guards can see everything that goes on in every cell. When we contemplate all the electronic data that is now gathered about each of us as we move through our everyday lives --- intelligent highway systems, consumer transactions, traffic patterns on the internet, medical records, financial records, and so on --- there seems little doubt that we are moving into a panopticon. The social issues that arise from this are too numerous to detail here, but data retention is an important part of it. In the paper-and-ink world, documents are filed, files are boxed, boxes are put away or thrown away. The capacity for data retrieval and manipulation is, thereby, limited by the sheer difficulty and cost of storing, finding, searching, and manipulating large numbers of paper files. This inconvenience functions as a mechanism whereby the system forgets past information, not unlike the way we ourselves forget. However, the story is very different in the digital world; digital information is easy to store, easy to search and manipulate, and inexpensive to keep over extensive periods of time. Digitalized information systems tend, therefore, to collect extensive ancillary information and to retain this information indefinitely. Such lack of forgetfulness is likely to hamper the ability of individuals to shed their past, and start over with a clean slate. Concerns about data retention were expressed in the early literature on the social impact of computing, but for the most part the issue has dropped from sight. Rarely, has the social good of discarding accumulated personal data been addressed. In this paper, we want to make the case by examining diverse cases in which retention of information by either business or governmental institutions hinders the ability of individuals to start over or to act autonomously. We hope our argument for the good of forgetfulness will challenge the standard framework in which such issues have traditionally been debated. The privacy debate exemplifies the traditional framework insofar as it has been characterized as involving an inherent tension between, on the one hand, the needs of organizations and institutions for more accurate and efficient information systems so as to further their goals and, on the other hand, the desire of individuals to have information about them kept private. Regan argues against this framing of the privacy issue in favor of one that recognizes the social importance of personal privacy. We will examine the non-forgetfulness of information systems as a problem threatening not just individual interests but social good as well. Cryptography is often cited as the technology that will give us privacy and mediate against surveillance. One of the uses of cryptography, encryption, will allow us, some hope, to create confidentiality and relationships of trust that will facilitate many of the social arrangements we now have and perhaps make them even more secure than they are now. Electronic cash, for example, could be created in such a form that it would have the anonymity associated now with hard cash Others are less optimistic of the potential for cryptography to re-create relationships of trust in the new medium. One important point that already seems clear is that even if encryption technology will protect the confidentiality and integrity of electronic transactions and data, it will NOT stop the observation of traffic patterns on networks. This seems an important distinction to put on the table. Our patterns of communication will continue to be available, no matter what is encrypted, and an amazing amount of information can be gleaned from this data. In a sense, it means content integrity but no anonymity. This will indubitably impact how we interact and with whom we interact. (shrink)

Modern computing is generally taken to consist primarily of symbol manipulation. But symbols are abstract, and computers are physical. How can a physical device manipulate abstract symbols? Neither Church nor Turing considered this question. My answer is that the bit, as a hardware-implemented abstract data type, serves as a bridge between materiality and abstraction. Computing also relies on three other primitive—but more straightforward—abstractions: Sequentiality, State, and Transition. These physically-implemented abstractions define the borderline between hardware and software (...) and between physicality and abstraction. At a deeper level, asking how a physical device can interact with abstract symbols is the wrong question. The relationship between symbols and physical devices begins with the realization that human beings already know what it means to manipulate symbols. We build and program computers to do what we understand to be symbol manipulation. To understand what that means, consider a light switch. A light switch doesn’t turn a light on or off. Those are abstractions. Light switches don’t operate with abstractions. We build light switches, so that when flipped, the world is changed in such a way that we understand the light to be on or off. Similarly, we build computers to perform operations that we understand as manipulating symbols. (shrink)

Abstract: Tomatoes are part of the major crops in food security. Tomatoes are plants grown in temperate and hot regions of South American origin from Peru, and then spread to most countries of the world. Tomatoes contain a lot of vitamin C and mineral salts, and are recommended for people with constipation, diabetes and patients with heart and body diseases. Studies and scientific studies have proven the importance of eating tomato juice in reducing the activity of platelets in diabetics, (...) which helps in protecting them from developing deadly blood clots. A tomato classification approach is presented with a data set containing approximately 5,266 images with 7 species belonging to tomatoes. The Neural Network Algorithms (CNN), a deep learning technique applied widely in image recognition, is used for this task. (shrink)

Abstract:We analyzed data from a survey of employees of a large military base in order to assess possible differences in the whistle-blowing process due to type of wrongdoing observed. Employees who observed perceived wrongdoing involving mismanagement, sexual harassment, or unspecified legal violations were significantly more likely to report it than were employees who observed stealing, waste, safety problems, or discrimination. Further, type of wrongdoing was significantly related to reasons given by employees who observed wrongdoing but did not report (...) it, across all forms of wrongdoing. However, the primary reason that observers did not report it was that they thought nothing could be done to rectify the situation. Finally, type of wrongdoing was significantly related to the cost of the wrongdoing, the quality of the evidence about the wrongdoing, and the comprehensiveness of retaliation against the whistle-blower. These findings suggest that type of wrongdoing makes a difference in the whistle-blowing process, and it should be examined in future research. (shrink)

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...) (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

Body part terms (BPTs) are used extensively in Mesoamerican languages to name object parts. The process through which BPTs might be extended to refer to a part of an object and further serve as a relator in describing the relation between objects in space has often been attributed to metaphorical processes. This study proposes an alternative analysis following a Structure–Mapping Theory approach (Gentner, 1983, inter alia), based on data from Diidxazá (Isthmus Zapotec, Otomanguean) obtained through elicitation and experimental tasks. (...) The data show that structure mapping does not depend on a 1:1 match of attributes; frequency of use shed light on principles that constrain the semantic extension of most BPTs; a core set of six BPTs are extended by abstraction of the set of intersecting axes of the body. The detailed nature of this study enables an analysis of the mental representations underlying the semantic extension of BPTs. This in turn elucidates on aspects of the relation between spatial language and spatial cognition. In addition, this study allows us to address questions about the categorial status of BPTs in Diidxazá and their lexicographic representation. (shrink)

ABSTRACT Thematic analysis is the most widely used method for analysing qualitative data. Recent debates, highlighting the binary distinctions between reflexive TA grounded within the qualitative paradigm and codebook TA with neo-positivist orientations, have emphasized the existence of numerous tensions that researchers must navigate to produce coherent and rigorous research. This article attempts to resolve some of these tensions through developing an approach to TA underpinned by realist philosophy of science. Focusing on interview data, we propose the (...) use of three types of themes and the use of corresponding validity indicators. Using an illustrative example, we outline the conceptual foundations of a realist approach to TA and present recommendations for conducting it in practice. This approach, we claim, reconciles several existing binaries between distinctive types of TA by incorporating the contributions of both for the development of different types of themes. (shrink)

DP hypothesis of Abney (1987), the syntactic unit that had formerly been known as noun phrase should in fact be analyzed as a phrase headed by a determiner, hence the label DP. Quite independently of this syntactic development, Partee (1987) proposed a type shifting paradigm for the semantic analysis of nominals (now called DPs). In Partee's proposal DPs are ambiguous between a referential reading of type e, a predicative reading of type et and a quantificational reading of type (et)t. DP (...) meanings can flexibly move between their different readings due to covert application of semantic operators. The present paper proposes some strong relationships between these syntactic and semantic paradigms. It is argued that the structure of the DP affects its semantics in that the NP level within the DP is purely predicative and the DP level itself is purely quantificational. However, the intermediate D' level is flexible between the predicate/quantifier semantic categories, due to the covert application of semantic operators at this level. Partee's assumption, adopted from Discourse Representation Theory and more traditional approaches in philosophical logic, that some DPs need to have a (discourse) referential reading, is withdrawn. Instead of Partee's type shifting operators between the three semantic categories she assumes, two operators are used between predicates and quantifiers. The choice function operation of Reinhart (1997) and Winter (1997) is used as a general operator from predicates to quantifiers. The minimum operator of Winter (1996) is used as a general operator from quantifiers to predicates. These two operations, referred to as category shifting operators , account for most of the Partee data and substantially extend the theory of flexibility to treat some intricate phenomena in the domains of coordination, plurality and scope. (shrink)

BackgroundImportant sex and gender differences have been found in research on diabetes complications and treatment. Reporting on whether and how sex and gender impact research findings is crucial for developing tailored diabetes care strategies. To analyze the extent to which this information is available in current diabetes research, we examined original investigations on diabetes for the integration of sex and gender in study reporting.MethodsWe examined original investigations on diabetes published between January 1 and December 31, 2015, in the top five (...) general medicine journals and top five diabetes-specific journals (by 2015 impact factor). Data were extracted on sex and gender integration across seven article sections: title, abstract, introduction, methods, results, discussion, and limitations.ResultsWe identified 155 original investigations on diabetes, including 115 randomized controlled trials (RCTs) and 40 observational studies. Sex and gender were rarely incorporated in article titles, abstracts and introductions. Most methods sections did not describe plans for sex/gender analyses; 47 (30.3%) articles described plans to control for sex/gender in the analysis and 12 (7.7%) described plans to stratify results by sex/gender. While most articles (151, 97.4%) reported the sex/gender of study participants, only 10 (6.5%) of all articles reported all study outcomes separately by sex/gender. Discussion of sex-related issues was incorporated into 21 (13.5%) original investigations; however, just 1 (0.6%) discussed gender-related issues. Comparison by journal type (general medicine vs. diabetes specific) yielded only minor differences from the overall integration results. In contrast, RCTs performed more poorly on multiple sex/gender assessment metrics compared to observational studies.ConclusionsSex and gender are poorly integrated in current diabetes original investigations, suggesting that substantial improvements in sex and gender data reporting are needed to inform the evidence to support sex- and gender-specific diabetes care. (shrink)

Languages are complex systems that allow speakers to produce novel grammatical utterances. Yet, linguists differ as to how general and abstract they think the mental representation of speakers have to be to give rise to this grammatical creativity. In order to shed light on these questions, the present study looks at one specific construction type, English comparative correlatives, that turns out to be particularly interesting in this context: on the one hand it has been described in terms of one (...) of the most abstract and general syntactic rules, on the other hand it shows specific idiomatic structures that are often produced without any variation. While the syntax and semantics of the English Comparative Correlative construction have received considerable attention in the literature, so far only a small number of usage-based analyses have been published on the topic. These either only relied on small databases or focussed only on the productivity of one slot in the construction. In contrast to this, the present study analyses more than 1,400 CC tokens sampled from COCA. The results of the present study yield important results concerning English CC constructions, including the schematicity and generality of their mental representations. (shrink)

There is a widespread assumption in Construction Grammar that the meanings of verbs correlate with or even determine their complementation forms and patterns. There is much less research on noun complementation, however, although this category is even more interesting for a number of reasons such as the potential for valency reduction, nominal topicalization constructions, and additional complementation options, e.g.of-PPs and existential constructions.In this paper we focus on the class of nouns reporting commissive illocutionary acts, and address the question of whether (...) there is a correlation between the meaning of these nouns and their preferred complementation patterns, and between their semantic similarity and their similarity in the distribution of complementation patterns.We report the results of a study of a set of 17 commissive nouns chosen from a wider collection of illocutionary nouns. Two types of analysis were carried out in order to compare the semantic and grammatical characteristics of these nouns. The semantic analysis was based on insights from speech act theory and the philosophy of language. We developed a framework for a systematic comparative description of the nouns in our word field. The results were tallied with a corpus-based grammatical analysis. Two hundred tokens of each noun type were randomly sampled from the Corpus of Contemporary American English. Using these data, the 17 nouns were subjected to an analysis of the relative frequencies of their complementation patterns.Results indicate a general match between noun meanings and complementation patterns. More specifically, however, they indicate that the closeness of this match depends on the prototypicality of nouns as members of the class of commissives.The study, then, contributes to our understanding of the relation between lexis and syntax. At the same time, it confirms the need for a close semantic analysis to account for the great extent to which item-specific information, i.e. properties of individual nouns, have to be taken into consideration at the expense of large-scale generalizations. (shrink)

The nature of universals became an explicit problem for Western philosophy with Socrates. From the Milesians on, the search for a fundamental substance underlying and connecting all phenomena implied the conception; but it was not until Socrates disentangled the question of universality from that of reality in his theory of definitions that it emerged as the traditional problem we know, and one even capable of solution. In so doing, Socrates may be called the founder of a type of inquiry at (...) once abstract and yet specific which we characterize as “phenomenological”. But Plato, coming immediately after him, again muddied the waters by re-introducing the notion of reality in the Ideas before philosophers had a chance to profit by the separation of the two difficulties. In this manner the composite problem was passed on to Aristotle, who, though he differed in his conception of the nature of the reality, nevertheless considered it involved. And from Aristotle the confusion was handed down to posterity, culminating in the deadlock of the theological debates of the Middle Ages. (shrink)

IntroductionThe abstracts of a conference are important for informing the participants about the results that are communicated. However, there is poor reporting in conference abstracts in disability research. This paper aims to assess the reporting in the abstracts presented at the 5th African Network for Evidence-to-Action in Disability (AfriNEAD) Conference in Ghana.MethodsThis descriptive study extracted information from the abstracts presented at the 5th AfriNEAD Conference. Three reviewers independently reviewed all the included abstracts using a predefined data extraction form. Descriptive (...) statistics were used to analyze the extracted information, using Stata version 15.ResultsOf the 76 abstracts assessed, 54 met the inclusion criteria, while 22 were excluded. More than half of all the included abstracts (32/54; 59.26%) were studies conducted in Ghana. Some of the included abstracts did not report on the study design (37/54; 68.5%), the type of analysis performed (30/54; 55.56%), the sampling (27/54; 50%), and the sample size (18/54; 33.33%). Almost all the included abstracts did not report the age distribution and the gender of the participants.ConclusionThe study findings confirm that there is poor reporting of methods and findings in conference abstracts. Future conference organizers should critically examine abstracts to ensure that these issues are adequately addressed, so that findings are effectively communicated to participants. (shrink)

The Cell Ontology (CL) is designed to provide a standardized representation of cell types for data annotation. Currently, the CL employs multiple is_a relations, defining cell types in terms of histological, functional, and lineage properties, and the majority of definitions are written with sufficient generality to hold across multiple species. This approach limits the CL’s utility for cross-species data integration. To address this problem, we developed a method for the ontological representation of cells and applied this (...) method to develop a dendritic cell ontology (DC-CL). DC-CL subtypes are delineated on the basis of surface protein expression, systematically including both species-general and species-specific types and optimizing DC-CL for the analysis of flow cytometry data. This approach brings benefits in the form of increased accuracy, support for reasoning, and interoperability with other ontology resources. 104. Barry Smith, “Toward a Realistic Science of Environments”, Ecological Psychology, 2009, 21 (2), April-June, 121-130. Abstract: The perceptual psychologist J. J. Gibson embraces a radically externalistic view of mind and action. We have, for Gibson, not a Cartesian mind or soul, with its interior theater of contents and the consequent problem of explaining how this mind or soul and its psychological environment can succeed in grasping physical objects external to itself. Rather, we have a perceiving, acting organism, whose perceptions and actions are always already tuned to the parts and moments, the things and surfaces, of its external environment. We describe how on this basis Gibson sought to develop a realist science of environments which will be ‘consistent with physics, mechanics, optics, acoustics, and chemistry’. (shrink)

Background Biobanking and genomic research requires collection and storage of human tissue from study participants. From participants’ perspectives within the African context, this can be associated with fears and misgivings due to a myriad of factors including myths and mistrust of researchers. From the researchers angle ethical dilemmas may arise especially with consenting and sample reuse during storage. The aim of this paper was to explore these ethical considerations in the establishment and conduct of biobanking and genomic studies in Africa. (...) Methods We conducted a narrative synthesis following a comprehensive search of nine (9) databases and grey literature. All primary research study designs were eligible for inclusion as well as both quantitative and qualitative evidence from peer reviewed journals, spanning a maximum of 20 years (2000–2020). It focused on research work conducted in Africa, even if data was stored or analysed outside the region. Results Of 2,663 title and abstracts screened, 94 full texts were retrieved and reviewed for eligibility. We included 12 studies (7 qualitative; 4 quantitative and one mixed methods). Ethical issues described in these papers related to community knowledge and understanding of biobanking and genomic research, regulation, and governance of same by research ethics committees, enrolment of participants, types of informed consents, data collection, storage, usage and sharing as well as material transfer, returning results and benefit sharing. ca. Biospecimen collection and storage is given in trust and participants expect confidentially of data and results generated. Most participants are comfortable with broad consent due to trust in researchers, though a few would like to be contacted for reconsenting in future studies, and this would depend on whether the new research is for good cause. Sharing data with external partners is welcome in some contexts but some research participants did not trust foreign researchers. Conclusion Biobanking and genomic studies are a real need in Africa. Linked to this are ethical considerations related to setting up and participation in biobanks as well as data storage, export, use and sharing. There is emerging or pre-existing consensus around the acceptability of broad consent as a suitable model of consent, the need for Africans to take the lead in international collaborative studies, with deliberate efforts to build capacity in local storage and analysis of samples and employ processes of sample collection and use that build trust of communities and potential study participants. Research ethics committees, researchers and communities need to work together to work together to adapt and use clearly defined ethical frameworks, guidelines, and policy documents to harmonize the establishment and running of biobanking and genomic research in Africa. (shrink)

This Handbook is a combination of authoritative exposition, comprehensive survey, and fundamental research exploring the underlying unifying themes in the various areas. The intended audience is graduate students and researchers in the areas of computing and logic, as well as other people interested in the subject. We assume as background some mathematical sophistication. Much of the material will also be of interest to logicians and mathematicians.

In lieu of an abstract, here is a brief excerpt of the content:Feminist Studies 44, no. 2. © 2018 by Feminist Studies, Inc. 281 Allison Kimmich National Women’s Studies Association: Women’s, Gender, and Sexuality Studies Placement Data 2018 In response to a request from the National Women’s Studies Association, the institutions listed in Table 1 provided data about their PhD students’ placement in the categories listed in Table 2. The institutions provided data about all WGSS PhD (...) graduates since the programs began. Longstanding programs have graduated nearly 100 PhDs; more recent programs have graduated fewer than 10. 282 Allison Kimmich Institution Name Year First Class Matriculated Arizona State University 2007 Emory University 1990 Indiana University 2006 Ohio State University 2002 Pennsylvania State University 2001 Rutgers, the State University of New Jersey 2001 Texas Woman’s University 2010 University of California, Los Angeles 2000 University of California, Santa Barbara 2009 University of Kansas 2011 University of Kentucky 2013 University of Maryland 2000 University of Michigan 1994 University of Minnesota 1998 University of Washington 1998 Table 1  Year of Inception for WGSS Departments That Provided Data to NWSA Allison Kimmich 283 Type of Position Number of Students Percentage Tenure-track/Tenured 207 45.5% Post-doctoral fellowship/Visiting professorship 38 8.4% Lecturer/Adjunct 50 10.9% Administrative (higher education) 32 7% Researcher 14 3.1% Nonprofit 14 3.1% High school teacher 3 0.7% Currently searching/Unknown 63 13.8% Other (i.e., writer, attorney, consultant) 34 7.5% TOTAL: 455 100% Table 2 Placement of WGSS PhD Students from Departments Listed in Table 1... (shrink)

This paper investigates frequency effects in the L2 acquisition of the catenative verb construction by German learners of English from a usage-based perspective by presenting findings from two experimental studies and a complementary corpus study. It was examined if and to what extent the frequency of the verb in the catenative verb construction affects the choice of the target-like complement type and if the catenative verb construction with a to-infinitive complement, which is highly frequent in English, is more accurately acquired (...) and entrenched than the less frequent variant with an -ing complement. In all three studies, the more frequent construction with a to-infinitive yielded higher numbers of target-like complement choices. Furthermore, it was shown that the verb’s faithfulness to the construction made a significant prediction of a target-like complement preference. It is argued that a higher faithfulness promotes a target-like entrenchment of the construction and motivates a taxonomic generalisation across related exemplars. Furthermore, the results provide support for the idea that the mental representation of language is comprised of item-specific as well as more abstract schema knowledge, where frequency determines the specificity with which the construction is entrenched. (shrink)

Objective Cluster randomised trial (CRT) investigators face challenges in seeking informed consent from individual patients (cluster members). This study examined associations between reporting of patient consent in healthcare CRTs and characteristics of these trials. Study design Consent practices and study characteristics were abstracted from a random sample of 160 CRTs performed in primary or hospital care settings that were published from 2000 to 2008. Multivariable logistic regression was used to examine associations between reporting of patient consent and methodological characteristics, as (...) well as publication features such as date and journal of publication. Results 82 (53.8%) of 160 studies reported obtaining informed consent from individual patients. Reporting of patient consent was independently and positively associated with: smaller cluster size, the evaluation of experimental interventions targeted at patients, data collection from individual patients, publication later than 2004 and publication in higher-impact journals. Conclusions Reporting of consent practices in published CRTs should be improved. Consent practices in published CRTs appear to be related to the type of interventions under study, as well as journal impact and trends in research ethics practices. These findings will inform best practices in trial conduct and ethics review, remediation of errors in consent practices and ethics review and the development of regulatory guidance for CRTs. (shrink)

We define and study the class of all stack algebras as the class of all minimal algebras in a variety defined by an infinite recursively enumerable set of equations. Among a number of results, we show that the initial model of the variety is computable, that its equational theory is decidable, but that its equational deduction problem is undecidable. We show that it cannot be finitely axiomatised by equations, but it can be finitely axiomatised by equations with a hidden sort (...) and functions. This class of all stack algebras, together with its specifications, can be used to survey the many models in the literature on stacks in a systematic way, and hence give the study of the stack some mathematical coherence. Article Outline. (shrink)

Since their introduction by Partee and Rooth (1983) into linguistic theory, type shifting principles have been extensively employed in various linguistic domains, including nominal predicates (Partee 1987), kind denoting NPs (Chierchia 1998), interrogatives (Groenendijk and Stokhof 1989), scrambled definites (De Hoop and Van der Does 1998) and plurals (Winter 2001,2002). Most of the accounts that use type shifting principles employ them as ``last resort'' mechanisms, which apply only when other compositional mechanisms fail. This failure is often sloppily referred to as (...) type mismatch . The motivation for introducing type mismatch into the compositional mechanism is twofold: on the one hand it allows lexical items to be assigned the minimal types that are needed for describing their denotation; on the other hand, it has been argued that the ``last resort'' strategy of type shifting prevents derivation of undesired meanings. The first goal of this paper is to define a simple notion of type mismatch, which will rather closely follow Partee and Rooth's original proposal but will be expressed within more familiar terms of categorial semantics. After introducing this implementation of traditional type mismatch, it will be argued that in fact, it covers only one possible kind of trigger for type shifting principles. Partee and Rooth's notion of mismatch is ``external'' in that the type of an expression is changed only when it combines with another type to which it cannot compose using the ``normal'' compositional mechanism. It will be argued that, within an appropriate type system, another notion of mismatch is also useful. This is the kind of mismatch in which the semantic type of an expression does not match its syntactic category. Two such cases will be explored: mismatch between morpho-syntactic number (singular or plural) and semantic number (a denotation ranging over atoms or sets), and mismatch between syntactic category (noun, DP, adjective etc.) and semantic role (predicate, quantifier, predicate modifier etc.).. (shrink)

I argue that Kant’s Categorical Imperative should be applied to individual maxim tokens rather than abstract maxim types. The article is divided into five sections. In the first, I explain my thesis. In the second, I show that my thesis disagrees with Rawls. In the third, I argue for my thesis on the basis of the wording of the Categorical Imperative and on the basis of considerations about autonomy. In the fourth, I argue for my thesis on the (...) basis of considerations about the ‘ought implies can’ principle. In the fifth, I provide a summary of the main argumentative moves and also explain some of the philosophical advantages of my thesis. (shrink)

The storage operators were introduced by J.L. Krivine ([6]); they are closed λ-terms which, for some fixed data type (the integers for example), allow to simulate “call by value” while using “call by name”. J.L. Krivine showed that such operators can be typed, in the type system, using Gödel's translation from classical to intuitionistic logic ([8]).This paper studies the existence of storage operators which give a normal form as result (strong storage operators) for recursive and iterative representation of (...) class='Hi'>data in λ-calculus. We obtain the following result:We can find typed strong storage operators for the recursive representations of data type, but that is not the case for the iterative representations of an infinite data type.We give the proof of this result in the case of integers. (shrink)

One of the main problems in computer science is to ensure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry-Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, (...) where the axioms define the abstract data types, using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ω-rule . A discussion about the use of the finitary induction instead of computational ω-rule concludes the work. (shrink)

This book describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning. The idea of knowledge bases lies at the heart of symbolic, or "traditional," artificial intelligence. A knowledge-based system decides how to act by running formal reasoning procedures over a body of explicitly represented knowledge—a knowledge base. The system is not programmed for specific tasks; rather, it (...) is told what it needs to know and expected to infer the rest. This book is about the logic of such knowledge bases. It describes in detail the relationship between symbolic representations of knowledge and abstract states of knowledge, exploring along the way the foundations of knowledge, knowledge bases, knowledge-based systems, and knowledge representation and reasoning. Assuming some familiarity with first-order predicate logic, the book offers a new mathematical model of knowledge that is general and expressive yet more workable in practice than previous models. The book presents a style of semantic argument and formal analysis that would be cumbersome or completely impractical with other approaches. It also shows how to treat a knowledge base as an abstract data type, completely specified in an abstract way by the knowledge-level operations defined over it. (shrink)

The theory of constructive (recursive) models follows from works of Froehlich, Shepherdson, Mal'tsev, Kuznetsov, Rabin, and Vaught in the 50s. Within the framework of this theory, algorithmic properties of abstract models are investigated by constructing representations on the set of natural numbers and studying relations between algorithmic and structural properties of these models. This book is a very readable exposition of the modern theory of constructive models and describes methods and approaches developed by representatives of the Siberian school of (...) algebra and logic and some other researchers (in particular, Nerode and his colleagues). The main themes are the existence of recursive models and applications to fields, algebras, and ordered sets (Ershov), the existence of decidable prime models (Goncharov, Harrington), the existence of decidable saturated models (Morley), the existence of decidable homogeneous models (Goncharov and Peretyat'kin), properties of the Ehrenfeucht theories (Millar, Ash, and Reed), the theory of algorithmic dimension and conditions of autostability (Goncharov, Ash, Shore, Khusainov, Ventsov, and others), and the theory of computable classes of models with various properties. Future perspectives of the theory of constructive models are also discussed. Most of the results in the book are presented in monograph form for the first time. The theory of constructive models serves as a basis for recursive mathematics. It is also useful in computer science, in particular, in the study of programming languages, higher level languages of specification, abstract data types, and problems of synthesis and verification of programs. Therefore, the book will be useful for not only specialists in mathematical logic and the theory of algorithms but also for scientists interested in the mathematical fundamentals of computer science. The authors are eminent specialists in mathematical logic. They have established fundamental results on elementary theories, model theory, the theory of algorithms, field theory, group theory, applied logic, computable numberings, the theory of constructive models, and the theoretical computer science. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of large subsystems of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that (...) provide computational procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

In the 80's Pierangelo Miglioli, starting from motivations in the framework of Abstract Data Types and Program Synthesis, introduced semiconstructive theories, a family of “large subsystems” of classical theories that guarantee the computability of functions and predicates represented by suitable formulas. In general, the above computability results are guaranteed by algorithms based on a recursive enumeration of the theorems of the whole system. In this paper we present a family of semiconstructive systems, we call uniformly semiconstructive, that (...) provide computational procedures only involving formulas with bounded complexity. We present several examples of uniformly semiconstructive systems containing Harrop theories, induction principles and some well-known predicate intermediate principles. Among these, we give an account of semiconstructive and uniformly semiconstructive systems which lie between Intuitionistic and Classical Arithmetic and we discuss their constructive incompatibility. (shrink)

Some varieties that are extensions of relational algebras with two constants that play the role of projections are studied. The classes have as a subvariety the abstract fork algebra equivalent variety involving projections. They are obtained by weakening some laws valid in AFA. Some applications of the varieties in the literature and in the specification of abstract data types are exhibited. For each of the classes obtained, an answer is given to the question: 'Is the relational (...) reduct of the class representable?'. For the subvarieties formed with the models that have a representable relational reduct, a representation theorem is proved. For them the finitization problem is studied. Next the varieties presented are compared by means of the inclusion order. For each class the problem of characterizing finite models is considered. Simple models in the varieties are studied. Finally the existence of equivalent classes with a binary operation like fork is studied. (shrink)

In this book, Linda Wetzel examines the distinction between types and tokens and argues that types exist (as abstract objects, since they lack a unique ...

The distinction between the modeling of information and the modeling of data in the creation of automated systems has historically been important because the development tools available to programmers have been wedded to machine oriented data types and processes. However, advances in software engineering, particularly the move toward data abstraction in software design, allow activities reasonably described as information modeling to be performed in the software creation process. An examination of the evolution of programming languages and (...) development of general programming paradigms, including object-oriented design and implementation, suggests that while data modeling will necessarily continue to be a programmer's concern, more and more of the programming process itself is coming to be characterized by information modeling activities. (shrink)

If numbers were identified with any of their standard set-theoretic realizations, then they would have various non-arithmetical properties that mathematicians are reluctant to ascribe to them. Dedekind and later structuralists conclude that we should refrain from ascribing to numbers such ‘foreign’ properties. We first rehearse why it is hard to provide an acceptable formulation of this conclusion. Then we investigate some forms of abstraction meant to purge mathematical objects of all ‘foreign’ properties. One form is inspired by Frege; the other (...) by Dedekind. We argue that both face problems. (shrink)

Machamer, Darden, and Craver's account of the nature and role of mechanisms in the special sciences has been very influential. Unfortunately, a confusing array of ontic, epistemic, and pragmatic distinctions is required to individuate their mechanisms, mechanism schemata, and mechanism sketches. I diagnose this as a conflation of token-level causal relations with type-level relations. I propose instead that a mechanism is an abstraction that relates entity types and activity types on the model of a directed graph. Mechanisms have (...) an ontic status distinct from the causal chains of token entities and token activities that instantiate them. (shrink)

We suggest a method of finding a notion of type to abstract elementary classes and determine under what assumption on these types the class has a well-behaved homogeneous and universal "monster" model, where homogeneous and universal are defined relative to our notion of type.

Neuroscience influences education, and these two areas have converged in a new field denominated “Neuroeducation.” However, the growing interest in the education–brain relationship does not match the proper use of research findings. In 2007, the Organization for Economic Cooperation and Development warned of the misunderstandings about the brain among teachers, labeling them as neuromyths. The main objective here is to observe the prevalence of the neuromyths in educators over time. After two decades of publications of research on neuromyths among in-service (...) or prospective teachers, this work presents a systematic scientific review. To select the articles, we used the words: “teachers,” “preservice teachers,” “neuromyths” combined with the Boolean data type “and.” The search was filtered according to the following criteria: identifiable author, written in English, Spanish, French, Italian, or Portuguese, word neuromyth in title, abstract, or keywords, research with a participant's survey, sample focused on educators, peer-review publication index in JCR, SJR, or ESCI. The documents were found through Web of Science, Scopus, PubMed, Dialnet, ProQuest, EBSCO-host, and Google Scholar. After the search, 24 articles were identified as being of sufficiently high quality for this systematic review. This result highlights that neuromyths are still the subject of attention almost two decades after their definition. The findings present neuromyths as the consequence of a lack of scientific knowledge, a communicative gap between scientists and teachers, and the low-quality information sources consulted by teachers. In addition, the data on protectors and predictors of neuromyths is inconsistent. There is also no standard scientific methodology nor a guideline to determine a new neuromyth. The results show the need to improve the scientific content in higher education and the importance of in-service teacher training. This research justifies the requirement for university professors to be active researchers and to establish a close link with educators from other fields and levels. Neuroeducation will be the bridge that unites scientific knowledge and practical application in education, with a rigorous, standard method for the entire scientific-educational community. (shrink)

We study Lascar strong types and Galois types and especially their relation to notions of type which have finite character. We define a notion of a strong type with finite character, the so-called Lascar type. We show that this notion is stronger than Galois type over countable sets in simple and superstable finitary AECs. Furthermore, we give an example where the Galois type itself does not have finite character in such a class.

The chapter outlines an abstract theoretical framework that is currently (re-)emerging in the course of a theoretical convergence of several disciplines. In the first section, the fundamental problem of perception theory is formulated, namely, the generation, by the perceptual system, of meaningful categories from physicogeometric energy patterns. In the second section, it deals with basic intuitions and assumptions underlying what can be regarded as the current Standard Model of Perceptual Psychology and points out why this model is profoundly inadequate (...) for dealing with the fundamental problem of perception theory. In the third section, it discusses a level of analysis that promises to be fruitful for dealing, in conformity with established procedures of the natural sciences, with the problem of perceptual “meaning” and the problem of what constitutes a “perceptual object.” In the fourth section, it outlines a theoretical perspective on basic principles of the perceptual system which centers on the notions of complex data types and conceptual forms, and draws an entirely different theoretical picture of the role of the sensory input than traditional accounts. The final section focusses on the issue of material qualities and discusses, within the general theoretical framework outlined, some observations and results on the perception of certain material properties, namely, lustrous and glassy appearances. (shrink)

ABSTRACT In this paper, I present data involving the use of the Romanian slur ‘țigan’, consideration of which leads to the postulation of a sui-generis, irreducible type of use of slurs. This type of use is potentially problematic for extant theories of slurs. In addition, together with other well-established uses, it shows that there is more variation in the use of slurs than previously acknowledged. I explain this variation by construing slurs as polysemous. To implement this idea, I (...) appeal to a rich-lexicon account of polysemy. I show how such a theory can be applied to slurs and discuss several important issues that arise. (shrink)

In finite type arithmetic, the real numbers are represented by rapidly converging Cauchy sequences of rational numbers. Ulrich Kohlenbach introduced abstract types for certain structures such as metric spaces, normed spaces, Hilbert spaces, etc. With these types, the elements of the spaces are given directly, not through the mediation of a representation. However, these abstract spaces presuppose the real numbers. In this paper, we show how to set up an abstract type for the real numbers. (...) The appropriateness of our construction works in tandem with the bounded functional interpretation. (shrink)

Cognitive states as well as cognitive commodities play central though distinct roles in our epistemological theories. By being attentive to how a difference in their roles affects our way of referring to them, we can undoubtedly accrue our understanding of the structure and functioning of our main epistemological theories. In this paper we propose an analysis of the dichotomy between states and commodities in terms of the method of abstraction, and more specifically by means of infomorphisms between different ways to (...) classify states of information, information-bases, and evidential situations. (shrink)