Syntactic And Semantic Representations For Domains

This thesis investigates the methods and techniques that are necessary for representations of some domain categories in the framework of logic.Domains equipped with Scott-continuous functions are the mathematical foundation of denotational semantics of programming languages.Under a logical approach to representing them,elements of a domain are thought of as some theories of a logical calculus or as some filters of the Lindenbaum algebra of a logical calculus,and Scott-continuous functions are thought of as inference engines.This approach provides a simple and suggestive concrete representation about domains,making it easier to study the notions and properties in domain theory and to find and motivate new notions and constructions.For the category of bounded complete domains with Scott-continuous functions,we build a logical system named a conjunctive sequent calculus.It is a conjunctive fragment of the classical Gentzen propositional sequent calculus.We prove that each bounded complete continuous domain D is order-isomorphic to the poset of all logical points of the conjunctive sequent calculus induced by D.By defining a valid sequent between conjunctive sequent calculi,we present a new multi-lingual sequent calculus.The inferences between multi-lingual sequent calculi are called conjunctive consequence relations,which can be used to represent the Scott-continuous functions between complete bounded domains.Moreover,we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category,which is equivalent to that bounded complete domains with Scott-continuous functions.Then a concrete logical characterization for the category of bounded complete domains in the framework of conjunctive sequent calculus is obtained.Every principal ideal in a continuous L-domain is a special bounded complete domain.Noticing this observation,we introduce for every continuous L-domain a logical system within which the local property of continuous L-domains can be easily understood.Such a logical system is called a locally conjunctive sequent calculus and satisfies all the inference rules of a conjunctive sequent in a local sense.The set of logical points of a locally conjunctive sequent calculus forms a continuous L-domain,and each continuous L-domain can be obtained in this way,up to isomorphism.Then we show that conjunctive consequence relations between locally sequent calculi and Scott-continuous functions between continuous L-domains can be induced each other,and thus generalize the relationship between locally conjunctive sequent calculi and continuous L-domains to a categorical equivalence.Based on the disjunctive propositional logic introduced by Yi-xiang Chen etc.,we provide a purely syntactic characterization for algebraic L-domains.We show a special theory of a disjunctive propositional logic generate an algebraic L-domain.To develop the representation theory of disjunctive propositional logic,we definite a category whose objects are the disjunctive propositional calculi.This category is equivalent to that of algebraic L-domains with Scott-continuous functions.In particular,we also give a logical syntactic representation of Scott-domain in the framework of disjunctive propositional logic,and expose interrelationships and fundamental differences between algebraic L-domains and Scott domains on logical level.Finally,by replacing an arbitrary disjunctive connective with a binary disjunctive connective we define the concept of a N-sequent calculus.We show it is sound and complete with FD-lattices.Based on this logic,we provide two kinds of logical representations of Lawson compact algebraic L-domains.The first representation takes FD-lattices as research objects.The use of prime filters achieves the connection between our logic and Lawson compact algebraic L-domains.This approach is inspired by the theory of disjunctive propositional logic.However,there are essential differences from it at the morphisms part.For the second representation,we directly adopt N-sequent calculi themselves as objects instead of the logical algebras.A category induced is equivalent to that of Lawson compact algebraic L-domains with Scott continuous functions.These result allow us to integrate the semantic representation and the syntactic representation of certain domains into the same logical framework.