An approach to deciding the observational equivalence of Algol-like languages

We prove that the observational equivalence of third-order finitary (i.e. recursion-free) Idealized Algol (IA) is decidable using Game Semantics. By modelling the state explicitly in our games, we show that the denotation of a term M of this fragment of IA is a compactly innocent strategy-with-state, i.e. the strategy is generated by a finite view function f_M. Given any such f_M, we construct a real-time deterministic pushdown automaton (DPDA) that recognizes the complete plays of the knowing-strategy denotation of M. Since such plays characterize observational equivalence, and there is an algorithm for deciding whether any two DPDAs recognize the same language, we obtain a procedure for deciding the observational equivalence of third-order finitary IA. Restricted to second-order terms, the DPDA representation cuts down to a deterministic finite automaton; thus our approach gives a new proof of Ghica and McCusker’s regular-expression characterization for this fragment. Our algorithmic representation of program meanings, which is compositional, provides a foundation for model-checking a wide range of behavioural properties of IA and other cognate programming languages. Another result concerns second-order IA with full recursion: we show that observational equivalence for this fragment is undecidable.     

Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals

Probabilistic team semantics is a framework for logical analysis of probabilistic dependencies. Our focus is on the axiomatizability, complexity, and expressivity of probabilistic inclusion logic and its extensions. We identify a natural fragment of existential second-order logic with additive real arithmetic that captures exactly the expressivity of probabilistic inclusion logic. We furthermore relate these formalisms to linear programming, and doing so obtain PTIME data complexity for the logics. Moreover, on finite structures, we show that the full existential second-order logic with additive real arithmetic can only express NP properties. Lastly, we present a sound and complete axiomatization for probabilistic inclusion logic at the atomic level.     

On intermediate inquisitive and dependence logics: An algebraic study

This article provides an algebraic study of intermediate inquisitive and dependence logics. While these logics are usually investigated using team semantics, here we introduce an alternative algebraic semantics and we prove it is complete for all intermediate inquisitive and dependence logics. To this end, we define inquisitive and dependence algebras and we investigate their model-theoretic properties. We then focus on finite, core-generated, well-connected inquisitive and dependence algebras: we show they witness the validity of formulas true in inquisitive algebras, and of formulas true in well-connected dependence algebras. Finally, we obtain representation theorems for finite, core-generated, well-connected, inquisitive and dependence algebras and we prove some results connecting team and algebraic semantics.     

Unifying hidden-variable problems from quantum mechanics by logics of dependence and independence

We study hidden-variable models from quantum mechanics and their abstractions in purely probabilistic and relational frameworks by means of logics of dependence and independence, which are based on team semantics. We show that common desirable properties of hidden-variable models can be defined in an elegant and concise way in dependence and independence logic. The relationship between different properties and their simultaneous realisability can thus be formulated and proven on a purely logical level, as problems of entailment and satisfiability of logical formulae. Connections between probabilistic and relational entailment in dependence and independence logic allow us to simplify proofs. In many cases, we can establish results on both probabilistic and relational hidden-variable models by a single proof, because one case implies the other, depending on purely syntactic criteria. We also discuss the ‘no-go’ theorems by Bell and Kochen-Specker and provide a purely logical variant of the latter, introducing non-contextual choice as a team-semantical property.     

Efficient simulation of general stochastic hybrid systems

General Stochastic Hybrid System (SHS) are characterised by Stochastic Differential Equations (SDEs) with discontinuities and Poisson jump processes. SHS are useful in model based design of Cyber-Physical System (CPS) controllers under uncertainty. Industry standard model based design tools such as Simulink/Stateflow® are inefficient when simulating, testing, and validating SHS, because of dependence on fixed-step Euler–Maruyama (EM) integration and discontinuity detection. We present a novel efficient adaptive step-size simulation/integration technique for general SHSs modelled as a network of Stochastic Hybrid Automatons (SHAs). We propose a simulation algorithm where each SHA in the network executes synchronously with the other, at an integration step-size computed using adaptive step-size integration. Ito’ multi-dimensional lemma and the inverse sampling theorem are leveraged to compute the integration step-size by making the SDEs and Poisson jump rate integration dependent upon discontinuities. Existence and convergence analysis along with experimental results show that the proposed technique is substantially faster than Simulink/Stateflow®when simulating general SHSs.     

Reasoning about proof and knowledge

In previous work [15], we presented a hierarchy of classical modal systems, along with algebraic semantics, for the reasoning about intuitionistic truth, belief and knowledge. Deviating from Gödel's interpretation of IPC in S4, our modal systems contain IPC in the way established in [13]. The modal operator can be viewed as a predicate for intuitionistic truth, i.e. proof. Epistemic principles are partially adopted from Intuitionistic Epistemic Logic IEL [4]. In the present paper, we show that the S5-style systems of our hierarchy correspond to an extended Brouwer–Heyting–Kolmogorov interpretation and are complete w.r.t. a relational semantics based on intuitionistic general frames. In this sense, our S5-style logics are adequate and complete systems for the reasoning about proof combined with belief or knowledge. The proposed relational semantics is a uniform framework in which also IEL can be modeled. Verification-based intuitionistic knowledge formalized in IEL turns out to be a special case of the kind of knowledge described by our S5-style systems.     

Inductive Construction of Repletion

The aim of this paper is to give a purely logical construction of repletion, i.e. the reflection of an arbitrary set to a replete one. Replete sets within constructive logic were introduced independently by M. Hyland and P. Taylor as the most restrictive but sufficiently general notion of predomain suitable for the purposes of denotational semantics à la Scott.For any set A its repletion R(A) appears as an inductively defined subset of S²(A) (A S) S which can be expressed within the internal language of a model of type theory. More explicitly, R(A) is the least subset of S²(A) containing all point filters and closed under a class of generalised limit processes. Improvements of our construction arise from several results saying that it suffices for the purpose of repletion to consider more restrictive classes of generalised limit processes.     

Computational Modeling of Organizations Comes of Age

As they are maturing—i.e., as they are becoming validated, calibrated and refined—computational emulation models of organizations are evolving into: powerful new kinds of organizational design tools for predicting and mitigating organizational risks; and flexible new kinds of organizational theorem-provers for validating extant organization theory and developing new theory. Over the past 50 years, computational modeling and simulation have had enormous impacts on the rate of advancement of knowledge in fields like physics, chemistry and, more recently, biology; and their subsequent application has enabled whole new areas of engineering practice. In the same way, as our young discipline comes of age, computational organizational models are beginning to impact behavioral, organizational and economic science, and management consulting practice. This paper attempts to draw parallels between computational modeling in natural sciences and computational modeling of organizations as a contributor to both social science and management practice.To illustrate the lifecycle of a computational organizational model that is now relatively mature, this paper traces the evolution of the Virtual Design Team (VDT) computational modeling and simulation research project at Stanford University from its origins in 1988 to the present. It lays out the steps in the process of validating VDT as a computational emulation model of organizations to the point that VDT began to influence management practice and, subsequently, to advance organizational science. We discuss alternate research trajectories that can be taken by computational and mathematical modelers who prefer the typical natural science validation trajectory—i.e., who attempt to impact organizational science first and, perhaps subsequently, to impact management practice.The paper concludes with a discussion of the current state-of-the-art of computational modeling of organizations and some thoughts about where, and how rapidly, the field is headed.     

The semantics of knowledge attributions

The basic idea of conversational contextualism is that knowledge attributions are context sensitive in that a given knowledge attribution may be true if made in one context but false if made in another, owing to differences in the attributors’ conversational contexts. Moreover, the context sensitivity involved is traced back to the context sensitivity of the word “know,” which, in turn, is commonly modelled on the case either of genuine indexicals such as “I” or “here” or of comparative adjectives such as “tall” or “rich.” But contextualism faces various problems. I argue that in order to solve these problems we need to look for another account of the context sensitivity involved in knowledge attributions and I sketch an alternative proposal.     

A Labelled Deductive System for Relational Semantics of the Lambek Calculus

We present a labelled version of Lambek Calculus without unit, and we use it to prove a completeness theorem for Lambek Calculus with respect to some relational semantics.