Fundamenta Informaticae - Volume 32, issue 1

Authors: Frias, Marcelo F. | Baum, Gabriel A. | Haeberer, Armando M.

Article Type: Research Article

Abstract: Since the main themes at the Helena Rasiowa memorial were algebra, logic and computer science, we will present a survey of results on fork algebras from these points of view. In this paper we study fork algebras from the points of view of their algebraic and logical properties and applications. These results will prove to be essential, in a future work, for the definition of a wide-spectrum calculus for program construction.

DOI: 10.3233/FI-1997-32101

Citation: Fundamenta Informaticae, vol. 32, no. 1, pp. 1-25, 1997

Authors: Kasangian, Stefano | Vigna, Sebastiano

Article Type: Research Article

Abstract: In this paper a we give a semantics for SCCS using the constructions of the topos of labelled trees. The semantics accounts for all aspects of the original formulation of SCCS, including unbounded non-determinism. Then, a partial solution to the problem of characterizing bisimulation in terms of a class of morphisms is proposed. We define a class of morphisms of the topos of trees, called conflict preserving, such that two trees T and U are bisimilar iff there is a pair of conflict preserving morphisms f : T → U and g : U → T such that fgf = …f and gfg = g. It is the first characterization which does not require the existence of a third quotient object. The results can be easily extended to more general transition systems. Show more

Keywords: process algebras, semantics, category theory, topos theory

DOI: 10.3233/FI-1997-32102

Citation: Fundamenta Informaticae, vol. 32, no. 1, pp. 27-45, 1997

Authors: Pigozzi, Don | Salibra, Antonino

Article Type: Research Article

Abstract: 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 (β)-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. Show more

Keywords: lambda calculus, cylindric algebras, polyadic algebras, abstract substitution, combinatory algebras, lambda algebras, lambda models, representation theorems

DOI: 10.3233/FI-1997-32103

Citation: Fundamenta Informaticae, vol. 32, no. 1, pp. 47-90, 1997

Authors: Tyszkiewicz, Jerzy

Article Type: Research Article

Abstract: We consider two kinds of reflective relational machines: the usual ones, which use first order queries, and existential reflective machines, which use only first order existential queries. We compare these two computation models. We build on already existing results for standard relational machines, obtained by Abiteboul, Pa-padimitriou and Vianu [2], so we prove only results for existential machines. First we show that for both standard and existential reflective machines the set of polynomial time computable Boolean queries consists precisely of all 𝒫𝒮𝒫𝒜𝒞ℰ computable queries. Then we go further and compare which classes of algorithms both kinds of machines represent. Unless …𝒫𝒮𝒫𝒜𝒞ℰ = 𝒫𝒩𝒫 , there are 𝒫𝒮𝒫𝒜𝒞ℰ queries which cannot be computed by polynomial time existential reflective machines which use only polynomial amount of relational memory, while it is possible for standard reflective machines. We conclude that existential reflective machines, being equivalent in computational power to unrestricted machines, implement substantially worse algorithms than the latter. Concerning deciding 𝒫 classes of structures, every fixpoint query can be evaluated by a polynomial time unrestricted reflective machine using constant number of variables, while existential reflective machines need [n/2] variables to implement the graph connectivity query. So again the algorithms represented by existential reflective machines are worse. Finally, for each k we get a characterization of the Δk+1p level in the polynomial time hierarchy in terms of reflective relational machines which use either Πk0 or Σkp queries. Show more

Keywords: Reflective relational machines, quality of algorithms, polynomial time, polynomial space, polynomial hierarchy

DOI: 10.3233/FI-1997-32104

Citation: Fundamenta Informaticae, vol. 32, no. 1, pp. 91-105, 1997