Towards a computation system based on set theory

An axiomatic theory of sets and rules is formulated, which permits the use of sets as data structures and allows rules to operate on rules, numbers, or sets. We might call it a “polymorphic set theory”. Our theory combines the λ-calculus with traditional set theories. A natural set-theoretic model of the theory is constructed, establishing the consistency of the theory and bounding its proof-theoretic strength, and giving in a sense its denotational semantics. Another model, a natural recursion-theoretic model, is constructed, in which only recursive operations from integers to integers are represented, even though the logic can be classical. Some related philosophical considerations on the notions of set, type, and data structure are given in an appendix.     

Constructive Hypervolume Modeling

This paper deals with modeling point sets with attributes. A point set in a geometric space of an arbitrary dimension is a geometric model of a real/abstract object or process under consideration. An attribute is a mathematical model of an object property of arbitrary nature (material, photometric, physical, statistical, etc.) defined at any point of the point set. We provide a brief survey of different modeling techniques related to point sets with attributes. It spans such different areas as solid modeling, heterogeneous objects modeling, scalar fields or “implicit surface” modeling and volume graphics. Then, on the basis of this survey we formulate requirements to a general model of hypervolumes (multidimensional point sets with multiple attributes). A general hypervolume model and its components such as objects, operations, and relations are introduced and discussed. A function representation (FRep) is used as the basic model for the point set geometry and attributes represented independently using real-valued scalar functions of several variables. Each function defining the geometry or an attribute is evaluated at the given point by a procedure traversing a constructive tree structure with primitives in the leaves and operations in the nodes of the tree. This reflects the constructive nature of the symmetric approach to modeling geometry and associated attributes in multidimensional space. To demonstrate a particular application of the proposed general model, we consider in detail the problem of texturing, introduce a model of constructive hypervolume texture, and then discuss its implementation, as well as the special modeling language we used for modeling hypervolume objects.     

On the cardinal number of complete sets of Boolean operations†

It is shown in the literature (using the Post—Yablonsky theorem) that a complete set of Boolean operations cannot have a cardinal number greater than four. It is the object of this paper to improve this bound and prove that a complete set can have a cardinal number of at most three or, in other words, there does not exist a complete (non–redundant) set of more than three Boolean operations. The proof given here is constructive, using the Post—Yablonsky theorem, truth tables and combinatorial set theory.     

Intuitionistic general fuzzy automata

In this paper, by considering the notions of general fuzzy automata, admissible relation, admissible partition and intuitionistic fuzzy set based on the Atanassov (Fuzzy Sets Syst 20(1):87–96, 1986), we define the concepts intuitionistic general fuzzy automaton (IGFA), max–min intuitionistic general fuzzy automaton, admissible relation for the IGFA, admissible partition for the IGFA, quotient IGFA and language for an IGFA. In particular, a connection between the admissible partition and the quotient IGFA is presented and it is shown that any quotient of a given IGFA and the IGFA itself has the same language. Also, using the above notions, some related theorems are proved and, finally, some examples are given to clarify these new notions.     

Combining Sets with Cardinals

We introduce a quantifier-free set-theoretic language for combining sets with elements in the presence of the cardinality operator. We prove that the language is decidable by providing a combination method specifically tailored to the combination domain of sets, cardinal numbers, and elements. Our method uses as black boxes a decision procedure for the elements and a decision procedure for cardinal numbers. To be correct, our method requires that the theory of elements be stably infinite. However, we show that if we restrict set variables to range over finite sets only, then one can modify our method so that it works even when the theory of the elements is not stably infinite.     

Recognizability,hypergraph operations,and logical types

We study several algebras of graphs and hypergraphs and the corresponding notions of equational sets and recognizable sets. We generalize and unify several existing results which compare the associated equational and recognizable sets. The basic algebra on relational structures is based on disjoint union and quantifier-free definable operations. We expand it to an equivalent one by adding operations definable with “few quantifiers”, i.e., operations that take into account local information about elements or tuples. We also consider monadic second-order transductions and we prove that the inverse image of a recognizable set under such a transduction is recognizable.     

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.     

Sur la Structure de l'Ensemble d'Accessibilité de Certains Systèmes: Application à l'Equivalence des Systèmes

For a large class of systems, the interior of the closure of the accessibility set from a point is the interior of this set. As a consequence, equivalent systems, in the Jurdjevic—Kupka's sense, have the same interior and the same boundary for their accessibility sets. This result is used to prove a conjecture of L. R. Hunt.     

Continuous operations on languages

Most of the operations of interest in language theory arecontinuous in a certain technical sense. For such operations, there always exist infinite sets of languages that areindependent in the sense that no language in such a set can be generated from the other languages in the set by the operations in question.     

Aspects as Modular Language Extensions

Extensible programming languages and their compilers use highly modular specifications of languages and language extensions that allow a variety of different language feature sets to be easily imported into the programming environment by the programmer. Our model of extensible languages is based on higher-order attribute grammars and an extension called “forwarding” that mimics a simple rewriting process. It is designed so that no additional attribute definitions need to be written when combining a language with language extensions. Thus, programmers can remain unaware of the underlying attribute grammars when building customized languages by importing various extensions. In this paper we show how aspects and the aspect weaving process from Aspect-Oriented Programming can be specified as a modular language extension and imported into a base language specified in an extensible programming language framework.     

Regular algebra applied to language problems

Many functions on context-free languages can be expressed in the form of the least fixed point of a function whose definition mimics the grammar of the given language. Examples include the function returning the length of the shortest word in a language, and the function returning the smallest number of edit operations required to transform a given word into a word in a language.This paper presents the basic theory that explains when a function on a context-free language can be defined in this way. It is shown how the theory can be applied in a methodology for programming the evaluation of such functions.Specific results include a novel definition of a regular algebra focusing on the existence of so-called “factors”, and several constructions of non-trivial regular algebras. Several challenging problems are given as examples, some of which are old and some of which are new.     

Cardinal Consistency of Reciprocal Preference Relations: A Characterization of Multiplicative Transitivity

Consistency of preferences is related to rationality, which is associated with the transitivity property. Many properties suggested to model transitivity of preferences are inappropriate for reciprocal preference relations. In this paper, a functional equation is put forward to model the “cardinal consistency in the strength of preferences” of reciprocal preference relations. We show that under the assumptions of continuity and monotonicity properties, the set of representable uninorm operators is characterized as the solution to this functional equation. Cardinal consistency with the conjunctive representable cross ratio uninorm is equivalent to Tanino's multiplicative transitivity property. Because any two representable uninorms are order isomorphic, we conclude that multiplicative transitivity is the most appropriate property for modeling cardinal consistency of reciprocal preference relations. Results toward the characterization of this uninorm consistency property based on a restricted set of $(n-1)$ preference values, which can be used in practical cases to construct perfect consistent preference relations, are also presented.      

On the Communication Complexity of Multilateral Trading: Extended Report

We study the complexity of a multilateral negotiation framework, where autonomous agents agree on a sequence of deals to exchange sets of discrete resources in order to both further their own goals and to achieve a distribution of resources that is socially optimal. When analysing such a framework, we can distinguish different aspects of complexity: How many deals are required to reach an optimal allocation of resources? How many communicative exchanges are required to agree on one such deal? How complex a communication language do we require? And finally, how complex is the reasoning task faced by each agent?“This revised version was published online in June 2005 with corrections to the capitalization of authors’ names.”     

Minimality in template-guided recombination

Ciliates are unicellular organisms, some of which perform complicated rearrangements of their DNA. Template-guided recombination (TGR) is a formal model for the DNA recombination which occurs in ciliates. TGR has been the subject of much research in formal language theory, as it can be viewed as an operation on formal languages. In TGR, a set of templates serves as a parameter to a language operation which controls which rearrangements can take place; thus, a set of templates is itself a language.Recently, the concept of equivalence in TGR has been considered: given two sets of templates, do they define the same language operation? This paper considers the related question of minimality: given a set of templates T, what is the smallest set of templates (with respect to inclusion) equivalent to T? We show that the minimal set of templates is unique, and consider closure properties and decidability questions related to minimality. We define an operational characterization for equivalence which is useful for results on minimality.     

Abstract Regular Tree Model Checking

Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word or tree automata, and operations of the systems being examined as finite word or tree transducers. The reachability set is then computed by a repeated application of the transducers on the automata representing the currently known set of reachable configurations. In order to facilitate termination of RMC, various acceleration schemas have been proposed. One of them is a combination of RMC with the abstract-check-refine paradigm yielding the so-called abstract regular model checking (ARMC). ARMC has originally been proposed for word automata and transducers only and thus for dealing with systems with linear (or easily linearisable) structure. In this paper, we propose a generalisation of ARMC to the case of dealing with trees which arise naturally in a lot of modelling and verification contexts. In particular, we first propose abstractions of tree automata based on collapsing their states having an equal language of trees up to some bounded height. Then, we propose an abstraction based on collapsing states having a non-empty intersection (and thus “satisfying”) the same bottom-up tree “predicate” languages. Finally, we show on several examples that the methods we propose give us very encouraging verification results.     

Characterization of rough set approximations in Atanassov intuitionistic fuzzy set theory

The primitive notions in rough set theory are lower and upper approximation operators defined by a fixed binary relation and satisfying many interesting properties. Many types of generalized rough set models have been proposed in the literature. This paper discusses the rough approximations of Atanassov intuitionistic fuzzy sets in crisp and fuzzy approximation spaces in which both constructive and axiomatic approaches are used. In the constructive approach, concepts of rough intuitionistic fuzzy sets and intuitionistic fuzzy rough sets are defined, properties of rough intuitionistic fuzzy approximation operators and intuitionistic fuzzy rough approximation operators are examined. Different classes of rough intuitionistic fuzzy set algebras and intuitionistic fuzzy rough set algebras are obtained from different types of fuzzy relations. In the axiomatic approach, an operator-oriented characterization of rough sets is proposed, that is, rough intuitionistic fuzzy approximation operators and intuitionistic fuzzy rough approximation operators are defined by axioms. Different axiom sets of upper and lower intuitionistic fuzzy set-theoretic operators guarantee the existence of different types of crisp/fuzzy relations which produce the same operators.     

Proving properties of Pascal programs in MIZAR 2

Summary In this paper we present the so called natural semantics for a subset of Pascal programming language. A set of sentences of first order predicate calculus defines the meaning of the Pascal language constructs. The meaning of a specific program is defined separately by another set of sentences which can be generated automatically. Both these sets together constitute axiomatics of a theory, called the theory of a specific program. The axiomatics is built in such a way that its logical consequences describe all the computational processes defined by the program. Proofs of properties for two small programs are discussed in detail. These properties and their proofs are recorded in the MIZAR 2 language — a computer formalization of predicate calculus. MIZAR 2 proof checker was used to verify the proofs.