The Relations Among Potentials, Perturbation Analysis, and Markov Decision Processes

This paper provides an introductory discussion for an important concept, the performance potentials of Markov processes, and its relations with perturbation analysis (PA), average-cost Markov decision processes (MDP), Poisson equations, -potentials, the fundamental matrix, and the group inverse of the transition matrix (or the infinitesimal generators). Applications to single sample path-based performance sensitivity estimation and performance optimization are also discussed. On-line algorithms for performance sensitivity estimates and on-line schemes for policy iteration methods are presented. The approach is closely related to reinforcement learning algorithms.     

Fast Online Q(λ)

Q()-learning uses TD()-methods to accelerate Q-learning. The update complexity of previous online Q() implementations based on lookup tables is bounded by the size of the state/action space. Our faster algorithm's update complexity is bounded by the number of actions. The method is based on the observation that Q-value updates may be postponed until they are needed.     

Reinforcement Learning Soccer Teams with Incomplete World Models

We use reinforcement learning (RL) to compute strategies for multiagent soccer teams. RL may profit significantly from world models (WMs) estimating state transition probabilities and rewards. In high-dimensional, continuous input spaces, however, learning accurate WMs is intractable. Here we show that incomplete WMs can help to quickly find good action selection policies. Our approach is based on a novel combination of CMACs and prioritized sweeping-like algorithms. Variants thereof outperform both Q()-learning with CMACs and the evolutionary method Probabilistic Incremental Program Evolution (PIPE) which performed best in previous comparisons.     

From Pre-Historic to Post-Modern Symbolic Model Checking

Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating expressions that represent state sets. Traditionally, symbolic model-checking tools are based on backward state traversal; their basic operation is the function pre, which, given a set of states, returns the set of all predecessor states. This is because specifiers usually employ formalisms with future-time modalities, which are naturally evaluated by iterating applications of pre. It has been shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which, given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only parts of the state space that are reachable from an initial state and relevant for the satisfaction or violation of the specification are explored; that is, errors can be detected as soon as possible.In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation, and the post- calculus is based on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.     

Mechanical procedure for proof construction via closed terms in typed λ calculus

In this paper is presented an algorithm for constructing natural deduction proofs in the propositional intuitionistic and classical logics according to the analogy relating intuitionistic propositional formulas and natural deduction proofs, respectively, to types and terms of simple type theory. Proofs are constructed as closed terms in the simple typed calculus. The soundness and completeness of this method are proved.     

The historical workstation project

Since 1978 research in the development of software dedicated to the specific problems of historical research has been undertaken at the Max-Planck-Institute für Geschichte in Göttingen. From a background of practical experiences during these years, a concept of what an appropriate workstation for an historian would be has been derived. It stresses the necessity of three components: (a) software, derived from a detailed analysis of what differentiates information contained in historical sources from such present in current material, (b) databases which are as easily available as printed books and (c) knowledge bases which allow software and data bases to draw upon the information contained in historical reference works. A loose network of European research projects, dedicated to the realization of such a setup, is described.Manfred Thaller has a Ph.D. (1975) in Modern and Medieval History and held a post-doctoral fellowship in sociology at the Institute for Advanced Studies (Vienna). Since 1978 he has been at the Max-Planck-Institute for History, where he is a research fellow for Historical Information Science.     

More Church–Rosser Proofs

The proofs of the Church–Rosser theorems for , , and reduction in untyped -calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For -reduction, both the standard proof and Takahashi's are given and compared. All proofs are based on a general theory of commutating relations that supports an almost geometric style of reasoning about confluence diagrams.     

The essence of eta-expansion in partial evaluation

Selective eta-expansion is a powerful binding-time improvement,i.e., a source-program modification that makes a partial evaluator yield better results. But like most binding-time improvements, the exact problem it solves and the reason why have not been formalized and are only understood by few.In this paper, we describe the problem and the effect of eta-redexes in terms of monovariant binding-time propagation: eta-redexes preserve the static data flow of a source program by interfacingstatic higher-order values in dynamic contexts anddynamic higher-order values in static contexts. They contribute to twodistinct binding-time improvements.We present two extensions of Gomard's monovariant binding-time analysis for the pure -calculus. Our extensions annotateand eta-expand -terms. The first one eta-expands static higher-order values in dynamic contexts. The second also eta-expands dynamic higher-order values in static contexts.As a significant application, we show that our first binding-time analysis suffices to reformulate the traditional formulation of a CPS transformation into a modern one-pass CPS transformer. This binding-time improvement is known, but it is still left unexplained in contemporary literature,e.g., about cps-based partial evaluation.We also outline the counterpart of eta-expansion for partially static data structures.     

Analysis of local operators applied to discrete tracking problems

This article investigates various local operators in a discrete (1, )-setting applied to tracking problems, a specific class of non-stationary problems. In the first instance, the influence of operator properties on the tracking performance is examined. Both the enforcement of bigger steps and, especially, directed mutations are found to increase the tracking accuracy considerably. For the examination of highly time restricted problems, a correlation between the population size and the severity of the problem dynamics is assumed. Relatively large population sizes are found to be advantageous if the number of evaluations has a big influence on the severity. All results are obtained using a fixpoint analysis of a worst-case model as well as simulations within a two-dimensional Markov model.     

Modal Pure Type Systems

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.     

The π-Calculus in Direct Style

We introduce a calculus which is a direct extension of both the and the calculi. We give a simple type system for it, that encompasses both Curry's type inference for the -calculus, and Milner's sorting for the -calculus as particular cases of typing. We observe that the various continuation passing style transformations for -terms, written in our calculus, actually correspond to encodings already given by Milner and others for evaluation strategies of -terms into the -calculus. Furthermore, the associated sortings correspond to well-known double negation translations on types. Finally we provide an adequate CPS transform from our calculus to the -calculus. This shows that the latter may be regarded as an assembly language, while our calculus seems to provide a better programming notation for higher-order concurrency. We conclude by discussing some alternative design decisions.     

Computing with Contexts

We investigate a representation of contexts, expressions with holes in them, that enables them to be meaningfully transformed, in particular -converted and -reduced. In particular we generalize the set of -expressions to include holes, and on these generalized entities define -reduction (i.e., substitution) and filling so that these operations preserve -congruence and commute. The theory is then applied to allow the encoding of reduction systems and operational semantics of call-by-value calculi enriched with control, imperative and concurrent features.     

Reduction and unification in lambda calculi with a general notion of subtype

Reduction, equality, and unification are studied for a family of simply typed -calculi with subtypes. The subtype relation is required to relate base types only to base types and to satisfy some order-theoretic conditions. Constants are required to have a least type, that is, no overloading. We define the usual and a subtype-dependent -reduction. These are related to a typed equality relation and shown to be confluent in a certain sense. We present a generic algorithm for preunification modulo -conversion and an arbitrary subtype relation. Furthermore it is shown that unification with respect to any subtype relation is universal.     

Formal Foundations of Operational Semantics

In this paper we report on the results of a sophisticated and substantial use of PVS to establish a recent result in operational semantics. The result we establish is a context lemma for operational equivalence for very wide class of programming languages, known as the CIU theorem. The proof uses the annotated holes technique to represent contexts and compute with them. Thus this paper demonstrates that that it is possible to use PVS as a tool in the development of modern operational techniques, and a productive tool at that. The process of formalizing the CIU theorem revealed several gaps in published proof. The proof of the CIU theorem in PVS took approximately six months to develop. The actual machine checked proof involves the proving of around one thousand facts, and takes PVS slightly less than three hours of CPU time running on a Linux machine configured with 2 GBytes of main memory and four 550 MHz Xeon PIII processors.     

Global culture, local cultures and the internet: The Thai example

This paper addresses the questions of whether and, if so, how and to what extent the Internet brings about homogenisation of local cultures in the world. It examines a particular case, that of Thai culture, through an investigation and interpretation of a Usenet newsgroup, soc.culture.thai. Two threads of discussion in the newsgroup are selected. One deals with criticisms of the Thai government and political leaders, and the other focuses on whether the Thai language should be a medium, or perhaps the only medium, of communication in the newsgroup. It is found that, instead of erasing local cultural boundaries, creating a worldwide monolithic culture, the Internet reduplicates the existing cultural boundaries. What the Internet does, on the contrary, is to create an umbrella cosmopolitan culture which is necessary for communication among people from disparate cultures. That culture, however, is devoid of thick backgrounds, in Michael Walzer's sense.     

A predicate transformer for the progress property ‘to-always’

The temporal property to-always has been proposed for specifying progress properties of concurrent programs. Although the to-always properties are a subset of the leads-to properties for a given program, to-always has more convenient proof rules and in some cases more accurately describes the desired system behavior. In this paper, we give a predicate transformerwta, derive some of its properties, and use it to define to-always. Proof rules for to-always are derived from the properties ofwta. We conclude by briefly describing two application areas, nondeterministic data flow networks and self-stabilizing systems where to-always properties are useful.     

Reasoning about programs in continuation-passing style

Plotkin's _v -calculus for call-by-value programs is weaker than the -calculus for the same programs in continuation-passing style (CPS). To identify the call-by-value axioms that correspond to on CPS terms, we define a new CPS transformation and an inverse mapping, both of which are interesting in their own right. Using the new CPS transformation, we determine the precise language of CPS terms closed under -transformations, as well as the call-by-value axioms that correspond to the so-called administrative -reductions on CPS terms. Using the inverse mapping, we map the remaining and equalities on CPS terms to axioms on call-by-value terms. On the pure (constant free) set of -terms, the resulting set of axioms is equivalent to Moggi's computational -calculus. If the call-by-value language includes the control operatorsabort andcall-with-current-continuation, the axioms are equivalent to an extension of Felleisenet al.'s _v -C-calculus and to the equational subtheory of Talcott's logic IOCC.This article is a revised and extended version of the conference paper with the same title [42]. The technical report of the same title contains additional material.The authors were supported in part by NSF grant CCR 89-17022 and by Texas ATP grant 91-003604014.     

Unchecked Exceptions Can Be Strictly More Powerful Than Call/CC

We demonstrate that in the context of statically-typed purely-functional lambda calculi without recursion, unchecked exceptions (e.g., SML exceptions) can be strictly more powerful than call/cc. More precisely, we prove that a natural extension of the simply-typed lambda calculus with unchecked exceptions is strictly more powerful than all known sound extensions of Girard's F (a superset of the simply-typed lambda calculus) with call/cc.This result is established by showing that the first language is Turing complete while the later languages permit only a subset of the recursive functions to be written. We show that our natural extension of the simply-typed lambda calculus with unchecked exceptions is Turing complete by reducing the untyped lambda calculus to it by means of a novel method for simulating recursive types using unchecked-exception–returning functions. The result concerning extensions of F with call/cc stems from previous work of the author and Robert Harper.     

Integration of parametric and “ad hoc” second order polymorphism in a calculus with subtyping

In this paper we define an extension ofF [CUG92] to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit parametric polymorphism ofF by an explicit ad hoc polymorphism (according the classification of [Str67]). We prove that the calculus we obtain, calledF ^& , enjoys the properties of Church-Rosser and Subject Reduction and that its proof system is coherent. We also define a significant subcalculus for which the subtyping is decidable. This extension has not only a logical interest but it is strongly motivated by the foundation of a broadly used programming style: object-oriented programming. The connections betweenF ^& and object-oriented languages are widely stressed, and the modelling byF ^& of some features of the object-oriented style is described, continuing the work of [CGL96].Part of this work has appeared under the title F ^& : integrating parametric and ad hoc second order polymorphism in the 4th International Workshop on Database Programming Languages. New York City, August 1993.The author was supported by grant n. 203.01.56 of the Consiglio Nazionale delle Ricerche-Comitato Nazionale delle Scienze Matematiche to work at LIENS.     

Verifying programs in the calculus of inductive constructions

This paper deals with a particular approach to the verification of functional programs. A specification of a program can be represented by a logical formula [Con86, NPS90]. In a constructive framework, developing a program then corresponds to proving this formula. Given a specification and a program, we focus on reconstructing a proof of the specification whose algorithmic contents corresponds to the given program. The best we can hope is to generate proof obligations on atomic parts of the program corresponding to logical properties to be verified. First, this paper studies a weak extraction of a program from a proof that keeps track of intermediate specifications. From such a program, we prove the determinism of retrieving proof obligations. Then, heuristic methods are proposed for retrieving the proof from a natural program containing only partial annotations. Finally, the implementation of this method as a tactic of theCoq proof assistant is presented.This research was partly supported by ESPRIT Basic Research Action Types for Proofs and Programs and by Programme de Recherche Coordonnes and CNRS Groupement de Recherche Programmation.