Fundamenta Informaticae - Volume 5, issue 2

Article Type: Other

DOI: 10.3233/FI-1982-5201

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. i-vi, 1982

Authors: Dezani-Ciancaglini, Mariangola | Ermine, Françoise

Article Type: Research Article

Abstract: 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.

Keywords: Type, λ-calculus, normal form, termination property

DOI: 10.3233/FI-1982-5202

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 129-141, 1982

Authors: Bergstra, Jan A. | Meyer, John-Jules Ch.

Article Type: Research Article

Abstract: In [5] it has been proved that by using hidden functions the number of equations needed to specify a finite data type is bounded by numbers depending only on the signature of that data type. In the special case of a finite minimal unoid, however, it seems to be relevant to ask whether or not a specification can also be made by a bounded number of equations using only unary hidden functions. In this paper we prove that this can be done.

Keywords: algebraic data types, finite data types, unoids, equational specifications with hidden functions, boundedness properties

DOI: 10.3233/FI-1982-5203

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 143-170, 1982

Authors: Bloom, Stephen L.

Article Type: Research Article

Abstract: A review is given of some of the late C.C. Elgot’s ideas on the syntax and semantics of monadic flowchart algorithms. In particular, the motivation for his “iterative algebraic theories” is explained.

DOI: 10.3233/FI-1982-5204

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 171-186, 1982

Authors: Troeger, Douglas R.

Article Type: Research Article

Abstract: 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.

Keywords: iterative theories, fixed points, metric interpretations

DOI: 10.3233/FI-1982-5205

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 187-216, 1982

Authors: Sandring, Sylvely | Starke, Peter H.

Article Type: Research Article

Abstract: 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.

Keywords: Petri net, liveness, extended-free-choice nets, reachability problem

DOI: 10.3233/FI-1982-5206

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 217-232, 1982

Authors: Kowalczyk, Wojciech

Article Type: Research Article

Abstract: 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.

Keywords: independence, consistency, nonstandard model of Peano Arithmetic, indicator, provably recursive function, P=NP problem

DOI: 10.3233/FI-1982-5207

Citation: Fundamenta Informaticae, vol. 5, no. 2, pp. 233-245, 1982