Probability Calculation And The Likelihood Of Computing The Domain Semantics

With computer technology and network technology development, people turn attention toparallel computation and distributed computation from sequential computation. Parallelcomputation and distributed computation result in the non-determinism of programs, thenon-deterministic computation of programs is an important topic of investigation in computerscience, whose research results can be applied to program specification, program refinement,software combination, the analysis and design of complex software and hardware systems andso on. This kind of nondeterminism has two di?erent cases: classical non-determinism andprobabilistic non-determinism. The former refers to produce the di?erent possible outcomes ofthe program for the same input value, this kind of non-determinism is modelled by three kindsof powerdomains, i.e., Plotkin powerdomain, Smyth powerdomain and Hoare powerdomain.The latter refers to give a probabilistic value of possible outcomes of program for the sameinput, this kind of non-determinism is modelled by probabilistic powerdomain, recently whichis a popular topic, more theoretic computer scientists and mathematician devoted themselvesto this field and got many important results. Since the non-deterministic phenomenons inthe real world include many possibilistic phenomenons besides probabilistic phenomenons, forthis reason, we propose the notion of possibilistic computation, which refers to give a possi-bilistic value of the possible computation outcome of program, this kind of non-determinismis modelled by possibilistic powerdomain.The main aim of this thesis is to provide semantic models for the probabilistic and possi-bilistic non-deterministic computation, main researches consist in the following three aspects:Part 1: Semantic Model of Probabilistic ComputationThe research of probabilistic programs came from Kozen's original work, now there aremain four kinds of the semantic models of probabilistic programs: Kozen's model, C.Jones'model, He's model and C.Morgan's et al models. Our probabilistic computation model isbased on C.Morgan's et al probabilistic computation model. Our researches can be dividedinto two parts: sub-probabilistic programs and probabilistic programs. On sub-probabilisticprograms, introduce sub-probabilistic program language, give its axiomatic semantics and denotational semantics and prove its soundness and completeness theorem. On probabilis-tic programs, our researches can also be divided into two parts: deterministic probabilisticprograms and non-deterministic probabilistic programs. About deterministic probabilisticprograms, we give an approach di?erent from C.Morgran's to characterize healthiness con-ditions, succeed in setting up equivalence between probabilistic predicate transformers anddeterministic probabilistic state transformers. On the other hand, we study non-deterministicprobabilistic programs. Propose the notion of pre-healthiness and prove one side of equiva-lence between pre-healthy probabilistic predicate transformers and non-deterministic proba-bilistic state transformers.Part 2: Semantic Model of Possibilistic ComputationIn this part, we give a kind of possibilistic computation model by the notion of possibilityvaluation, aiming at studying program semantics with possibility. Prove that the possibilisticpowerdomain functor is a monadic functor on the directed complete partial set categoryDcpo. Then point out the equivalence between possibilistic state transformer semantics andpossibilistic predicate transformer semantics. At the same time, put the possibility and theangelic non-determinism together to discuss and give their universal properties.Part 3: Refinement CalculusRefinement calculus is an extension and further development of Dijkstra's weakest pre-condition calculus, recently, Mingsheng Ying studied refinement calculus of probabilistic pro-grams. Based on Mingsheng Ying's some ideas, in this part, our researches consist of twoparts: probabilistic refinement calculus and possibilistic refinement calculus. On one hand,we discuss probabilistic refinement and probabilistic correctness between sub-probabilisticprograms. The two notions re?ect the degree that a sub-probabilistic program is refinedby another sub-probabilistic program and the degree of correctness of a sub-probabilistictriple respectively. Prove that probabilistic refinement between sub-probabilistic programscan be described by probabilistic correctness. On the other hand, we introduce a kind ofrefinement calculus model based on possibility, the aim is to further formalize possibilisticcomputation. We introduce possibilistic belief logic, prove the dualities theorems betweenbasic predicate transformers. Give a su?cient and necessary condition for a possibilistic predicate transformer to be a possibilistic angelic update or possibilistic demonic update.Further, prove the normal form theorem which says that any strongly monotonic possibilisticpredicate transformers can be written as a statement term consisting of a possibilistic angelicupdate followed by a possibilistic demonic update. Moreover, homomorphism properties ofpossibilistic predicate transformers are discussed. At last, we study some important pos-sibilistic predicate transformers: monotone possibilistic predicate transformers, conjunctivepossibilistic predicate transformers and disjunctive possibilistic predicate transformers andprove that all program statements are all strongly monotonic.