In 1990, J. L. Krivine introduced the notion of storage operator to simulate “call by value” in the “call by name” strategy. J. L. Krivine has showed that, using Gödel translation of classical into intuitionistic logic, one can find a simple type for the storage operators in AF2 type system. This paper studies the ∀-positive types and the Gödel transformations of TTR type system. We generalize by using syntactical methods Krivine's theorem about these types and (...) for these transformations. We give a proof of this result in the case of the type of recursive integers. (shrink)

In 1990, J.L. Krivine introduced the notion of storage operator to simulate 'call by value' in the 'call by name' strategy. J.L. Krivine has shown that, using Gödel translation of classical into intuitionitic logic, we can find a simple type for the storage operators in AF2 type system. This paper studies the $forall$-positive types (the universal second order quantifier appears positively in these types), and the Gödel transformations (a generalization of classical Gödel translation) of TTR type (...) system. We generalize, by using syntaxical methods, the J.L. Krivine's Theorem about these types and for these transformations. We give a proof of this result in the case of the type of recursive integers. (shrink)

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) (...) do, but the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD! (shrink)

Pure Type Systems, PTSs, were introduced as a generalization of the type systems of Barendregt's lambda cube and were designed to provide a foundation for actual proof assistants which will verify proofs. Systems of illative combinatory logic or lambda calculus, ICLs, were introduced by Curry and Church as a foundation for logic and mathematics. In an earlier paper we considered two changes to the rules of the PTSs which made these rules more like ICL rules. This led to (...) four kinds of PTSs. Most importantly PTSs are about statements of the form M:A, where M is a term and A a type. In ICLs there are no explicit types and the statements are terms. In this paper we show that for each of the four forms of PTS there is an equivalent form of ICL, sometimes if certain conditions hold. (shrink)

Pure Type Systems, PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic. First (...) we consider a simplification of the start and weakening rules of PTSs, which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems. A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications. (shrink)

We introduce a new type system called “System ST” , based on subtyping, and prove the basic property of the system. We show the extraordinary expressive power of the system which leads us to think that it could be a good candidate for doing both proof and extraction of programs.

The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these (...) systems it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] that this emptiness problem is decidable for the sytem including (η), but without ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ E) and (η), into equivalence classes according to their strength in typing λ-terms and also according to their strength in possessing inhabitants. This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants. (shrink)

We present a framework for intensional reasoning in typed -calculus. In this family of calculi, called Modal Pure Type Systems (MPTSs), a propositions-as-types-interpretation can be given for normal modal logics. MPTSs are an extension of the Pure Type Systems (PTSs) of Barendregt (1992). We show that they retain the desirable meta-theoretical properties of PTSs, and briefly discuss applications in the area of knowledge representation.

Tait's proof of strong normalization for the simply typed λ-calculus is interpreted in a general model theoretical framework by means of the specification of a certain theory T and a certain model /oU of T. The argumentation is partly reduced to formal predicate logic by the application of certain derivability properties of T. The resulting version of Tait's proof is, within the same framework, systematically generalized to the Calculus of Constructions and other advanced type systems. The generalization proceeds along (...) the formal level in the sense that T is modified first and that the new theory partly dictates the subsequent transformation of /oU, which is carried out in stages. The uniform and standardized character of the argumentation contributes to its perspicuity. (shrink)

We introduce and analyze two theories for typed inductive definitions and establish their proof-theoretic ordinal to be the small Veblen ordinal \. We investigate on the one hand the applicative theory \ of functions, inductive definitions, and types. It includes a simple type structure and is a natural generalization of S. Feferman’s system \\). On the other hand, we investigate the arithmetical theory \ of typed inductive definitions, a natural subsystem of \, and carry out a wellordering proof (...) within \ that makes use of fundamental sequences for ordinal notations in an ordinal notation system based on the finitary Veblen functions. The essential properties for describing the ordinal notation system are worked out. (shrink)

In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, (...) predicative logic still plays an influential role in Computer Science.An important example is the proof checker Nuprl, which is basedon Martin-Löf''s Type Theory which uses type universes. Those type universes,and also degrees of expressions in AUTOMATH, are closely related toorders. In this paper, we show that orders have not disappeared from modern logic and computer science, rather, orders play a crucial role in understanding the hierarchy of modern systems. In order to achieve our goal, we concentrate on a subsystem of Nuprl.The novelty of our paper lies in: (1) a modest revival of Russell's orders, (2) the placing of the historical system RTT underlying the famous Principia Mathematica in a context with a modern system of computer mathematics (Nuprl) and modern type theories (Martin-Löf''s type theory and PTSs), and (3) the presentation of acomplex type system (Nuprl) as a simple and compact PTS. (shrink)

The logic of the weak law of excluded middleKC p is obtained by adding the formula A A as an axiom scheme to Heyting's intuitionistic logicH p . A cut-free sequent calculus for this logic is given. As the consequences of the cut-elimination theorem, we get the decidability of the propositional part of this calculus, its separability, equality of the negationless fragments ofKC p andH p , interpolation theorems and so on. From the proof-theoretical point of view, the formulation presented (...) in this paper makes clearer the relations betweenKC p ,H p , and the classical logic. In the end, an interpretation of classical propositional logic in the propositional part ofKC p is given. (shrink)

BackgroundType-Token Ratio, given its relatively simple hand computation, is one of the few LSA measures calculated by clinicians in everyday practice. However, it has significant well-documented shortcomings; these include instability as a function of sample size, and absence of clear developmental profiles over early childhood. A variety of alternative measures of lexical diversity have been proposed; some, such as Number of Different Words/100 can also be computed by hand. However, others, such as Vocabulary Diversity and the Moving Average Type (...) Token Ratio rely on complex resampling algorithms that cannot be conducted by hand. To date, no large-scale study of all four measures has evaluated how well any capture typical developmental trends over early childhood, or whether any reliably distinguish typical from atypical profiles of expressive child language ability.Materials and MethodsWe conducted linear and non-linear regression analyses for TTR, NDW, VocD, and MATTR scores for samples taken from 946 corpora from typically developing preschool children, engaged in adult-child toy play, from the Child Language Data Exchange System. These were contrasted with 504 samples from children known to have delayed expressive language skills. We also conducted a separate sub-analysis which examined possible contextual effects of sampling environment on lexical diversity.ResultsOnly VocD showed significantly different mean scores between the typically -developing children and delayed developing children group. Using TTR would actually misdiagnose typical children and miss children with known language impairment. However, computation of VocD as a function of toy interactions was significant and emerges as a further caution in use of lexical diversity as a valid proxy index of children’s expressive vocabulary skill.DiscussionThis large scale statistical comparison of computer-implemented algorithms for expressive lexical profiles in young children with traditional, hand-calculated measures showed that only VocD met criteria for evidence-based use in LSA. However, VocD was impacted by sample elicitation context, suggesting that non-linguistic factors, such as engagement with elicitation props, contaminate estimates of spoken lexical skill in young children. Implications and suggested directions are discussed. (shrink)

The Five Elements brings the wisdom of an ancient healing system to the modern reader. Many people today are interested in knowing themselves better, as evidenced by the popularity of personality tests online and in magazines. They want to know the reason behind their responses to situations. In this book, Dondi Dahlin shows us that we are all born with individual rhythms that go beyond the influence of our genes and upbringing. The five elements originated in ancient Chinese medicine (...) over 2,000 years ago--when scholars theorized that the universe is composed of five forces: water, wood, fire, earth, and metal. Understanding these elements helps us stay in balance physically, mentally, spiritually, and emotionally. By explaining the efficacy of wood, the depth of water, the joy of fire, the compassion of earth, and the wisdom of metal, this book helps people understand themselves and form lasting connections to others, answering the age-old question of why we do what we do. (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)

In this paper we describe the Curry-Howard-De Bruijn isomorphism between Higher Order Many Sorted Intuitionistic Predicate Logic PREDω and the type system λPREDω, which can be considered a subsystem of the Calculus of Constructions. The type system is presented using the concept of a Pure Type System, which is a very elegant framework for describing type systems. We show in great detail how formulae and proof trees of the logic relate to types and (...) terms of the type system, respectively. Finally, we discuss some consequences of the isomorphism with respect to the relation between the systems discussed in this paper. (shrink)

Error related potentials, which are elicited in the EEG in response to a perceived error, have been used for error correction and adaption in the event related potential -based brain computer interfaces designed for typing. In these typing interfaces, ERP evidence is collected in response to a sequence of stimuli presented usually in the visual form and the intended user stimulus is probabilistically inferred and presented to the user as the decision. If the inferred stimulus is incorrect, ErrP is expected (...) to be elicited in the EEG. Early approaches to use ErrP in the design of typing interfaces attempt to make hard decisions on the perceived error such that the perceived error is corrected and either the sequence of stimuli are repeated to obtain further ERP evidence, or without further repetition the stimulus with the second highest probability is presented to the user as the decision of the system. Moreover, none of the existing approaches use a language model to increase the performance of typing. In this work, unlike the existing approaches, we study the potential benefits of fusing feedback related potentials, a form of ErrP, with ERP and context information in a Bayesian fashion to detect the user intent. We present experimental results based on data from 12 healthy participants using RSVP Keyboard™ to complete a copy-phrase-task. Three paradigms are compared: [P1] uses only ERP/LM Bayesian fusion; [P2] each RSVP sequence is appended with the top candidate in the alphabet according to posterior after ERP evidence fusion; corresponding FRP is then incorporated; and [P3] the top candidate is shown as a prospect to generate FRP evidence only if its posterior exceeds a threshold. Analyses indicate that ERP/LM/FRP evidence fusion during decision making yields significant speed-accuracy benefits for the user. (shrink)

A rejection system, also referred to as a complementary calculus, is a proof system axiomatising the invalid formulas of a logic, in contrast to traditional calculi which axiomatise the valid ones. Rejection systems therefore introduce a purely syntactic way of determining non-validity without having to consider countermodels, which can be useful in procedures for automated deduction and proof search. Rejection calculi have first been formally introduced by Łukasiewicz in the context of Aristotelian syllogistic and subsequently rejection systems for (...) many well-known logics have been proposed. In this paper, we deal with rejection systems for so-called non-deterministic finite-valued logics, a special case of non-deterministic many-valued logics which were introduced by Avron and Lev as a generalisation of traditional many-valued logics. More specifically, we introduce a systematic method for constructing sequent-style rejection systems for any given non-deterministic finite-valued logic. Furthermore, as special instances of our method, we provide concrete calculi for specific paraconsistent logics which can be characterised in terms of non-deterministic two- and three-valued semantics, respectively. (shrink)

It is often said that in a purely formal perspective, intuitionistic logic has no obvious advantage to deal with the liar-type paradoxes. In this paper, we will argue that the standard intuitionistic natural deduction systems are vulnerable to the liar-type paradoxes in the sense that the acceptance of the liar-type sentences results in inference to absurdity (⊥). The result shows that the restriction of the Double Negation Elimination (DNE) fails to block the inference to ⊥. It is, (...) however, not the problem of the intuitionistic approaches to the liar-type paradoxes but the lack of expressive power of the standard intuitionistic natural deduction system. We introduce a meta-level negation for a given system and a meta-level absurdity, ⋏, to the intuitionistic system. We shall show that in the system, the inference to ⊥ is not given without the assumption that the system is complete. Moreover, we consider the Double Meta-Level Negation Elimination rules (DMNE) which implicitly assume the completeness of the system. Then, the restriction of DMNE can rule out the inference to ⊥. (shrink)

The necessity to provide for a stable regional development as one of the main priorities of regional social and economic policies in the unstable world economics is justified. A wide classification of stability types in region development is considered and factors influencing the institutional stability are singled out.

The notions of a hyper MV-deductive system, a -hyper MV-deductive system, a - hyper MV-deductive system, a -hyper MV-deductive system, a -hyper MV-deductive system and a -hyper MV-deductive system are introduced, and then their relations are investigated.

We study the cube of type assignment systems, as introduced in Giannini et al. 87–126), and confront it with Barendregt's typed gl-cube . The first is obtained from the latter through applying a natural type erasing function E to derivation rules, that erases type information from terms. In particular, we address the question whether a judgement, derivable in a type assignment system, is always an erasure of a derivable judgement in a corresponding typed system; (...) we show that this property holds only for systems without polymorphism. The type assignment systems we consider satisfy the properties ‘subject reduction’ and ‘strong normalization’. Moreover, we define a new type assignment cube that is isomorphic to the typed one. (shrink)

This study explores the type-based vocational education system from the perspective of China. General education and vocational education are equal types of education in status, but not based on different levels of education in China. Specifically, the connotation of vocational education as type-based education is mainly embodied in ‘three directions’. The outstanding problems of vocational education as a type-based education include ‘four aspects’. Vocational education as a type-based education reform path is considered as ‘four reforms’. (...) We should strengthen management, improve the comprehensive quality of vocational college students and make clear the direction and explore the new path of reform and development of vocational colleges. In addition, we need to optimize investment and make innovations in the system and mechanism of funding for China’s vocational education. (shrink)

We introduce type-theoretic algebraic weak factorisation systems and show how they give rise to homotopy-theoretic models of Martin-Löf type theory. This is done by showing that the comprehension category associated with a type-theoretic algebraic weak factorisation system satisfies the assumptions necessary to apply a right adjoint method for splitting comprehension categories. We then provide methods for constructing several examples of type-theoretic algebraic weak factorisation systems, encompassing the existing groupoid and cubical sets models, as well as (...) new models based on normal fibrations. (shrink)

This article intends to show that ideology is always organized systemically by undertaking the opposition between conformity and diversity as its fundamental criterion. In order to underpin this hypothesis, the present article examines the inner structure of five classic ideologies, that can be understood as ideal ideological types. The analysis reveals that ideologies do not form a system because at the core of any ideology there is a key-concept not determined nor influenced by the key concepts of other ideologies.

Interval type-2 fuzzy logic systems have favorable abilities to cope with uncertainties in many applications. While the block type-reduction under the guidance of inference plays the central role in the systems, Karnik-Mendel iterative algorithms are standard algorithms to perform the type-reduction; however, the high computational cost of type-reduction process may hinder them from real applications. The comparison between the KM algorithms and other alternative algorithms is still an open problem. This paper introduces the related theory of (...) interval type-2 fuzzy sets and discusses the blocks of fuzzy reasoning, type-reduction, and defuzzification of interval type-2 fuzzy logic systems by combining the Nagar-Bardini and Nie-Tan noniterative algorithms for solving the centroids of output interval type-2 fuzzy sets. Moreover, the continuous version of NT algorithms is proved to be accurate algorithms for performing the type-reduction. Four computer simulation examples are provided to illustrate and analyze the performances of two kinds of noniterative algorithms. The NB and NT algorithms are superior to the KM algorithms on both calculation accuracy and time, which afford the potential application value for designer and adopters of type-2 fuzzy logic systems. (shrink)

In this paper, we extend the system AF2 in order to have the subject reduction for the $betaeta$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.

Girard and Reynolds independently invented System F to handle problems in logic and computer programming language design, respectively. Viewing F in the Curry style, which associates types with untyped lambda terms, raises the questions of typability and type checking. Typability asks for a term whether there exists some type it can be given. Type checking asks, for a particular term and type, whether the term can be given that type. The decidability of these problems (...) has been settled for restrictions and extensions of F and related systems and complexity lower-bounds have been determined for typability in F, but this report is the first to resolve whether these problems are decidable for System F. This report proves that type checking in F is undecidable, by a reduction from semi-unification, and that typability in F is undecidable, by a reduction from type checking. Because there is an easy reduction from typability to type checking, the two problems are equivalent. The reduction from type checking to typability uses a novel method of constructing lambda terms that simulate arbitrarily chosen type environments. All of the results also hold for the λI-calculus. (shrink)

We present a formal theory of contextuality for a set of random variables grouped into different subsets corresponding to different, mutually incompatible conditions. Within each context the random variables are jointly distributed, but across different contexts they are stochastically unrelated. The theory of contextuality is based on the analysis of the extent to which some of these random variables can be viewed as preserving their identity across different contexts when one considers all possible joint distributions imposed on the entire set (...) of the random variables. We illustrate the theory on three systems of traditional interest in quantum physics. These are systems of the Klyachko–Can–Binicioglu–Shumovsky-type, Einstein–Podolsky–Rosen–Bell-type, and Suppes–Zanotti–Leggett–Garg-type. Listed in this order, each of them is formally a special case of the previous one. For each of them we derive necessary and sufficient conditions for contextuality while allowing for experimental errors and contextual biases or signaling. Based on the same principles that underly these derivations we also propose a measure for the degree of contextuality and compute it for the three systems in question. (shrink)

Multiteam systems are complex organizational forms comprising interdependent teams that work towards their own proximal goals within and across teams to also accomplish a shared superordinate goal. MTSs operate within high-stakes, dangerous contexts with high consequences for suboptimal performance. We answer calls for nuanced exploration and cross-context comparison of MTSs “in the wild” by leveraging the MTS action sub-phase behavioral taxonomy to determine where and how MTS failures occur. To our knowledge, this is the first study to also examine how (...) key MTS attributes influence MTS processes and performance. We conducted historiometric analysis on 40 cases of failed MTS performance across various contexts to uncover patterns of within- and between-team behaviors of failing MTSs, resulting in four themes. First, component teams of failing MTSs over-engaged in within-team alignment behaviors by enacting acting, monitoring, and recalibrating behaviors more often within than between teams. Second, failing MTSs over-focused on acting behaviors and tended to not fully enact the action sub-phase cycle. Third and fourth, boundary status and goal type exacerbated these behavioral patterns, as external and physical MTSs were less likely to enact sufficient between-team behaviors or fully enact the action sub-phase cycle compared to internal and intellectual MTSs. We propose entrainment as a mechanism for facilitating MTS performance wherein specific, cyclical behavioral patterns enacted by teams align to facilitate goal achievement via three multilevel behavioral cycles. We argue that the degree to which these cycles are aligned both between teams and with the overarching MTS goal determines whether and how an MTS fails. Our findings add nuance beyond single-context MTS studies by showing that the identified behavioral patterns hold both across contexts and almost all types of MTS action-phase behaviors. We show that these patterns vary by MTS boundary status and goal type. Our findings inform MTS training best practices, which should be structured to integrate all component teams and tailored to both MTS attributes and situation type. (shrink)

Significant associations have been found between specific human leukocyte antigen (HLA) alleles and organ transplant rejection, autoimmune disease development, and the response to infection. Traditional searches for disease associations have conventionally measured risk associated with the presence of individual HLA alleles. However, given the high level of HLA polymorphism, the pattern of amino acid variability, and the fact that most of the HLA variation occurs at functionally important sites, it may be that a combination of variable amino acid sites shared (...) by several alleles (shared epitopes) are better descriptors of the actual causative genetic variants. Here we describe a novel approach to genetic association analysis in which genes/proteins are broken down into smaller sequence features and then variant types defined for each feature, allowing for independent analysis of disease association with each sequence feature variant type. We have used this approach to analyze a cohort of systemic sclerosis patients and show that a sequence feature composed of specific amino acid residues in peptide binding pockets 4 and 7 of HLA-DRB1 explains much of the molecular determinant of risk for systemic sclerosis. (shrink)

The Type VI secretion system is a multiprotein and mosaic apparatus that delivers protein effectors into prokaryotic or eukaryotic cells. Recent data on the enteroaggregative Escherichia coli T6SS have provided evidence that the TssA protein is a key component during T6SS biogenesis. The T6SS comprises a trans-envelope complex that docks the baseplate, a cytoplasmic complex that represents the assembly platform for the tail. The T6SS tail is structurally, evolutionarily and functionally similar to the contractile tails of bacteriophages. We (...) have shown that TssA docks to the membrane complex, recruits the baseplate complex and initiates and coordinates the polymerization of the inner tube with that of the sheath. Here, we review these recent findings, discuss the variations within TssA-like proteins, speculate on the role of EAEC TssA in T6SS biogenesis and propose future research perspectives. In the environment, bacteria have to cope with other microbial species and therefore have evolved anti-microbial mechanisms. The bacterial Type VI secretion system transports toxins into bacterial and/or eukaryotic cells using a contractile mechanism. At the architectural level, the T6SS could be viewed as a nano-speargun assembled in the bacterial cytoplasm and anchored to a trans-envelope complex. We describe and speculate on recent findings demonstrating that the TssA subunit is involved in the different stages of T6SS biogenesis. (shrink)