Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g.,...
详细信息
ISBN:
(纸本)9781450367127
Concurrent and distributed programming is notoriously hard. Modern languages and toolkits ease this difficulty by offering message-passing abstractions, such as actors (e.g., Erlang, Akka, Orleans) or processes (e.g., Go): they allow for simpler reasoning w.r.t. shared-memory concurrency, but do not ensure that a program implements a given specification. To address this challenge, it would be desirable to specify and verify the intended behaviour of message-passing applications using types, and ensure that, if a program type-checks and compiles, then it will run and communicate as desired. We develop this idea in theory and practice. We formalise a concurrent functional language lambda(pi)(<=), with a new blend of behavioural types (from pi-calculus theory), and dependent function types (from the Dotty programming language, a.k.a. the future Scala 3). Our theory yields four main payoffs: (1) it verifies safety and liveness properties of programs via types-level model checking;(2) unlike previous work, it accurately verifies channel-passing (covering a typical pattern of actor programs) and higher-order interaction (i.e., sending/receiving mobile code);(3) it is directly embedded in Dotty, as a toolkit called Effpi, offering a simplified actor-based API;(4) it enables an efficient runtime system for Effpi, for highly concurrent programs with millions of processes/actors.
This paper presents an early version of a decision-making "eco" system. We refer to it as an "eco" system because it is primarily based on mathematical logic and combines concepts and principles fr...
详细信息
ISBN:
(纸本)9783030113940;9783030113957
This paper presents an early version of a decision-making "eco" system. We refer to it as an "eco" system because it is primarily based on mathematical logic and combines concepts and principles from the fields of statistics, decision theory, artificial intelligence and modeling of human behavior. The primary goal of the proposed approach is to address errors that occur resulting from the misuse of statistical methods. In practice, such errors often occur either owning to the use of inappropriate statistical methods or wrong interpretations of results. The proposed approach relies on the LPwNF (logicprogramming without Negation as Failure) framework of non-monotonic reasoning as provided by Gorgias. The proposed system enables automatic selection of the appropriate statistical method, based on the characteristics of the problem and the sample. The expected impact could be twofold: it can enhance the use of statistical systems like R and, combined with a Java-based interface to Gorgias, make non-monotonic reasoning easy to use in the proposed context.
logic underlies many fundamental techniques in computer science. It helps us to rigorously formalize these techniques and prove them correct. The last decade has witnessed a growing interest in the use of computationa...
logic underlies many fundamental techniques in computer science. It helps us to rigorously formalize these techniques and prove them correct. The last decade has witnessed a growing interest in the use of computational logic methods for program verification. It has attracted researchers from both computational logic and program verification communities, giving rise to a fruitful exchange of ideas and experiences.
Declarative languages offer unprecedented opportunities for the use of parallelism to speed up execution. A declarative language, being not procedural, removes the need to perform operations in a strict order and redu...
Declarative languages offer unprecedented opportunities for the use of parallelism to speed up execution. A declarative language, being not procedural, removes the need to perform operations in a strict order and reduces the number of dependencies among operations, thus opening the doors for concurrent execution. The potential for transparent exploitation of parallelism in logicprogramming emerged almost immediately with the birth of the paradigm (Pollard 1981).
We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the...
详细信息
We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Sigma(1) level of the Mints hierarchy in first-order intuitionistic logic. It follows that Sigma(1) formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in theory and practice of logic programming.
Techniques for the generation of constrained and optimized geometry play a key role in the automated design of ships, particularly in the early stages. So called "form parameter design" systems are state-of-...
详细信息
ISBN:
(纸本)9783030219208;9783030219192
Techniques for the generation of constrained and optimized geometry play a key role in the automated design of ships, particularly in the early stages. So called "form parameter design" systems are state-of-the-art for such ship hull geometry generation tasks. These systems solve a sequence of constrained nonlinear optimization problems to generate ship hull form geometry which conforms to constraints (form parameters). With such a system, a human expert, or search algorithm capable of discarding infeasible designs, is needed to pick constraint combinations that are at once feasible and also result in a high quality design. Simply finding a feasible set of form parameters is non-trivial enough that form parameter design of ship hulls has remained mostly an academic practice. Commercial tools exist, but their uptake by industry has been slow because this issue has given such tools a reputation for being hard to use. In this paper a modified approach for hull shape generation is proposed, combining form parameter design with interval constraint logicprogramming. We use a constraint solver to pre-process the design space, ensuring all constraints are feasible. This ensures that the form parameter design tool always operates within the feasible sub-domain of the total design space. The new approach is briefly described. Its effectiveness is demonstrated by using a random number generator together with the constraint solver to generate feasible design candidates, and then valid ship hull geometry is generated by our form parameter design program.
A quantum annealer exploits quantum effects to solve a particular type of optimization problem. The advantage of this specialized hardware is that it effectively considers all possible solutions in parallel, thereby p...
详细信息
A quantum annealer exploits quantum effects to solve a particular type of optimization problem. The advantage of this specialized hardware is that it effectively considers all possible solutions in parallel, thereby potentially outperforming classical computing systems. However, despite quantum annealers having recently become commercially available, there are relatively few high-level programming models that target these devices. In this article, we show how to compile a subset of Prolog enhanced with support for constraint logicprogramming into a two-local Ising-model Hamiltonian suitable for execution on a quantum annealer. In particular, we describe the series of transformations one can apply to convert constraint logic programs expressed in Prolog into an executable form that bears virtually no resemblance to a classical machine model yet that evaluates the specified constraints in a fully parallel manner. We evaluate our efforts on a 1,095-qubit D-Wave 2X quantum annealer and describe the approach's associated capabilities and shortcomings.
A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques au...
详细信息
A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques automating this labour-intensive process. A prominent example is the successful use of randomness, in particular, random typable lambda-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable lambda-terms, no effective uniform sampling method is known, setting it as a fundamental open problem in the random software testing approach. In this paper, we combine the framework of Boltzmann samplers, a powerful technique of random combinatorial structure generation, with today's Prolog systems offering a synergy between logic variables, unification with occurs check and efficient backtracking. This allows us to develop a novel sampling mechanism able to construct uniformly random closed simply typed lambda-terms of up size 120. We apply our techniques to the generation of uniformly random closed simply typed normal forms and design a parallel execution mechanism pushing forward the achievable term size to 140.
We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic funct...
详细信息
We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs.
In this paper, we introduce an alternative approach to Temporal Answer Set programming that relies on a variation of Temporal Equilibrium logic (TEL) for finite traces. This approach allows us to even out the expressi...
In this paper, we introduce an alternative approach to Temporal Answer Set programming that relies on a variation of Temporal Equilibrium logic (TEL) for finite traces. This approach allows us to even out the expressiveness of TEL over infinite traces with the computational capacity of (incremental) Answer Set programming (ASP). Also, we argue that finite traces are more natural when reasoning about action and change. As a result, our approach is readily implementable via multi-shot ASP systems and benefits from an extension of ASP's full-fledged input language with temporal operators. This includes future as well as past operators whose combination offers a rich temporal modeling language. For computation, we identify the class of temporal logic programs and prove that it constitutes a normal form for our approach. Finally, we outline two implementations, a generic one and an extension of the ASP system clingo. Under consideration for publication in theory and practice of logic programming (TPLP)
暂无评论