Industrial computing devices, in particular cyber-physical, real-time and safety-critical systems, focus on reacting to external events and the need to cooperate with other devices to create a functional system. They ...
详细信息
ISBN:
(纸本)9781538640432
Industrial computing devices, in particular cyber-physical, real-time and safety-critical systems, focus on reacting to external events and the need to cooperate with other devices to create a functional system. They are often implemented with languages that focus on a simple, local description of how a component reacts to external input data and stimuli. Despite the trend in modern software architectures to structure systems into largely independent components, the remaining interdependencies still create rich behavioural dynamics even for small systems. Standard and industrial programming approaches do usually not model or extensively describe the global properties of an entire system. Although a large number of approaches to solve this dilemma have been suggested, it remains a hard and error-prone task to implement systems with complex interdependencies correctly. We introduce multiple coupled finite state machines (McFSMs), a novel mechanism that allows us to model and manage such interdependencies. It is based on a consistent, well-structured and simple global description. A sound theoretical foundation is provided, and associated tools allow us to generate efficient low-level code in various programming languages using model-driven techniques. We also present a domain specific language to express McFSMs and their connections to other systems, to model their dynamic behaviour, and to investigate their efficiency and correctness at compile-time.
The structured approach to argumentation has seen a surge of models, introducing a multitude of ways to deal with the formalisation of arguments. However, while the development of the mathematical models have flourish...
详细信息
ISBN:
(纸本)9783939897637
The structured approach to argumentation has seen a surge of models, introducing a multitude of ways to deal with the formalisation of arguments. However, while the development of the mathematical models have flourished, the actual implementations and development of methods for implementation of these models have been lagging behind. This paper attempts to alleviate this problem by providing methods that simplify implementation, i.e. we demonstrate how the functionalprogramming language Haskell can naturally express mathematical definitions and sketch how a theorem prover can verify this implementation. Furthermore, we provide methods to streamline the documenting of code, showing how literate programming allows the implementer to write formal definition, implementation and documentation in one file. All code has been made publicly available and reusable.
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming l...
详细信息
ISBN:
(纸本)9781450302555
This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functionalprogramming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double-Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).
Using a bijection between natural numbers and hereditarily finite functions we derive a new reversible variable length self-delimiting code through a bitstring representation in a balanced parenthesis language. The co...
详细信息
ISBN:
(纸本)9781450302555
Using a bijection between natural numbers and hereditarily finite functions we derive a new reversible variable length self-delimiting code through a bitstring representation in a balanced parenthesis language. The code features the ability to encode arbitrarily nested data types, can represent huge (low "complexity") numbers, and is decodable from its beginning or its end. Besides its possible practical applications to media stream encodings, a comparison with the well-known Elias omega code and a conjecture about its asymptotic: behavior under the Kraft inequality suggest it as an interesting object of study for experimental mathematicians. The paper is organized as a self-contained literate Haskell program inviting the reader to explore its content independently. Its code is available at http://***/tarau/research/2010/***.
The proceedings contain 5 papers. The topics discussed include: hereditary substitutions for simple types, formalized;hereditarily finite representations of natural numbers and self-delimiting codes;foundational progr...
ISBN:
(纸本)9781450302555
The proceedings contain 5 papers. The topics discussed include: hereditary substitutions for simple types, formalized;hereditarily finite representations of natural numbers and self-delimiting codes;foundational program verification in Coq with automated proofs;type inference in context;and arrows are strong monads.
When learning from very large databases, the reduction of complexity is extremely important. Two extremes of making knowledge discovery in databases (KDD) feasible have been put forward. One extreme is to choose a ver...
详细信息
When learning from very large databases, the reduction of complexity is extremely important. Two extremes of making knowledge discovery in databases (KDD) feasible have been put forward. One extreme is to choose a very simple hypothesis language, thereby being capable of very fast learning on real-world databases. The opposite extreme is to select a small data set, thereby being able to learn very expressive (first-order logic) hypotheses. A multistrategy approach allows one to include most of these advantages and exclude most of the disadvantages. Simpler learning algorithms detect hierarchies which are used to structure the hypothesis space for a more complex learning algorithm. The better structured the hypothesis space is, the better learning can prune away uninteresting or losing hypotheses and the faster it becomes. We have combined inductive logic programming (ILP) directly with a relational database management system. The ILP algorithm is controlled in a model-driven way by the user and in a data-driven way by structures that are induced by three simple learning algorithms.
This paper presents an algebraic and categorical approach to the mathematical modeling of imperative programming languages. In particular we model languages with block structure, records and variants, user definable r...
详细信息
暂无评论