To appear in Theoretical Computer Science.
Order-Incompleteness and Finite Lambda Reduction Models
Peter Selinger
Abstract
Many familiar models of the untyped lambda calculus are constructed by order theoretic methods.This paper pro-
vides some basic new facts about ordered models of the lambda calculus.We show that in any partially ordered model
that is complete for the theory of-or-conversion,the partial order is trivial on term denotations.Equivalently,the
open and closed term algebras of the untyped lambda calculus cannot be non-trivially partially ordered.Our second
result is a syntactical characterization,in terms of so-called generalized Mal’cev operators,of those lambda theories
which cannot be induced by any non-trivially partially ordered model.We also consider a notion of?nite models for
the untyped lambda calculus,or more precisely,?nite models of reduction.We demonstrate how such models can be
used as practical tools for giving?nitary proofs of term inequalities.
1Introduction
Perhaps the most important contribution in the area of mathematical programming semantics was the discovery,by D.Scott in the late1960’s,that models for the untyped lambda calculus could be obtained by a combination of order-
theoretic and topological methods.A long tradition of research in domain theory ensued,and Scott’s methods have
been successfully applied to many aspects of programming semantics.
On the other hand,there are results that indicate that Scott’s methods may not in general be complete:Honsell and
Ronchi Della Rocca[8]have shown that there exists a lambda theory that does not arise as the theory of a re?exive model in the cartesian-closed category of complete partial orders and Scott-continuous functions.Moreover,there are
desirable properties of a model that are incompatible with the presence of a partial order:for instance,Plotkin[13],
answering a question of H.Friedman,has recently shown that there exists an extensional lambda algebra which is ?nitely separable.A?nitely separable algebra can never be non-trivially partially ordered.
In this paper we establish some basic new facts about ordered models of the untyped lambda calculus.We show
that the standard open and closed term algebras are unorderable,i.e.,they cannot be non-trivially partially ordered as combinatory algebras.Recall that the standard term algebras are made up from lambda terms,taken up to-or -equivalence.It follows that if a partially ordered model of the untyped lambda calculus is complete for one of the theories,then the denotations of closed terms in that model are pairwise incomparable,i.e.,the term
denotations form an anti-chain.
We also consider the related question of order-incompleteness:does there exist a lambda theory(possibly with constants)which does not arise as the theory of a non-trivially ordered model?Equivalently,does there exist a lambda algebra which cannot be embedded in a non-trivially ordered model?Let us call such an algebra absolutely unorder-able.Plotkin conjectures in[13]that an absolutely unorderable lambda algebra exists.Here,we give an algebraic characterization,in terms of so-called Mal’cev operators,of the absolutely unorderable-algebras in any algebraic variety.This reduces the question of order-incompleteness for the lambda calculus to the question whether one can consistently add a family of Mal’cev operators to the lambda calculus.The answer is still unknown in the general case,but we prove that it is inconsistent for.
The characterization of absolutely unorderable-algebras in terms of Mal’cev operators leads to an interesting technical observation about free order-algebras and dcpo-algebras.In a given variety of order-algebras,one may consider the free order-algebra ord generated by a poset.The question arises under what conditions ord is conservative over,i.e.,under what conditions the canonical map ord is order-re?ecting.An analogous
1
question can be asked for dcpo-algebras.Here,we give a necessary and suf?cient condition:we show that the answer
is completely determined by whether the given variety has a family of Mal’cev operators.
In the last part of this paper,we introduce a novel technique for proving inequalities of lambda terms.At the heart of this technique is the notion of a?nite lambda reduction model.It is well-known that a model of an equational
theory of the lambda calculus can never be?nite or even recursive[2].Instead,we consider models of reduction, which are not subject to the same limitations on size and complexity.A model of reduction is equipped with a partial order,and it satis?es a soundness property of the form,where denotes e.g.-or-
reduction[6,10,12].One can understand such models as making precise certain invariants of terms under reduction. By combining this with the Church-Rosser property,one recovers a limited form of reasoning about convertibility.
Our key observation is that models of reduction,unlike models of conversion,may be?nite,and that even a?nite such model can carry non-trivial information.We give a practical method for constructing such models,and we give two examples in which we use?nite reduction models to demonstrate the inequality of some unsolvable lambda terms.
2Unorderability
The main result of this section is that the open and closed term algebras of the untyped lambda calculus do not admit a
non-trivial partial order compatible with the model structure.We follow Barendregt’s notation for the lambda calculus [2].Let us begin by?xing some terminology.A preorder is said to be discrete if implies,indiscrete
if holds for all,and symmetric if.By a trivial preorder,we mean either the discrete or indiscrete preorder.A partial order is of course trivial iff it is discrete iff it is symmetric.
Recall that a combinatory algebra consists of a set,a binary operation,and
distinguished elements satisfying and.As usual,we write for and for .We say that a preorder on a combinatory algebra is compatible if application is monotone in both arguments,i.e.,and implies.
A combinatory algebra is called unorderable if every compatible partial order on it is trivial.It is known that such algebras exist.For example,Plotkin[13]has recently constructed a?nitely separable algebra,a property which implies unorderability.Here is said to be?nitely separable if for every?nite subset,every function is the restriction of some,meaning that for all,.Finitely separable combinatory algebras do not allow non-trivial preorders,because if for some,then for all via some with and.The present result differs from this,because our unorderable algebras,the open and closed term algebras of the untyped lambda calculus,occur“naturally”.
2.1Lambda terms cannot be ordered
Let be the set of(-equivalence classes of)untyped lambda terms,build from a set of constant symbols and a countable supply of variables.Let be the subset of closed terms.
De?nition.The open term algebra of the-calculus is the combinatory algebra,where is the application operation on terms,and and are the terms and,respectively.The closed term algebra is de?ned analogously,and similarly for the-calculus.
Note that these term algebras are not?nitely separable:e.g.the terms and cannot be separated,since the?rst one is unsolvable[2].Also,the term algebras allow non-trivial pre orders:for instance, two terms are ordered if and only if their meanings in the standard-model are ordered.
Suppose now that we want to construct a partial order on,say,the open term algebra of the-calculus.An obvious approach is the following:take two distinct variables and,and let be the preorder generated by a single inequation.It is not hard to see that for this preorder,one has iff is obtained from up to-equivalence by replacing some,but not necessarily all occurrences of the variable by.More precisely,iff there is a term(not itself containing or)such that and.
It follows that,and thus this preorder is non-trivial.However,the following proposition implies that is not a partial order.
2
Proposition2.1.There exists a closed term of the untyped lambda calculus,such that,but ,for variables.
Proof.The idea of the proof is as follows:Via a?xpoint combinator,de?ne a term such that
for variables.In other words,any three applications of are equivalent to a single application.Now let
.Then clearly.It remains to be shown that.We delay the proof of this inequality until Section4.4.2below,where we prove it using the notion of?nite lambda reduction models.
Note that the proposition implies that is not a partial https://www.doczj.com/doc/8f17786696.html,ly,one has
,but since,the preorder is not antisymmetric.
By the same reasoning,and cannot be related in any compatible partial order on open terms.Thus any such partial order is discrete on variables.To show this section’s main result,we need to lift this reasoning from variables to arbitrary terms.This is achieved by the following lemma,which states that,if is a fresh variable,then and behave essentially like indeterminates:any equation that holds for and will hold for variables and .Let be one of the theories,and let be the corresponding reduction relation.
Lemma2.2.Let be terms that are distinct in,and let be a variable not free in.Then for all terms with FV,and for variables,
implies
Proof.Let FV.In the following,we assume without loss of generality that the names of all bound variables are different from elements of.Let be the set of all lambda terms with the following property:the variable occurs only in subterms of the form,where for some.For each,let be the lambda term obtained from by replacing each subterm of the form by if.Formally ,,,if,and if.Then the following hold:
(a)For all and,and.
(b)For all,if then and.
(c)For all,if then.
(a)and(b)are easily proved by induction.(c)follows from(b)by the Church-Rosser property of.Finally, the lemma follows by observing that and are in,and and.
Theorem2.3.Let be the open or the closed term algebra of the-or-calculus.Then does not allow a non-trivial compatible partial order.
Proof.Let be a compatible partial order on.Let,and assume,by way of contradiction,that .Let be as in Proposition2.1,and let be a fresh variable.Then by compatibility,
hence,by antisymmetry,
Applying Lemma2.2to and,one gets for variables and, contradicting the choice of.Consequently,the order is trivial.
Corollary2.4.In any partially ordered model of the untyped lambda calculus whose theory is,the deno-tations of closed terms are pairwise incomparable.
3
2.2Lambda unorderability
We have called a preorder on a combinatory algebra compatible if it respects the application operation.In addition,one can require that also respects abstraction.Abstraction is a well-de?ned operation if is a lambda algebra[2,14].Thus,we de?ne a lambda preorder on a lambda algebra to be a compatible preorder such that
models:an unorderable model can still arise from an order-theoretic construction,for instance as a subalgebra of some orderable model.
Indeed,it is not hard to see that the open and closed term algebras,as considered in the previous section,can be embedded in an orderable model:this follows e.g.from Theorem3.4below.A different(and,from a model-theoretic point of view,more interesting)construction of an ordered model in which the open term algebra is embedded can be found in Di Gianantonio et al.[5].
This leads us to the related question of absolute unorderability:a model is absolutely unorderable if it cannot be embedded in an orderable one.Plotkin conjectures in[13]that an absolutely unorderable combinatory algebra exists,but the question is still open whether this is so.In this section,we present what is known:we give a syntactic characterization of the absolutely unorderable algebras in any algebraic variety in terms of the existence of a family of Mal’cev operators.Plotkin’s conjecture is thus reduced to the question whether Mal’cev operators are consistent with the lambda calculus.
The question of absolute unorderability can also be formulated in terms of theories,rather than models.In this form,we refer to it as the order-incompleteness question:does there exist a lambda theory(possibly with constants) which does not arise as the theory of an ordered model?This question is obviously equivalent to the question of the existence of an absolutely unorderable algebra.
A property that is related to order-incompleteness,but much weaker,is the well-known topological incompleteness. Addressing the latter,Honsell and Ronchi Della Rocca[8]have shown that there is a lambda theory which is not the theory of any re?exive CPO-model.However,their theory is not order-incomplete,and the methods used in investigating topological incompleteness are quite different from those used here.We should mention that the question whether arises as the theory of a re?exive CPO-model is still open.
3.1A characterization of absolutely unorderable algebras
Let be an algebraic variety(given by a signature and equations).We say that a preorder on a-algebra is compatible if for implies,for each-ary function symbol in the signature of.Notice that compatible preorders are closed under arbitrary intersections.If is compatible,then so is the dual preorder.Every compatible preorder determines a congruence on,which is the intersection of and.Also notice that naturally de?nes a partial order on.
A-algebra is said to be unorderable if it does not allow a non-trivial compatible partial order.Also,is said to be absolutely unorderable if for any embedding of-algebras,is unorderable.
Now consider a-algebra.As usual,denotes the-algebra obtained from by freely adjoining indeterminates.We regard as a subset of.Let be the smallest compatible preorder on such that.
Lemma3.1.is discrete on,i.e.,for.
Proof.Let be the kernel of the canonical homomorphism which sends both and to.Then and is discrete on.
Lemma3.2.is absolutely unorderable if and only if.
Proof.For the left-to-right implication,suppose is absolutely unorderable.Consider the natural map .Lemma3.1implies that the composition is an embedding,hence must be discrete as a partial order on.Equivalently,as a preorder on is symmetric,and thus.For the converse,suppose is not absolutely unorderable.Then there is an embedding of-algebras where has a non-trivial compatible partial order.Choose such that,and consider the unique map such that,and.De?ne in iff in.Then is a compatible preorder on with,hence is contained in.But,hence.
Further,has the following explicit description:On,de?ne if and only if there is a polynomial such that and.
Lemma3.3.is the transitive closure of.
5
Proof.Let be the transitive closure.Clearly,is a preorder contained in,and it satis?es.Moreover,, and thus,is compatible,as can be seen by considering terms of the form
for each-ary function symbol.Since is smallest with these properties,it follows that.
Putting together Lemmas3.2and3.3,we get the following characterization of absolutely unorderable algebras. We say that an equation holds absolutely in if it holds in.
Theorem3.4.Characterization of absolutely unorderable-algebras.Let be an algebraic variety.A-algebra is absolutely unorderable if and only if,for some,there exist polynomials M, for,such that the following equations hold absolutely in:
M
M M
M M(2)
..
.
M
Proof.By Lemmas3.2and3.3,is absolutely unorderable if and only if there are such that .The theorem follows by de?nition of.
In the case,the equations(2)have the simple form M and M.A ternary operator M satisfying these equations is called a Mal’cev operator,after A.I.Mal’cev,who studied such operators to characterize varieties of congruence-permutable algebras[11].Accordingly,we call M M satisfying(2)a family of gen-eralized Mal’cev operators,and we call the equations(2)the generalized Mal’cev axioms.Hagemann and Mitschke [7]have shown that an algebraic variety has-permutable congruences if and only if it has a family of generalized Mal’cev operators.It was proved by W.Taylor[15,4]that algebras in a variety with-permutable congruences are unorderable;however,the converse is a new result.Also note that Theorem3.4characterizes individual algebras that are absolutely unorderable,rather than varieties of unorderable algebras.
3.2An application to order-algebras and dcpo-algebras
A compatibly partially ordered algebra over a given signature is called an-order-algebra.Moreover,it is called a-dcpo-algebra if the order is directed complete and the algebra operations are continuous.Let be a set of inequations between terms in the language of.A-order-algebra satisfying these inequations is called a -order-algebra,and similarly for dcpo-algebras.For more details,see[1]or[14].
Fix and.For any poset,there exists a free-order-algebra ord,with a canonical monotone map
ord.Similarly,for any dcpo,there exists a free-dcpo-algebra dcpo with a canonical continuous map dcpo[1].
One may ask under which circumstances the canonical map is order-re?ecting,i.e.,under what conditions the free order-or dcpo-algebra conservatively extends the order on the generators.The following theorem shows that the answer depends only on the presence of generalized Mal’cev operators in.Recall that a-ary operation in is simply a term in the signature.
Theorem3.5.Let be a signature and a set of inequations.Let be a non-trivially ordered dcpo,and let be a non-trivially ordered poset.The following are equivalent:
1.The canonical map dcpo from into the free-dcpo-algebra is not order-re?ecting.
2.Every-dcpo-algebra is trivially ordered.
3.The canonical map dcpo from into the free-order-algebra is not order-re?ecting.
4.Every-order-algebra is trivially ordered.
6
5.There are ternary operations M M in such that entails
M
M M
M M(3)
..
.
M
Proof.1. 2.:Suppose is a non-trivially ordered-dcpo-algebra with elements.We show that is order-re?ecting.Let with.De?ne by
if
if
Then is continuous;therefore,by the universal property of dcpo,there exists a unique continuous homomorphism
dcpo such that.By monotonicity of,we get,hence .
2. 1.:A map dcpo from a non-trivially ordered set into a trivially ordered one cannot be order-re?ecting.
3. 4.:Same as1. 2.,replacing the word“continuous”by“monotone”.
2. 4.:Suppose there is a non-trivially ordered-order-algebra.We consider the ideal completion of:
A subset is an ideal if it is downward closed and directed.Let Idl be the ideal completion of,i.e.,the set of all ideals,ordered by inclusion.Abramsky and Jung[1]prove that Idl is a-dcpo-algebra.Moreover,the map Idl is order preserving and re?ecting,and hence Idl is non-trivially ordered.
4. 5.:Let be a countable set of variables,and let ord be the free-order-algebra over discrete.If every
-order-algebra is trivially ordered,then so is ord,which implies that ineq iff ineq.We can therefore regard as a set of equations.The claim follows by applying Theorem3.4to ord.
5. 2.:Suppose has operators satisfying(3).Then for any-dcpo-algebra,if,then
M M M,hence is trivially ordered.
Remark.Notice that the implication5. 4.shows that the inequalities(3)already imply the corresponding equalities (2).
3.3Absolute unorderability and the lambda calculus
In the lambda calculus,a term M can be expressed in curried form as M.Plotkin posed the question whether an absolutely unorderable lambda algebra exists[13].Clearly,this is the case if and only if,for some,the equations(2)are consistent with the lambda calculus.Unfortunately,it is not known whether this is true except in the cases and.In these cases,(2)is inconsistent with the lambda calculus,as we will now show.Notice that if the axioms are consistent for some,then also for all,by letting M M
Let be any?xpoint operator of combinatory logic,for instance the paradoxical?xpoint combinator
.We write for.The operator satis?es the?xpoint property:
(?x)
The diagonal axiom is
Lemma3.6(Plotkin,Simpson).Assuming the diagonal axiom,the generalized Mal’cev axioms(2)are inconsistent with the lambda calculus for all.
7
Proof.Let be arbitrary.Then
M by(2)
M by
M by(?x)
M by(2)
M
by(2).
Hence for all,which is an inconsistency.
Theorem3.7(Plotkin,Simpson).For,the Mal’cev axioms are inconsistent with the lambda calculus. Proof.Suppose M is a Mal’cev operator.Let be arbitrary and let M.Then
(?x)M(?x)M
hence M M.
Theorem3.8(Plotkin,Selinger).For,the generalized Mal’cev axioms are inconsistent with the lambda calculus.
Proof.Suppose M and M are operators satisfying the generalized Mal’cev axioms(2).De?ne and by mutual recursion such that
M M
M M
Then
M M by(?x)
M M by(2)
by(?x).
So M M M M,which is the diagonal axiom.By Lemma3.6,this leads to an inconsistency.
4Finite Lambda Reduction Models
It is well-known that a model of the untyped lambda calculus,in the traditional equational sense,can never be?nite or even recursive[2].Consequently,model constructions of the lambda calculus typically involve passing to an in?nite limit,yielding unwieldy models in which term denotations or equality of terms are not effectively computable.
By contrast,if one considers models of reduction,rather than of conversion,there is no such limitation on size or complexity.As we will see,it is quite possible for a model of reduction to be?nite and yet https://www.doczj.com/doc/8f17786696.html,rmally,by a model of conversion,we mean a model with a soundness property of the form
where is e.g.-or-convertibility,and is the semantic interpretation function.On the other hand,a model of reduction has an underlying partial order and a soundness property of the form
where is e.g.-or-reduction.Models of reduction have been considered by different authors[6,10,12].We will focus here on a formulation which was given by Plotkin[12]in the spirit of the familiar syntactical lambda models [2].
8
4.1Syntactical models of reduction
As before,let be the set of variables of the lambda calculus,and let be the set of untyped lambda terms up to -equivalence.To keep the notation simple,we do not consider constant symbols in this section,although they could be easily added.For a partially ordered set,let be the set of all valuations,i.e.,functions from to.
De?nition.(Plotkin[12])A syntactical model of-reduction consists of a poset,a monotone binary operation,and an interpretation function
such that the following properties are satis?ed:
1.
2.
3.,for all
4.FV FV
5.
Moreover,we say is a syntactical model of-reduction,if it also satis?es the property
6.,if FV.
The usual syntactical lambda models(of conversion)[2]arise as the special case where is discretely ordered.
Note that properties1.–3.do not form an inductive de?nition of the function.In general,is not uniquely determined by.
Notice that the partial order on a model of reduction differs from the partial order on a model of conversion,as considered in the?rst part of this paper.The order on an ordered model of conversion is commonly understood as an information order,where means that is“less de?ned”than.On the other hand,models of reduction have a reduction order,where means reduces to.One has the following soundness properties:
Proposition4.1(Plotkin[12]).The following are properties of syntactical models of-reduction:
1.Monotonicity.If for all,then.
2.Substitution..
3.Soundness for reduction.If,then.In a syntactical model of-reduction:If,
then.
The soundness property for reduction does not in general yield useful information about convertibility,since in-terconvertible terms may have different denotations.However,if the reduction relation satis?es the Church-Rosser property,as is the case for-and-reduction,then implies that and for some term.Thus,in a model of-or-reduction,we get the following,restricted form of soundness for convertibility. Recall that two elements and in a poset are called compatible,in symbols,if there exists with and .
(4)
This property can be useful for reasoning about non-equality of terms,particularly if the underlying poset has many pairs of incompatible elements.For this reason,we will be especially interested in the cases where is a?at partial order,or a tree,or more generally,a bounded complete domain.Recall that a bounded complete domain is a non-empty poset in which all bounded subsets and all directed subsets have a least upper bound.Note that any bounded complete domain has a least element.
9
4.2Constructing models of-reduction
Syntactical models of-reduction are constructed much more easily than models of conversion.To start with a trivial example,take any pointed poset and monotone function,and de?ne,somewhat uningeniously, .Among the possible interpretation functions for given and,this choice is the minimal one.
Much more interesting is the situation in which there exists a maximal choice for.Note that,in light of the soundness property for convertibility(4),it is desirable for to be as large as possible,so as to discriminate more terms.We will now explore a suf?cient condition for a maximal to exist,in the case where is a bounded complete domain.
De?nition.A monotone function is compatible-extensional if for all,
The construction in Proposition4.2yields a model of-reduction if is order-extensional.More generally: Lemma4.4.If is a syntactical model of-reduction and is order-extensional,then is a model of-reduction.
10
Table1:Multiplication table for a?at model
.. ...
.
..
.
..
.
..
.
..
.
Proof.Suppose FV.Then for all,,hence .
We note that in the special case where is a tree,order-extensionality is a consequence of compatible-extensionality and extensionality:
Lemma4.5.If is a tree,and if is compatible-extensional and extensional,then it is also order-extensional. Proof.Suppose for all,,hence,hence by compatible-extensionality.Since is a tree,either or.In the?rst case,we are done;in the second case,,and hence,for all,which implies by extensionality.
4.4Examples:two?at models
In the following examples,we consider models where the underlying poset is?at,i.e.,for a discrete set, and where the application operation is strict in both arguments.We call these models?at models,and remark that the application operation on such a model is equivalently given by a partial function.If is?nite,the function can be given by a“multiplication table”,and it is easy to read properties such as compatible-extensionality from the de?ning table.For instance,is compatible-extensional if no two rows of the table are compatible,and it is order-extensional if no row is subsumed by another.In particular,if the table is everywhere de?ned,then both compatible-extensionality and order-extensionality coincide with(ordinary)extensionality.
4.4.1A class of?nite models to distinguish the terms
Let be a variable and de?ne and for.Let and.None of these terms,for,have a normal form,e.g.reduces only to itself.The terms are unsolvable; therefore,their interpretations coincide with in the-model[9,16].We will now give a class of?nite?at models that distinguishes them.
Fix an integer and let,regarded as integers modulo with addition and subtraction. De?ne by
if
if
A“multiplication table”for this operation is shown in Table1.Clearly,the application operation de?ned in this way is compatible-extensional and order-extensional.De?ne as in Proposition4.2to get a model of-reduction.For ,we calculate and for.Hence,for all and,
11
Table2:Values for and
Hence,for,and we have iff.Thus,each pair of terms,is distinguished in one of these models.
Note that the syntactic invariant picked out by these models can also be formulated syntactically,approximately as follows:in a term of the form,pick out the last subterm,and determine the power of in it.In general,the invariants picked out by a?nite model can be much more complex.
4.4.2Proof of Proposition2.1:A non-trivial3-element model
In this section,we will apply a?nite model of reduction to?nish the proof of Proposition2.1.Recall that we are showing that there exists a closed term of the untyped lambda calculus,such that,but ,for variables.As outlined before,the idea is to let,where is a term such that.Such an can be easily constructed via a?xpoint combinator.We de?ne via the paradoxical?xpoint combinator,which leads to the following concrete term for:
,where.
Clearly.To see that for variables and,we will construct a3-element?at model.Let,and let be de?ned by the following“multiplication table”:
checked that this is again a model of-,respectively,-reduction.As a trivial consequence,one has the following completeness theorem for convertibility in models of reduction:
https://www.doczj.com/doc/8f17786696.html,pleteness:If,then there exists a?at reduction model and for which. If,then the model can be chosen to be compatible-extensional.
Proof.Take a model of conversion such that for some,e.g.a term model.Then its lift is a?at model with.
Of course this completeness property is not very interesting.A much more interesting question is how close one can come to a?nite completeness theorem for models of reduction.Can every inequality be demonstrated in a?nite model of reduction?The answer to this question is no,since such a?nite completeness theorem would yield a decision procedure for convertibility of lambda terms,which is known to be an undecidable problem.However,it would be interesting to identify subclasses of terms for which a?nite completeness property holds,or to describe the class of equations that hold in all?nite models of reduction,in all?at models,etc.
4.6Categorical models of reduction
In this section,we investigate the relationship between syntactic and categorical models of reduction.By an order-enriched cartesian-closed category,we mean a cartesian-closed category(ccc)where each hom-set is equipped with a partial order,such that composition is monotone,and such that the natural isomorphisms
and are order-isomorphisms.
De?nition.A categorical model of-reduction is given by an object in an order-enriched ccc,together with a pair of morphisms and,such that,in diagrams:
If moreover,then is a categorical model of-reduction.
Categorical models of reduction have been studied by various authors,e.g.by Girard[6]for the case of qualitative domains,or by Jacobs et al.[10],where they are called models of expansion.For a detailed discussion of these and other references,see Plotkin[12].One can interpret each lambda term with free variables in as a morphism in the standard way by induction on.Here is used in the interpretation of application,and in the interpretation of abstraction.One gets the following soundness property:
Proposition4.7.Soundness for reduction.In a categorical model of-reduction,if,then. In a categorical model of-reduction,if,then.
We say that an object in an order-enriched ccc is order-well-pointed if for all,whenever
for all,then.Notice that this implies that is well-pointed.But in addition,it implies that the hom-set is ordered pointwise,which is not a consequence of well-pointedness,as can be seen in any ccc of stable functions[3].
Proposition4.8.Suppose is a categorical model of-reduction and is order-well-pointed.Then a syn-tactical model of-reduction is obtained by setting,,and by de?ning inductively:
Moreover,if,then is a syntactical model of-reduction.
13
Proof.The only interesting part is to show that,an abuse of notation,denotes a well-de?ned morphism. This is best seen by observing that for any,
In Section4.2,we considered the situation where can be chosen maximally with respect to given.In the categorical setting,this corresponds to the situation where is right adjoint to.The following is the analogue of Proposition4.2in categorical language:
Proposition4.9.In the category of posets,let be a bounded complete domain,and let preserve bounded suprema.De?ne.Then has a right adjoint in the category of posets if and only if is compatible-extensional.
Proof.For one direction,suppose has a right adjoint.Suppose such that for all .De?ne for every.The function is monotone,and, hence,and thus.Therefore,is compatible-extensional.Conversely,suppose is compatible-extensional.For any,consider the set.Since is strict,is non-empty.Consider any.Because,we have for all,hence by strong extensionality.Let .Because preserves existing suprema,.Hence,is directed,and we can de?ne. Clearly,the function thus de?ned is monotone,and iff iff.Therefore.
Note that the right adjoint need not in general be continuous.For this reason,the proposition refers to the category of posets,and not to the category of bounded complete domains.
4.7Models of reduction and-models
Consider a categorical model of reduction in the category CPO,such that.For instance,any?nite model of-reduction of the kind discussed in Section4.2is of this form.Then and form an embedding-projection pair,and one can use them as the basis for carrying out Scott’s-construction.It is natural to ask how the resulting -model is related to the original model of reduction.
As usual,construct the model as the bilimit of the sequence and,connected by embedding-projection pairs.Let and be the limiting morphisms.
Note that each is a categorical model of reduction,and is a categorical model of conversion.Let and be the respective interpretation functions.They are related as follows.For a valuation ,let.Then for all lambda terms,
In particular,it follows that for every,and by applying to both sides,. Equality does not in general hold.The following proposition further relates these models:
Proposition4.10.If and are lambda terms such that,then for all,.The converse holds if is bounded complete(this is the case,for instance,if was bounded complete).
Proof.Suppose.Let such that.Then,and similarly for.For the converse,assume is bounded complete.Assume that for all,. Then for all.Let in.Then is an increasing sequence and,and similarly,hence.
As a consequence,any two terms that can be distinguished in a?nite model of-reduction,of the kind discussed in Section4.2,can also be distinguished in a-model over a?nite base domain.In particular,the terms can be distinguished in such a model,as can the terms and of Proposition2.1.This is perhaps surprising, since such unsolvable terms are identi?ed with in the“standard”model constructed from a two-element domain.
14
Acknowledgments
I would like to thank Gordon Plotkin for introducing me to the problem of partial orders on term models,and for many stimulating discussions.Thanks to Furio Honsell,Simona Ronchi,and Alex Simpson for helpful discussions, and to Martina Fischer for pointing me to the application to dcpo-algebras.Thanks to the anonymous referees for their valuable comments.
References
[1]S.Abramsky and A.Jung.Domain theory.In S.Abramsky,D.M.Gabbay,and T.S.E.Maibaum,editors,
Handbook of Logic in Computer Science,volume3,pages1–168.Clarendon Press,1994.
[2]H.P.Barendregt.The Lambda Calculus,its Syntax and Semantics.North-Holland,2nd edition,1984.
[3]G.Berry.Stable models of typed-calculi.In Proceedings of the5th International Colloquium on Automata,
Languages and Programming,Springer LNCS62,pages72–89,1978.
[4]S.Bulman-Fleming and W.Taylor.Union-indecomposable varieties.Colloquium Mathematicum,35:189–199,
1976.
[5]P.Di Gianantonio,F.Honsell,S.Liani,and G.D.Plotkin.Countable non-determinism and uncountable limits.
In Proceedings of CONCUR’94,Springer LNCS836,1994.See also:Uncountable limits and the Lambda Calculus,Nordic Journal of Computing2,1995.
[6]J.-Y.Girard.The system of variable types,?fteen years later.Theoretical Computer Science,45:159–192,
1986.
[7]J.Hagemann and A.Mitschke.On-permutable congruences.Algebra Universalis,3:8–12,1973.
[8]F.Honsell and S.Ronchi Della Rocca.An approximation theorem for topological lambda models and the
topological incompleteness of lambda calculus.Journal of Computer and System Sciences,45(1),1992.
[9]M.Hyland.A syntactic characterization of the equality in some models for the lambda calculus.J.London Math.
Soc.,12:361–370,1976.
[10]B.Jacobs,I.Margaria,and M.Zacchi.Filter models with polymorphic types.Theoretical Computer Science,
95:143–158,1992.
[11]A.I.Mal’cev.K obˇsˇc eˇ?teorii algebraiˇc eskih sistem.Mat.Sb.N.S.35(77),pages3–20,1954.
[12]G.D.Plotkin.A semantics for static type https://www.doczj.com/doc/8f17786696.html,rmation and Computation,109:256–299,1994.
[13]G.D.Plotkin.On a question of https://www.doczj.com/doc/8f17786696.html,rmation and Computation,126(1):74–77,1996.
[14]P.Selinger.Functionality,Polymorphism,and Concurrency:A Mathematical Investigation of Programming
Paradigms.PhD thesis,University of Pennsylvania,1997.
[15]W.Taylor.Structures incompatible with varieties,Abstract74T-A224.Notices of the American Mathematical
Society,21:A-529,1974.
[16]C.P.Wadsworth.The relation between computational and denotational properties for Scott’s-models of the
lambda-calculus.SIAM Journal on Computing,5:488–521,1976.
15
疾病名：高脂血症 英文名：hyperlipoidemia 缩写：HL 别名：hyperlipemia；高脂血；血脂过多 ICD号：E78.5 分类：代谢科 概述：血脂是血浆中的中性脂肪(三酰甘油和胆固醇)和类脂(磷脂、糖脂、固醇、类固醇)的总称，广泛存在于人体中，它们是生命细胞基础代谢的必须物质。血脂中的主要成分是三酰甘油和胆固醇，其中三酰甘油参与人体内能量代谢，而胆固醇主要用于合成细胞浆膜、类固醇激素和胆汁酸。 脂质是体内的一种重要组成成分，广泛存在于各种膜的结构中。脂质为疏水性的分子，不溶或微溶于水，其在维持细胞的完整性方面具有非常重要的作用，并可使血浆中的物质通过直接弥散或经载体进入细胞内。同时，脂质是体内能量贮存的主要形式，也是肾上腺和性腺类固醇激素以及胆酸合成的前体物质。此外，脂质还是血液中许多可溶性复合物运输的载体。 脂质分为：脂肪酸(FA)、三酰甘油(TG)、胆固醇(Ch)和磷脂(PL)。其中三酰甘油和磷脂为复合脂质。血浆中的胆固醇又分游离胆固醇(FC)和胆固醇脂(CE)两种，二者统称为血浆总胆固醇(TC)。 高脂血症(hyperlipoidemia)是指血脂水平过高，可直接引起一些严重危害人体健康的疾病，如动脉粥样硬化、冠心病、胰腺炎等。 流行病学：血脂水平与遗传和饮食习惯密切相关，因此不同种族人群和饮食情况下的血脂水平存在一定的差异。例如：西方男性的平均胆固醇水平为5.4mmol/L，而日本男性相对较低，仅为4.3mmol/L。我国人群的胆固醇水平亦低于欧美人群，平均为3.8～5.14mmol/L。 我国正常人的各种血脂水平(表1)。
体内的血脂水平随着年龄增长逐渐升高。儿童的血脂水平低于成人，其高脂血症的标准为：胆固醇＞5.2mmol/L(200mg/dl)，三酰甘油＞1.6mmol/L(140mg/dl)。此外，血脂亦受性别和生理状态的影响。女性从青春期起直至绝经期，其三酰甘油和胆固醇水平均低于男性，而HDL水平高于同龄男性。 1.高胆固醇血症 高胆固醇血症的原因包括基础值偏高、高胆固醇和高饱和脂肪酸摄入、热量过多、年龄及女性更年期的影响、遗传基因的异常、多基因缺陷与环境因素的相互作用。 (1)基础血浆低密度脂蛋白-胆固醇(LDL-C)水平高：与各种属的动物相比，人类的基础LDL-C水平较高，可能与人体内胆固醇转化为胆汁酸延缓，肝内胆固醇含量升高，抑制LDL受体活性有关。这种较高的基础LDL-C是人类临界高胆固醇血症的主要原因之一。 (2)饮食中胆固醇含量高：胆固醇摄入量从200mg/d增加到400mg/d，血胆固醇可升高0.13mmol/L(5mg/dl)，其机制可能与肝脏胆固醇含量增加，LDL受体合成减少有关。临床研究表明，在健康青年人中，每天饮食中胆固醇摄入量增加100mg，女性血胆固醇水平上升较男性明显。 (3)饮食中饱和脂肪酸含量高：每人每天摄入饱和脂肪酸理想的量应为每天总热卡的7%，若饱和脂肪酸摄入量占每天总热卡的14%，可致血胆固醇增高大约0.52mmol/L (20mg/dl)，其中主要是LDL-C。研究表明，饱和脂肪酸可抑制LDL受体的活性。虽然确切的机制尚不清楚，但可能与下列5方面有关：①抑制胆固醇酯在肝内合成；②促进无活性的非酯化胆固醇转入活性池；③促进调节性氧化类固醇的形成；④降低细胞表面LDL受体活性；⑤降低LDL与LDL受体的亲和性。 (4)体重增加：研究表明，体重增加可使血浆胆固醇升高，肥胖是血浆胆固醇升高的一个重要原因，因为肥胖促进肝脏输出含载脂蛋白B的脂蛋白，继而使LDL生成增
高脂蛋白血症的分型 WHO Ⅰ型：高乳糜微粒血症，血清外观有“奶油”样顶层，下层澄清，血清三酰甘油含量显著增加，胆固醇正常或轻度增加，电泳有深染的乳糜微粒带，超速离心乳糜微粒增加与VLDL带分离不清，TC／TG比率＜0.1仅见于I型有诊断价值。 Ⅱ型：高β脂蛋白血症，Ⅱa型血清外观澄清，胆固醇含量增加，三酰甘油含量正常，TC／TG比率＞1.5，电泳β带深染，甚至看不到前β带，超离心LDL含量增加，VLDL和HDL含量正常，Ⅱb型血清外观澄清或轻混，血清胆固醇和三酰甘油含量均增加，TC／TG比率可变、电泳β和前β带均深染，超离心LDL和VLDL均增加。 Ⅲ型：异常β脂蛋白血症或称“漂浮β或阔β”型高脂蛋白血症。血清外观混浊，常具有一模糊的乳糜微粒“奶油”样顶层，血清三酰甘油和胆固醇均增高，琼脂糖或醋酸纤维素薄脂电泳见一条自β位置扩展到前β位置的“阔β"带，这是因为在VLDL部分存在异常的LDL，聚丙烯酰胺凝胶电泳则不见β带，而仅见阔前β带。血浆在盐密度为1.006超离心后的上清液部分作醋酸纤维素薄膜电泳，显示β迁移脂蛋白有肯定性诊断价值，因为正常血浆在此密度下超离心，其上清部分仅存在前β迁移脂蛋白。 Ⅳ型：高前β脂蛋白血症，血清外观澄清或完全混浊，主要视三酰甘油含量而定，无“奶油”样顶层，血清胆固醇正常或增高，三酰甘油增高，前β带深染，超离心VLDL增高，LDL正常。 Ⅴ型：高前β脂蛋白血症及乳糜微粒血症。血清外观有“奶油”样顶层，下层混浊，血清胆固醇和三酰甘油均增加，电泳前β带深染且拖尾至原点，原点出现深染乳糜微粒带超离心乳糜微粒存在，VLDL增加。 Ⅱb型和Ⅳ型有时不易确定，应用下列公式可资鉴别： LDL－C=TC－(TG/5＋HDL－C) 当LDL－C＞130mg／dl(过高界限)时为Ⅱb型，否则为Ⅳ型。
1976年WHO建议将高脂血症分为六型： (1)Ⅰ型高脂蛋白血症：主要是血浆中乳糜微粒浓度增加所致。将血浆至于4℃冰箱中过夜，见血浆外观顶层呈“奶油样”，下层澄清。测定血脂主要为甘油三酯升高，胆固醇水平正常或轻度增加，此型在临床上较为罕见。 (2)Ⅱ型高脂蛋白血症，又分为Ⅱa型和Ⅱb型。 ①Ⅱa型高脂蛋白血症：血浆中LDL水平单纯性增加。血浆外观澄清或轻微混浊。测定血脂只有单纯性胆固醇水平升高，而甘油三酯水平则正常，此型临床常见。 ②Ⅱb型高脂蛋白血症：血浆中VLDL和LDL水平增加。血浆外观澄清或轻微混浊。测定血脂见胆固醇和甘油三酯均增加。此型临床相当常见。 (3)Ⅲ型高脂蛋白血症：又称为异常β-脂蛋白血症，主要是血浆中乳糜微粒残粒和VLDL残粒水平增加，其血浆外观混浊，常可见一模糊的“奶油样”顶层。血浆中胆固醇和甘油三酯浓度均明显增加，且两者升高的程度（以mg/dL为单位）大致相当。此型在临床上很少见。 (4)Ⅳ型高脂蛋白血症：血浆VLDL增加，血浆外观可以澄清也可以混浊，主要视血浆甘油三酯升高的程度而定，一般无“奶油样”顶层，血浆甘油三酯明显升高，胆固醇水平可正常或偏高。 (5)Ⅴ型高脂蛋白血症：血浆中乳糜微粒和VLDL水平均升高，血浆外观有“奶油样”顶层，下层混浊，血浆甘油三酯和胆固醇均升高，以甘油三酯升高为主。 高脂血症的分类 血脂主要是指血清中的胆固醇和甘油三酯。无论是胆固醇含量增高，还是甘油三酯的含量增高，或是两者皆增高，统称为高脂血症。 1、根据血清总胆固醇、甘油三酯和高密度脂蛋白-胆固醇的测定结果，高脂血症分为以下四种类型： （1）高胆固醇血症：血清总胆固醇含量增高，超过5.72毫摩尔/升，而甘油三酯含量正常，即甘油三酯<1.70毫摩尔/升。 （2）高甘油三酯血症：约占20%血清甘油三酯含量增高，超过1.70毫摩尔/升，而总胆固醇含量正常，即总胆固醇<5.72毫摩尔/升。 （3）混合型高脂血症：血清总胆固醇和甘油三酯含量均增高，即总胆固醇超过5.72毫摩尔/升，甘油三酯超过1．70毫摩尔/升。 （4）低高密度脂蛋白血症：血清高密度脂蛋白-胆固醇（HDL-胆固醇）含量降低，<0.9毫摩尔/升。 2、根据病因，高脂血症的分类有： （1）原发性高脂血症：包括家族性高甘油三酯血症，家族性Ⅲ型高脂蛋白血症，家族性高胆固醇血症；家族性脂蛋白酶缺乏症；多脂蛋白型高
1976年WHO!议将高脂血症分为六型： (1) I型高脂蛋白血症：主要是血浆中乳糜微粒浓度增加所致。将血浆至于4C 冰箱中过夜，见血浆外观顶层呈“奶油样”，下层澄清。测定血脂主要为甘油三酯升高，胆固醇水平正常或轻度增加，此型在临床上较为罕 见。 (2) U型高脂蛋白血症，又分为Ua 型和Ub型。 ①Ua型高脂蛋白血症：血浆中LDL水平单纯性增加。血浆外观澄清或轻微混浊。测定血脂只有单纯性胆固醇水平升高，而甘油三酯水平则正常， 此型临床常见。 ②Ub型高脂蛋白血症：血浆中VLDL和LDL水平增加。血浆外观澄清或轻微混浊。测定血脂见胆固醇和甘油三酯均增加。此型临床相当常见。 (3) 川型高脂蛋白血症：又称为异常B -脂蛋白血症，主要是血浆中乳糜微粒残粒和VLDL残粒水平增加，其血浆外观混浊，常可见一模糊的“奶油样”顶层。血浆中胆固醇和甘油三酯浓度均明显增加，且两者升高的程 度(以mg/dL为单位)大致相当。此型在临床上很少见。 ⑷W型高脂蛋白血症：血浆VLDL增加，血浆外观可以澄清也可以混浊，主要视血浆甘油三酯升高的程度而定，一般无“奶油样”顶层，血浆甘油三酯明显升高，胆固醇水平可正常或偏高。 (5) V型高脂蛋白血症：血浆中乳糜微粒和VLDL水平均升高，血浆外观有“奶油样”顶层，下层混浊，血浆甘油三酯和胆固醇均升高，以甘油三酯升咼为主。 高脂血症的分类 血脂主要是指血清中的胆固醇和甘油三酯。无论是胆固醇含量增高，还是甘油三酯的含量增高，或是两者皆增高，统称为高脂血症。 1、根据血清总胆固醇、甘油三酯和高密度脂蛋白-胆固醇的测定结果，高脂血症分为以下四种类型： (1)高胆固醇血症：血清总胆固醇含量增高，超过 5.72毫摩尔/ 升, 而甘油三酯含量正常，即甘油三酯<1.70毫摩尔/升。 (2)高甘油三酯血症：约占20%血清甘油三酯含量增高，超过1.70毫摩尔/升，而总胆固醇含量正常，即总胆固醇<5.72毫摩尔/升。 (3)混合型高脂血症：血清总胆固醇和甘油三酯含量均增高，即总胆固醇超过5.72毫摩尔/升，甘油三酯超过 1 . 70毫摩尔/升。 (4)低高密度脂蛋白血症：血清高密度脂蛋白-胆固醇(HDL-胆固醇) 含量降低，<0.9毫摩尔/升。 2、根据病因，高脂血症的分类有： (1)原发性高脂血症：包括家族性高甘油三酯血症，家族性川型高脂
高脂血症健康指导 1、定义 血脂代谢发生紊乱；脂肪代谢或转运异常；血浆中一种或几种脂质浓度，包括血浆TC及TG水平过高或血浆HDL水平过低；人体血浆中TC、TG和各种脂蛋白含量高于同龄正常值者均称高脂血症。高TC血症和高TG血症均属于高脂血症，既可表现为单纯高TC血症或单纯高TG血症，也可表现为高TC合并高TG混合型高脂血症。 2、症状 高脂血症的临床表现主要包括两大方面: ?脂质在真皮内沉积所引起的黄色瘤； ?脂质在血管内皮沉积所引起的动脉粥样硬化, 产生冠心病和周围血管病等。 由于高脂血症时黄色瘤的发生率并不十分高, 动脉粥样硬化的发生和发展则需要相当长的时间, 所以多数高脂血症患者并无任何症状和异常体征发现。 而患者的高脂血症则常常是在进行血液生化检验(测定血胆固醇和甘油三酯)时被发现的。 3、病因 低密度脂蛋白受体亦称为Apo B、E受体，是一种细胞表面糖蛋白，以肝细胞含量最多。低密度脂蛋白受体基因位于人类第19号染色体，家族性高胆固醇血症发病的原因是低密度脂蛋白受体基因的自然突变，包括缺失、插入、无义突变和错义突变。已发现数十种低密度脂蛋白受体基因突变，可分为五大类。 ?Ⅰ类突变：其特点是突变基因不产生可测定的低密度脂蛋白受体，细胞膜上 无低密度脂蛋白受体存在，是最常见的突变类型。
?Ⅱ类突变：其特点是突变基因合成的低密度脂蛋白受体在细胞内成熟和运输 障碍，细胞膜上低密度脂蛋白受体明显减少，也较常见。 ?Ⅲ类突变：其特点是突变基因合成的低密度脂蛋白受体可到细胞表面，但不 能与配体结合。 ?Ⅳ类突变：此类突变是成熟的低密度脂蛋白受体到达细胞表面后虽能结合低 密度脂蛋白，但不能出现内移。 ?Ⅴ类突变：其特点是低密度脂蛋白受体的合成、与低密度脂蛋白的结合以及 其后的内移均正常，但受体不能再循环到细胞膜上。 不同种族，低密度脂蛋白受体突变的发生有差异，例如French-Canadians的杂合子家族性高胆固醇血症中，受体基因缺失所致的突变占60%。低密度脂蛋白受体的缺陷最突出的异常是低密度脂蛋白从血浆中分解减慢。在低密度脂蛋白受体正常时，部分中间密度脂蛋白可直接被肝脏低密度脂蛋白受体摄取而分解，而在家族性高胆固醇血症，低密度脂蛋白不能被分解，造成更多的中间密度脂蛋白转化为低密度脂蛋白，使低密度脂蛋白产生增加。 4、风险因素 高脂血症的风险因素包括： ?遗传因素原发性系由于脂质和脂蛋白代谢先天性缺陷引起。 ?某些疾病继发性者主要继发于某种疾病，如糖尿病、肝脏疾病、肾脏疾病、 甲状腺疾病等， ?生活方式以及饮酒、肥胖、饮食与生活方式等环境因素的影响。 长期高脂血症易导致动脉硬化加速，如果长期动脉硬化不但会使硬化的血管变得脆弱，发生破裂，而且还会发生脑梗寒或心梗等。 5、诊断手段 高脂血症相关的检查项目： ?测定血脂谱全套包括空腹TC、TG、LDL-C、HDL-C。 ?判断血浆中有无乳糜微粒存在可采用简易的方法，即把血浆放置4℃冰箱
1.2.1信息系统的概念 信息系统是与信息加工，信息传递，信息存储以及信息利用等有关的系统。任何 一类信息系统都是由信源、信道和信宿（通信终端）三者构成。先前的信息系统 并不涉及计算机等现代技术，但是，现代通信与计算机技术的发展，使信息系统 的处理能力得到很多的提高。现在各种信息系统中已经离不开现代通信与计算机 技术，我们现在所说的信息系统一般均指人、机共存的系统。信息系统一般包括 数据处理系统，管理信息系统、决策支持系统和办公自动化系统。 数据处理系统是由设备、方法、过程，以及人所组成并完成特定的数据处理功能的系统。它包括对数据进行收集、存储、传输或变换等过程，如数据的识 别、复制、比较、分类、压缩、变形及计算等。 管理信息系统是收集、存储和分析信息，并向组织中的管理人员提供有用信息的系统。它的特是面向管理工作，提供管理所需要的各种信息。按照管理信息 系统所面向的管理组织和存取数据的方式，可以分为文件系统和数据库系统。按 其处理作业方式，可以分为批处理和实时处理系统。按其各部分之间的联系方式，可以分集中式和分布式两种类型。 决策支持系统是把数据处理的功能和各种模型等决策工具结合起来,以帮助决策的电子计算机信息处理系统.它能够在复杂的迅速变化的外部环境中,给各级 管理人员或决策者提供有关的信息资料,并协助决策者制定和分析决策。决策支 持系统使用的电子计算机技术是数据库、模型库以及可能进行实时处理的计算机 网络系统。 办公自动化系统是由计算机、办公自动化软件、通信网络、工作站等设备组成使办公过程实现自动化的系统。办公自动化软件具有办公、信息管理以及决策 支持等功能。通信网络：可以是简单的字符终端或图形终端，也可以是数据、文 字、图像、语音相结合的多功能的工作站：可以是简单的字符终端或图形终端，也可以是数据、文字、图像、语音相结合的工作站，一个比较完整的办公自动化 系统含有信息采集、信息加工、信息传输、信息保存 4 个基本环节，其核心任 务是向它的各层次的办公人员提供所需的信息，所以该系统综合体现了人、机、信息资源三者之间的关系。 他通过资源管理提高计算机系统的效率。操作系统是计算机系统的资源管理者，它含有对系统软件、硬件资源实施管理的一组程序。其首要作用就是通过 cpu管理、存储管理、设备管理和文件管理，对各种资源进行合理的分配，增大 资源的共享和利用程度，最大限度地提高计算机系统的工作效率，增强计算机系 统处理工作的能力。 改善人机界限面，想用户提供友好的工作环境。操作系统不仅是计算机硬件和各种软件之间的接口，而且是用户与计算机之间的接口。试想如果不安装操作 系统，用户将要面对01代码和以一些难懂的机器指令，通过按钮或开关来操作 计算机，这样既笨拙又费时间。安装操作系统后我以为,中国历史上最激动人心 的工程不是长城,而是都江堰. 长成当然也是非常伟大,不管孟姜女们如何痛苦流涕，站远了看，这个苦难的民族竟用人力在荒山茫漠间修了一条万里屏障，为我们生存的星球留下了一种 人类意志力的骄傲。长城到八达岭一带已经没有什么味道，而在甘肃，陕西、山 西、内蒙一带，劲历的寒风在水浒传又名、江湖豪客传、是施耐庵根据宋金时期 宋江起义故事改编而成的中国第一部长篇白话小说。这是一部描写农民斗争的伟 大史诗，在中国文学史上首开英雄传奇小说的先河，其思想艺术成就是前所未有
高脂蛋白血症分型 *导读：高脂蛋白血症是指三酰甘油和血浆中胆固醇升高，其临床表现为黄色瘤及动脉粥样硬化。高脂蛋白血症分为原发性和继发性两大类型，不同类型症状及治疗有所不同。今天，我们主要来探讨一下原发性高脂蛋白血症分型。…… 高脂蛋白血症是指三酰甘油和血浆中胆固醇升高，其临床表现为黄色瘤及动脉粥样硬化。高脂蛋白血症分为原发性和继发性两大类型，不同类型症状及治疗有所不同。今天，我们主要来探讨一下原发性高脂蛋白血症分型。 *一、原发性高脂蛋白血症Ⅰ型 本症是常染色体隐性遗传疾病。由于脂打败脂酶严重减低或缺乏，外源性食物中的甘油三脂不能分解代谢，造成大量乳糜微粒在血中积聚而出现临床症状。发病年龄不等，可在婴幼儿或儿童期发病，也有在成年期发病，或在查体时才发现。 临床变现有黄色瘤、视网膜病变、腹痛。治疗要点为：第一，食用低脂肪食物，降低血脂；第二，降低食欲，减少食用过量热量高的食物。 *二、原发性高脂蛋白血症Ⅱ型 本症是常染色体隐性遗传病，是原发性高脂蛋白血症中最常见的一种，约占40%。由于基因缺陷，胆固醇合成显著增加，引起临床症状。患者出生时即有高胆固醇血症。纯合子型症状严重，
发病早，进展快。 临床表现为黄色瘤、青年角膜环、动脉粥样硬化及心肌梗塞。治疗要点为：第一控制饮食，给予低脂、低糖、高担保饮食，胆固醇每日摄取量限于300mg以下；第二药物治疗，治疗原发性高脂蛋白血症Ⅱ型的药物有消胆胺、降脂树脂、胰弹性酶、B-谷固醇、复方磷酸脂酶篇、去脂钙、降脂平、烟酸肌醇脂、益寿宁及脉通；第三血浆除去法，每月1次；第四中药治疗法，可用茯苓、猪苓、泽泻、陈皮、虎杖、茵陈及首乌等。 *三、原发性高脂蛋白血症Ⅲ型 本症是常染色体隐性遗传病。由于极低度密度脂蛋白和乳糜微粒的分解代谢缺陷，使中间密脂蛋白或极低密度脂蛋白剩余量异常。多在20岁后发病。 临床表现为黄色瘤、动脉粥样硬化症。治疗要点为：第一饮食中用多种不保和脂肪酸，不用饱和脂肪酸，降低甘油三脂、控制胆固醇；第二口服降血脂药物，使血脂正常，黄色瘤小时。第三消除肥胖，补充L-甲状腺钠或甲状腺干粉片。 以上就是原发性高脂蛋白血症分型，如果大家还有相关疑问，欢迎相关专栏的医生或者询问各大医院的专业医生。
第1章管理信息系统的定义和概念 [教学目的与要求]:通过学习，使学生了解管理信息系统的定义、性质、概念、开发等内容。 [教学重点]：管理信息系统的定义和性质 [教学难点]：管理信息系统的概念 [教学课时]：2课时 1.1 定义 Management Information Systems 1970 Walter T. Kennevan 以书面或口头的形式,在合适的时间向经理、职员以及外界人员提供过去的、现在的以及预测未来的有关企业内部及其环境的信息, 以帮助他们进行决策。 注意：从应用目的出发 未明确包含人 这里没有任何计算机字眼 1985 Gordon B. Davis 它是一个利用计算机硬件和软件,手工作业,分析、计划、控制和决策模型,以及数据库的用户-机器系统。它能提供信息支持企业或组织的运行、管理和决策功能。 这个定义最大的特点是它指出了计算机的存在。在当时的美国可以说，所有信息系统均有计算机。这也就是说，没有计算机也有信息系统，但只有有了计算机才能算是先进的信息系统。这个定义还指出组成信息系统的各个部件，而且指出了管理信息系统是个用户-机器系统，也就是人-机系统。可是我们日常的理解中最大的错误就是不把人当成信息系统的组成部分。 这个定义还更深入地指出了它能支持企业的三个层次的工作，即基层运行，中层管理，高层决策。 注意：仍有目的 有了计算机及其组成人-机系统 1985 中国企业管理百科全书 一个由人,计算机等组成的能进行信息的收集、传递、储存、加工、维护和使用的系统。管理信息系统能实测企业的各种运行情况;利用过去的数据预测未来; 从全局出发辅助企业进行决策;利用信息控制企业的行为;帮助企业实现其
对信息系统边界定义的探讨 摘要：文章通过较全面地阐述信息系统边界的内涵，分析信息系统边界的特殊性，归纳定义了信息系统边界的概念；通过分析目前信息系统的主要表示方法，选择并推荐了一种能较科学地表示信息系统边界而又便于应用的信息系统边界的表示方法。 关键词：信息系统；边界；定义；系统概况图 一、引言 任何一个系统都有一个边界的问题。边界问题就是确定系统和相邻系统交接部分，哪些元素属于本系统，哪些元素属于相邻系统。对一般的物质性系统，其边界通常比较容易通过物理的方法确定，以物理的形式表达。小区边界可以以围墙或街道划分；企业边界可以用围墙，也可以用业务范围划分等等。但对信息系统的边界，学术界一直没有一种权威的定义和表示方法。其难度主耍在于信息系统是一个融于物质系统的特殊系统，其本身既包含有一定的物质成分，又包含一些非物质成分。同时，所有这些成分几乎都又融于其相邻的系统中， 难以单独分割。 信息系统边界的定义对于分析与设计信息系统都十分重要。有了明确的边界就知道了信息系统分析与设计的范围，可以更好地分析与设计信息系统的内部流程、信息处理方式、信息组织方式；同时，也可以更好地确定与设计信息系统与外部信息系统的信息联系。特别是在企业信息系统多个子系统分析与设计的过程中，子系统的边界的确定对于整个信息系统的信息流程优化等方而具有举足轻重的意义。 本文将应用现有的关于信息系统的知识，按照作者对信息系统边界的理解进行归纳定义；同时，在此定义下探讨信息系统边界的表示方法。 二、信息系统边界的定义 在许多关于信息系统的教科书和论文中，都提及信息系统边界的概念，但均未对之有明确的定义。关于边界的概念，应该有这样一些内涵：边界是用于划分系统与其他系统，特别是相邻系统关系的一种方法；边界应该能说明那些元素是属丁?本系统的，那些元素不是本系统的，是属于系统外部环境的；边界的划分除了能界定本系统的元素外，还应能界定与表示本系统对外的输入与输出，即本系统与环境的关系。 为了更科学的定义信息系统的边界，首先来分析信息系统的特殊性。其特殊性包括：信息系统涉及到的两个最基础概念一信息与系统，国内外专家学者仍有不同观点与看法，这就使得我们对它的认识存在一定的局限性和主观性。目前大家认同的信息系统构成要素中，如计算机、网络、数据库、软件、人员、信息流程、信息处理方法等，特别是有形的要素，许多并不仅仅扮演信息系统元素的角色，同时还扮演了其他系统的要素。如信息系统的工作人员，其同时可能又是生产系统的工作人员；信息系统的计算机，可能同时又用于生产控制，
高脂蛋白血症及其分类 …… 高脂蛋白血症是指血液中的一种或几种脂蛋白的升高。所有脂蛋白都含有脂质，因此只要脂蛋白过量（高脂蛋白血症），就会引 起血脂水平升高（高脂血症）。高脂血症与高脂蛋白血症看上去 是两个不同的概念，但是由于血脂在血液中是以脂蛋白的形式进行运转的，因此高脂血症实际上也可认为是高脂蛋白血症，只是两种不同的提法而已。目前已确定有五种类型的脂蛋白水平异常，即五种高脂蛋白血症。 高脂蛋白血症分为I、II、Ⅲ、IV和V型，五型中的任何一型脂蛋白代谢异常都会导致某种特定脂蛋白升高。通过判断哪一种脂蛋白的升高，就可以诊断是哪一种类型的高脂蛋白血症。最为常见的是I和IV型。 Ⅱ型高脂蛋白血症最常见，也是与动脉粥样硬化最密切相关的一型。。Ⅱ型的主要问题在于低密度脂蛋白（LDL）的增高。LDL以正常速度产生，但由干细胞表面LDL受体数减少，引起LDL的血浆清除率下降，导致其在血液中堆积。因为LDL是胆固醇的主要载体，所以Ⅱ型病人的血浆胆固醇水平升高。Ⅱ型又分成为Ⅱa 和Ⅱb型，它们的区别在于：Ⅱb型LDL和极低密度脂蛋白（VLDL）水平都升高，而Ⅱa型只有LDL的升高。Ⅱa型只有LDL水平升高，因此只引起胆固醇水平的升高，甘油三酯水平正常。Ⅱb型
LDL和VLDL同时升高，由于VLDL含55％～65％甘油三酯，因此Ⅱb型患者甘油三酯随胆固醇水平一起升高。 IV型的发生率低于Ⅱ型，但仍很常见。IV型的最主要特征是VLDL 升高，由于VLDL是肝内合成的甘油三酯和胆固醇的主要载体，因此引起甘油三酯的升高，有时也可引起胆固醇水平的升高。 I型极罕见，在医学文献报道中只有100例左右，I型患者由于脂蛋白脂酶（一种负责把乳磨微粒从血中清除出去的酶）缺陷或缺乏，而导致乳糜微粒水平的升高。乳糜微粒升高伴随着甘油三酯水平升高和胆固醇水平的轻度升高。 Ⅲ型也不常见，它是一种因VLDL向LDL的不完全转化而产生的一种异常脂蛋白疾病。这种异常升高的脂蛋白称为异常的LDL，它的成分与一般的LDL不同。异常的LDL比正常型LDL含高得多的甘油三酯。 V型患者，乳糜微粒和VLDL都升高，由于这种脂蛋白运载体内绝大多数的甘油三酯，所以在V型高脂蛋白血症中，血浆甘油三酯水平显著升高，胆固醇只有轻微升高。
第1章信息系统的基本概念 【重点知识讲解】 一、信息的定义 （一）信息的定义： 信息既是可以通信的数据和知识，又是管理和决策的重要依据。（二）信息是事物运动状态的陈述 运动状态本身（例如观察到的事实、现象）是直接信息或一次信息。关于事物运动状态的陈述则是间接信息或二次信息。 （三）信息的特性 1．信息的相对性：一方面，对于同一事物，不同的观察者获得的信息量并不相同；另一方面，不同的用户对象信息的需求也不相同。 2．信息的转移性：信息可以在空间上从一点转移到另一点。在时间上的转移称为存储；在空间上的转移称为通信。 3．信息的变换性：信息是可变换的，它可以由不同的载体和不同的方法来载荷。 4．信息的有序性：信息可以增加系统的有序性，信息本身也可以根据一定的规则编码。 5．信息的动态性：信息是事物运动的状态和状态的改变方式，事物本身是在不断发展变化的，信息也会不断地随着变化。 7．信息的时效性：信息是有生命的。 8．信息的共享性：信息可以被无限制地进行复制、传播或分配给众多的用户，为大家所共享。 9．信息的媒介性：争取及时的信息可以节约物质、能量或时间，信息被人们有效地利用。 四、信息的概念结构： 信源、信宿、信道（名词） 五、系统： 六、系统的特性： 1）目的性：系统的最重要的特性。 2）系统的整体性： 3）层次性： 4）相关性：
5）开放性：（梅特卡夫法则） 6）系统的稳定性： 7）相似性 七、决策支持系统、客户管理系统、计算机辅助设计系统、（英文缩写） 八、信息系统（名词解释） 九、信息系统的概念结构：信息源、信息处理器、信息用户和信息管理者。 十、信息系统的层次结构：战略决策、战术管理和业务处理。 十一|、物理： 【往年试题】 2008年10月 一、选择题 1.从总体说，管理信息系统是由4个部分组成的，这四个部分是( ) A.信息源，信息处理器，信息用户和信息管理者 B.数据库，信息处理器，信息存储器和信息管理者 C.数据库，信息处理器，信息用户和信息存储器 D.信息源，计算机，数据库和信息管理者 2.MIS从管理层次上进行纵向划分时，可分为高层战略层，中层______和基层执行层。 ( ) A.指挥层 B.战术层 C.计划层 D.操作层 二、填空题 6.信息系统从概念上来看是由信息源、__________、__________和信息管理者四大部分组成。 三、名词解释 1.系统 2009年1月
1976年W H O建议将高脂血症分为六型： (1)：主要是血浆中乳糜微粒浓度增加所致。将血浆至于4℃冰箱中过夜，见血浆外观顶层呈“奶油样”，下层澄清。测定血脂主要为甘油三酯升高，胆固醇水平正常或轻度增加，此型在临床上较为罕见。 (2)，又分为Ⅱa型和Ⅱb型。 ①Ⅱa型高脂蛋白血症：血浆中LDL水平单纯性增加。血浆外观澄清或轻微混浊。测定血脂只有单纯性胆固醇水平升高，而甘油三酯水平则正常，此型临床常见。 ②Ⅱb型高脂蛋白血症：血浆中VLDL和LDL水平增加。血浆外观澄清或轻微混浊。测定血脂见胆固醇和甘油三酯均增加。此型临床相当常见。 (3)Ⅲ型高脂蛋白血症：又称为异常β-脂蛋白血症，主要是血浆中乳糜微粒残粒和VLDL残粒水平增加，其血浆外观混浊，常可见一模糊的“奶油样”顶层。血浆中胆固醇和甘油三酯浓度均明显增加，且两者升高的程度（以mg/dL为单位）大致相当。此型在临床上很少见。 (4)：血浆VLDL增加，血浆外观可以澄清也可以混浊，主要视血浆甘油三酯升高的程度而定，一般无“奶油样”顶层，血浆甘油三酯明显升高，胆固醇水平可正常或偏高。 (5)：血浆中乳糜微粒和VLDL水平均升高，血浆外观有“奶油样”顶层，下层混浊，血浆甘油三酯和胆固醇均升高，以甘油三酯升高为主。 高脂血症的分类 血脂主要是指血清中的胆固醇和甘油三酯。无论是胆固醇含量增高，还是甘油三酯的含量增高，或是两者皆增高，统称为高脂血症。 1、根据、甘油三酯和高密度脂蛋白-胆固醇的测定结果，高脂血症分为以下四种类型： （1）：血清总胆固醇含量增高，超过毫摩尔/升，而甘油三酯含量正常，即甘油三酯<毫摩尔/升。 （2）高甘油三酯：约占20%含量增高，超过毫摩尔/升，而总胆固醇含量正常，即总胆固醇<毫摩尔/升。 （3）混合型高脂血症：血清总胆固醇和甘油三酯含量均增高，即总胆固醇超过毫摩尔/升，甘油三酯超过1．70毫摩尔/升。 （4）：血清高密度脂蛋白-胆固醇（HDL-胆固醇）含量降低，<毫摩尔/升。 2、根据病因，高脂血症的分类有： （1）原发性高脂血症：包括家族性高甘油三酯血症，家族性Ⅲ型，家族性高胆固醇血症；家族性脂缺乏症；多脂蛋白型高脂血症；原因未明的原发性高脂蛋
第一章管理信息系统的基本概念 1、何为数据？何为信息？信息和数据有何区别？ 所谓数据是由原始事实组成的。要表示数据通常有三个方面事情要做：数据名称、数据类型、数据长度。 当原始事实按照具有一定意义的方式组织和安排在一起时，它就成了信息。 信息是按一定的规则组织在一起的数据集合，是对数据进行处理而产生的。这种组织规则和方式具有超出数据本身以外的额外价值。 2、什么叫系统？五个基本要素？特性？有哪几类系统？ 系统是由相互联系、相互作用的多个元素（部件）有机集合而成的，能够执行特定功能的综合体。 五个基本要素：输入，处理，输出，反馈，控制。 特性：目的性，整体性，层次性，相关性，开放性，稳定性，相似性。 按抽象程度分类：概念系统，逻辑系统，实在系统 按系统功能分类：社会，经济，军事，企业管理 按与外界关系分类：封闭式与开放式 按系统内部结构分类：开环系统和闭环系统。 3、什么是系统方法？什么是系统观点？说出系统方法解决问题的主要步骤？ 系统方法，就是按照事物本身的系统性把对象放在系统的形式中加以考察的一种方法，是一种立足整体、统筹兼顾、使整体与部分辩证地统一起来的科学方法。 所谓系统观点，就是不着眼于个别要素的优良与否，而是把一个系统内部的各个环节、各个部分，把一个系统的内部和外部环境都看成是相互联系、相互影响、相互制约着的综合体，从整体上追求系统的功能最优。 系统方法解决问题的主演步骤： ①定义问题：列出一个或一组希望达到的目标 ②列出资源和约束：供选择的技术或手段以及每个系统所需的“成本”或资源 ③给出方案：一个或一组数学模型 ④评估被选方案 ⑤选择最佳方案并实施 ⑥总结解决方案的有效性 4、什么是信息系统？ 信息系统是一系列相互关联的可以输入、处理、输出数据和信息，并提供反馈、控制机制以实现某个目标的元素或组成部分的集合。 5、什么叫管理？如何理解管理信息系统的概念？其主要特征是什么？ 管理是人有目的、有意识的实践活动，是管理者在一定的条件下，为了实现预定目标，对各种资源和实践环节进行规划安排、优化控制的总称。 管理信息系统是运用系统管理的理论和方法，以计算机技术、网络通信技术和信息处理技术为工具和手段，具有对信息进行加工处理、存储和传递等功能，同时具有预测、控制、组织和决策等功能的人——机系统。 管理信息系统的特征： ①它是一个人——机系统，在管理信息系统中，需要充分发挥人和计算机系统的长处，一些工作由计算机系统处理，一些工作要由人进行处理，使人和计算机系统和谐工作。
概述高脂血症是指血浆中胆固醇和（或）三酰甘油水平升高。由于血浆中的胆固醇和三酰甘油是疏水分子，不能直接在血液中被转运，必须与血液中的蛋白质及其他类脂，如磷脂一起组成亲水性的脂蛋白。高脂血症表现为血浆中某一类或某几类脂蛋白升高，严格说来应称为高脂蛋白血症。【病因发病机制】高脂血症的病因包括原发性和继发性两大类。原发性是由于脂质和脂蛋白代谢先天性缺陷（或遗传性缺陷）及某些环境因素（包括饮食、营养等）通过未知的机制而引起的；继发性者主要继发于某些疾病，如糖尿病、肝脏疾病、肾脏疾病、甲状腺疾病等，也受环境因素的影响。【分型】临床上根据血中升高的脂蛋白（或脂质）的不同将高脂蛋白血症分为五型。类型血浆中升高的主要成份脂蛋白类型主要脂类I型乳糜微粒三酰甘油Ⅱa型LDL胆固醇Ⅱb型LDL和VLDL胆固醇和三酰甘油Ⅲ型乳糜微粒残余物和IDL三酰甘油和胆固醇Ⅳ型VLDL三酰甘油Ⅴ型VLDL和乳糜微粒三酰甘油和胆固醇临床表现 1．I型高脂蛋白血症又称家族性高乳糜微粒血症、家族性高三酰甘油血症。以空腹高乳糜微粒血症为特征，与V型表现相似，但血浆VLDL正常。其生化缺陷是LPL（脂蛋白酯酶）缺乏或激活LPL的Ap.cⅡ先天性缺陷。呈常染色体隐性遗传，纯合子患者临床表现典型，杂合子患者血脂正常，仅表现为脂肪组织LPL降低。本型在人群中罕见，原发性者见于儿童，继发性者多在20岁后发病。最常见的症状为腹痛，表现轻重不一，重者可酷似急腹症，腹痛呈弥漫性或局限于上腹，常放射至背部，腹痛的机制未明。可发生急性胰腺炎。体检可发现肝、脾肿大。特征性改变是视网膜脂血症和发疹性黄色瘤病；黄色瘤多在躯干、上臂伸侧、臀部和大腿，在红斑基础上有直径约l～5mm的黄色小丘疹。本型较少合并动脉粥样硬化。2．V型高脂蛋白血症又称混合型高三酰甘油血症、混合型高脂血症。其缺陷未明。症状和体征与I型相同，可发生致命的急性胰腺炎。常伴有肥胖、葡萄糖耐量异常（或糖尿病）、高胰岛素血症、高尿酸血症、冠状动脉粥样硬化性心脏病。3．Ⅱ型高脂蛋白血症又称家族性高胆固醇血症、家族性高β脂蛋白血症、家族性高胆固醇黄色瘤病。本病呈常染色体显性遗传。发病机制是由于机体细胞缺乏LDL受体以致血浆LDL.移除障碍，故本症以LDL（β一脂蛋白）升高为特征。由于LDL是胆固醇和胆固醇酯进入血浆的主要运载工具，故本症患者血浆胆固醇呈中度至重度升高。可分为两个亚型，Ⅱa型血浆三酰甘油正常，Ⅱb型血浆三酰甘油升高。临床上主要表现为早年发生动脉粥样硬化症、冠状动脉粥样硬化性心脏病、结节性黄色瘤和腱黄瘤，后两者为皮肤和筋腱LDL浸润所致。黄斑瘤呈黄色，扁平状，多位于上、下眼睑；腱黄瘤多在肢体伸侧肌腱，如鹰嘴、髌、足跟部。严重高胆固醇血症者，黄色瘤呈块状，多见于手掌、肘、臀部。黄色瘤的发生与高胆固醇血症的病程和病情有关。纯合子患者在年幼时甚至出生时已有黄色瘤，杂合子则在20～40岁出现。纯合子可在20岁前发生冠心病，杂合子在40岁前发生。其他动脉粥样硬化性疾病（如脑卒中、周围血管病）也常见。甲状腺功能减退症和肾病虽然可以引起严重高胆固醇血症，但其程度低于家族性高胆固醇血症。4．Ⅲ型高脂蛋白血症又称宽β型或漂浮β型高脂蛋白血症、家族性异常B脂蛋白血症。本型相对少见，表现为vLDL、IDL异常。本型患者冠心病和周围血管病患病率高，最具特征性的临床表现是手掌块状黄色瘤。5．Ⅳ型高脂蛋白血症又称高前β脂蛋白血症。主要表现为vLDL升高而无乳糜微粒血症，LDL也不增加，可为原发性或继发性。许多患者无症状而于常规检查时发现。45岁以上易患冠心病，但周围血管病、黄色瘤、黄斑瘤不常见。继发性常见于肥胖、慢性肾功能衰竭、肾病综合征、糖尿病、甲状腺功能减退症、过量饮酒者。检查检验 1．血脂血脂浓度受饮食、性别、年龄等多种因素的影响，很难对血脂规定一个正常水平。通常认为，血浆总胆固醇< 5.2mmool／L（200ma／dl）是理想水平；5．2～6．2mmol ／L（200～239mg／dl）为临界；≥6．2mmol／I（240ma／dl）可肯定过高。血浆三酰甘油<1．7mmol／L（150mg／dl）最为理想；1．7～2．3mmol／L（150～200mg／dl）为临界；≥2．3mmol／L（200mg／d1）肯定过高。2．脂蛋白禁食12～14小时抽血，血浆放置4C 过夜，然后观察其分层现象及混浊度，可初步估计血浆中各种脂蛋白变化情况。如标本表面
第一篇概念篇 第一章管理信息系统的定义、概念和结构 1.1管理信息系统的定义 ?以书面或口头的形式,在合适的时间向经理、职员以及外界人员提供过去的、现在的、预测未来的有关企业内部及环境的信息，以帮助他们进行决策。 ?它是一个利用计算机硬件和软件，手工作业，分析、计划、控制和决策模型，以及数据库的用户——机器系统。它能提供信息，支持企业或组织的运行、管理和决策功能； ?一个由人、计算机等组成的能进行信息的收集、传递、储存、加工、维护和使用的系统； ?一个由人、机械（计算机等）组成的系统，它从全局出发辅助企业进行决策，它利用过去的数据预测未来，它实测企业的各种功能情况，它利用信息控制企业行为，以期达到企业的长远目标。 管理信息系统的环境、目标、功能、内涵等均有很大的变化： 环境：世界已变成市场全球化，需求多元化，竞争激烈化，战略短现化。一切事物变化加快，企业不得不更加重视变化管理和战略管理。 目标：企业要在激烈的竞争中立于不败之地，首先产品或服务要适应市场的需要，其次企业要有效益和效率。企业的管理信息系统应有利于企业战略竞争优势，有利于企业提高效益和效率，有利于改善交货时间（T）、产品或服务质量（Q）和产品或服务成本（C）。 支持层次：高、中、低 功能：进行信息的收集、传输、加工、存储、更新和维护。 组成：人工手续、计算机硬件、软件、通信网络、其他办公设备（复印、传真、电话等）以及人员。 管理信息系统简称M I S(M a n a g e m e n t I n f o r m a t i o n S y s t e m)，它是一个以人为主导，利用计算机硬件、软件、网络通信设备以及其他办公设备，进行信息的收集、传输、加工、储存、更新和维护，以企业战略竞优、提高效益和效率为目的，支持企业高层决策、中层控制、基层运作的集成化的人机系统。 1.2 管理信息系统的概念 1.2.1概念
国家标准《政务信息系统定义和范围》（征求意见稿）编制 说明 一、工作简况 1、任务来源 2019年4月，根据国家标准化管理委员会关于下达第一批推荐性国家标准计划的通知（国标委发〔2019〕11号），《政务信息系统定义和范围》正式立项，计划号为20190834-T-469，制定周期12个月，全国信息技术标准化技术委员会归口，中国电子技术标准化研究院为主编单位。 2、主要工作过程 2018年4月16日，主编单位中国电子技术标准化研究院面向全国信标委大数据标准话化工作组成员征集参编单位，定向邀请研究机构、高校等单位参与，共有16家企事业单位报名参与，范围覆盖产、学、研、用。 2018年5月28日，在北京召开第一次起草会。经过讨论，将标准结构初步定为：1、范围，2、规范性引用文件，3、术语与定义，4、政务信息系统参考模型，5、政务信息系统的范围，附录（规范性附录）为政务信息系统的清理和整合，并明确标准的适用范围。 2018年6月3日，参加信标委组织的开题答辩，并按照专家意见进行修改。 2018年7月，工作组对标准的内容进行进一步梳理，去掉参考模型内容。 2018年8月，工作组对术语和定义进行了讨论，并确定标准结构为：1、范围，2、规范性引用文件，3、术语与定义，4、政务信息系统定义，5、政务信息系统的范围，附录（规范性附录）为政务信息系统的清理和整合。 2018年9月5日，在北京召开第二次起草会，逐字逐句确定标准内容，形成标准征求意见稿。 3、标准编制的主要成员单位及其所做的工作 中国电子技术标准化研究院：作为标准的主编单位，负责组织起草会，确定标准框架及内容，主笔标准的编制； ——国家信息中心：负责政务信息系统的范围结构调整及内容研究； ——启迪区块链集团：负责政务信息系统定义内容研究；
信息系统服务是一个范围相当广泛的概念，所有以满足企业和机构的业务发展所带来的信息化需求为目的，基于信息技术和信息化理念而提供的专业信息技术咨询服务、系统集成服务、技术支持服务等工作，都属于信息系统服务的范畴。其中信息技术咨询服务是信息系统服务的前端环节，为企业提供信息化建设规划和解决方案。而根据信息化建设方案选择合适的软硬件产品搭建信息化平台，根据企业的业务流程和管理要求进行软件和应用开发，以及系统建成后的长期维护和升级换代等，属于信息系绕服务的中间及下游环节，是信息系统服务在不同时期、不同阶段的具体表现，覆盖了各行各业信息化建设的全过程。 在我国的信息化建设过程中，信息系统服务存在诸多问题，普遍存在的主要问题如下。 （1）系统质量不能满足应用的基本需求。 （2）工程进度拖后延期。 （3）项目资金使用不合理或严重超出预算。 （4）项目文档不全甚至严重缺失。 （5）在项目实施过程中系统业务需求一变再变。 （6）在项目实施过程中经常出现扯皮、推诿现象。 （7）系统存在着安全漏洞和隐患。 （8）重硬件轻软件，重开发轻维护，重建设轻使用。
这些问题严重阻碍着信息化建设进程，甚至产生了令人痛心的豆腐渣工程。有些项目，虽然资金投入了，系统却没有建起来：或者，虽然系统建立了，却是个运转不起来的死系统，等等。于是导致投资见不到效果，见不到效益，使国家和用户单位蒙受极大经济损失。 究其原因，自然要具体问题具体分析，而且不同项目之间也往往存在着差异，但概括起来，主要有以下4点。 （1）不具备能力的单位搅乱系统集成市场。 （2）-些建设单位在选择项目承建单位和进行业务需求分析方面有误。 （3）信息系统集成企业自身建设有待加强。 （4）缺乏相应的机制和制度。 我国信息产业与信息化建设的主管部门和领导机构，在积极推进信息化建设的过程中对所产生的问题予以密切关注并且逐步采取了有效措施，各省、自治区、直辖市、计划单列市等地方政府的信息产业及信息化主管部门也积极参与并且发挥创造性，进行了有益的探索。 为了保证信息系统工程项目投资、质量、进度及效果各方面处于良好的可控状态，在针对出现的问题不断采取相应措施的探索过程中，逐步形成了我们的信息系统服务管理体系。当前我国信息系统服务管理的主要内容如下。 （l）计算机信息系统集成单位资质管理。 （2）倍息系统项目经理资格管理。 （3）信息系统工程监理单位资质管理。