Fundamenta Informaticae - Volume 20, issue 4

Authors: Tendera, Lidia

Article Type: Research Article

Abstract: The Σ1 1 (∀∃∀) class is the class of all existential second-order sentences whose first-order part is in the prenex form with prefix of the form ∀∃∀. In this paper we prove that every rational number in the interval [0,1] is the asymptotic probability for some Σ1 1 (∀∃∀) sentence. This result completes the classification of asymptotic probabilities for the existential second-order minimal classes.

DOI: 10.3233/FI-1994-2041

Citation: Fundamenta Informaticae, vol. 20, no. 4, pp. 277-285, 1994

Authors: Noll, Thomas | Vogler, Heiko

Article Type: Research Article

Abstract: This paper introduces a machinery called attributed top–down parsing automaton which performs top-down parsing of strings and, simultaneously, the evaluation of arbitrary noncircular attribute grammars. The strategy of the machinery is based on a single depth–first left–to–right traversal over the syntax tree. There is no need to traverse parts of the syntax tree more than once, and hence, the syntax tree itself does not have to be maintained. Attribute values are stored in a graph component, and values of attributes which are needed but not yet computed are represented by particular nodes. Values of attributes which refer to such uncomputed …attributes are represented by trees over operation symbols in which pointers to the particular nodes at their leaves are maintained. Whenever eventually the needed attribute value is computed, it is glued into the graph at the appropriate nodes. Show more

DOI: 10.3233/FI-1994-2042

Citation: Fundamenta Informaticae, vol. 20, no. 4, pp. 285-332, 1994

Authors: Laneve, Cosimo

Article Type: Research Article

Abstract: In this paper we address the problem of encoding evaluation strategies for the λ-calculus into prime event structures. In order for this to be possible the derivation spaces yielded by the evaluation mechanism must be prime algebraic cpo's. This requirement is not met by permutation equivalence (the standard concurrent semantics with which λ-calculus is equipped) since the derivation spaces it yields are upper semi-lattices. We solve this problem by taking the coarsest congruence contained in permutation equivalence such that permutations of disjoint reductions are equated and the downward closure of every derivation is a distributive lattice. This equivalence, called distributive …permutation equivalence, is characterized directly by restricting permutations of redexes to those sets U which are distributive, i.e. for every u ∈ U, the development of every V ⊆ (U\{u}) does not duplicate or delete u. A simple consequence of our results is that the derivation spaces of the call-by-value λ-calculus are distributive lattices. Finally, we show that a sequential evaluation mechanism can not, in general, be effectively transformed into a maximally distributive one. Show more

DOI: 10.3233/FI-1994-2043

Citation: Fundamenta Informaticae, vol. 20, no. 4, pp. 333-352, 1994

Authors: Baaz, Matthias | Leitsch, Alexander

Article Type: Research Article

Abstract: The impact of Skolemization on the complexity of proofs in the sequent calculus is investigated. It is shown that prefix Skolemization may result in a nonelementary increase of Herbrand complexity (i. e. the minimal number of constituents in a Herbrand disjunction) versus structural Skolemization. Moreover it is shown that restricting the range of quantifiers never increases Herbrand complexity. The results provide a general mathematical justification for minimizing the range of quantifiers (by means of shifting) before Skolemization of formulas.

DOI: 10.3233/FI-1994-2044

Citation: Fundamenta Informaticae, vol. 20, no. 4, pp. 353-379, 1994

Authors: Skandalis, Kostas

Article Type: Research Article

Abstract: In [1] it is proved that for real closed fields the output sets (of computing machines) are also input sets. In this work it is shown that the converse holds for a class of ordered fields. It follows that the uncountable subfields of R are real closed if and only if their output sets are also input sets. Similar results for unordered fields of characteristic 0 are obtained.

DOI: 10.3233/FI-1994-2045

Citation: Fundamenta Informaticae, vol. 20, no. 4, pp. 381-392, 1994