[Objective] The aim was to conduct post-evaluation on environmental planning by means of logical framework approach. [Method] Taking environmental planning during '11th Five-year Plan' in a certain province fo...[Objective] The aim was to conduct post-evaluation on environmental planning by means of logical framework approach. [Method] Taking environmental planning during '11th Five-year Plan' in a certain province for example, by means of logical framework approach (LFA), the post-evaluation on environmental planning was carried out from the aspects of evaluation content, index system, implementation steps, evaluation feedback and input-output analysis of environmental planning. [Result] The post-evaluation on environmental planning by means of LFA achieved expected purpose and various indexes at different stages of environmental planning was assessed, and then corresponding countermeasures were put forward according to the problems which were found by problem tree of environmental planning project. [Conclusion] The study could provide theoretical references for the post-evaluation on environmental planning in future.展开更多
The paper discusses semalltics of encodings in logical frameworkswhere equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. T...The paper discusses semalltics of encodings in logical frameworkswhere equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. Two morphisms ina category are Leibniz equal if they are seen so by an internal category. The usualcategorical properties are then relativized to r-properties by requiring mediatingmorphisms to be unique up to some Leibniz equality. Using these terminologies,it is shown, by an example, that the term model of the encoding of an adequatelyrepresented object calculus is r-isomorphic to the term model of the object language.展开更多
This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott'...This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott's algoritbJn for λ∑.The notation of normal forms plays a vital role in higher-order unification.The weak head normal forms in the extended troe theory is defined to reveal the ultimate 'top level structures' of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algoritlun can construct recuxsive functions automatically.展开更多
文摘[Objective] The aim was to conduct post-evaluation on environmental planning by means of logical framework approach. [Method] Taking environmental planning during '11th Five-year Plan' in a certain province for example, by means of logical framework approach (LFA), the post-evaluation on environmental planning was carried out from the aspects of evaluation content, index system, implementation steps, evaluation feedback and input-output analysis of environmental planning. [Result] The post-evaluation on environmental planning by means of LFA achieved expected purpose and various indexes at different stages of environmental planning was assessed, and then corresponding countermeasures were put forward according to the problems which were found by problem tree of environmental planning project. [Conclusion] The study could provide theoretical references for the post-evaluation on environmental planning in future.
文摘The paper discusses semalltics of encodings in logical frameworkswhere equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. Two morphisms ina category are Leibniz equal if they are seen so by an internal category. The usualcategorical properties are then relativized to r-properties by requiring mediatingmorphisms to be unique up to some Leibniz equality. Using these terminologies,it is shown, by an example, that the term model of the encoding of an adequatelyrepresented object calculus is r-isomorphic to the term model of the object language.
文摘This paper presents a method to define a set of mutuaJly recursive inductive types, and develops a higherorder unilication algorithm for Anz extended with inductive types. The algorithm is an extension of Eiliott's algoritbJn for λ∑.The notation of normal forms plays a vital role in higher-order unification.The weak head normal forms in the extended troe theory is defined to reveal the ultimate 'top level structures' of the fully normalized terms and types. Unification transformation rules are designed to deal with inductive types, a recursive operator and its reduction rule. The algoritlun can construct recuxsive functions automatically.
