Abstracts of Fundamenta Informaticae Volume 33.

Number 1 
L. CZAJA
Minimal-Maximal Time Cause-Effect Structures
pages 1-16

It is shown that minimal-time singly-valued (counterparts of 1-safe Petri nets) cause-effect (c-e) structures are of the same expressive power as no-time singly-valued c-e structures, while maximal-time multi-valued c-e structures are of essentially greater expressive power than no-time multi-valued c-e structures.
 L. CZAJA
Cause-Effect Structures - Structural and Semantic Properties Revisited
pages 17-42

G. DIMOV and D. VAKARELOV
On Scott Consequence Systems
pages 43-70

The notion of Scott consequence system (briefly, S-system) was introduced by D. Vakarelov in [32] in an analogy to a similar notion given by D. Scott in [26]. In part one of the paper we study the category SSyst of all S-systems and all their morphisms. We show  that the category {\bf DLat} of all distributive lattices and all lattice homomorphisms is isomorphic to a reflective full  subcategory of the category {\bf SSyst}. Extending the representation theory of D. Vakarelov [32] for S-systems in P-systems,we develop an isomorphism theory for S-systems and forTarski consequence systems.
In part two of the paper we prove that the separation theorem for S-systems is equivalent in ZF to some other separation principles, including the separation theorem for filters  and ideals in Boolean algebras and separation theorem for convex sets in convexity spaces.
 
V. SCHMITT
CR-Structures
pages 71-83

In this paper CR-structures are introduced. They consist of a slight generalization of general event structures [16], and supply a representation theorem for concurrency domains, which are called here CR-domains for short. We recall that the latter domains are exactly the unfoldings of concurrent automata [7], [3]. This result also generalizes Droste's characterization of domains of configurations of general event structures [6].
L. VIGNERON
Automated Deduction Techniques for Studying Rough Algebras
pages 85-103

We present a non-exhaustive state of the art in the domain of deduction in first-order logic with equality, describing different strategies introduced over the years: strategies for selecting  deduction steps, for eliminating redundant information, for delaying the resolution of unsolved or too difficult problems, for applying deductions with uilt-in properties. We also present the system   daTac that implements our deduction techniques modulo associative-commutative properties. Finally we detail an application of those techniques to the study of non-classical logics, work realised in collaboration with Prof. Wasilewska (Stony Brook University, New York).
Number 2 
C. S. CALUDE and P. H. HERTLING
Computable Approximations of Reals:An Information-Theoretic Analysis
pages 105-120

How fast can one approximate a real by a computable sequence of rationals? Rather surprisingly, we show that the answer to this question depends very much on the information content in the finite prefixes of the binary expansion of the real. Computable reals, whose binary expansions have a very low information content, can be approximated (very fast) with a computable convergence rate. Random reals, whose binary expansions contain very much information in their prefixes, can be approximated only very slowly by computable sequences of rationals (this is the case, for example, for Chaitin's $\Omega$ numbers) if they can be computably approximated at all.
We also show that one can computably approximate any computable real very slowly, with a convergence rate slower than any computable function. However, there is still a large gap between computable reals and random reals: any computable sequence of rationals which converges (monotonically) to a random real converges slower than any computable sequence of rationals which converges (monotonically) to a computable real.
T. PANKOWSKI
Powerdomain of paths for representing object structures
pages 121-148

A new method for viewing and manipulating identity-based object structures is proposed. The method is founded on the viewing the object structure as an object graph which in turn is represented as a set of paths. Over a power set of paths we construct a powerdomain which forms a lattice with well-defined meet and join operations. In our construction of the powerdomain of paths we combine the Hoare ordering (appropriate for ordering of tuple objects) with the Smyth ordering (appropriate for ordering of set objects) into a new ordering appropriate for set of paths capturing information conveyed by both tuple and set objects. The approach allows to deal with incomplete tuple objects as well as with partially described sets. The goal of the powerdomain construction is to provide a semantic domain for a path calculus language [20], where path calculus variables range over paths and path calculus queries give sets of paths as their answers.
D. PIGOZZI and A. SALIBRA
Lambda Abstraction Algebras: Coordinatizing Models of Lambda Calculus
pages 149-200

Lambda abstraction algebras are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order logic; they are intended as an alternative to combinatory algebras in this regard. Like combinatory algebras they can be defined by true identities and thus form a variety in the sense of universal algebra. One feature of lambda abstraction algebras that sets them apart from combinatory algebras is the way variables in the lambda calculus are abtracted; this provides each lambda abstraction algebra with an implicit coordinate system. Another peculiar feature is the algebraic reformulation of ($\beta$)-conversion as the definition of abstract substitution. Functional lambda abstraction algebras arise as the ``coordinatizations'' of environment models or lambda models, the natural combinatory models of the lambda calculus. As in the case of cylindric and polyadic algebras, questions of the functional representation of various subclasses of lambda abstraction algebras are an important part of the theory. The main result of the paper is a stronger version of the functional representation theorem for locally finite lambda abstraction algebras, the algebraic analogue of the completeness theorem of lambda calculus. This result is used to study the connection between the combinatory models of the lambda calculus and lambda abstraction algebras. Two significant results of this kind are the existence of a strong categorical equivalence between lambda algebras and locally finite lambda abstraction algebras, and between lambda models and rich, locally finite lambda abstraction algebras.
D. PLUMP
Termination of graph rewriting is undecidable
pages 201-209

It is shown that it is undecidable in general whether a graph rewriting system (in the ``double pushout approach") is terminating. The proof is by a reduction of the Post Correspondence Problem. It is also argued that there is no straightforward reduction of the halting problem for Turing machines or of the termination problem for string rewriting systems to the present problem.
Number 3
SPECIAL ISSUE: GRAMMAR SYSTEMS
Editorial: Solomon Marcus
R. GRAMATOVICI
An Efficient Parser for a Class of Contextual Languages
pages 211-237

A class of Marcus contextual languages containing non-context-free languages is defined. A parser for this class of languages is developed. The parser uses an operatorial automaton and it works in square time in the length of the input words.
L. ILIE
Generalized Factors of Words
pages 239-247
We introduce and study relations on words which generalize the factor relation, being restrictions of the subword relation. We give an equivalent condition for the finite basis property for these relations which generalizes the well-known theorem of Higman.  Some language-theoretic gaps for infinite antichains are also presented.
M. KUDLEK and A. MATEESCU
Algebraic, Linear and Rational Languages Defined by Mix Operation
pages 249-264

We consider operations between languages, based on splitting the underlying alphabet into two disjoint sets, one of them having some priority. Such operations are generalizations of the classical catenation or shuffle operation, with which rational, linear and algebraic languages can be defined similar to the classical case. The basic  properties of the corresponding language families are investigated too.
P. MARTINEK
Limits of Pure Grammars with Monotone Productions
pages 265-280

The grammatical inference problem is solved for a class of languages which can be generated by pure grammars with non-shortening productions. Necessary and sufficient condition for determination whether a~language belongs to this class is formulated and proved. Finally, an algorithm for assigning a~pure grammar to any language from the class is described.
V. MITRANA
Parallelism in Contextual Grammars
pages 281-294

Two strategies of parallel adjoining of contexts are considered for contextual grammars with choice. After a short comparison between them,  there are provided  Chomsky-Schutzenberger type characterizations of context-free and recursively enumerable languages. Finally, we discuss some decision problems.   
M. NOVOTNY
Reduction of Pregrammars
pages  295-307

In [13] pure generalized grammars were studied, in particular, the problem of reducing a pure generalized grammar to a pure grammar. These results are transferred to the so called  pregrammars in the present paper. The obtained results may be applied not only to pure generalized grammars but also to other structures.
Number 4
M. BRANDT and F. HENGLEIN
Coinductive Axiomatization of Recursive Type Equality and Subtyping
pages 309-338

We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types.  The rules are motivated by coinductive characterizations of type containment and type equality via simulation and bisimulation, respectively.  The main novelty of the axiomatization is the  fixpoint rule (or coinduction principle).  It states that from \(A, P \vdash P \) one may deduce \( A \vdash P \),  where P is either a type equality $\tau = \tau'$ or type containment $\tau \leq \tau'$ and the proof of the premise must be contractive in a sense we define in this paper.
In particular, a proof of $A, P \vdash P$ using the assumption axiom is not contractive.
The fixpoint rule embodies a finitary coinduction principle and thus allows us to capture a coinductive relation in the fundamentally inductive framework of inference systems.
The new axiomatizations are more concise than previous axiomatizations, particularly so for type containment since no separate axiomatization of type equality is required, as in Amadio and Cardelli's axiomatization. They give rise to a natural operational interpretation of proofs as coercions.  In  particular, the fixpoint rule corresponds to definition by recursion. Finally, the axiomatization is closely related to (known) efficient algorithms for deciding type equality and type containment.  These can be modified to not only  decide type equality and  type containment, but also construct proofs in our axiomatizations efficiently. In connection with the operational interpretation of proofs as coercions this gives  efficient ($O(n^2)$ time) algorithms for  constructing  efficient coercions from a type to any of its supertypes or isomorphic types.
More generally, we show how adding the fixpoint rule makes it possible to characterize  inductively a set that is  coinductively defined as the kernel (greatest fixed point) of an inference system.
T. BRAUNER
 A Simple Adequate Categorical Model for PCF, II
pages 339-368

Usually types of PCF are interpreted as cpos and terms as continuous functions. It is then the case that non-termination of a closed term of ground type corresponds to the interpretation being bottom; we say that the semantics is adequate. We shall here present an axiomatic approach to adequacy for PCF in the sense that we will introduce
categorical axioms enabling an adequate semantics to be given. We assume the presence of certain ``undefined'' maps with the role of being the interpretation of on-terminating terms, but the order-structure is left out. This is different from previous approaches where some kind of order-theoretic structure has been considered as part of an adequate categorical model for PCF. We take the point of view that partiality is the fundamental notion from which order-structure should be derived, which is corroborated by the observation that our categorical model induces an order-theoretic model for PCF in a canonical way.
I. STARK
Names, Equations, Relations:
pages  369-396

The nu-calculus of Pitts and Stark is a typed lambda-calculus, extended with state in the form of dynamically-generated  names.  These names can be created locally, passed around, and compared with one another.  Through the interaction between names and functions, the language can capture notions of scope, visibility and sharing.  Originally motivated by the study of references in  Standard~ML, the nu-calculus has connections to local declarations in general; to the mobile processes of the \pi$-calculus; and to security protocols in the spi-calculus. This paper introduces a logic of equations and relations which allows one to reason about expressions of the nu-calculus: this uses a simple representation of the private and public scope of names, and allows straightforward proofs of contextual equivalence (also known as observational, or observable, equivalence).  The logic is based on earlier operational techniques, providing the same power but in a much more accessible form.  In particular it allows intuitive  and direct proofs of all contextual equivalences between first-order functions with local names.
I. TAKEUTI
An Axiomatic System of Parametricity
pages 397-432

Plotkin and Abadi have proposed a syntactic system for parametricity based on a second order predicate logic. This paper shows three theorems about that system. The first is consistency of the system, which is proved by the method of  relativization. The second is that polyadic parametricities of recursive types are equivalent to each other. The third is that the theory of parametricity for recursive types is self-realizable. As a corollary of the third theorem, the theory of parametricity for recursive types satisfies the term extraction property.