Fundamenta Informaticae - Volume 37, issue 4

Authors: Böhm, Corrado

Article Type: Research Article

Abstract: Solutions of the equations X = ZX and X = XZ are found and discussed for Z, X normal terms of the lambda-calculus. Obviously fixed point combinators are of no help. Solutions will be independent from any kind of gödelization or coding of data structures, they will be provided by typeless self-application. Different approaches will be shown: algebraic properties, one side invertibility and idempotency. Certain subsets of proper combinators and Church algebras between them will be proved to be domains consisting only of fixed points of combinators.

Keywords: Lambda Calculus, Abstract Algebras, Fixed Point Equations

DOI: 10.3233/FI-1999-37401

Citation: Fundamenta Informaticae, vol. 37, no. 4, pp. 329-342, 1999

Authors: Czaja, Ludwik

Article Type: Research Article

Abstract: It is shown how control aspects of the CSP-like communication mechanism may be represented as cause-effect structures, by using their calculus. A correctness proof of this transformation, i.e. its preserving of behaviour, has been given. A CSP-like parallel combinator for c-e structures is proposed, as well as its semantic counterpart. Compositionality property is proved.

DOI: 10.3233/FI-1999-37402

Citation: Fundamenta Informaticae, vol. 37, no. 4, pp. 343-368, 1999

Authors: Jung, Achim | Kegelmann, Mathias | Moshier, M. Andrew

Article Type: Research Article

Abstract: We study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalised in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition …in a suitable category of logical systems. As it turns out, this category is equivalent to coherent spaces with certain relations between them. Finally, cut elimination in this set-up can be employed to provide a new explanation of the domain constructions in Samson Abramsky's Domain Theory in Logical Form. Show more

Keywords: Domain Theory, coherent spaces, sequent calculus, observation logic, cut elimination

DOI: 10.3233/FI-1999-37403

Citation: Fundamenta Informaticae, vol. 37, no. 4, pp. 369-412, 1999

Authors: Kudlek, Manfred

Article Type: Research Article

Abstract: Using general iteration lemmata for languages defined by rational, linear, and algebraic systems of equations on ω-complete semirings, it can be shown that such iteration lemmata hold for certain classes of word and trace languages, and for process algebra classes related to them. The basic operation has to be associative with a neutral element, and is extended to sets of elements, such that the structure defined by it together with union and ∅ is an ω-complete semiring. With this property rational, linear and algebraic systems of equations can be defined, having a unique minimal solution as least fixed points. To …guarantee iteration lemmata for the corresponding rational, linear and algebraic classes, a norm on the structure has to exist, fulfilling some monotonicity on union and extended operation on sets. This article is an extended version of the paper presented at the workshop CS&P'98 in Berlin, September 28-30, 1998. Show more

DOI: 10.3233/FI-1999-37404

Citation: Fundamenta Informaticae, vol. 37, no. 4, pp. 413-422, 1999