Fundamenta Informaticae - Volume 26, issue 2

Authors: Fokkink, Wan

Article Type: Research Article

Abstract: This paper studies the interaction of prefix iteration with the silent step in the setting of branching bisimulation. We present a finite equational axiomatization for Basic Process Algebra with deadlock, empty process and the silent step, extended with prefix iteration, and prove that this axiomatization is complete with respect to rooted branching bisimulation equivalence.

DOI: 10.3233/FI-1996-26201

Citation: Fundamenta Informaticae, vol. 26, no. 2, pp. 103-113, 1996

Authors: Fu, Yuxi

Article Type: Research Article

Abstract: We give an interpretation of Martin-Löf's type theory (with universes) extended with generalized inductive types. The model is an extension of the recursive model given by Beeson. By restricting our attention to PER model, we show that the strictness of positivity condition in the definition of generalized inductive types can be dropped. It therefore gives an interpretation of general inductive types in Martin-Löf's type theory.

DOI: 10.3233/FI-1996-26202

Citation: Fundamenta Informaticae, vol. 26, no. 2, pp. 115-131, 1996

Authors: Knijnenburg, Peter M.W.

Article Type: Research Article

DOI: 10.3233/FI-1996-26203

Citation: Fundamenta Informaticae, vol. 26, no. 2, pp. 133-139, 1996

Authors: Bakel, Steffen van

Article Type: Research Article

Abstract: A notion of type assignment on Curryfied Term Rewriting Systems is introduced that uses Intersection Types of Rank 2, and in which all function symbols are assumed to have a type. Type assignment will consist of specifying derivation rules that describe how types can be assigned to terms, using the types of function symbols. Using a modified unification procedure, for each term the principal pair (of basis and type) will be defined in the following sense: from these all admissible pairs can be generated by chains of operations on pairs, consisting of the operations substitution, copying, and weakening. In general, …given an arbitrary typeable GTRS, the subject reduction property does not hold. Using the principal type for the left-hand side of a rewrite rule, a sufficient and decidable condition will be formulated that typeable rewrite rules should satisfy in order to obtain this property. Show more

DOI: 10.3233/FI-1996-26204

Citation: Fundamenta Informaticae, vol. 26, no. 2, pp. 141-166, 1996

Authors: Konikowska, Beata

Article Type: Research Article

Abstract: The paper introduces a notion of an algebra corresponding to the three-valued logical calculus designed by McCarthy for computation purposes and used in several existing software system. The algebra, called McCarthy algebra, is a generalization of a Boolean algebra. It is defined extensionally, but a set of sound equality axioms is also given. From these axioms, various non-classical properties of the elements of such algebras are deduced. A representation theorem for two classes of McCarthy algebras is presented.

DOI: 10.3233/FI-1996-26205

Citation: Fundamenta Informaticae, vol. 26, no. 2, pp. 167-203, 1996