scholarly journals Resourceful Program Synthesis from Graded Linear Types

2021 ◽  
pp. 151-170
Author(s):  
Jack Hughes ◽  
Dominic Orchard
Keyword(s):  
Resource Constraints ◽  
Program Synthesis ◽  
Search Space ◽  
Linear Type ◽  
Synthesis Algorithm ◽  
Implementation Challenges ◽  
Fine Grained ◽  
Linear Types ◽  
Additional Constraints ◽  
Modal Types

AbstractLinear types provide a way to constrain programs by specifying that some values must be used exactly once. Recent work on graded modal types augments and refines this notion, enabling fine-grained, quantitative specification of data use in programs. The information provided by graded modal types appears to be useful for type-directed program synthesis, where these additional constraints can be used to prune the search space of candidate programs. We explore one of the major implementation challenges of a synthesis algorithm in this setting: how does the synthesis algorithm efficiently ensure that resource constraints are satisfied throughout program generation? We provide two solutions to this resource management problem, adapting Hodas and Miller’s input-output model of linear context management to a graded modal linear type theory. We evaluate the performance of both approaches via their implementation as a program synthesis tool for the programming language Granule, which provides linear and graded modal typing.

scholarly journals Gauss: program synthesis by reasoning over graphs

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Rohan Bavishi ◽  
Caroline Lemieux ◽  
Koushik Sen ◽  
Ion Stoica
Keyword(s):  
State Of The Art ◽  
Program Synthesis ◽  
Search Space ◽  
Input Output ◽  
Natural Form ◽  
Synthesis Algorithm ◽  
User Intent ◽  
Speed Up ◽  
Available Information ◽  
Reasoning Algorithm

While input-output examples are a natural form of specification for program synthesis engines, they can be imprecise for domains such as table transformations. In this paper, we investigate how extracting readily-available information about the user intent behind these input-output examples helps speed up synthesis and reduce overfitting. We present Gauss, a synthesis algorithm for table transformations that accepts partial input-output examples, along with user intent graphs. Gauss includes a novel conflict-resolution reasoning algorithm over graphs that enables it to learn from mistakes made during the search and use that knowledge to explore the space of programs even faster. It also ensures the final program is consistent with the user intent specification, reducing overfitting. We implement Gauss for the domain of table transformations (supporting Pandas and R), and compare it to three state-of-the-art synthesizers accepting only input-output examples. We find that it is able to reduce the search space by 56×, 73× and 664× on average, resulting in 7×, 26× and 7× speedups in synthesis times on average, respectively.

Placement of Digital Microfluidic Biochips via a New Evolutionary Algorithm

2021 ◽  
Vol 26 (6) ◽  
pp. 1-22
Author(s):  
Chen Jiang ◽  
Bo Yuan ◽  
Tsung-Yi Ho ◽  
Xin Yao
Keyword(s):  
Evolutionary Algorithm ◽  
Resource Constraints ◽  
Scheduling Algorithm ◽  
Search Space ◽  
Placement Problem ◽  
Heuristic Scheduling ◽  
Microfluidic Biochips ◽  
Feasible Solutions ◽  
Digital Microfluidic ◽  
Operation Scheduling

Digital microfluidic biochips (DMFBs) have been a revolutionary platform for automating and miniaturizing laboratory procedures with the advantages of flexibility and reconfigurability. The placement problem is one of the most challenging issues in the design automation of DMFBs. It contains three interacting NP-hard sub-problems: resource binding, operation scheduling, and module placement. Besides, during the optimization of placement, complex constraints must be satisfied to guarantee feasible solutions, such as precedence constraints, storage constraints, and resource constraints. In this article, a new placement method for DMFB is proposed based on an evolutionary algorithm with novel heuristic-based decoding strategies for both operation scheduling and module placement. Specifically, instead of using the previous list scheduler and path scheduler for decoding operation scheduling chromosomes, we introduce a new heuristic scheduling algorithm (called order scheduler) with fewer limitations on the search space for operation scheduling solutions. Besides, a new 3D placer that combines both scheduling and placement is proposed where the usage of the microfluidic array over time in the chip is recorded flexibly, which is able to represent more feasible solutions for module placement. Compared with the state-of-the-art placement methods (T-tree and 3D-DDM), the experimental results demonstrate the superiority of the proposed method based on several real-world bioassay benchmarks. The proposed method can find the optimal results with the minimum assay completion time for all test cases.

scholarly journals A fine-grained arc-consistency algorithm for non-normalized constraint satisfaction problems

2011 ◽  
Vol 21 (4) ◽  
pp. 733-744 ◽  
Author(s):  
Marlene Arangú ◽  
Miguel Salido
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Programming ◽  
Real Life ◽  
Search Space ◽  
Constraint Satisfaction Problems ◽  
Fine Grained ◽  
Arc Consistency ◽  
Life Problems ◽  
Programming Techniques ◽  
Np Complete

A fine-grained arc-consistency algorithm for non-normalized constraint satisfaction problems Constraint programming is a powerful software technology for solving numerous real-life problems. Many of these problems can be modeled as Constraint Satisfaction Problems (CSPs) and solved using constraint programming techniques. However, solving a CSP is NP-complete so filtering techniques to reduce the search space are still necessary. Arc-consistency algorithms are widely used to prune the search space. The concept of arc-consistency is bidirectional, i.e., it must be ensured in both directions of the constraint (direct and inverse constraints). Two of the most well-known and frequently used arc-consistency algorithms for filtering CSPs are AC3 and AC4. These algorithms repeatedly carry out revisions and require support checks for identifying and deleting all unsupported values from the domains. Nevertheless, many revisions are ineffective, i.e., they cannot delete any value and consume a lot of checks and time. In this paper, we present AC4-OP, an optimized version of AC4 that manages the binary and non-normalized constraints in only one direction, storing the inverse founded supports for their later evaluation. Thus, it reduces the propagation phase avoiding unnecessary or ineffective checking. The use of AC4-OP reduces the number of constraint checks by 50% while pruning the same search space as AC4. The evaluation section shows the improvement of AC4-OP over AC4, AC6 and AC7 in random and non-normalized instances.

scholarly journals Neuroevolutionary Control for Autonomous Soaring

Aerospace ◽  
2021 ◽  
Vol 8 (9) ◽  
pp. 267
Author(s):  
Eric J. Kim ◽  
Ruben E. Perez
Keyword(s):  
Neural Networks ◽  
Autonomous Vehicles ◽  
Energy Savings ◽  
Search Space ◽  
Small Scale ◽  
Biologically Inspired ◽  
Implementation Challenges ◽  
Naturally Occurring ◽  
Novel Method ◽  
Autonomous Soaring

The energy efficiency and flight endurance of small unmanned aerial vehicles (SUAVs) can be improved through the implementation of autonomous soaring strategies. Biologically inspired flight techniques such as dynamic and thermal soaring offer significant energy savings through the exploitation of naturally occurring wind phenomena for thrustless flight. Recent interest in the application of artificial intelligence algorithms for autonomous soaring has been motivated by the pursuit of instilling generalized behavior in control systems, centered around the use of neural networks. However, the topology of such networks is usually predetermined, restricting the search space of potential solutions, while often resulting in complex neural networks that can pose implementation challenges for the limited hardware onboard small-scale autonomous vehicles. In exploring a novel method of generating neurocontrollers, this paper presents a neural network-based soaring strategy to extend flight times and advance the potential operational capability of SUAVs. In this study, the Neuroevolution of Augmenting Topologies (NEAT) algorithm is used to train efficient and effective neurocontrollers that can control a simulated aircraft along sustained dynamic and thermal soaring trajectories. The proposed approach evolves interpretable neural networks in a way that preserves simplicity while maximizing performance without requiring extensive training datasets. As a result, the combined trajectory planning and aircraft control strategy is suitable for real-time implementation on SUAV platforms.

scholarly journals APIfix: output-oriented program synthesis for combating breaking changes in libraries

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-27
Author(s):  
Xiang Gao ◽  
Arjun Radhakrishna ◽  
Gustavo Soares ◽  
Ridwan Shariffdeen ◽  
Sumit Gulwani ◽  
...  
Keyword(s):  
Program Synthesis ◽  
Application Programming Interface ◽  
Third Party ◽  
Security Vulnerabilities ◽  
Synthesis Algorithm ◽  
Transformation Rules ◽  
Art Program ◽  
Application Programming ◽  
Api Usage ◽  
Programming Interface

Use of third-party libraries is extremely common in application software. The libraries evolve to accommodate new features or mitigate security vulnerabilities, thereby breaking the Application Programming Interface(API) used by the software. Such breaking changes in the libraries may discourage client code from using the new library versions thereby keeping the application vulnerable and not up-to-date. We propose a novel output-oriented program synthesis algorithm to automate API usage adaptations via program transformation. Our aim is not only to rely on the few example human adaptations of the clients from the old library version to the new library version, since this can lead to over-fitting transformation rules. Instead, we also rely on example usages of the new updated library in clients, which provide valuable context for synthesizing and applying the transformation rules. Our tool APIFix provides an automated mechanism to transform application code using the old library versions to code using the new library versions - thereby achieving automated API usage adaptation to fix the effect of breaking changes. Our evaluation shows that the transformation rules inferred by APIFix achieve 98.7% precision and 91.5% recall. By comparing our approach to state-of-the-art program synthesis approaches, we show that our approach significantly reduces over-fitting while synthesizing transformation rules for API usage adaptations.

Optimisation of Assembly Line Balancing Type-E with Resource Constraints Using NSGA-II

2016 ◽  
Vol 701 ◽  
pp. 195-199 ◽  
Author(s):  
Masitah Jusop ◽  
Mohd Fadzil Faisae Ab Rashid
Keyword(s):  
Genetic Algorithm ◽  
Assembly Line ◽  
Resource Constraints ◽  
Hybrid Genetic Algorithm ◽  
Assembly Line Balancing ◽  
Search Space ◽  
Line Balancing ◽  
Benchmark Problems ◽  
Nsga Ii ◽  
Multi Objective Genetic Algorithm

Assembly line balancing of Type-E problem (ALB-E) is an attempt to assign the tasks to the various workstations along the line so that the precedence relations are satisfied and some performance measures are optimised. A majority of the recent studies in ALB-E assume that any assembly task can be assigned to any workstation. This assumption lead to higher usage of resource required in assembly line. This research studies assembly line balancing of Type-E problem with resource constraint (ALBE-RC) for a single-model. In this work, three objective functions are considered, i.e. minimise number of workstation, cycle time and number of resources. In this paper, an Elitist Non-dominated Sorting Genetic Algorithm (NSGA-II) has been proposed to optimise the problem. Six benchmark problems have been used to test the optimisation algorithm and the results are compared to multi-objective genetic algorithm (MOGA) and hybrid genetic algorithm (HGA). From the computational test, it was found NSGA-II has the ability to explore search space, has better accuracy of solution and also has a uniformly spaced solution. In future, a research to improve the solution accuracy is proposed to enhance the performance of the algorithm.

scholarly journals Special Issue on Exact and Heuristic Scheduling Algorithms

Algorithms ◽  
2019 ◽  
Vol 13 (1) ◽  
pp. 9 ◽  
Author(s):  
Frank Werner ◽  
Larysa Burtseva ◽  
Yuri N. Sotskov
Keyword(s):  
Resource Constraints ◽  
Lot Sizing ◽  
Scheduling Algorithms ◽  
Traditional Scheduling ◽  
Scheduling Problems ◽  
Special Issue ◽  
Practical Applications ◽  
Heuristic Scheduling ◽  
Additional Constraints

This special issue of Algorithms is a follow-up issue of an earlier one, entitled ‘Algorithms for Scheduling Problems’. In particular, the new issue is devoted to the development of exact and heuristic scheduling algorithms. Submissions were welcome both for traditional scheduling problems as well as for new practical applications. In the Call for Papers, we mentioned topics such as single-criterion and multi-criteria scheduling problems with additional constraints including setup times (costs), precedence constraints, batching (lot sizing), resource constraints as well as scheduling problems arising in emerging applications.

scholarly journals Linear type theory for asynchronous session types

2009 ◽  
Vol 20 (1) ◽  
pp. 19-50 ◽  
Author(s):  
SIMON J. GAY ◽  
VASCO T. VASCONCELOS
Keyword(s):  
Type Theory ◽  
Business Processes ◽  
Operational Semantics ◽  
Synchronous Communication ◽  
Linear Type ◽  
Session Types ◽  
Secure Foundation ◽  
Linear Types ◽  
Session Type ◽  
Functional Setting

AbstractSession types support a type-theoretic formulation of structured patterns of communication, so that the communication behaviour of agents in a distributed system can be verified by static typechecking. Applications include network protocols, business processes and operating system services. In this paper we define a multithreaded functional language with session types, which unifies, simplifies and extends previous work. There are four main contributions. First is an operational semantics with buffered channels, instead of the synchronous communication of previous work. Second, we prove that the session type of a channel gives an upper bound on the necessary size of the buffer. Third, session types are manipulated by means of the standard structures of a linear type theory, rather than by means of new forms of typing judgement. Fourth, a notion of subtyping, including the standard subtyping relation for session types (imported into the functional setting), and a novel form of subtyping between standard and linear function types, which allows the typechecker to handle linear types conveniently. Our new approach significantly simplifies session types in the functional setting, clarifies their essential features and provides a secure foundation for language developments such as polymorphism and object-orientation.

scholarly journals Foundations of the Socio-Physical Model of Activities (SOMA) for Autonomous Robotic Agents1

2021 ◽  
Author(s):  
Daniel Beßler ◽  
Robert Porzel ◽  
Mihai Pomarlan ◽  
Abhijit Vyas ◽  
Sebastian Höffner ◽  
...  
Keyword(s):  
Social Context ◽  
Physical Model ◽  
Search Space ◽  
Human Cognition ◽  
Levels Of Abstraction ◽  
Fine Grained ◽  
Socially Constructed ◽  
Abstract Knowledge ◽  
The Social ◽  
Social Entities

In this paper, we present foundations of the Socio-physical Model of Activities (SOMA). SOMA represents both the physical as well as the social context of everyday activities. Such tasks seem to be trivial for humans, however, they pose severe problems for artificial agents. For starters, a natural language command requesting something will leave many pieces of information necessary for performing the task unspecified. Humans can solve such problems fast as we reduce the search space by recourse to prior knowledge such as a connected collection of plans that describe how certain goals can be achieved at various levels of abstraction. Rather than enumerating fine-grained physical contexts SOMA sets out to include socially constructed knowledge about the functions of actions to achieve a variety of goals or the roles objects can play in a given situation. As the human cognition system is capable of generalizing experiences into abstract knowledge pieces applicable to novel situations, we argue that both physical and social context need be modeled to tackle these challenges in a general manner. The central contribution of this work, therefore, lies in a comprehensive model connecting physical and social entities, that enables flexibility of executions by the robotic agents via symbolic reasoning with the model. This is, by and large, facilitated by the link between the physical and social context in SOMA where relationships are established between occurrences and generalizations of them, which has been demonstrated in several use cases in the domain of everyday activites that validate SOMA.

Sign in / Sign up

Export Citation Format

Share Document