A limited form of dependent types, called Generalized Algebraic Data Types (GADTs), has recently been added to the list of Haskell extensions supported by the Glasgow Haskell Compiler. Despite not being full-fledged d...
详细信息
ISBN:
(纸本)9781595930644
A limited form of dependent types, called Generalized Algebraic Data Types (GADTs), has recently been added to the list of Haskell extensions supported by the Glasgow Haskell Compiler. Despite not being full-fledged dependent types, GADTs still offer considerably enlarged scope for enforcing important code and data invariants statically. Moreover, GADTs offer the tantalizing possibility of writing more efficient programs since capturing invariants statically through the type system sometimes obviates entire layers of dynamic tests and associated data markup. this paper is a case study on the applications of GADTs in the context of Yampa, a domain-specific language for functional Reactive programming in the form of a self-optimizing, arrow-based Haskell combinator library. the paper has two aims. Firstly, to explore what kind of optimizations GADTs make possible in this context. Much of that should also be relevant for other domain-specific embedded language implementations, in particular arrow-based ones. Secondly, as the actual performance impact of the GADT-based optimizations is not obvious, to quantify this impact, both on tailored micro benchmarks, to establish the effectiveness of individual optimizations, and on two fairly large, realistic applications, to gauge the overall impact. the performance gains for the micro benchmarks are substantial. this implies that the Yampa API could be simplified as a number of "pre-composed" primitives that were there mainly for performance reasons are no longer needed. As to the applications, a worthwhile performance gain was obtained in one case whereas the performance was more or less unchanged in the other.
this paper combines work done in the areas of Artificial Intelligence, Multimedia Systems and Coordination programming to derive a framework for Distributed Multimedia Systems based on asynchronous timed computations ...
详细信息
this paper combines work done in the areas of Artificial Intelligence, Multimedia Systems and Coordination programming to derive a framework for Distributed Multimedia Systems based on asynchronous timed computations expressed in a certain coordination formalism. More to the point, we propose the development of multimedia programming frameworks based on the declarative logic programming setting and in particular the framework of object-oriented timed concurrent constraint programming (OO-TCCP). the real-time extensions that have been proposed for the concurrent constraint programming framework are coupled withthe object-oriented and inheritance mechanisms that have been developed for logic programs yielding an integrated declarative environment for multimedia objects modelling, composition and synchronisation. Furthermore, we show how the framework can be implemented in the general-purpose coordination language MANIFOLD without the need for using special architectures or real-time languages. (c) 2004 Elsevier B.V. All rights reserved.
Tuple centres allow for dynamic programming of the coordination media: coordination laws are expressed and enforced as the behaviour specification of tuple centres, and can change over time. Since time is essential in...
详细信息
ISBN:
(纸本)354025630X
Tuple centres allow for dynamic programming of the coordination media: coordination laws are expressed and enforced as the behaviour specification of tuple centres, and can change over time. Since time is essential in a large number of coordination problems and patterns (involving timeouts, obligations, commitments), coordination laws should be expressive enough to capture and govern time-related issues. Along this line, in this paper we discuss how tuple centres and the ReSpecT language for programming logic tuple centres can be extended to catch with time, and to support the definition and enforcement of time-aware coordination policies. Some examples are provided to demonstrate the expressiveness of the ReSpecT language to model timed coordination primitives and laws.
Bunker fuel oil, one of the products of petroleum refining, has a strong impact on the production process because it drives the availability of heavy residues that depend on the crude quality. Based on the uncertainty...
详细信息
ISBN:
(纸本)9974002745
Bunker fuel oil, one of the products of petroleum refining, has a strong impact on the production process because it drives the availability of heavy residues that depend on the crude quality. Based on the uncertainty of its demand, a stochastic model is proposed, where the benefit of the production is optimized, taking decision on the more suitable raw material, intermediate products and its final blend in order to fulfill the quality and demand requirements of final products. three different crude qualities are supposed to be available for the first stage decision and their prices include an estimation of the storage cost for different scenarios. the optimum implies the most expensive quality to be bought due to a lack of incentive in the production of extra amounts of fuel oil at a non attractive price. Results are compared withthe solution of a deterministic model with mean demand. In spite of being more complex than the deterministic model, the stochastic model solution's shows how the refinery should operate for each scenario of bunker fuel oil demand. Relative value between raw material and products, storage cost and some constraints in the demand have strong impact in the solution. Finally, a first approach to a procedure for building a stochastic model for linear programming packages, of common use in the refining industry, is exposed.
A new impulse detector design method for image impulse noise is presented. Robust statistics of local pixel neighborhood present features in a binary classification scheme. Classifier is developed through the evolutio...
详细信息
ISBN:
(纸本)354029032X
A new impulse detector design method for image impulse noise is presented. Robust statistics of local pixel neighborhood present features in a binary classification scheme. Classifier is developed through the evolutionary process realized by genetic programming. the proposed filter shows very good results in suppressing both fixed-valued and random-valued impulse noise, for any noise probability, and on all test images.
Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. this paper further develops the monadic programming paradigm by investigati...
详细信息
ISBN:
(纸本)9781595930644
Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. this paper further develops the monadic programming paradigm by investigating the extent to which monadic computations can be optimised by using generalisations of short cut fusion to eliminate monadic structures whose sole purpose is to "glue together" monadic program components. We make several contributions. First, we show that every inductive type has an associated build combinator and an associated short cut fusion rule. Second, we introduce the notion of an inductive monad to describe those monads that give rise to inductive types, and we give examples of such monads which are widely used in functionalprogramming. third, we generalise the standard augment combinators and cata/augment fusion rules for algebraic data types to types induced by inductive monads. this allows us to give the first cata/augment rules for some common data types, such as rose trees. Fourth, we demonstrate the practical applicability of our generalisations by providing Haskell implementations for all concepts and examples in the paper. Finally, we offer deep theoretical insights by showing that the augment combinators are monadic in nature, and thus that our cata/build and cata/augment rules are arguably the best generally applicable fusion rules obtainable.
In this paper, we propose a group-oriented management or key trees. Traditional approach to manage key tress such as TGDH cannot retain characteristics of subgroups and it costs a great quantity of exponentiation comp...
详细信息
ISBN:
(纸本)8955191235
In this paper, we propose a group-oriented management or key trees. Traditional approach to manage key tress such as TGDH cannot retain characteristics of subgroups and it costs a great quantity of exponentiation computation to calculate the group key due to its algorithm. By means of group-oriented management of key trees, we reduce the cost of re-keying and the message size that is consultation to evaluate performance of key trees. therefore, our Approach applied to group key management not only performs well but also supplies members with more information.
We show that the standard normalization-by-evaluation construction for the simply-typed lambda(beta eta)-calculus has a natural counterpart for the untyped lambda(beta)-calculus, withthe central type-indexed logical ...
详细信息
We show that the standard normalization-by-evaluation construction for the simply-typed lambda(beta eta)-calculus has a natural counterpart for the untyped lambda(beta)-calculus, withthe central type-indexed logical relation replaced by a "recursively defined" invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation. In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of soundness (the output term, if any, is in normal form and beta-equivalent to the input term);identification (beta-equivalent terms are mapped to the same result);and completeness (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like, call-by-value language. Finally, we generalize the construction to produce an infinitary variant of normal forms, namely Bohm trees. We show that the three-part characterization of correctness, as well as the proofs, extend naturally to this generalization.
An untyped algorithm to test beta eta-equality for Martin-Lof's Logical Framework with strong Sigma-types is presented and proven complete using a model of partial equivalence relations between untyped terms.
ISBN:
(数字)9783540320142
ISBN:
(纸本)3540255931
An untyped algorithm to test beta eta-equality for Martin-Lof's Logical Framework with strong Sigma-types is presented and proven complete using a model of partial equivalence relations between untyped terms.
Advanced techniques in separation of concerns such as Aspect-Oriented programming, help to develop more maintainable and more efficient applications by providing means for modularizing crosscutting concerns. However, ...
详细信息
ISBN:
(纸本)3540261818
Advanced techniques in separation of concerns such as Aspect-Oriented programming, help to develop more maintainable and more efficient applications by providing means for modularizing crosscutting concerns. However, conflicts may appear when several concerns need to be composed for the same application, especially when dealing with around advice. We call this problem the Aspect Composition Issue (ACI). Based on our experience in programming aspects, this paper presents a language called CompAr, which allows the programmer to abstractly define an execution domain, the advice codes, and their execution constraints. the CompAr compiler then evaluates the definitions in order to check if the execution constraints are fulfilled. Using a concrete AOP case study, we show how to use the CompAr language in order to detect and avoid ACIs.
暂无评论