A Finite Equational Axiomatization of the Functional Algebras for the Lambda Calculus

A lambda theory satisfies an equation between contexts, where a context is aλ-term with some “holes” in it, if all the instances of the equation fall within the lambda theory. In the main result of this paper it is shown that the equations (between contexts) valid in every lambda theory have an explicit finite equational axiomatization. The variety of algebras determined by the above equational theory is characterized as the class of isomorphic images of functional lambda abstraction algebras. These are algebras of functions and naturally arise as the “coordinatizations” of environment models or lambda models, the natural combinatory models of the lambda calculus. The main result of this paper is also applied to obtain a completeness theorem for the infinitary lambda calculus recently introduced by Berarducci.     

A Measurement-Theoretic Axiomatization of Trapezoidal Membership Functions

In many applications of fuzzy set theory, the membership of an object is not defined directly. One of its attributes (like height, age, weight, etc.) is first mapped to a real number (often by means of a physical instrument) and a parametric function then maps this real number to a membership degree in some fuzzy set (like "tall," "old," "heavy," etc.). A very common parametric function is the trapezoidal one. This paper presents some conditions guaranteeing the existence of such a trapezoidal membership function representing the knowledge of an expert. Further experimental research is needed for testing whether these conditions are satisfied by human agents     

A Complete Axiomatization of Finite-state ACSR Processes

A real-time process algebra, called ACSR, has been developed to facilitate the specification and analysis of real-time systems. ACSR supports synchronous timed actions and asynchronous instantaneous events. Timed actions are used to represent the usage of resources and to model the passage of time. Events are used to capture synchronization between processes. To be able to specify real-time systems accurately, ACSR supports a notion of priority that can be used to arbitrate among timed actions competing for the use of resources and among events that are ready for synchronization. In addition to operators common to process algebra, ACSR includes the scope operator, which can be used to model timeouts and interrupts. Equivalence between ACSR terms is based on the notion of strong bisimulation. This paper briefly describes the syntax and semantics of ACSR and then presents a set of algebraic laws that can be used to prove equivalence of ACSR processes. The contribution of this paper is the soundness and completeness proofs of this set of laws. The completeness proof is for finite-state ACSR processes, which are defined to be processes without free variables under parallel operator or scope operator.     

A Formal Axiomatization for Alphabet Reasoning with Parametrized Processes

In the process-algebraic verification of systems with three or more components put in parallel, alphabet axioms are considered to be useful. These are rules that exploit the information about the alphabets of the processes involved. The alphabet of a process is the set of actions it can perform. In this paper, we extend μCRL (a formal proof system for ACP_τ + data) with such axioms. The alphabet axioms that are added to the proof theory are completely formal and therefore highly suited for computer-checked verification. This is new compared to previous papers where the formulation of alphabet axioms relies for a considerable amount on informal data parameters and implicit (infinite) set theory. Received April 1995 / Accepted in revised form March 1998     

A Thorough Axiomatization of a Principle of Conditional Preservation in Belief Revision

Although the crucial role of if-then-conditionals for the dynamics of knowledge has been known for several decades, they do not seem to fit well in the framework of classical belief revision theory. In particular, the propositional paradigm of minimal change guiding the AGM-postulates of belief revision proved to be inadequate for preserving conditional beliefs under revision. In this paper, we present a thorough axiomatization of a principle of conditional preservation in a very general framework, considering the revision of epistemic states by sets of conditionals. This axiomatization is based on a nonstandard approach to conditionals, which focuses on their dynamic aspects, and uses the newly introduced notion of conditional valuation functions as representations of epistemic states. In this way, probabilistic revision as well as possibilistic revision and the revision of ranking functions can all be dealt with within one framework. Moreover, we show that our approach can also be applied in a merely qualitative environment, extending AGM-style revision to properly handling conditional beliefs.     

An Equational Axiomatization for Multi-exit Iteration

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the form wherenis a positive integer and theP_iand theQ_iare process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA*). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA*. An expressiveness hierarchy for the family ofk-exit iteration operators proposed by Bergstra, Bethke, and Ponse is also offered.     

Cut-Rule Axiomatization of the Syntactic Calculus NL0

An axiomatics of the product-free syntactic calculus L ofLambek has been presented whose only rule is the cut rule. It was alsoproved that there is no finite axiomatics of that kind. The proofs weresubsequently simplified. Analogous results for the nonassociativevariant NL of L were obtained by Kandulski. InLambek's original version of the calculus, sequent antecedents arerequired to be nonempty. By removing this restriction, we obtain theextensions L ₀ and NL ₀ ofL and NL, respectively. Later, the finiteaxiomatization problem for L ₀ andNL ₀ was partially solved, viz., for formulas withoutleft (or, equivalently, right) division and an (infinite) cut-ruleaxiomatics for the whole of L ₀ has been given. Thepresent paper yields an analogous axiomatics forNL ₀. Like in the author's previous work, the notionof rank of an axiom is introduced which, although inessentialfor the results given below, may be useful for the expectednonfinite-axiomatizability proof.     

Cut-Rule Axiomatization of the Syntactic Calculus L0

In Zielonka (1981a, 1989), I found an axiomatics for the product-free calculus L of Lambek whose only rule is the cut rule. Following Buszkowski (1987), we shall call such an axiomatics linear. It was proved that there is no finite axiomatics of that kind. In Lambek's original version of the calculus (cf. Lambek, 1958), sequent antecedents are non empty. By dropping this restriction, we obtain the variant L ₀ of L. This modification, introduced in the early 1980s (see, e.g., Buszkowski, 1985; Zielonka, 1981b), did not gain much popularity initially; a more common use of L ₀ has only occurred within the last few years (cf. Roorda, 1991: 29). In Zielonka (1988), I established analogous results for the restriction of L ₀ to sequents without left (or, equivalently, right) division. Here, I present a similar (cut-rule) axiomatics for the whole of L ₀. This paper is an extended, corrected, and completed version of Zielonka (1997). Unlike in Zielonka (1997), the notion of rank of an axiom is introduced which, although inessential for the results given below, may be useful for the expected non-finite-axiomatizability proof. The paper follows the same way of subject exposition as Zielonka (2000) but it is technically much less complicated. I restrict myself to giving bare results; all the ideological background is exactly the same as in case of the non-associative calculusNL ₀ and those who are interested in it are requested to consult the introductory section of Zielonka (2000). This revised version was published online in August 2006 with corrections to the Cover Date.     

Axiomatization of the Evolution of XML Database Schema

Database schema consists of constructs that model relationships between its entities. Changes made to the schema with time are called the schema evolution. An axiomatic model of the XML database schema is suggested that automatically maintains its integrity when basic changes are made to the schema. A classification of changes is described.     

An Equational Axiomatization of Dynamic Negation and Relational Composition

We consider algebras on binary relations with two main operators: relational composition and dynamic negation. Relational composition has its standard interpretation, while dynamic negation is an operator familiar to students of Dynamic Predicate Logic (DPL) (Groenendijk and Stokhof, 1991): given a relation R its dynamic negation R is a test that contains precisely those pairs (s,s) for which s is not in the domain of R. These two operators comprise precisely the propositional part of DPL.This paper contains a finite equational axiomatization for these dynamic relation algebras. The completenessresult uses techniques from modal logic. We also lookat the variety generated by the class of dynamic relation algebras and note that there exist nonrepresentable algebras in this variety, ones which cannot be construedas spaces of relations. These results are also proved for an extension to a signature containing atomic tests and union.     

Metrics for weighted transition systems: Axiomatization and complexity

Simulation distances are essentially approximations of simulation which provide a measure of the extent by which behaviors in systems are inequivalent. In this paper, we consider the general quantitative model of weighted transition systems, where transitions are labeled with elements of a finite metric space. We study the so-called point-wise and accumulating simulation distances which provide extensions to the well-known Boolean notion of simulation on labeled transition systems.We introduce weighted process algebras for finite and regular behavior and offer sound and (approximate) complete inference systems for the proposed simulation distances. We also settle the algorithmic complexity of computing the simulation distances.     

Axiomatization and conditions for neighborhoods in a covering to form a partition

In this paper, we study the axiomatic issue of a type of covering upper approximation operations. This issue was proposed as an open problem. We also further some known results by using only a single covering approximation operator to characterize the conditions for neighborhood {N(x): x ∈ U} to form a partition of universe U.     

A Finite Soluble Quotient Algorithm

An algorithm for computing power conjugate presentations for finite soluble quotients of predetermined structure of finitely presented groups is described. Practical aspects of an implementation are discussed.