Partial Type Assignment in Left Linear Applicative Term Rewriting Systems
Partial Type Assignment
in
Left Linear Applicative Term Rewriting Systems
Theory,Applications and Implementation.
Steffen van Bakel Sjaak Smetsers Simon Brock )Department of Informatics,Faculty of Mathematics and Informatics,University of Nijmegen,To-
ernooiveld1,6525ED Nijmegen,The Netherlands.
)School of Information Systems,University of East Anglia,Norwich NR47TJ,United Kingdom.
Abstract
This paper introduces a notion of partial type assignment on left linear applicative term rewriting systems that is based on the extension de?ned by Mycroft of Curry’s type assignment system.The left linear applicative TRS we consider are extensions to those suggested by most functional programming languages in that they do not discriminate against the varieties of function symbols that can be used in patterns.As such there is no distinction between function symbols(such as append and plus)and constructor symbols(such as cons and succ).Terms and rewrite rules will be written as trees,and type assignment will consist of assigning types to function symbols,nodes and edges between nodes.
The only constraints on this system are imposed by the relation between the type assigned to a node and those assigned to its incoming and out-going edges.We will show that every typeable term has a principal type,and formulate a needed and suf?cient condition typeable rewrite rules should satisfy in order to gain preservance of types under rewriting.As an example we will show that the optimisation function performed after bracket abstraction is typeable.Finally we will present a type check algorithm that checks if rewrite rules are correctly typed,and?nds the principal pair for typeable terms. Introduction
In the recent years several paradigms have been investigated for the implementation of functional pro-gramming languages.Not only the lambda calculus[Barendregt’84],but also term rewriting sys-tems[Klop’92]and graph rewriting systems[Barendregt et al.’87]are topics of https://www.wendangku.net/doc/378408203.html,mbda calculus(or rather combinator systems)forms the underlying model for the functional programming language Miranda[Turner’85],term rewriting systems are used in the underlying model for the lan-guage OBJ[Futatsugi et al.’85],and graph rewriting systems is the model for the language Clean[Brus et al.’87,N¨o cker et al.’91].
There exists a well understood and well de?ned notion of type assignment on lambda terms,known as the Curry type assignment system[Curry&Feys’58].This type assignment system is the basis for many type checkers and inferers used in functional programming languages.For example the type assignment system for the language ML[Milner’78],as de?ned by https://www.wendangku.net/doc/378408203.html,ner forms in fact an extension of Curry’s system.The type inference algorithm for the functional programming language Miranda works in roughly the same way as the one for ML.A real difference between these languages
lies in the fact that Miranda also contains a type check algorithm,which is based on the type assignment system de?ned by A.Mycroft,an extension of Milner’s type assignment system[Mycroft’84,Kfoury et al.’88].
To provide a formal type system for all languages that use pattern matching this paper presents a formal notion of type assignment on left linear applicative term rewriting systems.As shown in this paper type assignment in term rewriting systems in general does not satisfy the subject reduction property:i.e.types are not preserved under rewriting.The main result of this paper,the formulation of a needed and suf?cient condition on rewrite rules to obtain subject reduction,could be used to prove that all rewrite rules that can be de?ned in a language like Miranda are safe in that respect.Also if at?rst sight one could think that the generalization of type assignments from functional programming languages to term rewriting systems would be straightforward,this is not true,as is shown from the conditions given to guarantee preservance of types under rewriting.
It is our aim to extend the notion presented in this paper to a notion of type assignment for term graph rewriting systems,and,possibly,general graph rewriting systems.
The type assignment system we present in this paper is a partial system in the sense of[Pfenning’88], because we not only de?ne how terms and rewrite rules can be typed,but also provide a type for each function symbol.There are several reasons to do so.
For symbols for which there is a rewrite rule(called de?ned symbols),and for symbols for which such a rule does not exist(called constants),there must be some way of determining what type can be used for an occurrence.Instead of for de?ned symbols investigating their rule every time the symbol is encountered,we can store the type of the symbol in a mapping from symbols to types,and use this mapping instead.Of course it makes no difference to assume the existence from the start of such a mapping from symbols to types,and to de?ne type assignment using that mapping.This mapping is also convenient to make sure that types assigned to different occurrences of constants do not con?ict. In fact,the approach we take here is very much the same as the one taken by Hindley in[Hindley’69], where he de?nes the principal type scheme of an object in Combinatory Logic.Even his notion of type assignment could be regarded as a partial one.Moreover,since combinator systems can easily be translated into left linear applicative term rewriting systems,the results of this paper,when restricting the allowed rewrite rules to those that correspond to combinators,are the same as in[Hindley’69].
In section1we de?ne the left linear applicative term rewriting systems,as the subclass of term rewriting systems that contain a prede?ned symbol,and in which all rewrite rules are left linear.The de?nition of applicative term rewriting systems is not the one normally used,but more general:in the systems we consider,is not the only function symbol.
The notion of type assignment on left linear applicative term rewriting systems as de?ned in sub-section3.2is in fact de?ned on the tree representation of terms and rewrite rules,de?ned in section 2,by assigning in a consistent way types(as de?ned in subsection3.1)to nodes and edges.The only constraints on this system are imposed by the relation between the type assigned to a node and those assigned to its incoming and out-going edges.It is based on the Mycroft type assignment system as used in Miranda.
In subsection3.3we will show that for every basis,term,type and substitution S:if: (i.e.is typeable by starting from the set of typed term variables),then also
S():S().In that subsection we will also show that for every typeable term,there is a principal pair,for,i.e.for every pair,such that:there is a substitution S such that S(,)=,.
Another result presented in that subsection is that if,is the principal pair for,and’is obtained from by replacing(in a consistent way)term variables by terms,and’is typeable by,
then there is a substitution S such that:S()=,and for every:occurring in,the replacement of is typeable by S().
In subsection4.1we show that if type assignment is done in the most obvious,straightforward way, there are rewrite rules that are typeable,that match a term typeable with,but for which the result of the application of the rewrite rule on is not typeable with.In subsection4.2we formulate a condition that typeable rewrite rules should satisfy in order to guarantee preservance of types under rewriting.In that subsection we prove this condition to be needed and suf?cient.
In section5we show that the usually de?ned optimisation algorithm after bracket abstraction(a translation of lambda terms to combinator expressions)is typeable in our system.In the appendix we present a type check algorithm,that checks if rewrite rules are correctly typed,and?nds the principal pair for typeable terms.
1Left linear applicative term rewriting systems
In this paper we study left linear applicative term rewriting systems(LLATRS),which are a subclass of term rewriting systems,as de?ned in[Klop’92].LLATRS’s are de?ned as the class of term rewriting systems that(can)contain a special binary operator,and in which all rewrite rules are left linear.To distinguish them from the term rewriting systems that have only the function symbol,we call the latter the pure applicative term rewriting systems.
The motivation for the use of applicative term rewriting systems instead of the general term rewriting systems can be illustrated by the following example:If we would want to translate Combinatory Logic (CL)
=
=
=
into a term rewriting system,then it could look like(making the implicit application explicit):
However,we prefer to see the symbols,and as functions,with3,2and1operands respectively. If we try to capture that view in our translation,we would need to de?ne also the Curried versions of those symbol:
We consider the applicative rewriting systems,because they are far more general than the subclass of systems in which there exists only the function symbol.Since the pure left linear applicative
term rewriting systems are a subclass of the left linear applicative term rewriting systems,all results obtained in this paper are also valid for that subclass.
We take the view that in a rewrite rule a certain symbol is de?ned,and it is clear that the rules added to obtain the Curried versions of symbols in the translation of CL into a rewriting system are not intended as de?nitions for,which is more or less a‘prede?ned function’,but as de?nitions for the Curried versions.
However,in general term rewriting systems are not sensitive for the names used for functions sym-bols.So the rewriting system given above is in fact the same as the one obtained by replacing all’s by,and then all rewrite rules starting with could be seen as rules that de?ne.In order to avoid this problem,we regard those rewriting systems that have a‘prede?ned’binary function,called, which then cannot be renamed.The symbol is neglected when we are looking for the symbol that is de?ned in a rewrite rule.
In the lambda calculus there is a clear difference between free and bound variables of a term.In term rewriting systems a term variable that occurs in the left hand side of a rewrite rule can be seen as the binding occurrence of,binding the occurrences of in the right hand side.However,in general can occur more than once in the left hand side,making the notion of the binding occurrence obscure. In this paper we consider left linear rewriting systems,that contain only rewrite rules for which the left hand side is linear(term variables occur only once),because for those rules the binding occurrence of a term variable is unique.
The following de?nitions are based on de?nitions given in[Klop’92].De?nition1.1de?nes LLA-TRS’s,in the same way as the de?nition given by Klop for term rewriting systems,extended with part (i.c)to express the existence of the prede?ned symbol.De?nition1.2de?nes a notion of rewriting on LLATRS’s,in the same way as the de?nition of rewriting given by Klop for term rewriting systems, extended with part(ii.a.2)to express the left linearity of rewrite rules,part(ii.a.4)to express that the possible use of the symbol in the left hand side is restricted,and part(iii)to de?ne the notion of de?ned symbol of a rewrite rule.In fact,parts(ii.a.4)and(iii)are related.
We introduce in some parts a different notation,because some of the symbols or de?nitions normally used are also used in papers on type assignment,but with a different meaning.For example we use the word‘replacement’for the operation that replaces term variables by terms,instead of the word ‘substitution’,which will be used for operations that replace type variables by types.
Substitution and replacement are also operations de?ned in[Curry&Feys’58].Both operations are there de?ned as operations on terms,where substitution is de?ned as the operation that replaces term variables by terms,and replacement is de?ned as the operation that replaces subterms by terms.Note that our de?nition therefore differs from the one given in[Curry&Feys’58].
To denote a replacement,we use capital characters like‘R’,instead of greek symbols like‘’,which are used to denote types.We use the symbol‘’for the rewriting symbol,instead of‘’which is used as a type constructor.We use the notion‘constant symbol’for a symbol that cannot be rewritten, instead of for a function symbol with arity0.
De?nition1.1A Left Linear Applicative Term Rewriting System(LLATRS)is a pair(,R)of an alphabet or signature and a set of rewrite rules R.
i)The alphabet consists of:
a)A countable in?nite set of variables,,,...(or,,,’,’,...).
b)A non empty set of function symbols or operator symbols,,...,each equipped with
an‘arity’(a natural number),i.e.the number of‘arguments’it is supposed to have.We have 0-ary,unary,binary,ternary etc function symbols.
c)A special binary operator,called application().
ii)The set of terms(or expressions)‘over’is T and is de?ned inductively:
a),,,...T.
b)If Ap is an-ary symbol,and,...,T(),then
T.
The(=1,...,)are the arguments of the last term.
iii)Terms in which no variable occurs twice or more,are called linear.
De?nition1.2Let(,R)be a LLATRS.
i)A replacement R is a map from T to T satisfying
R()=(R(),...,R())
for every-ary function symbol(here).So,R is determined by its restriction to the set of variables.We also write T instead of R().
ii)a)A rewrite rule R is a pair(,)of terms T.Often a rewrite rule will get a name,e.g.r,and we write r:.Four conditions will be imposed:
1)is not a variable.
2)is linear.
3)The variables occurring in are contained in.
4)For every in,the left hand argument is not a variable.
b)A rewrite rule r:determines a set of rewrites Lhs Rhs for all replacements
R.The left hand side Lhs is called a redex;it may be replaced by its‘contractum’Rhs inside
a context C[];this gives rise to rewrite steps:
C[Lhs]C[Rhs].
c)We call the one-step rewrite relation generated by r.Concatenating rewrite steps we have
(possibly in?nite)rewrite sequences or rewrites for short.If
we also write,and is a rewrite of.
iii)a)In a rewrite rule,the leftmost,outermost symbol in the left hand side that is not an,is called the de?ned symbol of that rule.
b)If the symbol is the de?ned symbol of r,then r de?nes.
c)is a de?ned symbol,if there is a rewrite rule that de?nes.
d)is called a constant symbol if is not a de?ned symbol.
Part(ii.a.4)of de?nition1.2is added in order to avoid rewrite rules with left hand sides like, because such a rule would not have a de?ned symbol.
Proposition1.3Let be the de?ned symbol of the rewrite rule r:.Then there are 0,and,...,such that:
=.
and,...,are called the patterns of r.
Proof:Easy.
..
.
The added rules with,...,,,etc.give in fact the‘Curried’-versions of.
We could have de?ned a closure operation on LLATRS’s,by adding rules and extending the alphabet ,but it is easier to assume that every LLATRS is Curry-closed.When presenting a rewrite system however,we will only show the rules that are essential:we do not show the rules that de?ne the Curried-versions.
2Tree representation of terms and rewrite rules
De?nition2.1i)The tree representation of terms and rewrite rules is obtained in a straightforward way,by representing a term by:
3Type assignment in LLATRS’s
In this section we present a notion of partial type assignment on LLATRS’s,based on the Mycroft type assignment system[Mycroft’84,Kfoury et al.’88].Assigning types to a LLATRS will consist of labelling the nodes and edges in the tree representation of terms and rewrite rules with type information. Types are assigned to nodes to capture the notion of‘type of a function’,‘type of a constant’or‘type of a variable’,and are assigned to edges to capture the notion of‘type of a subterm’(or tree).The edge pointing to the the root of a term is called the root edge.
The difference between Milner’s and Mycroft’s type assignment system lies in the way they handle recursion.Would we have used Milner’s system,then we would have demanded that all occurrences of recursively de?ned objects are,within their de?nition,typed with the same type.Mycroft’s approach is a more general https://www.wendangku.net/doc/378408203.html,ing his system the only requirement for recursive de?nitions would be to demand that the separate occurrences of the object within the de?nition are typed with types that are substitution instances of the type of the object.
There is one major difference between the notion of type assignment we introduce in this paper and Curry’s type assignment system.In that system a basis is usually de?ned as a mapping from term variables to types,or,equivalently,as a set of statements with distinct term variables as subjects.The bases allowed in the system we present however can contain several different statements for the same term variable.This in fact corresponds to the de?nition of ML-type assignment as given in[Damas’85], and is used there for dealing with the let-construct.It could also be compared with using intersection types[Barendregt et al.’83]on free variables of terms.Unlike in lambda calculus,in term rewriting systems this causes no dif?culties,since there is no notion of‘abstraction’in this world.Moreover, condition(i.b)of de?nition3.2.3deals with this apparent anomaly.So in the system we present,it is possible to assign a type to the term.
3.1Types
The type system we de?ne in this subsection is based on the Curry type system,extended with type constants.
De?nition3.1.1i),the set of Curry types is inductively de?ned by:
a)All type variables,,....
b)All type constants,,....
c)If,,then.
ii)A statement is an expression of the form:,where T and.is the subject and the predicate of:.
iii)A basis is a set of statements with term variables,not necessarily distinct,as subjects.If a basis is denoted as:,...,:,the are distinct.
Remark3.1.2In the notation of types,often outermost and rightmost brackets are omitted.We will use the symbol to denote a type variable and all other greek characters to denote arbitrary types.Also, instead of indexed by a number,we will write the number.
De?nition3.1.3i)A substitution S:is as usual inductively de?ned by:
a)The substitution(),where is a type variable and,is de?ned by:
1)()()=.
2)()()=,if.
3)()()=.
4)()()=()()()().
b)If and are substitutions,then so is,where()=(()).
ii)If for,there is a substitution S such that S()=,then is called a(substitution)instance of. iii)If is an instance of,and is an instance of,then is called a trivial variant of.We identify types that are trivial variants of each other.
iv)S()=:S():.
v)S(,)=S(),S().
3.2Type assignment
Type assignment on a LLATRS(,R)is de?ned as the labelling of nodes and edges in the tree repre-sentation of terms and rewrite rules with types.If a node or edge is labelled with a type,we say that it is typed with,and is assigned to it.
In this labelling,we use that there is a mapping that provides a type in for every Ap. Such a mapping is called an environment.
De?nition3.2.1Let(,R)be a LLATRS.A mapping:Ap is called an environment if ()=(12)12,and for every with arity,()=()==().
De?nition3.2.2Let(,R)be a LLATRS.
i)We say that T is typeable by with respect to,if there exists an assignment of
types to edges and nodes that satis?es the following constraints:
a)The root edge of is typed with.
b)If a node contains a symbol Ap that has arity(),then there are,...,
and,such that this node is typed with,the out-going edges are from left to right typed with up to,and the in-going edge is typed with.
ii)Let T be typeable by with respect to.If is a basis containing all statements with variables as subjects that appear in the typed tree for:,we write:.
Notice that if:,then can contain more statements than needed to obtain:.
De?nition3.2.3Let(,R)be a LLATRS.
i)We say that r:R with de?ned symbol is naively typeable with respect to,if the
following constraints hold:
a)There are and basis such that:and:.
b)All nodes within r containing the same term variable,are typed with the same type.
c)The de?ning node of r,containing,is typed with().
ii)We say that(,R)is naively typeable with respect to,if for every r R:r is naively typeable with respect to.
Condition(i.c)is in fact added to make sure that the type provided by the environment for a function symbol is not in con?ict with the rewrite rules that de?ne.By restricting the type that can be assigned to the de?ning node to the type provided by the environment,we are sure that the rewrite rule is typed using that type,and not using a substitution instance.
In the rest of this paper,we will assume the environment to be?xed,so we omit the subscript on. Also,instead of saying‘(naively)typeable with respect to’,we just say‘typeable’.
It is easy to check that if is a function symbol with artity,and all rewrite rules that de?ne are typeable,then there are,...,,such that()=.
The use of an environment corresponds to the use of‘axiom-schemes’,and part(i.c)of de?nition
3.2.2to the use of‘axioms’as in[Hindley’69].
A typical example for part(i.b)of de?nition3.2.2is the function symbol,which has the type
(12)12.So for every occurrence of in a tree,there are and such that the following is part of the tree.
De?nition3.3.2We de?ne,for every term the notion()=,inductively by:
i)For all,:()=:,.
ii)If for every:()=,,()=,(we choose if necessary trivial variants such that the,are pairwise disjoint and these pairs share no type variables with ),and
S=(,),
where does not occur in any of the pairs,,nor in,then:
=S(),S().
The following theorem shows that substitution is a sound operation on trees.As illustrated in section 3.5,we cannot show such a result for rewrite rules.
Theorem3.3.3Soundness of substitution.If:,then for every substitution S:S():S(). Proof:By easy induction on the structure of.
=(),().
and S’()=S(),and S’()=S().
The following lemma plays an important part in the proof that the condition,as de?ned in de?nition 4.2.1,imposed on typeable rewrite rules is needed and suf?cient,as given in theorem4.2.3and for-mulates the relation between replacements performed on a term and possible type assignments for that term.
Lemma3.3.6i)If()=,,and for the replacement R there are and such that M:, then there is a substitution S,such that S()=,and for every statement:::S(). ii)If:,and R is a replacement and’a basis such that for every statement::’:, then’M:.
Proof:By induction on the structure of.
i)The proof is very much the same as the one for theorem3.3.4.
ii)Easy.
3
:(123)(12)13 :123
3
:123:1:12:1
1
:1
:1 Example3.4.2Using
()=((12)3)(12)2,
()=(123)(12)13,and
()=11
the rule of example2.3can be typed as follows:
:((12)13)((12)1)(12)3
:(12)13:(12)1
3.5About recursion
The rule can be typed using()=123:
3
:513
:1
:2(676)5
:2:676
Notice that because of de?nition3.2.2(i.c)the types assigned to the nodes containing in the right hand side need only be instances of123.
Not every substitution instance of the type123can be proven to be a correct type for.For example when using()=112,this rule cannot be typed.If?rst and second argument of should have the same type,then the only types possible for are the substitution instances of (121)(121)121.
However,by de?nition3.2.2(i.c)it is possible that occurs in a term with type112.This means of course that although we allow all substitutions on the environment types of de?ned symbols,we cannot prove that all the types that are obtained in this way,are correct types for the rewrite rule.
This means in fact that the Mycroft approach is not very well suited for type assignment in term rewriting systems.If instead of Mycroft’s approach we would use Milner’s,which would require that all occurrences of the de?ned symbol of a rule within that rule are typed with(),it is easy to verify that soundness of substitution can even be shown for rewrite rules.
4Safe type assignment
In this section we show that the naive type assignment is not safe:there are typeable rewrite rules that match a term typeable with,for which the result of the application of the rewrite rule on is not typeable with.We will formulate a condition typeable rewrite rules should satisfy in order to obtain preservance of types under rewriting.We will show that this condition is needed and suf?cient.
4.1Patterns cause problems
De?nitions3.2.1,3.2.2and3.2.3de?ne what a type assignment should be,just using the strategy as used in languages like for example Miranda.It is called naive,because it not suf?cient to guarantee preservance of types under rewriting.(This is also called the‘subject reduction property’.)Not even typeability is kept under rewriting.
Take for example the de?nition of as in example2.3,which can be typed as shown in example 3.4.2.If we take the term then it is easy to see that the rewrite is allowed,and that this term will be rewritten to:.
Although the?rst term is typeable in the following way:
:((45)(45)45)((45)45)(45)45
:(45)(45)45:(45)45
the term is not typeable with the type(45)5.In fact,it is not typeable at all.
4.2A needed and suf?cient condition for preservance of types under
rewriting
By de?nition1.2,if a term is rewritten to the term’using the rewrite rule,there is a subterm of,and a replacement R,such that Lhs=.’is obtained by replacing by Rhs.To guarantee the subject reduction property,we should accept only those rewrite rules ,that satisfy:
For all replacements R,bases and types:if Lhs:,then Rhs:. because then we are sure that all possible rewrites are safe.
In the notion of type assignment as presented in this paper,it is easy to formulate a condition that rewrite rules should satisfy in order to be accepted.
De?nition4.2.1i)We call a rewrite rule safe if:
If()=,,then:.
ii)The de?nition of a safe type assignment with respect to is the same as the one for a naive type assignment,by replacing in de?nition3.2.3condition(i.a)and(i.b)by:
If()=,,then:.
Notice that the notion()is de?ned independently from the de?nition of typeable rewrite rules. As an example of a rule that is not safe,take the typed rewrite rule in the next example:the types assigned to the nodes containing and are not the most general ones needed to?nd the type for the left hand side of the rewrite rule.
Example4.2.2Take the de?nition of as in example2.3.To obtain(),we assign types to nodes in the tree in the following way:
:((12)43)((12)4)(12)3
:(12)43:(12)4
If the right hand side should be typed with(12)2,the type needed for the node containing is (12)1.
In the following theorem,we prove that our solution is correct.The structure of the?rst proof depends greatly on the fact that for every type we can trivially?nd an,such that()=: we just pick a constant,not already used.We do not require in the proof that for every symbol there is a rewrite rule that de?nes.
Theorem4.2.3i)The condition is needed.Let,T,and r:be a ty-peable rewrite rule that is not safe.Then there there exists a replacement R,and a type,such that Lhs:&Rhs:.
ii)The condition is suf?cient.Let,T,and r:be a safe rewrite rule.
Then for every replacement R,basis and a type:Lhs:Rhs:.
Proof:i)Since r is typeable and left linear,we know that there are,...,,,and distinct,..., ,such that:
:,...,::&:,...,::.
Then by theorem3.3.4,and lemma3.3.5we know that there are bases,,types,...,, and a substitution,such that:
()=,&()=,&=:,...,:&
()=()=&()=()=:,...,:.
Let be the substitution such that for every:()=(the-th type constant),be a type such that()=,,...,be constants such that for every,()=(),and R be the replacement such that for every:=.Then by lemma3.3.6(ii):Lhs:.
(Notice that Lhs does not contain term variables.)Since r is not safe,we know that
:,...,::.
Suppose towards a contradiction that Rhs:.
Then by lemma3.3.6(i)there is a substitution such that
()=and for every:::().
By de?nition1.2(ii.a.3)for every:there is a such that=.Since replaces type variables by type constants,the type assigned to can only be().This implies that for every:there is a such that=and()=().It is straightforward to verify that,since replaces type variables by type constants,there is a substitution such that =.So for every:there is a such that:=and=().But then by lemma3.3.3:
:,...,::().
Moreover,=()=()=(),so=().
ii)Since r is safe,there are,such that:if()=,,then:
Suppose()=,,and R is a replacement such that there are basis and type such that Lhs:,then by lemma3.3.6(i)there is a substitution S such that
S()=&:[:S()].
But then by lemma3.3.3:
S():S()&:[:S()].
So by lemma3.3.6(ii):Rhs:.
(The rules for Opt are not intended to be complete.)They can now be used in combination with the previous rules for bracket abstraction to produce simpli?ed combinator expressions.For example, the combinator expression that would be produced for(i.e.)will be evaluated as below:
Opt(
This is what we would expect for the above lambda expression.
Conjecture5.1As indicated above,some of the rewrite rules for Opt are not safe.By theorem4.2.3(i) we can give a term,typeable by such that one of the unsafe rewrite rules matches,but the result of rewriting with this rule is not typeable with.However,in this construction we use that the type system contains also type constants.If we would use a type system without type constants,we conjecture that the safeness condition can be formulated in such a way that the rewrite rules for Opt are all safe.
Appendix:A type check algorithm for LLATRS’s
In this section we present a type check algorithm that,when applied to a LLATRS and a environment determines whether this LLATRS is safely typeable with respect to the environment.The algorithm is speci?ed in a notation based on the programming language Clean.
A.1Representing LLATRS’s and Curry types
Since type assignment is syntax directed,it is convenient to make the structure of an LLATRS explicit, for such a structure enables us to use pattern matching to distinguish the different syntactical parts.In Clean new data structures are de?ned by means of algebraic type de?nitions,and Clean uses square brackets(i.e.‘[’and‘]’)to denote list types.
The algebraic type de?nitions for LLATRS’s that we use are the following:
TYPE
::TRS[Rule];
::Rule(Term,Term);
::Term Var Variable Symb Symbol[Term]DefSymb Symbol[Term];
::Variable...;
::Symbol Ap...;
The last alternative for Term(de?ning the constructor DefSymb)is used to indicate that the corre-sponding(sub)term starts with the de?ned symbol(de?nition1.2(iii.a)).So,using DefSymb makes only sense when specifying the left hand side of a rewrite rule.Note that it is very well possible to determine the de?ning node of a certain left hand side of a rewrite rule.This however would make the algorithm somewhat more complicated and therefore less clear.
A basis(de?nition3.1.1(iii))is a set of statements with term variables as subjects.Since there are no sets in Clean we use lists instead.Hence,the representation of bases becomes:
TYPE
::Statement(Variable,CurryType);
::Basis[Statement];
A.2The type check algorithm
The goal of the type check algorithm presented below is to determine whether a safe type assignment can be constructed such that all the conditions of de?nitions3.2.2and3.2.3are satis?ed.The main function of the algorithm,called TypeTRS,expects a LLATRS as well as a environment as parameters. It returns a boolean that indicates whether the construction of the type assignment was successful.
It is easy to prove that the algorithm presented here is correct and complete:
Theorem A.2.1i)If is typeable with respect to the environment,then TypeTerm returns ().
ii)If TypeTerm returns the pair,,then()=,.
iii)There is a safe type assignment with respect to for the LLATRS TRS,if and only if TypeTRS TRS returns TRUE.
Proof:By straightforward induction on the structure of terms and rewrite rules.
The algorithm does not perform any consistency check on its input so it assumes the input to be correct according to de?nitions1.1and1.2.Moreover,all possible error messages and error handling cases are omitted,and the algorithm returns only TRUE for rewrite systems that are safely typeable.It could easily be extended to an algorithm that accepts unsafe rewrite rules.
The algorithm as presented here is not purely functional.The0-ary function FreshVariable(used amongst others by TypeSymb and TypeVar)is supposed to return a new,unused type variable.It is obvious that such a function is not referential transparent,but for the sake of readability,we prefer not to be explicit on the handling of typevariables.
::TypeTRS TRS Environment BOOL;
TypeTRS[]TRUE
TypeTRS[r rules]And(TypeRule r)(TypeTRS rules);
Constraint3.2.2(i.b)describes that for every term variable occurring in a rewrite rule,all the nodes containing this variable in the bases for both the left and the right hand side should contain equal pred-icates.This is provided in TypeRule by unifying all predicates for each subject occurring in the bases after a rule has been type checked.These uni?cations are performed by the function UnifyBasis.Type-Rule also takes care of checking the safeness constraint as given in de?nition4.2.1(ii),by checking, using EqualBases,if the uni?cation of left and right hand sides of a rewrite rule has changed the left hand side basis.
::TypeRule Rule Environment BOOL;
TypeRule(,)EqualBases((()))
:UnifyBasis(()()),
:UnifyTypes,
(,):TypeTerm,
(,):TypeTerm;
The type of a symbol is either an instance of the type for that symbol given by the environment (in case of a Symb)or that type itself(in case of a DefSymb).The distinction between the two is determined by the function TypeTerm.The de?ning node of a rewrite rule can only be typed with one type,so any substitution resulting from a uni?cation is forbidden to change this type.This is solved by the uni?cation algorithm UnifyTypes,an extension of Robinsons uni?cation algorithm;it is capable of deciding whether or not a type variable is special(so it appears in some environment type)and it refuses to substitute this variable by other types.
::TypeTerm Term Environment(Basis,CurryType);
TypeTerm(Var)TypeVar
TypeTerm(Symb args)TypeSymb(Instance(()))args
TypeTerm(DefSymb args)TypeSymb(())args;
The function TypeSymb veri?es the constraints3.2.2(i.b)by the means of the method indicated by de?nition3.3.2.
::TypeSymb CurryType[Term]Environment(Basis,CurryType);
TypeSymb[](,)
TypeSymb terms(S(),S()),
S:UnifyTypes,
(,):TypeArguments terms,
:FreshVariable; TypeArguments is an auxiliary function that derives the types for all arguments of a node and
constructs an arrow type out of these types.Note that this function expects the last type of the arrow type that is constructed as a parameter:the type variable is passed to the function TypeArguments to make sure that the type is created,instead of().Besides the adjusted basis,this arrow type is delivered as a result.
::TypeArguments[Term]CurryType Environment(Basis,CurryType);
TypeArguments[](,)
TypeArguments[terms](,),
:,
(,):TypeTerm,
(,):TypeArguments terms;
TypeVar assigns a new type variable to a term variable.
::TypeVar Variable(Basis,CurryType);
TypeVar([(,)],),
:FreshVariable;
References
[Barendregt’84]Barendregt H.The Lambda Calculus:its Syntax and Semantics.North-Holland,Amsterdam, revised edition,1984.
[Barendregt et al.’83]Barendregt H.,M.Coppo,and M.Dezani-Ciancaglini.A?lter lambda model and the completeness of type assignment.The Journal of Symbolic Logic,48(4):931–940,1983.
[Barendregt et al.’87]Barendregt H.P.,M.C.J.D.van Eekelen,J.R.W.Glauert,J.R.Kennaway,M.J.Plasmeijer, and M.R.Sleep.Term graph rewriting.In Proceedings of PARLE,Parallel Architectures and Languages Europe,Eindhoven,The Netherlands,volume259-II of Lecture Notes in Computer Science,pages141–158.
Springer-Verlag,1987.
[Brus et al.’87]Brus T.,M.C.J.D.van Eekelen,M.O.van Leer,and M.J.Plasmeijer.Clean-A Language for Functional Graph Rewriting.In Proceedings of the Third International Conference on Functional Pro-gramming Languages and Computer Architecture,Portland,Oregon,USA,volume274of Lecture Notes in Computer Science,pages364–368.Springer-Verlag,1987.
[Curry&Feys’58]Curry H.B.and https://www.wendangku.net/doc/378408203.html,binatory Logic.volume1.North-Holland,Amsterdam,1958. [Damas’85]Damas L.M.M.Type Assignment in Programming Languages.PhD thesis,University of Edinburgh, Department of Computer Science,Edinburgh,1985.Thesis CST-33-85.
[Futatsugi et al.’85]Futatsugi K.,J.Goguen,J.P.Jouannaud,and J.Meseguer.Principles of OBJ2.In Proceed-ings12ACM Symposium on Principles of Programming Languages,pages52–66,1985.
[Hindley’69]Hindley J.R.The principal type scheme of an object in combinatory logic.Transactions of the American Mathematical Society,146:29–60,1969.
[Kfoury et al.’88]Kfoury A.J.,J.Tiuryn,and P.Urzyczyn.A proper extension of ML with an effective type-assignment.In Proceedings of the Fifteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,pages58–69,San Diego,California,1988.
[Klop’92]Klop J.W.Term Rewriting Systems.In S.Abramsky,Dov M.Gabbay,and T.S.E.Maibaum,editors, Handbook of Logic in Computer Science,volume2,chapter1,pages1–116.Clarendon Press,1992. [Milner’78]Milner R.A theory of type polymorphism in programming.Journal of Computer and System Sciences,17:348–375,1978.
[Mycroft’84]Mycroft A.Polymorphic type schemes and recursive de?nitions.In Proceedings of the Inter-national Symposium on Programming,Toulouse,volume167of Lecture Notes Computer Science,pages 217–239.Springer-Verlag,1984.
[N¨o cker et al.’91]N¨o cker E.G.J.M.H.,J.E.W.Smetsers,M.C.J.D.van Eekelen,and M.J.Plasmeijer.Concur-rent Clean.In Proceedings of PARLE’91,Parallel Architectures and Languages Europe,Eindhoven,The Netherlands,volume506-II of Lecture Notes in Computer Science,pages202–219.Springer-Verlag,1991.
[Pfenning’88]Pfenning F.Partial Polymorphic Type Inference and Higher-Order Uni?cation.In Proceedings of the1988conference on LISP and Functional Programming Languages,volume201of Lecture Notes in Computer Science,pages153–163.Springer-Verlag,1988.
[Robinson’65]Robinson J.A.A machine-oriented logic based on the resolution principle.Journal of the ACM, 12(1):23–41,1965.
[Turner’85]Turner D.A.Miranda:A non-strict functional language with polymorphic types.In Proceedings of the conference on Functional Programming Languages and Computer Architecture,volume201of Lecture Notes in Computer Science,pages1–16.Springer-Verlag,1985.
数据管理系统之数据可视化设计
数据管理系统企业级数据可视化项目Html5 应用实践 项目经理：李雪莉 组员：申欣邹丽丹陈广宇陈思 班级：大数据&数字新媒体 一、项目背景 随着大数据、云计算和移动互联网技术的不断发展，企业用户对数据可视化的需求日益迫切。用户希望能够随时随地简单直观的了解企业生产经营、绩效考核、关键业务、分支机构的运行情况，即时掌握突发性事件的详细信息，快速反应并作出决策。随着企业信息化的不断推进，企业不断的积累基础信息、生产运行、经营管理、绩效考核、经营分析等以不同形式分布在多个系统或个人电脑文档内的业务数据。如何将大量的数据进行分析整理，以简单、直观、高效的形式提供给管理者作为经营决策的依据是当前企业数据应用的迫切需求。传统的企业数据可视化方案多基于Java Applet、Flash、Silverlight 等浏览器插件技术进行开发，在当前互联网和移动互联网技术高速发展的背景下，Web技术标准也随之高速发展，用户对互联网技术安全性和使用体验的要求越来越高。Java Applet、Flash、Silverlight 等浏览器插件技术因为落后和封闭的技术架构，以及高功耗、高系统资源占用，已经被微软、谷歌、苹果、火狐等主流操作系统和浏览器厂商逐步放弃，转而不断支持和完善基于HTML5的新一代Web技术标
准 对数据进行直观的拖拉操作以及数据筛选等，无需技术背景，人人都能实现数据可视化无论是电子表格，数据库还是 Hadoop 和云服务，都可轻松分析其中的数据。 数据可视化是科学、艺术和设计的结合，当枯燥隐晦的数据被数据科学家们以优雅、简明、直观的视觉方式呈现时，带给人们的不仅仅是一种全新的观察世界的方法，而且往往具备艺术作品般的强大冲击力和说服力。如今数据可视化已经不局限于商业领域，在社会和人文领域的影响力也正在显现。 数据可视化的应用价值，其多样性和表现力吸引了许多从业者，而其创作过程中的每一环节都有强大的专业背景支持。无论是动态还是静态的可视化图形，都为我们搭建了新的桥梁，让我们能洞察世界的究竟、发现形形色色的关系，感受每时每刻围绕在我们身边的信息变化，还能让我们理解其他形式下不易发掘的事物。 二、项目简介 目前，金融机构（银行，保险，基金，证劵等）面临着诸如利率汇率自由化，消费者行为改变，互联网金融崛起等多个挑战。为满足企业的发展需要，要求管理者运用大数据管理以更为科学的手段对企业进行精准管理，从而更好地把握市场在竞争中胜出。德昂BI商务智能解决方案基于业务的数据分析正是帮助企业实现科学化管理的关键，因而获得客户的高度重视与高频度使用。 激烈的市场竞争下，通过对金融机构业务数据的汇总与整理实现
国际会计准则第36号
国际会计准则第号资产减值 国际会计准则第号 目的 本准则的目的是，规定企业用以确保其资产以不超过可收回价值（）的金额进行计量的程序。如果资产的帐面价值超过通过使用或销售而收回的价值，该资产就是按超过其可收回价值计量的，如果是这样，该资产应视为已经减值，本准则要求企业确认资产减值损失。本准则也规定了企业何时应冲回资产减值损失，以及减值资产的有关披露内容。 范围 .本准则适用于除下述资产以外的所有资产减值的会计核算： （）存货（参见《国际会计准则第号存货》）； （）建造合同形成的资产（参见《国际会计准则第号建造合同》）； （）递延所得税资产（参见《国际会计准则第号所得税》）； （）雇员福利形成的资产（参见《国际会计准则第号雇员福利》）； （）包括在《国际会计准则第号金融工具：披蹲和列报》范围内的金融资产。 .本准则不适用于存货、建造合同形成的资产、递延所得税资产或雇员福利形成的资产，因为适用于这些资产的现行国际会计准则已经包含了有关其确认和计量的特定要求。 .包括在《国际会计准则第号金融工具：披落和列报》范围内的金融资产，其减值损失的会计核算取决于国际会计准则委员会有关金融工具项目的结果。以下投资属于金融资产，但《国际会计准则第号金融工具：披露和列报》没有包括，因而本准则也适用于这些金融资产： （）《国际会计准则第号合并财务报表和对子公司投资的会计》中定义的子公司； （）《国际会计准则第号对联营企业投资的会计》中定义的联营企业； （）《国际会计准则第号合营中权益的财务报告》中定义的合营企业。 .根据其他国际会计准则，以重估价值（公允价值）计量的资产，如按《国际会计准则第号固定资产》以重估价值作为允许选用的方法计量的资产，本准则也适用。但是，认定某项重估资产是否已经减值，取决于用以确定其公允价值的基础： （）如果资产的公允价值是其市场价值，则资产的公允价值与其销售净价之间的唯一差额是处置该资产的直接增量费用：
国际会计科目对照表(中英)
精心整理 ccount?帐户 Accounting?system?会计系统? American?Accounting?Association?美国会计协会? American?Institute?of?CPAs?美国注册会计师协会? Audit?External?users?外部使用者? Financial?accounting?财务会计? Financial?Accounting?Standards?Board?财务会计准则委员会? Financial?forecast?财务预测? Generally?accepted?accounting?principles?公认会计原则? General-purpose?information?通用目的信息 Government?Accounting?Office?政府会计办公室? ? Management?accounting?管理会计? Return?of?investment?投资回报? Return?on?investment?投资报酬? Securities?and?Exchange?Commission?证券交易委员会?
Statement?of?cash?flow?现金流量表? Statement?of?financial?position?财务状况表? Tax?accounting?税务会计? Accounting?equation?会计等式? Assets? Creditor? Deflation? Disclosure?批露? Expenses?费用? Financial?statement?财务报表? Financial?activities?筹资活动? Going-concern?assumption?持续经营假设Inflation?通货膨涨? Investing?activities?投资活动? Liabilities?负债? Solvency?清偿能力? Stable-dollar?assumption?稳定货币假设? Stockholders?股东? Stockholders?equity?股东权益?
23.国际会计准则
对国际会计准则第8号——当期净损益、重大差错和会计政策变更（1993年修订）的改进建议1 1主译，丁度翻译Invitation to comment, Summary of main changes & Appendix，丁度主校对。
国际会计准则第8号——会计政策、会计估计变更和差错 （200X年修订） （备注：尽管本征求意见稿是以“清样稿”形式列示，上述标题仍以作出标记的形式列示建议的改动。）
征询意见 理事会将特别欢迎对下列问题的回答。意见中最好能指明有关的准则段落，包含明晰的基本原理，并在合适的地方提出备选措辞的建议。 问题1 您是否同意会计政策自愿变更和差错更正的允许选用的处理方法应当被删除，即这些变更和更正应当用追溯调整法处理，如同新的会计政策一直在运用或该差错从未发生那样（参见第20段、21段、32段和33段）？ 问题2 您是否同意删除重大差错和其他重要差错的区别（参见第32段和33段）？ 主要改动摘要 主要的改动建议有： ●通过下列方式修改本准则的范围： ?包含《国际会计准则第1号——会计报表的列报》的第20至22段，该 段详细说明了会计政策选择的标准； ?删除IAS8第7至18段涉及到收益表项目列报的要求。这些要求，包括 所作的修改，将转入IAS1。 因此，本准则的名称该为《会计政策、会计估计变更和差错》。 ●删除重大差错和其他重要差错的区别，并在建议的第3段增加差错的定 义。重大差错的概念被删除 ●删除IAS8第38至40段所列的差错更正允许选用的处理方法。因此，某个 实体不再被允许： ?将差错更正的金额包含在当期损益中；
中英文会计科目对照表
中英文会计科目对照表如下: 会计科目中英对照表会计科目 accounting subject 顺序号serial number 编号code number 会计科目名称accounting subject 会计科目适用范围accounting subject range of application 一、资产类 1 1001 库存现金 cash on hand 2 1002 银行存款 bank deposit 5 1015 其他货币资金 other monetary capital 9 1101 交易性金融资产 transaction monetary assets 11 1121 应收票据 notes receivable 12 1122 应收账款 Account receivable 13 1123 预付账款 account prepaid 14 1131 应收股利 dividend receivable 15 1132 应收利息 accrued interest receivable 21 1231 其他应收款 accounts receivable-others 22 1241 坏账准备 had debts reserve 28 1401 材料采购 procurement of materials 29 1402 在途物资 materials in transit 30 1403 原材料 raw materials 32 1406 库存商品 commodity stocks 33 1407 发出商品 goods in transit 36 1412 包装物及低值易耗品 wrappage and low value and easily wornout articles 42 1461 存货跌价准备 reserve against stock price declining 43 1501 待摊费用 fees to be apportioned 45 1521 持有至到期投资 hold investment due 46 1522 持有至到期投资减值准备 hold investment due reduction reserve
国际会计准则第无形资产
国际会计准则第38号无形资产 1998-06发布 发布时间：2000年08月27日 目的 本准则的目的是对其他国际会计准则中没有具体涉及的无形资产的会计处理进行规范。本准则要求，当且仅当特定条件满足时，企业应确认无形资产。本准则亦对如何计量无形资产的账面金额作了规定，并就无形资产的特定放过提出了要求。 范围 1．本准则应适用于所有企业除以下各项之外的无形资产的会计核算： (1)由其他国际会计准则规范的无形资产； (2)《国际会计准则第32号金融工具：披露和列报》中定义的金融资产； （3）矿产权，以及矿产、石油、天然气和类似非再生性资源的勘探支出或开发和采掘支出；
（4）保险公司与保单持有人之间签订的合同所产生的无形资产。 2．如果其他国际会计准则涉及了特定类型的无形资产，那么企业应运用该项准则而不是本准则。例如，本准则不适用于以下各项无形资产： （1）企业在正常经营过程中为出售而持有的无形资产（见《国际会计准则第2号存货》和《国际会计准则第11号建造合同》）； （2）递延所得税资产（见《国际会计准则第12号所得税》）； （3）属于《国际会计准则第17号租赁》范围内的租赁； （4）雇员福利所形成的资产（见《国际会计准则第19号雇员福利》）； （5）企业合并中形成的商誉（见《国际会计准则第22号企业合并》）； （6）《国际会计准则第32号金融工具：披露和列报》中定义的金融资产。金融资产的确认和计量由以下准则规范：《国际会计准则第27号合并财务报表和对于公司投资的会计》、《国际会计准则第28号在联营企业投资的会计》、《国际会计准则第31号合营中权益的
财务报告》和《国际会计准则第39号金融工具：确认和计量》。 3．一些无形资产可能会以实物为载体，例如磁盘（对计算机软件而言）、法律文件（对许可证或专利权而言）或胶片式确定一项包含无形和有形要素的资产应按《国际会计准则第历号一固定资产》核算，还是作为一项无形资产而按本准则核算，需要进行判断，以评价哪个要素更重要。例如，一台计算机控制的机械工具没有特定计算机软件就不能正常运行时，则说明该软件构成相关硬件不可缺少的组成部分，从而该软件应作为固定资产核算。同样的原则适用于计算机控作系统。如计算机软件不是相关硬件不可缺少的组成部分，则该软件应作为无形资产核算。 4．本准则还适用于广告、培训、开办活动、研究与开发活动支出等。研究与开发活动的目标是开发知识。因此，虽然这些活动可能会产生有实物形态的资产（例如，样品），但该资产的实物要素次于其无形要素（即含在实物要素中的知识）。 5．就融资租赁而言，标的资产可能是有形的，也可能是无形的。初始确认后，承租人应按本准则的规定核算因融资租赁而持有的无形资产。电影、录相、戏剧、手稿、专利权和版权等项目的许可证协议中的权利不在《国际会计准则第对号一租赁》范围之内，而在本准则范围之内。 6．如果某些活动或交易特殊，可能需要用其他方式进行会计处理，那么该活动或交易可能会被排除出某项国际会计准则的范围。采掘业中因石油、天然气和矿产的勘探或开发和采
会计科目中英对照表
资产Assets 流动资产Current assets 货币资金Cash at bank and on hand 交易性金融资产Financial assets held for trading 应收票据Notes receivable 应收账款Accounts receivable 预付款项Advances to suppliers 应收利息Interest receivable 应收股利Dividends receivable 其他应收款Other receivables 存货Inventories 一年内到期的非流动Current portion of non-current assets
资产 其他流动资产Other current assets 流动资产合计Total current assets 非流动资产Non-current assets 可供出售金融资产Available-for-sale financial assets 持有至到期投资Held-to-maturity investments 长期应收款Long-term receivables 长期股权投资Long-term equity investments 投资性房地产Investment properties 固定资产Fixed assets 在建工程Construction in progress 工程物资Construction materials
固定资产清理Fixed assets pending for disposal 生产性生物资产Bearer biological assets 油气资产Oil and gas assets 无形资产Intangible assets 开发支出Development costs 商誉Goodwill 长期待摊费用Long-term prepaid expenses 递延所得税资产Deferred tax assets 其他非流动资产Other non-current assets 非流动资产合计Total non-current assets 资产总计Total assets
企业会计准则第38号——首次执行企业会计准则
企业会计准则第38号——首次执行企业会计准则 第一章总则 第一条为了规范首次执行企业会计准则时的确认、计量和财务报表列报，根据《企业会计准则——基本准则》，制定本准则。 第二条首次执行企业会计准则，是指企业第一次执行2006年发布的企业会计准则体系，包括基本准则、各项具体准则和会计准则应用指南。 第三条首次执行企业会计准则后发生的会计政策变更，适用《企业会计准则第28号——会计政策、会计估计变更和差错更正》。 第二章确认和计量 第四条在首次执行日，企业应当对所有资产、负债和所有者权益按照企业会计准则的规定进行重新分类、确认和计量，并编制期初资产负债表，本准则规定不应追溯调整的除外。 第五条对于首次执行日的长期股权投资，应当分别下列情况处理： (一)对于按照《企业会计准则第20号——企业合并》规定，属于同一控制下企业合并产生的长期股权投资，尚未摊销完毕的股权投资差额全额冲销，并调整留存收益，以冲销股权投资差额后的长期股权投资账面价值作为首次执行日的认定成本。 (二)除上述第(一)项以外的其他采用权益法核算的长期股权投资，存在股权投资贷方差额的，应冲销贷方差额，调整留存收益，并以冲销贷方差额后的长期股权投资账面价值作为首次执行日的认定成本；存在股权投资借方差额的，应当将长期股权投资的账面价值作为首次执行目的认定成本。 第六条在首次执行日，企业应当根据《企业会计准则第3号——投资性房地产》，将符合投资性房地产定义、原包括在固定资产(或无形资产、存货)账面价值中的相应金额，确认为投资性房地产。 对于有确凿证据表明可以采用公允价值模式计量的投资性房地产，应当按照其公允价值进行计量，账面价值与公允价值的差额，调整留存收益。 第七条在首次执行日，对于符合预计负债确认条件且该日之前尚未计入固定资产成本的弃置费，应当增加该项资产成本和负债；同时，将应补提的折旧调整留存收益。
国际会计科目中英文对照
国际会计科目中英文对照Account帐户 Accounting system会计系统AmericanAccountingAssociation美国会计 协会 AmericanInstituteofCPAs美国注册会计师 协会 Audit审计 Balance sheet资产负债表 Bookkeepking簿记 Cash flow prospects现金流量预测 Certificate in Internal Auditing内部审计证书CertificateinManagementAccounting管理 会计证书 Certificate Public Accountant注册会计师 Cost accounting成本会计 External users外部使用者 Financial accounting财务会计 Financial Accounting Standards Board财务会 计准则委员会 Financial forecast财务预测
Generallyacceptedaccountingprinciples公认会计原则 General-purpose information通用目的信息GovernmentAccountingOffice政府会计办公室 Income statement损益表InstituteofInternalAuditors内部审计师协会InstituteofManagementAccountants管理会计师协会 Integrity整合性 Internal auditing内部审计 Internal control structure内部控制结构Internal Revenue Service国内收入署Internal users内部使用者 Management accounting管理会计Return of investment投资回报 Return on investment投资报酬SecuritiesandExchangeCommission证券交易委员会 Statement of cash flow现金流量表
企业会计准则第38号
企业会计准则第38号 财会[2006]3号 第一章总则 第一条为了规范首次执行企业会计准则对会计要素的确认、计量和财务报表列报，依照《企业会计准则——差不多准则》，制定本准则。 第二条首次执行企业会计准则，是指企业第一次执行企业会计准则体系，包括差不多准则、具体准则和会计准则应用指南。 第三条首次执行企业会计准则后发生的会计政策变更，适用《企业会计准则第28号——会计政策、会计估量变更和差错更正》。 第二章确认和计量 第四条在首次执行日，企业应当对所有资产、负债和所有者权益按照企业会计准则的规定进行重新分类、确认和计量，并编制期初资产负债表。 编制期初资产负债表时，除按照本准则第五条至第十九条规定要求追溯调整的项目外，其他项目不应追溯调整。 第五条关于首次执行日的长期股权投资，应当分别下列情形处理： （一）依照《企业会计准则第20号——企业合并》属于同一操纵下企业合并产生的长期股权投资，尚未摊销完毕的股权投资差额应全额冲销，并调整留存收益，以冲销股权投资差额后的长期股权投资账面余额作为首次执行日的认定成本。 （二）除上述（一）以外的其他采纳权益法核算的长期股权投资，存在股权投资贷方差额的，应冲销贷方差额，调整留存收益，并以冲销贷方差额后的长期股权投资账面余额作为首次执行日的认定成本； 存在股权投资借方差额的，应当将长期股权投资的账面余额作为首次执行日的认定成本。 第六条关于有确凿证据说明能够采纳公允价值模式计量的投资性房地产，在首次执行日能够按照公允价值进行计量，并将账面价值与公允价值的差额调整留存收益。 第七条在首次执行日，关于满足估量负债确认条件且该日之前尚未计入资产成本的弃置费用，应当增加该项资产成本，并确认相应的负债；同时，将应补提的折旧（折耗）调整留存收益。 第八条关于首次执行日存在的解除与职工的劳动关系打算，满足《企业会计准则第9号——职工薪酬》估量负债确认条件的，应当确认因解除与职工的劳动关系给予补偿而产生的负债，并调整留存收益。
图书管理系统数据流程图
图书管理系统数据流程图 2009-04-14 17:20 1.1 系统分析 1.1.1 图书馆管理信息系统的基本任务 该“图书馆管理信息系统”是一个具有万人以上的员工，并地理位置分布在大型企的图 书馆理系统，图书馆藏书 100 多万册，每天的借阅量近万册。在手工操作方式下，图书的编目和借阅等的工作量大，准确性低且不易修改维护，读者借书只能到图书馆手工方式查找书目，不能满足借阅需求。需要建立一套网络化的电子图书馆信息系统。 该图书馆管理信息系统服务对象有两部分人：注册用户和一般读者。一般读者经注册后成为注册用户，注册用户可以在图书馆借阅图书，其他人员只可查阅图书目录，但不能借阅图书。系统同时考虑提供电子读物服务，目前只提供电子读物的目录查询服务，不久的将来将提供电子读物全文服务。用户可通过网络方式访问读图书馆管理信息系统。 1.1.2 系统内部人员结构、组织及用户情况分析 为了对系统有一个全貌性的了解，首先要对系统内部人员结构、组织及用户情况有所了 解。图书馆系统的组织结构如图 1 － 1 所示。 图 1 － 1 图书馆管理信息系统的组织结构 图书馆由馆长负责全面工作，下设办公室、财务室、采编室、学术论文室、图书借阅室、电子阅览室、期刊阅览室和技术支持室。各部门的业务职责如下。
办公室：办公室协助馆长负责日常工作，了解客户需求，制定采购计划。 财务室：财务室负责财务方面的工作。 采编室：采编室负责图书的采购，入库和图书编目，编目后的图书粘贴标签，并送图书借阅室上架。 学术论文室：负责学术论文的收集整理。 图书借阅室：提供对读者的书目查询服务和图书借阅服务。 电子阅览室：收集整理电子读物，准备提供电子读物的借阅服务，目前可以提供目录查询和借阅。 期刊阅览室：负责情况的收集整理和借阅。 技术支持室：负责对图书馆的网络和计算机系统提供技术支持。 1.1.3 系统业务流程分析 系统的业务室系统要达到的业务目标，业务流程分析是系统分析的基础环节。图书馆管 理信息系统的业务流程如图 1 － 2 所示。
《最新国际会计科目中英文对照》(2013.9)
中国会计科目中英文对照 代码名称代码名称代码名称代码名称英译 1 资产assets 11~ 12 流动资产current assets 111 现金及约当现金cash and cash equivalents 1111 库存现金cash on hand 1112 零用金/周转金petty cash/revolving funds 1113 银行存款cash in banks 1116 在途现金cash in transit 1117 约当现金cash equivalents 1118 其它现金及约当现金other cash and cash equivalents 112 短期投资short-term investment 1121 短期投资-股票short-term investments - stock 1122 短期投资-短期票券short-term investments - short-term notes and bills 1123 短期投资-政府债券short-term investments - government bonds 1124 短期投资-受益凭证short-term investments - beneficiary certificates 1125 短期投资-公司债short-term investments - corporate bonds 1128 短期投资-其它short-term investments - other 1129 备抵短期投资跌价损失allowance for reduction of short-term investment to market 113 应收票据notes receivable 1131 应收票据notes receivable 1132 应收票据贴现discounted notes receivable 1137 应收票据-关系人notes receivable - related parties 1138 其它应收票据other notes receivable 1139 备抵呆帐－应收票据allowance for uncollec- tible accounts- notes receivable 114 应收帐款accounts receivable 1141 应收帐款accounts receivable 1142 应收分期帐款installment accounts receivable 1147 应收帐款-关系人accounts receivable - related parties 1149 备抵呆帐－应收帐款allowance for uncollec- tible accounts - accounts receivable 118 其它应收款other receivables 1181 应收出售远汇款forward exchange contract receivable 1182 应收远汇款-外币forward exchange contract receivable - foreign currencies 1183 买卖远汇折价discount on forward ex-change contract 1184 应收收益earned revenue receivable 1185 应收退税款income tax refund receivable 1187 其它应收款- 关系人other receivables - related parties 1188 其它应收款- 其它other receivables - other 1189 备抵呆帐- 其它应收款allowance for uncollec- tible accounts - other receivables 121~122 存货inventories 1211 商品存货merchandise inventory 1212 寄销商品consigned goods
新会计准则会计科目表(中英文对照)知识分享
一、资产类 1 1001 库存现金cash on hand 2 1002 银行存款bank deposit 5 1015 其他货币资金other monetary capital 9 1101 交易性金融资产transaction monetary assets 11 1121 应收票据notes receivable 12 1122 应收账款Account receivable 13 1123 预付账款account prepaid 14 1131 应收股利dividend receivable 15 1132 应收利息accrued interest receivable
21 1231 其他应收款accounts receivable-others 22 1241 坏账准备had debts reserve 28 1401 材料采购procurement of materials 29 1402 在途物资materials in transit 30 1403 原材料raw materials 32 1406 库存商品commodity stocks 33 1407 发出商品goods in transit 36 1412 包装物及低值易耗品wrappage and low value and easily wornout articles 42 1461 存货跌价准备reserve against
stock price declining 45 1521 持有至到期投资hold investment due 46 1522 持有至到期投资减值准备hold investment due reduction reserve 47 1523 可供出售金融资产financial assets available for sale 48 1524 长期股权投资long-term stock ownership investment 49 1525 长期股权投资减值准备long-term stock ownership investment reduction reserve 50 1526 投资性房地产investment real eastate 51 1531 长期应收款long-term account
国际会计科目对照表中英
ccount?帐户 Accounting?system?会计系统? American?Accounting?Association?美国会计协会? American?Institute?of?CPAs?美国注册会计师协会? Audit?审计? Balance?sheet?资产负债表? Bookkeepking?簿记? Cash?flow?prospects?现金流量预测? Certificate?in?Internal?Auditing?内部审计证书? Certificate?in?Management?Accounting?管理会计证书? Certificate?Public?Accountant注册会计师? Cost?accounting?成本会计? External?users?外部使用者? Financial?accounting?财务会计? Financial?Accounting?Standards?Board?财务会计准则委员会? Financial?forecast?财务预测? Generally?accepted?accounting?princip les?公认会计原则? General-purpose?information?通用目的信息 Government?Accounting?Office?政府会计办公室? Income?statement?损益表? Institute?of?Internal?Auditors?内部审计师协会? Institute?of?Management?Accountants?管理会计师协会? Integrity?整合性? Internal?auditing?内部审计?
最新国际会计准则ias41
目录 1 概述 2 目的 3 范围 4 定义 5 披露 6 生效日期和过渡性规定 二、目的 本准则的目的是规范农业活动的会计处理、财务报表列报和披露。 三、范围 1.当以下事项涉及农业活动时，本准则适用其会计处理： （1）生物资产 （2）收获时的农产品 （3）本准则34-45段涉及的政府补助 2.本准则不适用于： （1）与农业活动相关的土地（见《国际会计准则第16号-不动产、厂房和设备》以及《国际会计准则第40号-投资性房地产》）。 （2）与农业活动相关的无形资产（见《国际会计准则第38号-无形资产》）。 3.本准则只适用于作为企业生物资产收获物的农产品在收获时的核算，该时点之后适用存货和其他国际会计准则。因此，本准则不涉及收获后农产品的加工，例如种植葡萄的制酒商将葡萄加工成葡萄酒。虽然这种加工可能是农业活动自然和逻辑上的延伸，并且可能与生物转化有相似之处，但是这种加工并不包括在本准则所称的农业活动的定义之内。 4.下表给出了生物资产、农产品加工收获后加工而得的产品的例子： 生物资产农产品收获后加工而得产品 绵羊羊毛毛线地毯 人工林场中的林木原木木料 农作物棉花茎果棉线衣服食糖
奶牛牛奶乳烙 猪宰杀后的猪猪肉肠熏制火腿 灌木茎叶茶叶焙制的烟草 葡萄树鲜葡萄葡萄酒 果树采摘的水果加工后的水果 四、定义 有关农业的定义 5.本准则使用的下列术语，其含义为： 农业活动，指企业对生物资产转化为可售生物资产、农产品或其他生物资产的生物转化过程的管理。农产品，指企业生物资产的收获品。 生物资产，指活的动物或植物。 生物转化，指导致生物资产质量或数量发生变化的生长、蜕变、生产、繁殖的过程。 生物资产集群，指类似动物或植物的组合。 收获，指农产品从生物资产上分离，或生物资产的生长过程的结束。 6.农业活动包括了多种多样的活动。例如，牲畜饲养、林业、一年生或多年生物的收获、果树种植栽培、花木培植、水产养殖（包括养鱼）。各种农业活动存在有如下共同特点：（1）转化的能力。动物和植物能够进行生物转化。 （2）转化的管理。通过增强或者至少是稳定转化发生所必须的条件，管理能够促成生物转化的发生（例如营养、湿度、温度、地力和光照）。这种管理便农业活动与其它活动区分开来。例如，从未经管理的资源中收获（如海洋渔业和原始森林的采伐）并不是农业活动。 （3）转化的计量。对生物转化带来的质量（遗传价值、密度、成熟期、脂肪层、纤维强度）变化和数量（产果量重量、立方米、纤维的长度或直径）变化的计量和监控成为管理的日常职能。 7.生物转化产生下列结果： （1）通过以下途径资产发生变化：1）生长（动物域植物数量的增加或质量的提高）；2）蜕化（动物或植物数量的减少或质量的退化）；3）繁育（产生新的动物域植物）； （2）产生农产品，如橡浆、茶叶、羊毛、牛奶等。 一般定义 8.本准则所使用的下列术语，其含义为： 活跃市场，指具备下列所有条件的市场： （1）市场内的交易品是同质的； （2）任何时间均可以正常找到自愿的买者和卖者； （3）价格信息对公众公开。 账面价值，指资产在资产负债表中的资产确认价值。 公允价值，指在公平交易中，熟悉情况的当事人自愿据以进行资产交换或债务清偿的金额。 政府补助，定义见《国际会计准则第20号-政府补助会计和政府援助的披露》。 9.资产的公允价值取决于其当前的位置和条件。因此，例如，某牧场中牲畜的公允价值为相关市场中类似牲畜的价格减去将牧场中的牲畜运到市场的运费和其他费用。 确认和计量 10.企业只有在以下情况下才能确认生物资产： （1）企业因过去交易的结果而控制该资产； （2）与该资产相关的经济利益很可能流入企业；
会计科目中英对照表
资产负债表 Balance Sheet 项目 ITEM 货币资金 Cash 短期投资 Short term investments 应收票据 Notes receivable 应收股利 Dividend receivable 应收利息 Interest receivable 应收帐款 Accounts receivable 其他应收款 Other receivables 预付帐款 Accounts prepaid 期货保证金 Future guarantee 应收补贴款 Allowance receivable 应收出口退税 Export drawback receivable 存货 Inventories 其中：原材料 Including:Raw materials 产成品(库存商品) Finished goods 待摊费用 Prepaid and deferred expenses 待处理流动资产净损失 Unsettled G/L on current assets 一年内到期的长期债权投资 Long-term debenture investment falling due in a yaear 其他流动资产 Other current assets 流动资产合计 Total current assets 长期投资： Long-term investment： 其中:长期股权投资 Including long term equity investment 长期债权投资 Long term securities investment *合并价差 Incorporating price difference 长期投资合计 Total long-term investment 固定资产原价 Fixed assets-cost 减：累计折旧 Less:Accumulated Dpreciation 固定资产净值 Fixed assets-net value 减：固定资产减值准备 Less:Impairment of fixed assets 固定资产净额 Net value of fixed assets 固定资产清理 Disposal of fixed assets 工程物资 Project material 在建工程 Construction in Progress 待处理固定资产净损失 Unsettled G/L on fixed assets 固定资产合计 Total tangible assets 无形资产 Intangible assets 其中:土地使用权 Including and use rights 递延资产（长期待摊费用）Deferred assets 其中:固定资产修理 Including:Fixed assets repair 固定资产改良支出 Improvement expenditure of fixed assets 其他长期资产 Other long term assets 其中:特准储备物资 Among it:Specially approved reserving materials
会计科目英文对照表
会计科目英文对照表 1 资产assets 11~ 12 流动资产current assets 111 现金及约当现金cash and cash equivalents 1111 库存现金cash on hand 1112 零用金/周转金petty cash/revolving funds 1113 银行存款cash in banks 1116 在途现金cash in transit 1117 约当现金cash equivalents 1118 其它现金及约当现金other cash and cash equivalents 112 短期投资short-term investment 1121 短期投资-股票short-term investments - stock 1122 短期投资-短期票券short-term investments - short-term notes and bills 1123 短期投资-政府债券short-term investments - government bonds 1124 短期投资-受益凭证short-term investments - beneficiary certificates 1125 短期投资-公司债short-term investments - corporate bonds 1128 短期投资-其它short-term investments - other 1129 备抵短期投资跌价损失allowance for reduction of short-term investment to market 113 应收票据notes receivable 1131 应收票据notes receivable 1132 应收票据贴现discounted notes receivable 1137 应收票据-关系人notes receivable - related parties 1138 其它应收票据other notes receivable 1139 备抵呆帐－应收票据allowance for uncollec- tible accounts- notes receivable 114 应收帐款accounts receivable 1141 应收帐款accounts receivable 1142 应收分期帐款installment accounts receivable 1147 应收帐款-关系人accounts receivable - related parties 1149 备抵呆帐－应收帐款allowance for uncollec- tible accounts - accounts receivable 118 其它应收款other receivables 1181 应收出售远汇款forward exchange contract receivable 1182 应收远汇款-外币forward exchange contract receivable - foreign currencies 1183 买卖远汇折价discount on forward ex-change contract 1184 应收收益earned revenue receivable 1185 应收退税款income tax refund receivable 1187 其它应收款- 关系人other receivables - related parties 1188 其它应收款- 其它other receivables - other 1189 备抵呆帐- 其它应收款allowance for uncollec- tible accounts - other receivables 121~122 存货inventories 1211 商品存货merchandise inventory 1212 寄销商品consigned goods 1213 在途商品goods in transit 1219 备抵存货跌价损失allowance for reduction of inventory to market