A Calculus of Terms for Coalgebras of Polynomial Functors

A syntax and semantics of types, terms and formulas for coalgebras of polynomial functors is developed, extending earlier work [4] on monomial coalgebras to include functors constructed using coproducts. A modified ultrapower construction for polynomial coalgebras is introduced, adapting the conventional ultrapower to retain only those states that evaluate observable terms in a standard way.A special role is played by terms that take observable values and are “rigid”: their free variables do not occur in any state-valued subterm. The following “co-Birkhoff” theorem is proved: a class of polynomial coalgebras is definable by Boolean combinations of equations between rigid terms iff the class is closed under disjoint unions, images of bisimulations, and observable ultrapowers.     

Probabilistic π-Calculus and Event Structures

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event structures. The key technical point is a use of types to identify a good class of non-deterministic probabilistic behaviours which can preserve a compositionality of the parallel operator in the event structures and the calculus. We show an operational correspondence between the two semantics. This allows us to prove a “probabilistic confluence” result, which generalises the confluence of the linearly typed π-calculus.     

Expressing Priorities and External Probabilities in Process Algebra via Mixed Open/Closed Systems

Defining operational semantics for a process algebra is often based either on labeled transition systems that account for interaction with a context or on the so-called reduction semantics: we assume to have a representation of the whole system and we compute unlabeled reduction transitions (leading to a distribution over states in the probabilistic case). In this paper we consider mixed models with states where the system is still open (towards interaction with a context) and states where the system is already closed. The idea is that (open) parts of a system “P” can be closed via an operator “P↑G” that turns already synchronized actions whose “handle” is specified inside “G” into prioritized reduction transitions (and, therefore, states performing them into closed states). We show that we can use the operator “P↑G” to express multi-level priorities and external probabilistic choices (by assigning weights to handles inside G), and that, by considering reduction transitions as the only unobservable τ transitions, the proposed technique is compatible, for process algebra with general recursion, with both standard (probabilistic) observational congruence and a notion of equivalence which aggregates reduction transitions in a (much more aggregating) trace based manner. We also observe that the trace-based aggregated transition system can be obtained directly in operational semantics and we present the “aggregating” semantics. Finally, we discuss how the open/closed approach can be used to also express discrete and continuous (exponential probabilistic) time and we show that, in such timed contexts, the trace-based equivalence can aggregate more with respect to traditional lumping based equivalences over Markov Chains.     

No-Longer-Foreign: Teaching an ML compiler to speak C “natively”

We present a new foreign-function interface for SML/NJ. It is based on the idea of data-level interoperability—the ability of ML programs to inspect as well as manipulate C data structures directly.The core component of this work is an encoding of the almost² complete C type system in ML types. The encoding makes extensive use of a “folklore” typing trick, taking advantage of ML's polymorphism, its type constructors, its abstraction mechanisms, and even functors. A small low-level component which deals with C struct and union declarations as well as program linkage is hidden from the programmer's eye by a simple program-generator tool that translates C declarations to corresponding ML glue code.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

Towards coalgebraic behaviourism

In this paper we show that it is possible to model observable behaviour of coalgebras independently from their internal dynamics, but within the general framework of representing behaviour by a map into a “final” coalgebra.In the first part of the paper we characterise Set-endofunctors F with the property that bisimilarity of elements of F-coalgebras coincides with having the same observable behaviour. We show that such functors have the final coalgebra of a rather simple nature, and preserve some weak pullbacks. We also show that this is the case if and only if F-bisimilarity corresponds to logical equivalence in the finitary fragment of the coalgebraic logic.In the second part of the paper, we present a construction of a “final” coalgebra that captures the observable behaviour of F-coalgebras. We keep the word “final” quoted since the object we are going to construct need not belong to the original category. The construction is carried out for arbitrary Set-endofunctor F, throughout the construction we remain in Set, but the price to pay is the introduction of new morphisms. The paper concludes with a hint to a possible application to modelling weak bisimilarity for coalgebras.     

Context, situations, and design agents

The terms “context” and “situation” are often used interchangeably or to denote a variety of concepts. This paper aims to show that these are two different but related concepts and it reifies their difference within the framework of design agents. The external world of an agent is described as the aggregation of all entities that the agent could possibly sense or effect, where context is from its external world that an agent interacts with and is aware of. The interpreted world of an agent is described in terms of the experiences of that agent, where situations are processes that direct how interactive experiences proceed. Situations determine what part of the external world are in the current context, and situations influence interaction and so influence what and how common ground is acquired.     

Extensional PERs

A class of Partial Equivalence Relations (PERs) is described such that the resulting full subcategory of the realizability universe has the expected properties of a good category of CPOs; that is, it is a Cartesian closed category and every endomorphism has a canonical fixed point. Moreover, the reflection functor into the subcategory of strict maps (usually called the “lifting operation”) yields a good notion of “partial map,” a necessary condition if one wishes to maintain a connection between strict maps and partial maps. It is shown that all functors that arise in practice have canonical invariant objects; hence a host of domain equations are guaranteed to have solutions.     

Completeness of Continuation Models for λμ-Calculus

We show that a certain simple call-by-name continuation semantics of Parigot's λ_μ-calculus is complete. More precisely, for every λ_μ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λ_μ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λ_μ-category in the sense of L. Ong (1996, in “Proceedings of LICS '96,” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation,” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λ_μ developed by C.-H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997,” Assoc. Comput. Mach. Press, New York).     

prialt in Handel-C: an operational semantics

We describe an operational semantics for the hardware compilation language Handel-C [7], which is a C-like language with channel communication and parallel constructs which compiles down to mainly synchronously clocked hardware. The work in this paper builds on previous work describing the semantics of the “prialt” construct within Handel-C [5] and a denotational semantics for part of the language [6]. We describe a key subset of the language and show how a design decision for the real language, namely that default guards in a prialt statement executed in “zero-time”, has consequences for the complexity of the operational semantics. We present the operational semantics, along with a revised and completed prialt semantics, indicating clearly the interface between them. We then describe a notion of observational equivalence and present an example illustrating how we handle the complexity of nested prialts in default guards.     

Process expressions and Hoare's logic: Showing an irreconcilability of context-free recursion with Scott's induction rule

In this paper processes specifiable over a non-uniform language are considered. The language contains constants for a set of atomic actions and constructs for alternative and sequential composition. Furthermore it provides a mechanism for specifying processes recursively (including nested recursion). We consider processes as having a state: atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. Any process having some initial state can be associated with a transition system representing all possible courses of execution. This leads to an operational semantics in the style of Plotkin. The partial correctness assertion {α} p{β} expresses that for any transition system associated with the process p and having some initial state satisfying α, its final states representing successful execution satisfy β. A logic in the style of Hoare, containing a proof system for deriving partial correctness assertions, is presented. This proof system is sound and relatively complete, so any partial correctness assertion can be evaluated by investigating its derivability. Included is a short discussion about the extension of the process language with “guarded recursion”. It appears that such an extension violates the completeness of the Hoare logic. This reveals a remarkable property of Scott's induction rule in the context of non-determinism: only regular recursion allows a completeness result.     

The information processing explanation of Gestalt phenomena

Gestalt psychology has shown the importance in human thinking and problem solving of the behavior that it labels “intuition,” “insight,” and “understanding.” This paper discusses computer programs, already described in the published literature, that stimulate exactly these kinds of behaviors. It is shown that much of what has been discussed under the heading of “insight” can be explained in terms of recognition processes that are readily simulated. Computer simulation has shown itself a powerful tool for interpreting and explaining a wide range of phenomena associated with the kinds of thinking and understanding that have been so usefully emphasized in the Gestalt literature.     

Fuzzy functions with LSE

“Fuzzy Functions” are proposed to be determined by the least squares estimation (LSE) technique for the development of fuzzy system models. These functions, “Fuzzy Functions with LSE” are proposed as alternate representation and reasoning schemas to the fuzzy rule base approaches. These “Fuzzy Functions” can be more easily obtained and implemented by those who are not familiar with an in-depth knowledge of fuzzy theory. Working knowledge of a fuzzy clustering algorithm such as FCM or its variations would be sufficient to obtain membership values of input vectors. The membership values together with scalar input variables are then used by the LSE technique to determine “Fuzzy Functions” for each cluster identified by FCM. These functions are different from “Fuzzy Rule Base” approaches as well as “Fuzzy Regression” approaches. Various transformations of the membership values are included as new variables in addition to original selected scalar input variables; and at times, a logistic transformation of non-scalar original selected input variables may also be included as a new variable. A comparison of “Fuzzy Functions-LSE” with Ordinary Least Squares Estimation (OLSE)” approach show that “Fuzzy Function-LSE” provide better results in the order of 10% or better with respect to RMSE measure for both training and test cases of data sets.     

Towards an algebraic theory of information integration

Information integration systems provide uniform interfaces to varieties of heterogeneous information sources. For query answering in such systems, the current generation of query answering algorithms in local-as-view (source-centric) information integration systems all produce what has been thought of as “the best obtainable” answer, given the circumstances that the source-centric approach introduces incomplete information into the virtual global relations. However, this “best obtainable” answer does not include all information that can be extracted from the sources because it does not allow partial information. Neither does the “best obtainable” answer allow for composition of queries, meaning that querying a result of a previous query will not be equivalentto the composition of the two queries. In this paper, we provide a foundation for information integration, based on the algebraic theory of incomplete information. Our framework allows us to define the semantics of partial facts and introduce the notion of the exact answer—that is the answer that includes partial facts. We show that querying under the exact answer semantics is compositional. We also present two methods for actually computing the exact answer. The first method is tableau-based, and it is a generalization of the “inverse-rules” approach. The second, much more efficient method, is a generalization of the rewriting approach, and it is based on partial containment mappings introduced in the paper.     

Programming with logical queries, bulk updates, and hypotheticalreasoning

The paper presents a language of update programs that integrates logical queries, bulk updates and hypothetical reasoning in a seamless manner. There is no syntactic or semantic distinction between queries and updates. Update programs extend logic programs with negation in both syntax and semantics. They allow bulk updates in which an arbitrary update is applied simultaneously for all answers of an arbitrary query. Hypothetical reasoning is naturally supported by testing the success or failure of an update. We describe an alternating fixpoint semantics of update programs and show that it can express all nondeterministic database transformations     

Subtyping in Logical Form

By using intersection types and filter models we formulate a theory of types for a λ-calculus with record subtyping via a finitary programming logic. Types are interpreted as spaces of filters over a subset of the language of properties (the intersection types) which describes the underlying type free realizability structure. We show that such an interpretation is a PER semantics, proving that the quotient space arising from “logical” PERs taken with the intrinsic ordering is isomorphic to the filter semantics of types.     

Internal reinforcement in a connectionist genetic programming approach

Genetic programming (GP) can learn complex concepts by searching for the target concept through evolution of a population of candidate hypothesis programs. However, unlike some learning techniques, such as Artificial Neural Networks (ANNs), GP does not have a principled procedure for changing parts of a learned structure based on that structure's performance on the training data. GP is missing a clear, locally optimal update procedure, the equivalent of gradient-descent backpropagation for ANNs. This article introduces a new algorithm, “internal reinforcement”, for defining and using performance feedback on program evolution. This internal reinforcement principled mechanism is developed within a new connectionist representation for evolving parameterized programs, namely “neural programming”. We present the algorithms for the generation of credit and blame assignment in the process of learning programs using neural programming and internal reinforcement. The article includes a comprehensive overview of genetic programming and empirical experiments that demonstrate the increased learning rate obtained by using our principled program evolution approach.     

A Practical Approach to Partial Functions in CVC Lite

Most verification approaches assume a mathematical formalism in which functions are total, even though partial functions occur naturally in many applications. Furthermore, although there have been various proposals for logics of partial functions, there is no consensus on which is “the right” logic to use for verification applications. In this paper, we propose using a three-valued Kleene logic, where partial functions return the “undefined” value when applied outside of their domains. The particular semantics are chosen according to the principle of least surprise to the user; if there is disagreement among the various approaches on what the value of the formula should be, its evaluation is undefined. We show that the problem of checking validity in the three-valued logic can be reduced to checking validity in a standard two-valued logic, and describe how this approach has been successfully implemented in our tool, CVC Lite.     

Cooperation without deliberation: A minimal behavior-based approach to multi-robot teams

While terminology and some concepts of behavior-based robotics have become widespread, the central ideas are often lost as researchers try to scale behavior to higher levels of complexity. “Hybrid systems” with model-based strategies that plan in terms of behaviors rather than simple actions have become common for higher-level behavior. We claim that a strict behavior-based approach can scale to higher levels of complexity than many robotics researchers assume, and that the resulting systems are in many cases more efficient and robust than those that rely on “classical AI” deliberative approaches. Our focus is on systems of cooperative autonomous robots in dynamic environments. We will discuss both claims that deliberation and explicit communication are necessary to cooperation and systems that cooperate only through environmental interaction. In this context we introduce three design principles for complex cooperative behavior—minimalism, statelessness and tolerance—and present a RoboCup soccer system that matches the sophistication of many deliberative soccer systems while exceeding their robustness, through the use of strict behavior-based techniques with no explicit communication.