We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, withthe striking omi...
详细信息
ISBN:
(纸本)354043366X
We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, withthe striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.
the logic C(Q(u)) extends first-order logic by a generalized form of counting quantifiers ("the number of elements satisfying ... belongs to the set C"). this logic is investigated for structures with an inj...
详细信息
ISBN:
(纸本)3540330453
the logic C(Q(u)) extends first-order logic by a generalized form of counting quantifiers ("the number of elements satisfying ... belongs to the set C"). this logic is investigated for structures with an injective omega-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [4]. It is shown that, as in the case of automatic structures [13], also modulo-counting quantifiers as well as infinite cardinality quantifiers ("there are n many elements satisfying ...") lead to decidable theories. For a structure of bounded degree with injective omega-automatic presentation, the fragment of L(Q(u)) that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (omega-automaticity and bounded degree) are necessary for this result to hold.
We present a semantic analysis of a recently proposed formalism for local reasoning, where a specification (and hence proof) can concentrate on only those cells that a program accesses. Our main results are the soundn...
详细信息
ISBN:
(纸本)354043366X
We present a semantic analysis of a recently proposed formalism for local reasoning, where a specification (and hence proof) can concentrate on only those cells that a program accesses. Our main results are the soundness and, in a sense, completeness of a rule that allows frame axioms, which describe invariant properties of portions of heap memory, to be inferred automatically;thus, these axioms can be avoided when writing specifications.
Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper ...
详细信息
ISBN:
(数字)9783540319825
ISBN:
(纸本)3540253882
Term rewriting systems provide a versatile model of computation. An important property which allows to abstract from potential nondeterminism of parallel execution of the modelled program is confluence. In this paper we prove that confluence of a fairly large class of systems, namely right ground term rewriting systems, is decidable. We introduce a labelling of variables with colours and constrain substitutions according to these colours. We show how right ground rewriting systems can be reduced to simple systems with coloured variables. Such systems can be analysed using reduction-automata techniques which leads to an interesting decision procedure for confluence.
We present a calculus of "circular proofs": the graph underlying a proof is not a finite tree but instead it is allowed to contain a certain amount of cycles. the main challenge in developing a theory for th...
详细信息
ISBN:
(纸本)354043366X
We present a calculus of "circular proofs": the graph underlying a proof is not a finite tree but instead it is allowed to contain a certain amount of cycles. the main challenge in developing a theory for the calculus is to define the semantics of proofs, since the usual method by induction on the structure is not available. We solve this problem by associating to each proof a system of equations - defining relations among undetermined arrows of an arbitrary category with finite products and coproducts as well as constructible initial algebras and final coalgebras - and by proving that this system admits always a unique solution.
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing pr...
it is generally thought that reasoning about programs in memory safe, garbage collected languages is much easier than in languages where the programmer has more explicit control over memory. Paradoxically, existing program logics are based on a low-level view of storage that is sensitive to the presence or absence of unreachable cells, and Reynolds has pointed out that the Hoare triples derivable in these logics are even incompatible with garbage collection. We present a study of a small language whose operational semantics includes a rule for reclaiming garbage. Our main results include an analysis of propositions that are garbage insensitive, and full abstraction results connecting partial and total correctness to two natural notions of observational equivalence between programs. (C) 2002 Elsevier science B.V. All rights reserved.
A timed extension of pi-calculus with a transaction construct - the calculus Web pi - is studied. the underlying model of Web pi relies on networks of processes;time proceeds asynchronously at the network level, while...
详细信息
ISBN:
(数字)9783540319825
ISBN:
(纸本)3540253882
A timed extension of pi-calculus with a transaction construct - the calculus Web pi - is studied. the underlying model of Web pi relies on networks of processes;time proceeds asynchronously at the network level, while it is constrained by the local urgency at the process level. Namely process reductions cannot be delayed to favour idle steps. the extensional model - the timed bisimilarity - copes with time and asynchrony in a different way with respect to previous proposals. In particular, the discriminating power of timed bisimilarity is weaker when local urgency is dropped. A labelled characterization of timed bisimilarity is also discussed.
Differential dataflow is a recent approach to incremental computationthat relies on a partially ordered set of differences. In the present paper, we aim to develop its foundations. We define a small programming langu...
详细信息
ISBN:
(纸本)9783662466780;9783662466773
Differential dataflow is a recent approach to incremental computationthat relies on a partially ordered set of differences. In the present paper, we aim to develop its foundations. We define a small programming language whose types are abelian groups equipped with linear inverses, and provide both a standard and a differential denotational semantics. the two semantics coincide in that the differential semantics is the differential of the standard one. Mobius inversion, a well-known idea from combinatorics, permits a systematic treatment of various operators and constructs.
the domain decomposition method (DDM) is an efficient algorithmic tool for the parallelization of finite element computer codes. A variant of the DDM with direct solution algorithm is based on computation of Schur com...
详细信息
the domain decomposition method (DDM) is an efficient algorithmic tool for the parallelization of finite element computer codes. A variant of the DDM with direct solution algorithm is based on computation of Schur complement matrices for finite element partitions. this paper describes a simple technique that considerably improves execution rate of computationally intensive routines of the Schur complement computations, the technique uses 'block of columns' matrix operations and loop unrolling to reduce load instructions from cache memory and to increase instruction-level parallelism. For superscalar RISC processors, experimental results show that it is possible to improve performance of the DDM solution procedure by several times. (C) 2000 Civil-Comp Ltd. and Elsevier science Ltd. All rights reserved.
We show that there exist c.e. bounded Turing degrees a, b such that 0 = a. the result gives an unexpected definability theorem in the structure of bounded Turing reducibility.
We show that there exist c.e. bounded Turing degrees a, b such that 0 < a < 0', and that for any c.e. bounded Turing degree x, we have b boolean OR x = 0' if and only if x >= a. the result gives an unexpected definability theorem in the structure of bounded Turing reducibility.
暂无评论