Formal computations of non deterministic recursive program schemes

We extend to non deterministic recursive program schemes the methods and results which permit definition of the semantics of such schemes in the deterministic case. Under natural hypothesis the set of finite and infinite trees generated by a scheme is proved to be the greatest fixed point of the functional mapping usually attached to this scheme.     

A Standard Model—Theoretic Approach to Operational Semmantics of Recursiv Programs

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting thr rule“attacking the subtem of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpretation whic includes no undefined value in its domain,Finally,we prove that our new approach generates the same opeational semantics as the traditional one.It is also pointed out that we can use our strategy oto refute a claim of Loeckx and Sieber that the opperational semantics of recursive programs cannot be built based on predicate logic.     

Nondeterministic flowchart programs with recursive procedures: semantics and correctness I

In this paper, we study some aspects of the semantics of nondeterministic flowchart programs with recursive procedures. In the first part of this work we provide the operational semantics of programs using the concept of an execution tree. We propose a new definition of the semantics of a non-deterministic recursive program as a mapping from the input domain to the set of execution trees determined by the program. Using this new concept, we prove that every nondeterministic flowchart program with recursive procedures can be unfolded into a semantically equivalent infinite pure flowchart (without procedures). This result is applied in the second part of this work to prove the soundness of an inductive assertion method which is also complete with a finite number of assertions (contrary to De Bakker and Meertens's method [11]).     

Strict interpretations of deterministic pushdown acceptors

Three results are established. The first is that every nondeterministic strict interpretation of a deterministic pushdown acceptor (dpda) has an equivalent, deterministic, strict interpretation. The second is that ifM ₁ andM ₂ are two compatible strict interpretations of the dpdaM, then there exist deterministic strict interpretationsM andM such thatL(M ) =L(M ₁)L(M ₂) andL(M ) =L(M ₁)L(M ₂). The third states that there is no dpda whose strict interpretations yield all the deterministic context-free languages.This author was supported in part by the National Science Foundation under Grant MCS-77-22323.     

推广的确定性均匀递归树演化模型的拓扑性质

在URT (uniform recursive tree)模型的基础上,提出一种推广的确定性均匀递归树演化模型GDURT (generalized deterministic uniform recursive tree).通过精确推导,求得该模型的累计度分布、平均路径长度、度相关性等拓扑性质,表明了该类网络模型与URT和DURT网络模型类似,为小世界网络,且具有指数度分布和协调的度相关特性,并对产生这些特性的原因作出了分析.     

Information-theoretic characterizations of recursive infinite strings

Loveland and Meyer have studied necessary and sufficient conditions for an infinite binary string x to be recursive in terms of the program-size complexity relative to n of its n-bit prefixes x_n. Meyer has shown that x is recursive iff ?c, ?n, K(x_n?n) ? c, and Loveland has shown that this is false if one merely stipulates that K(x_n?n) ? c for infinitely many n. We strengthen Meyer's theorem. From the fact that there are few minimal-size programs for calculating n given result, we obtain a necessary and sufficient condition for x to be recursive in terms of the absolute program-size complexity of its prefixes: x is recursive iff ?c, ?n, K(x_n) ? K(n) + c. Again Loveland's method shows that this is no longer a sufficient condition for x to be recursive if one merely stipulates that K(x_n) ? K(n) + c for infinitely many n.     

Formalizing non-termination of recursive programs

In applicative theories the recursion theorem provides a term which solves recursive equations. However, it is not provable that a solution obtained by is minimal. In the present paper we introduce an applicative theory in which it is possible to define a least fixed point operator. Still, our theory has a standard recursion theoretic interpretation.     

Realizability of concurrent recursive programs

We study the realizability problem for concurrent recursive programs: given a distributed system architecture and a sequential specification over words, find a distributed automata implementation that is equivalent to the specification. This problem is well-studied as far as finite-state processes are concerned, and it has a solution in terms of Zielonka’s Theorem. We lift Zielonka’s Theorem to the case where processes are recursive and modeled as visibly pushdown (or, equivalently, nested-word) automata. However, contrarily to the finite-state case, it is undecidable whether a specification is realizable or not. Therefore, we also consider suitable underapproximation techniques from the literature developed for multi-pushdown systems, and we show that they lead to a realizability framework with effective algorithms.     

Denotational semantics of communicating sequential programs

A denotational semantics of Hoare's Communicating Sequential Programs is given based on a mathematical model of communicating processes as functions mapping for every initial state a stream of offers onto a set of streams of reactions plus a final state, which is defined only if the program terminates properly. The main purpose of this definition is found in serving as a reference for specification and verification methods.     

Fundamental properties of infinite trees

Infinite trees naturally arise in the formalization and the study of the semantics of programming languages. This paper investigates some of their combinatorial and algebraic properties that are especially relevant to semantics.This paper is concerned in particular with regular and algebraic infinite trees, not with regular or algebraic sets of infinite trees. For this reason most of the properties stated in this work become trivial when restricted either to finite trees or to infinite words.It presents a synthesis of various aspects of infinite trees, investigated by different authors in different contexts and hopes to be a unifying step towards a theory of infinite trees that could take place near the theory of formal languages and the combinatorics of thefree monoid.     

Functional semantics of programs with exceptions

Linguistic mechanisms for exception handling facilitate the production of reliable software and play an important role in fault tolerant computing. This paper describes the functional semantics of a Pascal-like language which supports exception handling and data abstraction. A program with exceptions is considered as having a standard semantics, as well as an exceptional semantics for each exception that may be signaled during its execution. Standard functional semantics methods provide rules to obtain the function representing the standard semantics. In this paper, we provide rules to determine the functions representing the exceptional semantics. We also describe a method for specifying and verifying the correctness of implementation of data types with exceptions.     

On basic semantics of untyped functional programs

The paper is devoted to untyped functional programs, which are defined as systems of equations with separating variables in the untyped γ-calculus [1, 2]. Basic semantics of such programs is usually defined by means of the fixed-point combinator Y. A theorem on semantics invariance with respect to the fixed-point combinator is proved.     

Static semantics for normal and disjunctive logic programs

In this paper, we propose a newsemantic framework for disjunctive logic programming by introducingstatic expansions of disjunctive programs. The class of static expansions extends both the classes of stable, well-founded and stationary models of normal programs and the class of minimal models of positive disjunctive programs. Any static expansion of a programP provides the corresponding semantics forP consisting of the set of all sentences logically implied by the expansion. We show that among all static expansions of a disjunctive programP there is always theleast static expansion, which we call thestatic completion ¯P ofP. The static completion¯P can be defined as the least fixed point of a naturalminimal model operator and can be constructed by means of a simpleiterative procedure. The semantics defined by the static completion¯P is called thestatic semantics ofP. It coincides with the set of sentences that are true inall static expansions ofP. For normal programs, it coincides with the well-founded semantics. The class of static expansions represents a semantic framework which differs significantly from the other semantics proposed recently for disjunctive programs and databases. It is also defined for a much broader class of programs.Dedicated to Jack MinkerPartially supported by the National Science Foundation grant # IRI-9313061.     

Recognisability for algebras of infinite trees

We develop an algebraic language theory for languages of infinite trees. We define a class of algebras called ω-hyperclones and we show that a language of infinite trees is regular if, and only if, it is recognised by a finitary path-continuous ω-hyperclone.     

Axiomatic semantics of R-schemas and verification of graphic programs

We propose an approach to verification of programs in a graphic language in the programming R-technology and introduce an axiomatic semantics of R-schemas and of graphic Pascal. We justify the advantages of graphic representation of programs for correctness proving and describe a support system for this approach under RAFOS and MS-DOS.Translated from Kibernetika, No. 1, pp. 21–27, January–February, 1990.     

Space efficient execution of deterministic parallel programs

We model a deterministic parallel program by a directed acyclic graph of tasks, where a task can execute as soon as all tasks preceding it have been executed. Each task can allocate or release an arbitrary amount of memory (i.e., heap memory allocation can be modeled). We call a parallel schedule “space efficient” if the amount of memory required is at most equal to the number of processors times the amount of memory required for some depth-first execution of the program by a single processor. We describe a simple, locally depth-first scheduling algorithm and show that it is always space efficient. Since the scheduling algorithm is greedy, it will be within a factor of two of being optimal with respect to time. For the special case of a program having a series-parallel structure, we show how to efficiently compute the worst case memory requirements over all possible depth-first executions of a program. Finally, we show how scheduling can be decentralized, making the approach scalable to a large number of processors when there is sufficient parallelism     

Well-founded semantics and stratification for ordered logic programs

This paper present an extension of traditional logic programming, called ordered logic (OL) programming, to support classical negation as well as constructs from the object-oriented paradigm. In particular, such an extension allows to cope with the notions of object, multiple inheritance and non-monotonic reasoning. The contribution of the work is mainly twofold. First, a rich wellfounded semantics for ordered logic programs is defined. Second, an efficient method for the well-founded model computation of a meaningful class of ordered logic programs, called stratified programs, is provided.     

Efficient parallel execution of irregular recursive programs

Programs whose parallelism stems from multiple recursion form an interesting subclass of parallel programs with many practical applications. The highly irregular shape of many recursion trees makes it difficult to obtain good load balancing with small overhead. We present a system, called REAPAR, that executes recursive C programs in parallel on SMP machines. Based on data from a single profiling run of the program, REAPAR selects a load-balancing strategy that is both effective and efficient and it generates parallel code implementing that strategy. The performance obtained by REAPAR on a diverse set of benchmarks matches that published for much more complex systems requiring high-level problem-oriented explicitly parallel constructs. A case study even found REAPAR to be competitive to handwritten (low-level, machine-oriented) thread-parallel code