bluuebunny/crossref_metadata_2025 huggingface dataset:
A theorem on the characteristics of non-sequential processes
Authors: Best Eike
Published: May 2021

Real non-sequential processes can be described in a consistent way if they are assumed to satisfy a certain density property. Density as defined in [1] can be interpreted as postulating that a “global state” consists of a “progress snap-shot” of all single activities which constitute it. The present report shows that postulating density amounts to postulating that (a) each single history of a process is either infinite or has a first cause (but not both), and (b) each single future of a process is either infinite or has a last effect (but not both). This result is interpreted and applied to the question of Turing-computability.
Simple EOL forms under uniform interpretation generating CF languages
Authors: Albert Jürgen , Maurer Hermann , Rozenberg Grzegorz
Published: May 2021

In this paper we consider simple EOL forms (forms with a single terminal and single nonterminal) under uniform interpretations. We present a contribution to the analysis of generative power of simple EOL forms by establishing easily decidable necessary and sufficient conditions for simple EOL forms to generate (under uniform interpretations) CF languages only.
HAS-Hierarchy; A natural tool for languae specification
Authors: Rus Teodor
Published: May 2021

This paper is an attempt to direct present-day research in programming language specification and their compiler construction towards a more natural approach. In order to do that, a language is considered for what it is, namely a communication device between systems. In view of this evidence, the first section of the paper develops a framework for the natural specification of language. Section two of the paper develops the HAS-Hierarchy as a device to be used in this natural language specification. Section three of the paper constructs a general model for programming language specification by the HAS-Hierarchy. Section four is devoted to the problem of compiler construction by using the HAS-Hierarchy as a natural tool for programming language specification.
Tree-codifications and convolutional codes
Authors: Atanasiu Adrian
Published: May 2021

The paper deals with some C-grammars and tree-codification properties extending the result in [1]. We try to exhibit new aspects and important results, e.g. that any algebraic convolutional code is a particular case of a tree-code, as well as the finite forms of the code-sets. They can result in new methods of decodification and error correction in the case of convolutional coding.
On intersections of context-free languages
Authors: Gorun Irina
Published: May 2021

Following the suggestion of Prof. S. Marcus we study the “Darboux properties” of the hierarchy of intersections of context-free languages, introduced by Liu and Weiner [5]. Some properties of the Parikh function defined on an intersection of context-free languages are infered. These results are useful in proving that a certain bounded matrix language is not an intersection of context-free languages.
Computational Fortmalism: Abstract Combinatory View-Point and Related First Order Logical Framework
Authors: Manca Vincenzo
Published: May 2021

A natural notion of computational formalism is here characterized by elaborating on the algebraic approach with Uniformly Reflexive Structures. Namely by dealing with the undefined within a first-order theory admitting partial functions. Here, quite generally, we obtain several limitative theorems about the computational formalisms.
Multiple Regularity and Binary ETOL-Systems1
Authors: Danecki Ryszard
Published: May 2021

Closure properties of binary ETOL-languages are investigated by means of multiple tree automata. Decidability of the equivalence problem of deterministic binary ETOL-systems is proved.
On the Semantics of Parallel Programs
Authors: Müldner Tomasz
Published: May 2021

The paper deals with the semantics of parallel programs. It is shown that there exist other semantics besides the well-known one, which reflects multiplexing and is defined as an interleaving of elementary actions. Those semantics are not necessarily equivalent with respect to the input (out-put) relation; moreover, they permit the investigation of the internal behaviour of a computation. A formalized language of parallel programs is defined. Definitions of computational semantics and of a tree of acceptable computations are given. As an example of computational semantics the semantics MULT (for multiplexing) is defined. Next a scheme of computational semantics is introduced. Given the scheme, one can define various computational semantics by means of several strategies. The most natural scheme of computational semantics is then given, followed by examples defined by it. Connections between different classes of computational semantics are examined.
A Logically Justified Model of Computation I
Authors: Miglioli Pierangelo , Ornaghi Mario
Published: May 2021

The aim of this paper is to provide a general explanation of the “algorithmic content” of proofs, according to a point of view adequate to computer science. Differently from the more usual attitude of program synthesis, where the “algorithmic content” is captured by translating proofs into standard algorithmic languages, here we propose a “direct” interpretation of “proofs as programs”. To do this, a clear explanation is needed of what is to be meant by “proof-execution”, a concept which must generalize the usual “program-execution”. In the first part of the paper we discuss the general conditions to be satisfied by the executions of proofs and consider, as a first example of proof-execution, Prawitz’s normalization. According to our analysis, simple normalization is not fully adequate to the goals of the theory of programs: so, in the second section we present an execution-procedure based on ideas more oriented to computer science than Prawitz’s. We provide a soundness theorem which states that our executions satisfy an appropriate adequacy condition, and discuss the sense according to which our “proof-algorithms” inherently involve parallelism and non determinism. The Properties of our computation model are analyzed and also a completeness theorem involving a notion of “uniform evaluation” of open formulas is stated. Finally, an “algorithmic completeness” theorem is given, which essentially states that every flow-chart program proved to be totally correct can be simulated by an appropriate “purely logical proof”.
On the Compilation of Parallel Programs
Authors: Müldner Tomasz
Published: May 2021

The paper examines the properties of a compilation of sequential and parallel programs with respect to computational semantics, defined in the earlier paper of the present author “On the Semantics of Parallel Programs”. A compilation of sequential programs is defined and proved to be stable, i.e. the sets of results of an arbitrary program and the corresponding compiled program coincide. Next, a natural compilation of parallel programs is defined and shown not to be stable with respect to natural semantics: The compiled program may give the results which are not results of the source program. Other semantics are defined and it is proved that in those semantics the given compilation is stable. The main corollary states that for parallel programs with synchronizing tools, a compilation is stable in natural semantics.
Implementation and Properties of Certain Tools for Parallel Computations
Authors: Müldner Tomasz
Published: May 2021

The paper is a continuation of the papers of the present author in which the semantics of parallel programs and several synchronizing tools (e.g. critical regions) for parallel programs were defined. Now, a universal synchronizing tool – a monitor, with delay, continue and delcont instructions, is defined. Then, an implementation of a monitor in the LOGLAN 77 programming language is given and proved to be correct. The implementation is given by means of a LOGLAN type Parallel in such a way that in order to use monitors in the user’s program it is sufficient to prefix that program by the Parallel.
On Partial Languages
Authors: Grabowski Jan
Published: May 2021

The paper studies the behavior of control structures of algorithms designed for (partly) parallel execution. A generalization of Peterson’s computation sequence set, the partial language, is discussed, which reflects the concurrency of events. In particular, the families of partial languages definable by Petri nets and by safe Petri nets are investigated with respect to closedness under certain operations. Trace languages (Mazurkiewicz) and path expressions (Campbell and Habermann) are included in the considerations.
A Remark of the Syntactic Partition
Authors: Rudnicki Piotr , Trybulec Andrzej
Published: May 2021

An analytic investigation of formal languages is of practical value, apart from their description by means of generative grammars. This paper deals with the problem of grouping into classes the vocabulary elements of similar syntactic properties. The introduction of types for variables in programming languages is an example of such a grouping. In [3] a notion of syntactic partition onto sets of words has been defined. We prove below that there is continuum of such partitions.
The Arbiter: An Active System Component for Implementing Synchronizing Primitives
Authors: Goeman Henk J.M.
Published: May 2021

An active system component, the arbiter, is proposed as a system structuring concept for the implementation of synchronizing primitives. The concept is illustrated by showing a new and very simple implementation of the critical section with a busy form of waiting. This implementation will be refined in such a way that it does not need the commonly stated postulate of atomicity, according to which assignments to and inspections of common store locations are indivisible, non interfering, atomic actions. Thus we refute the well-known and widely believed “paradox of the critical region”. The use of the arbiter is further illustrated by showing an implementation of the semaphore operations. These operations are implemented “on top of” the proposed implementation for the critical section, i.e. using the same busy form of waiting to ensure the mutual exclusion of concurrently issued individual semaphore operations. Nevertheless, the proposed implementation explicitly allows a nonbusy form of waiting to result from one of the semaphore operations by means of an interrupt mechanism.
A Classification and Closure Properties of Languages for Describing Concurrent System Behaviours
Authors: Szijártó Miklós
Published: May 2021

The correspondence between sequential program schemes and formal languages is well known (Blikle and Mazurkiewicz (1972), Engelfriet (1974)). The situation is more complicated in the case of parallel program schemes, and trace languages (Mazurkiewicz (1977)) have been introduced to describe them. We introduce the concept of the closure of a language on a so called independence relation on the alphabet of the language, and formulate several theorems about them and the trace languages. We investigate the closedness properties of Chomsky classes under closure on independence relations, and as a special case we derive a new necessary and sufficient condition for the regularity of the commutative closure of a language.
Logic of Effective Definitions
Authors: Tiuryn Jerzy
Published: May 2021

A new logic to deal with properties of algorithmic processes in an abstract structure is proposed. This logic is based on the class of (deterministic) effective definitional schemes. A complete (infinitary) proof system is given. The paper contains among the other results, a “computation” of Hanf number of the above-mentioned logic, which turns out to he unexpectedly high.
A Survey of Normal form Covers for Regular Grammars
Authors: Nijholt Anton
Published: May 2021

An overview is given of cover results for normal forms of regular grammars. Due to the special form of regular grammars and due to the results which are obtained it is sufficient to consider covering grammars in Greibach normal form. Among other things it is proved that any left-regular grammar can be left covered with a context-free grammar in Greibach normal form. All the cover results concerning the left- and right-regular grammars are listed, with respect to several types of covers, in a cover table.
Information Retrieval Systems an Algebraic Approach II
Authors: Raś Zbigniew
Published: May 2021

This paper is the second of the three parts of the work on the information retrieval systems proposed by Salton (see [13]). The system is defined by the notions of a partially ordered set of requests (A, ⩽), the set of documents X and a monotonic retrieval function U : A → 2X. Different conditions imposed on the set A and a function U make it possible to obtain various classes of information retrieval systems. We investigate systems in which (A, ⩽) is a partially ordered set, a lattice, a pseudo-Boolean algebra and a Boolean algebra. In my paper these systems are called partially ordered information retrieval systems (po-systems), lattice information retrieval systems (l-systems), pseudo-Boolean information retrieval systems (pB-systems) and Boolean information retrieval systems (B-systems). The first part concerned po-systems and l-systems. The second part deals with pB-systems and B-systems. In the third part systems with a partial access are investigated. The present part discusses the pB-systems and B-systems. The problems connected with the properties of sets of attributes are investigated. The method of constructing a selective system for a pB-system and a B-system is given. The problem related to the minimalization of systems are investigated.
Nonhomogeneous Stochastic Automata
Authors: Janicki Sławomir
Published: May 2021

In this note we consider a nonhomogeneous Markov chain type stochastic automaton which is a generalization of Bartoszyński’s stochastic automaton. The latter is a generalization of the Pawlak’s known machine in a stochastic direction. By nonhomogeneous stochastic automaton we mean a system ⟨ T, α, {A(n), n ⩾ 1}⟩, where T is a finite nonempty set, α, is an initial distribution on T, and {A(n), n ⩾ 1} is a matrix sequence whose every element is a stochastic matrix called a transition probability matrix. If A(n) = A for all n ⩾ 1, then we obtain Bartoszyński’s automaton. The sequence (ti0, ti1, …), tij ∈ T, j = 0, 1, 2, … is called a word of automata if α(ti0) > 0 and A(k)(tik-1, tik) > 0 for every k ⩾ 1. The goal of this note is to give necessary and sufficient conditions for the existence of an extension and a shrinkage of the automata under consideration. These problems for T, A were considered for the first time by Bartoszyński. The shrinkage problem deals with the existence of a stochastic automaton which generates only all sequences of states of T which are simultaneously generated by two given automata while the extension problem treats of the existence of a stochastic automaton which generates all sequences of states of which are generated by at least one of two given automata. Moreover, we introduce some new notions: attainable state, concordance of automata in a wide and a narrow sense, which help us to solve the problems mentioned above.
Algorithmic Logic with Recursive Functions
Authors: Szałas Andrzej
Published: May 2021

A language is considered in which the reader can express such properties of block-structured programs with recursive functions as correctness and partial correctness. The semantics of this language is fully described by a set of schemes of axioms and inference rules. The completeness theorem and the soundness theorem for this axiomatization are proved.
Regular Extensions of Iterative Algebras and Metric Interpretations
Authors: Bergstra Jan , Tiuryn Jerzy
Published: May 2021

An algebra is said to be iterative if every nontrivial finite system of fixed-point equations has unique solution. The paper discusses possibilities of finding topological structure for a given iterative algebra so that the unique solution of every system S can be approximated by a sequence of elements generated from S.
Automata in Random Environments1
Authors: Gould Jerren
Published: May 2021

In Gould and Wegman (1977), a model of a system located within an environment was introduced in which the transition function of the system is not only related to the present state and input, but also to the present configuration of the environment. In this paper we shall consider the case of automata operating within random environments. In contrast to the previous case, where we suppose we can control the environment, we shall assume that the realization of the environment is governed by some probabilistic structure. Hence, the sequence of environment configurations is a stochastic process. In considering automata in random environments (ARE) there is a dual nature to the randomness, the environment sequence is random and for each value the environment sequence assumes, the probabilistic state transitions are defined. In the ARE case the relative frequency of acceptance of a tape under a fixed random environment sequence estimates the expected acceptance probability. Accordingly, the notion of expected acceptance sets is defined. Finally, a mean equivalent canonical representation for automata in random environments which eliminates the randomness due to the probabilistic state transitions is formulated. That is, for any ARE with finite environment set, deterministic assignment of the initial state, and deterministic transitions which has a state distribution equivalent in the mean. This formulation of automata in random environments is useful when only certain probabilistic assumptions about the occurrence of any environment configuration can be made or when the environment configuration can only be measured by statistical techniques.
Representation Theorems for Terms in a Certain Model for Information Systems
Authors: Reusch Bernd , Szwillus Gerd
Published: May 2021

We study a term-language, which is used by the “Warsaw-School” in an abstract model for information systems. Various normal forms as well as standard expansions with respect to product terms are formulated and proved correct. It is shown that the shortest sums of so-called maximal sub-products are the shortest representations of terms and algorithms for their generation are given.
Complexity of Decompositions of Gödel Numberings
Authors: Schinzel Britta
Published: May 2021

It is shown that each Gödel numbering is effective sum of infinitely many pairwise incomparable Friedberg numberings, the complexity of which set of Friedberg numberings can be of any ordinal type.
Dynamic Information Systems
Authors: Orłowska Ewa
Published: May 2021

A model of information systems such that data depend on a state of the system is introduced. A logic is developed enabling us to define query languages for such systems.
On the Unwinding of Flow-Charts with Stacks
Authors: Urzyczyn Paweł
Published: May 2021

Let A be a structure with the property that every flow-chart with one stack /every recursive schema/, total over A, is strongly equivalent in A to a loop-free schema. We show that every total flow-chart with one stack can be unwound in A.
Maximal Monoids of Normal Form
Authors: Dezani-Ciancaglini Mariangola , Ermine Françoise
Published: May 2021

In this paper, a characterization of the sets of normal forms which are monoids with respect to the composition combinator is obtained as application of the type theory to λ-calculus developed in [5]. The main result is that there is a monoid of normal form which is maximal in the sense that all extensions lead to terms without normal forms.
Metric Iteration Theories
Authors: Troeger Douglas R.
Published: May 2021

It is known that it is possible to impose a metric on the free iteration theory Γtr of Γ-trees such that the iterate f† of any tree f : n → p + n is a limit of of ‘finite approximations’ of f. Since this notion of limiting computation corresponds to our intuitive notion of iteration, it is natural to ask which other theories in the variety generated by Γtr admit such a metric. An algebraic characterization of these theories is presented In this paper.
A Note on Liveness in Generalized Petri Nets
Authors: Sandring Sylvely , Starke Peter H.
Published: May 2021

We introduce the notions of homogeneity of generalized Petri nets and of sufficiently marked place sets which are basic for our generalization of COMMONERs liveness theorem to a subclass of all generalized Petri nots. We show that a corresponding decision problem (the nonsufficiency problem) is equivalent with the reachabllity problem.
A Sufficient Condition for the Consistency of P=NP with Peano Arithmetic
Authors: Kowalczyk Wojciech
Published: May 2021

In this paper we show how the indicators technique due to Paris and Kirby may be used to obtain independence or consistency results in Computer Science. We give an example of a sentence which is independent of PA and we formulate a sufficient condition for the consistency of P=NP with Peano Arithmetic.
Pseudo-Random Monte-Carlo Methods
Authors: Kramosil Ivan
Published: May 2021

In this paper we investigate the Monte-Carlo method for estimation of the unknown probability of a random event on the ground of relative frequencies and under the condition that random sampling is replaced by a deterministic side input producing binary sequences of high algorithmic complexity. It is proved that if this complexity exceeds a treshold value, the sequences may be used in the Monte-Carlo methods instead of random samples as the obtained estimates converge to the estimated probability when the length of these binary sequences increases.
Algorithms with Possibilities of Selflearning and Selfmodification
Authors: Eberbach Eugeniusz
Published: May 2021

This paper concerns a concept of selfperfecting and selflearning of digital computer systems. This idea is not new, but continuously in the state of elaborations. Such systems, i.e. with a possibility of selflearning and selfmodification would have undoubtedly greater possibilities and elastic properties in their behaviour than traditional digital systems. In the paper a digital system is treated as a complex system of algorithms. As an abstract model of real algorithms. so called Mazurkiewicz FC-algorithm is considered. FC-algorithms used in the paper have been extended to modifiable Fe-algorithms by adding a time-variant structure and the use of the notion of tolerance spaces. This structure allowed us to introduce a model of learning for modifiable FC-algorithms. Learning is understood as a goal directed process of changes of activities on the basis of experience.
On the Power of Model Theory in Specifying Abstract Data Types and in Capturing Their Recursiveness
Authors: Bertoni Alberto , Mauri Giancarlo , Miglioli Pierangelo
Published: May 2021

In this paper a comparative analysis of some algebraic and model-theoretic tools to specify abstract data types is presented: our aim is to show that, in order to capture a quite relevant feature such as the recursiveness of abstract data types, Model Theory works better than Category Theory. To do so, we analyze various notions such as “initiality”, “finality”, “monoinitiality”, “epifinality”, “weak monoinitiality” and “weak epifinality”, both from the point of view of “abstractness” and of “cardinality”, in a general model theoretical frame. For the second aspect, it is shown that only “initiality”, “monoinitiality”, “epifinality” and “weak epifinality” allow us to select countable models (for theories with a countable language), a necessary condition to get recursive data types, while this is not the case for “finality” and “weak monoinitiality”. An extensive analysis is then devoted to the problem of the recursiveness of abstract data types: we provide a formal definition of recursiveness and show that it neither collapses, nor it is incompatible with the “abstractness” requirement. We also show that none of the above quoted categorial notions captures recursiveness. Finally, we consider our own definition of “abstract data type”, based on typically model-theoretic notions, and illustrate the sense according to which it captures recursiveness.
On Connections Between Parallel Programs and Nondeterministic Sequential Programs
Authors: Sadowski Zenon
Published: May 2021

The paper contains an affirmative answer to the following question: Does nondeterministic sequential program equivalent with respect to the set of final valuations exist for every parallel program with semantics defined in paper[3]? It also includes an example of the construction of a nondeterministic sequential program equivalent with respect to the set of final valuations to the given parallel program.
Programmability in the Set of Real Numbers and Second-Order Recursion
Authors: Skandalis Kostas
Published: May 2021

In this paper we compare two notions of effectiveness in the ordered field of real numbers. The first one is introduced using the notion of program in the sense of algorithmic logic. The second is the recursiveness in Baire space. After an identification of the Baire space with the set of reals using an effective and natural mapping it turns out that these two notions are different. We also study a natural notion of effectiveness extending both these notions.
On a Representation of Rough Sets by Means of Information Systems
Authors: Novotný Miroslav , Pawlak Zdzisław
Published: May 2021

Rought sets are investigated as a tool for expressing uncertainty of the relation “to be an element of”. We give some representation theorems for rough sets expressed in terms of information systems.
Constrained Petri Nets. Part II: Generalizations and extensions
Authors: Goeman H.J.M. , Groenewegen L.P.J. , Kleijn H.C.M. , Rozenberg G.
Published: May 2021

This paper continues the investigation froll1 [Goeman et al.] concerning the use of sets of places of a Petri net as additional (to input places) constraints for granting concession. Now interpretations of more general constraints are considered and expressed as Boolean expressions. This gives rise to various classes of constrained Petri nets. These are compared in the language theoretical framework introduced in [Goeman et al.]. An upperbound for the language defining power is found in the class of context-free programmed languages.
Numerical Queries in Incomplete Information Data Bases
Authors: Jaegermann Michał , Lipski Witold
Published: May 2021

We consider the problem of answering numerical queries, i.e. queries involving cardinalities of sets of objects with specified conditions, in a data base where information is incomplete. We give an algorithm to compute a lower bound and an upper bound on the response to a numerical query. The bounds proceduced by the algorithm are the best logically derivable from the information available in the data base.
A Comparison of the Worst-Case Complexities of Two Algorithms for the Reaching Definitions Problem
Authors: Czech Zbigniew
Published: May 2021

An algorithm to solve the “reaching definitions” problem on reducible flow graphs is presented. It is based on the concept of a region of a flow graph, and has the worst-case time bound of O(n2) bit-vector operations. The algorithm is compared for time complexity with the well-known round-robin version of the iterative algorithm. The comparison shows that for every flow graph of n>2 nodes the region analysis algorithm for the “reaching definitions” problem requires in the worst case fewer bit-vector operations than the round-robin version of the iterative algorithm for the same problem.
Extending the Relational Algebra for Relations with Maybe Tuples and Existential and Universal Null Values
Authors: Biskup Joachim
Published: May 2021

We study operations on generalized database relations which possibly contain maybe tuples and two types of null values. The existential null value has the meaning “value at present unknown” whereas the universal null value has the meaning “value arbitrary”. For extending a usual relational operation to generalized relations we develop three requirements: adequacy, restrictedness, and feasibility. As demonstrated for the natural join as an example, we can essetially meet these requirements although we are faced with a minor tradeoff between restrictedness and feasibility.
Restricting the in-out Structure of Graphs of Petri Nets
Authors: Rozenberg Grzegorz , Verraedt Raymond
Published: May 2021

Petri nets are classified according to the restrictions on the possible in-out structure of nodes of the underlying graphs. Such a classification is investigated separately for the structure of transitions and the structure of places. The classification is done from the language theoretical point of view, i.e. behaviour of a net is expressed by the language it generates. Two approaches are used. Firstly, various classes of nets are compared with respect to the languages of firing sequences they generate. Secondly, the comparison results so obtained are sharpened (often quite drastically) by looking at nets as generators of the so-called subset languages.
Classes of Transfinite Sequences Accepted by Nondeterministic Finite Automata
Authors: Wojciechowski Jerzy
Published: May 2021

In this paper the notion of a nondeterministic finite automaton acting on arbitrary transfinite sequences is introduced. It is a generalization of the finite automaton on finite sequences and the finite automaton on ω-sequences. The basic properties of the behaviour of such automata are proved. The methods are shown how to construct automata accepting classes A ⋃ B, A ⋂ B, A ∘ B, A*, Aω, A# if we have automata accepting classes A and B. We prove that if a TF-automaton having k states accepts anything then it accepts an α-sequence for a certain, α ∈ { ∑ i = 0 m ω i · a i : ∑ i = 1 m i · a i + a 0 ⩽ k }. Using the foregoing fact, we show that the family of classes definable by TF-automata is not closed with respect to the complement operation, that nondeterministic automata are not equivalent to the deterministic ones and that the emptiness problem for TP-automata is decidable. In the last section we show the construction of TP-automata defining sets {∗α} for α < ω ω and having as few states as possible.
A Method for Synthesizing Algebras from Their Specification
Authors: Jantke Klaus P.
Published: May 2021

This paper is concerned with automatic implementation of final algebras. The result states that it is possible under the condition that there is an effective procedure generating all mutually nonequivalent (in the specified algebra) terms.
On Certain Property not Expressible in PAL
Authors: Mirkowska Grażyna
Published: May 2021

The property of finite degree of nondeterminism is not expressible by a formula and by any set of formulas in propositional algorithmic logic PAL.
A Formal System for Proving Some Properties of Programs in Iterative Combinatory Spaces
Authors: Skordev Dymiter
Published: May 2021

The paper presents an abstract tool for describing general properties of programs. Iterative combinatory space approach makes possible to transfer recursion – theoretical methods onto logical system which is constructed in this paper.
Algorithmic Logic with Stacks and Its Model-Theoretical Properties
Authors: Dańko Wiktor
Published: May 2021

In this paper we propose to transform the Algorithmic Theory of Stacks (cf. Salwicki [30]) into a logic for expressing and proving properties of programs with stacks. We compare this logic to the Weak Second Order Logic (cf. [11, 15]) and prove theorems concerning axiomatizability without quantifiers (an analogon of Łoś-Tarski theorem) and χ 0 - categoricity (an analogon of Ryll-Nardzewski’s theorem).
On the Semantics of the Relational Model of Database I
Authors: Marek Wiktor
Published: May 2021

We present a formalization of (tuple version) of Codd’s relational model of database. The presentation stresses the ontological problems related with this model.
Homogeneous Information Trees
Authors: Chen Keh-Hsun , Raś Zbigniew W.
Published: May 2021

By a homogeneous information tree we mean a tree with internal nodes labeled by attributes, edges by values of attributes and terminal nodes by sets of objects. Sets labeling terminal nodes form a partition of the set of objects classified by a homogeneous tree. Homogeneous information trees can be interpreted as models of expert systems, data bases with a menu or tree-structured data bases. The main problem we are dealing with concerns a minimization of a tree with respect to the storage cost. We propose a heuristic polynomial algorithm to construct an optimal tree.
Easy Terms in the Lambda Calculus
Authors: Jacopini Giuseppe , Venturini Zilli Marisa
Published: May 2021

This paper, a revised version of the one [4] presented at the Logic Colloquium ’82, concerns closed unsolvable λ-terms, named easy, which are terms such that they can be consistently equated to arbitrary closed ones. Some general results are obtained, mainly sufficient or necessary conditions for proving that an unsolvable λ-term is easy.
Effective Construction of Grammars for Languages of Two Particular Classes
Authors: Ostravský Jan
Published: May 2021

In this paper we solve inference problem for languages on two particular classes BC, BS. For any language (V,L) ∈ Bj, j ∈ {s,c}, and any natural number i, we define a grammar Gji(V,L) in an effective way. We prove that (V,L) ∈ Bj iff there exists a natural number i0 such that Gji(V,L) = Gji0(V,L) for any i ⩾ i0; the grammar Gji0(V,L) generates (V,L).
Axiomatizable Classes in Many-Sorted Logics of Programs
Authors: Danko Wktor
Published: May 2021

In this paper many-sorted logics of programs are considered (cf. Wand [16] and [3]). The aim is to characterize classes of structures axiomatizable by sets of algorithmic formulas. The results are formulated in terms of operations on classes of structures axiomatizable in the first order logic.
Monadic Second Order Definability as a Common Characterization of Finite Automata, Certain Classes of Programs and Logics
Authors: Wasilewska Anita
Published: May 2021

We introduce the notion of monadic second order definability (m.s.o definability) of automata, programs and logics and point out some classes of automata (theorem 7), programs (theorem 8) and logics (theorem 9) which are m.s.o definable.
Logic Approach to Information Systems
Authors: Orłowska Ewa
Published: May 2021

The purpose of the present paper is to give a logical framework which provides a uniform description of Pawlak’s information systems of deterministic, nondeterministic, and many-valued information. A language is introduced for representing and retrieving information. Logical aspects of dynamics of information systems are discussed.
Quadratic-Time Optimization of SPJ-Expressions Including Inequality Selections by Tableaux
Authors: Heinz Alois Peter , Vossen Gottfried
Published: May 2021

The problem of optimizing algebraic queries to relational databases which are formulated with the help of inequality selection, projection, and natural join is addressed: We generalize the well-known tableau formalism to handle this type of queries and provide a quadratic-time optimization procedure. We show how optimized tableaux can be translated back into extended SPJ-expressions, thereby dispensing with the computationally harder cartesian product.
Concurrent Transformations of Relational Structures
Authors: Ehrig Hartmut , Habel Annegret , Rosen Barry K.
Published: May 2021

This paper provides a common framework to study transformations of structures ranging from all kinds of graphs to relational data structures. Transformations of structures can be used as derivations of graphs in the sense of graph grammars, as update of relations in the sense of relational data bases, or even as operations on data structures in the sense of abstract data types. The main aim of the paper is to construct parallel and concurrent transformations from given sequential ones and to study sequentializability properties of complex transformations. The main results are three fundamental theorems concerning parallelism, concurrency and decomposition of transformations of structures. On one hand these results can be considered as a contribution to the study of con currency in graph grammars and on the other hand as a formal framework for consistent concurrent update of relational structures.
Modular Real-Time Trellis Automata
Authors: Černý Anton , Gruska Jozef
Published: May 2021

A new type of nonhomogeneous real time trellis automata, the so-called modular trellis automata, is introduced and various results concerning their normal forms, power, simulations, and decision problems are shown. Modular trellis automata are a mathematical abstraction, in the form of a recognizer, of an intuitive notion of an array of simple processors assembled in a simple and modular way. Distribution of processors in a real-time trellis automaton forms a two-dimensional structure called trellis. Basic characterizations and properties of modular trellises are summarized and modularity of various special trellises – regular, product, self-embedding, and self-overlapping – is investigated.
Almost Context-Free Languages
Authors: Chytil Michal P.
Published: May 2021

We define a superclass of the class of context-free languages, denoted ACFL (almost context-free languages) and construct an infinite sequence of non-context-free languages of decreasing complexity, belonging to ACFL. The languages in ACFL share many important properties of context-free languages. For example, a slight generalization of pumping lemma for context-free languages holds also for languages in ACFL. Similarly, some of the questions decidable for context-free languages are decidable in ACFL and start to be undecidable immediately outside the class. ACFL is a full AFL and contains an infinite strictly decreasing chain of full AFLs.
Algebraic Theories, Data Types, and Control Constructs
Authors: Wagner Eric G.
Published: May 2021

The aim of this paper is to model recursive types, equational types, and elementary programming control constructs (such as conditionals and while-do) in one, comparatively simple, algebraic framework, that can be used for theoretical studies and as a basis for data type and program specification. To this end we introduce a new kind of algebraic theory, the RV-theory. We give simple examples of the use of such theories for data type specification. We provide a mathematical semantics for these specifications that extends the initial algebra semantics for equational specification to include recursive types.
Proving Monitors Revisited: A First Step Towards Verifying Object Oriented Systems1
Authors: Gerth Rob , De Roever W.P.
Published: May 2021

An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete. This characterization is based on the fundamental notions of cooperation and interference, but does not use them as second order notions. The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between disjoint processes, as opposed to the interference freedom test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then, the cooperation test has been applied to characterize synchronous communication in Hoare’s Communicating Sequential Processes, Ichbia’s Ada, and Wirth’s Modula-2, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for a new monitor based programming language for concurrency (Communicating Modules, CM) which combines distributed message passing between processes with interference through local variables of a process which are shared between its sub-processes. As such this is a first step towards the formal verification of object oriented systems. In this context, we also show how the method, traditionally cauched in terms of proof outlines, can be rendered syntax directed in a precise and formal way. In a separate paper, the proof system has been shown to be sound and (relatively) complete.
Computations in Coordinated Pair Systems
Authors: Ehrenfeucht A. , Hoogeboom H.J. , Rozenberg G.
Published: May 2021

Selective substitution grammars provide a rather general framework for the grammatically oriented formal language theory (see, e.g., [R1], [K], and [KR]). They were generalized in [R2] to coordinated table selective substitution systems (ds systems) which provide a convenient unifying framework for both grammars and machines (automata). The present paper investigates coordinated pair (cp) systems which form a subclass of cts systems corresponding in a very natural way to push-down automata: thus cp systems generate context-free languages (all and only). This paper investigates the structure of computations in cp systems.
Iteration Theorems for Deterministic Families of Languages
Authors: Harrison Michael A.
Published: May 2021

In this paper, we consider the problem of finding iteration theorems for various subfamilies of deterministic languages. Because deterministic languages are constrained in their generation, it is not possible to merely “pump substrings” as in the general context free case. We lay out, in detail, a collection of techniques for proving theorems of this type for deterministic context free languages.
On Some Parameters Occurring in Certain Effective Constructions of Grammars
Authors: Păun Gheorghe , Novotný Miroslav
Published: May 2021

J. Ostravský considered two classes of languages – BS and BC – and described an effective construction assigning a pure grammar Gjk(V,L) to any j∈{s,c}, to any language (V,L), and to any integer k⩾1. He proved that (V,L)∈Bj if and only if there exists k0⩾1 such that Gjk(V,L) = Gjk0(V,L) for any k⩾k0. The least integer k0 with this property is a complexity measure of the language (V,L)∈Bj. Besides this complexity measure, we study another one introduced in connection with the above mentioned construction. We compare the complexity of languages with the complexity of languages obtained by usual operations from the given ones.
A Simple Algorithm and Proof for Type Inference1
Authors: Wand Mitchell
Published: May 2021

We present a simple proof of Hindley’s Theorem: that it is decidable whether a term of the untyped lambda calculus is the image under type-erasing of a term of the simply typed lambda calculus. The proof proceeds by a direct reduction to the unification problem for simple terms. This arrangement of the proof allows for easy extensibility to other type inference problems.
D-Continuity and Petri’s Axioms of Concurrency for Nonsequential Process Models
Authors: Best Eike , Merceron Agathe
Published: May 2021

A non-sequential process can be modelled by a partially ordered set. Conversely, one is led to study the properties to be fulfilled by a poset so that it can reasonably be viewed as the model of a non-sequential process. To this end, C.A. Petri has proposed a set of con currency axioms and a related property called D-continuity, a generalised version for partially ordered sets of Dedekind’s completeness property of the real numbers. In this paper we study Petri’s axioms of concurrency and some of their interdependencies. We also derive several characterisations of D-continuity and exhibit its relation with the axioms of concurrency. Furthermore we apply our work to Petri nets: we introduce occurrence nets, some special posets which model the processes of a system net and we present their relations to D-continuity and the axioms of con currency. Finally we identify the class of the system nets whose processes are D-continuous and satisfy the axioms of concurrency.
Variants of Determinacy in Parallel Program Schemata
Authors: Kelter Udo
Published: May 2021

Systems which use parallel processing to speed up response times are normally required to be determinate. Parallel program schemata are formal models of parallel systems which serve to exactly define determinacy. Three variants of determinacy have frequently been used in the literature: Two “semantic” ones, which refer to the final contents of variables and to the sequences of contents, and a “syntactic” one, which is based upon the notion of conflict. Variants of determinacy can be derived with a universal definition of determinacy (as presented in [K73]) which uses a parameter, namely an equivalence relation on computations. Each of the above variants corresponds to a certain equivalence relation. The main aim of this paper is to investigate the role of “read-only”-operations, e.g. pure tests. Results of tests do not matter for both semantic forms of determinacy, whereas they are relevant for the syntactic form. We will snow that different variants of semantic and syntactic determinacy can be obtained by judging read-only operations as relevant or not.
Concurrent Program Schemes
Authors: Kfoury A.J. , Urzyczyn P.
Published: May 2021

We study the programming formalism FD of “flow-diagrams” to which we gradually add various features of concurrency. The weakest form of concurrency is introduced by the construct “and”, which is dual to the nondeterministic choice “or” and plays a role similar to universal states in alternating Turing machines. Stronger (and more realistic) forms of concurrency are obtained when processes are allowed to communicate. We consider communication by channels and communication by messages. We calibrate the computational power of classes of concurrent programs FD+α against that of sequential programs, where α is the addition of one of the following features: {and}, {and, or}, {and, or, channels}, or {and, or, messages}.
Some Fixpoint Techniques in Algebraic Structures and Applications to Computer Science
Authors: Guessarian Irène
Published: May 2021

This paper recalls some fixpoint theorems in ordered algebraic structures and surveys some ways in which these theorems are applied in computer science. We describe via examples three main types of applications: in semantics and proof theory, in logic programming and in deductive data bases.
An Algebraic Model for Communicating Processes
Authors: Winkowski Jozef
Published: May 2021

A new semantics for communicating processes is introduced which modifies the ideas of Milner (1980) and Winskel (1982, 1983, and 1986). This semantics, inspired by a model of Staples and Nguyen (1985) for nondeterministic data flow, allows one to avoid explicit representation of hidden events of processes, which simplifies the concept of observation equivalence of processes. It offers also a framework to cope with indivisible sets of communication events.
Bases and Lattices in Non-Sequential Processes
Authors: Fernández C. Cesar , Merceron Agathe
Published: May 2021

In this paper, we introduce the notion of a basis to study non-sequential processes which are modelled by partially ordered sets. We show that -associated to lower sets and upper sets- this notion permits to characterise several properties of non-sequential processes. We show also that lower sets and upper sets with finite basis are the compact elements of the lattices of lower sets and upper sets.
Chains of Finite Automat a with Bounded Number of Chains1
Authors: Kutylowski Miroslaw
Published: May 2021

Chains of finite automata are considered. We show that if the lowest automaton in a chain controls movements of the common reading head then computing power of the chain is very limited. This is a generalization of Krohn-Rhodes theorem on one-way automata.
Rough Tolerance Equality and Tolerance Black Boxes
Authors: Nieminen Juhani
Published: May 2021

The rough equality concept of Z. Pawlak is modified and the rough top and the rough bottom tolerance equalities are given and characterized. The same tolerance idea is applied also to black box notion introduced by Novotný and Pawlak; the concept thus obtained is called tolerance black box. Tolerance black boxes are characterized and their properties are described.
A Temporal Logic for Event Structures
Authors: Penczek Wojciech
Published: May 2021

A temporal logic for event structures based on a partial order frame of local states is presented. Two modalities, for causality and conflict, are introduced. Completeness of the axiom system is proved. The finite model property and decidability are discussed.