We gratefully acknowledge support from
the Simons Foundation and member institutions.

Programming Languages

New submissions

[ total of 7 entries: 1-7 ]
[ showing up to 2000 entries per page: fewer | more ]

New submissions for Tue, 11 Aug 20

[1]  arXiv:2008.03441 [pdf, ps, other]
Title: dxo: A System for Relational Algebra and Differentiation
Subjects: Programming Languages (cs.PL)

We present dxo, a relational system for algebra and differentiation, written in miniKanren. dxo operates over math expressions, represented as s-expressions. dxo supports addition, multiplication, exponentiation, variables (represented as tagged symbols), and natural numbers (represented as little-endian binary lists). We show the full code for dxo, and describe in detail the four main relations that compose dxo. We present example problems dxo can solve by combining the main relations. Our differentiation relation, do, can differentiate polynomials, and by running backwards, can also integrate. Similarly, our simplification relation, simpo, can simplify expressions that include addition, multiplication, exponentiation, variables, and natural numbers, and by running backwards, can complicate any expression in simplified form. Our evaluation relation, evalo, takes the same types of expressions as simpo, along with an environment associating variables with natural numbers. By evaluating the expression with respect to the environment, evalo can produce a natural number; by running backwards, evalo can generate expressions (or the associated environments) that evaluate to a given value. reordero also takes the same types of expressions as simpo, and relates reordered expressions.

[2]  arXiv:2008.03649 [pdf, other]
Title: Code Building Genetic Programming
Comments: Proceedings of the 2020 Genetic and Evolutionary Computation Conference, Genetic Programming Track
Subjects: Programming Languages (cs.PL); Neural and Evolutionary Computing (cs.NE); Software Engineering (cs.SE)

In recent years the field of genetic programming has made significant advances towards automatic programming. Research and development of contemporary program synthesis methods, such as PushGP and Grammar Guided Genetic Programming, can produce programs that solve problems typically assigned in introductory academic settings. These problems focus on a narrow, predetermined set of simple data structures, basic control flow patterns, and primitive, non-overlapping data types (without, for example, inheritance or composite types). Few, if any, genetic programming methods for program synthesis have convincingly demonstrated the capability of synthesizing programs that use arbitrary data types, data structures, and specifications that are drawn from existing codebases. In this paper, we introduce Code Building Genetic Programming (CBGP) as a framework within which this can be done, by leveraging programming language features such as reflection and first-class specifications. CBGP produces a computational graph that can be executed or translated into source code of a host language. To demonstrate the novel capabilities of CBGP, we present results on new benchmarks that use non-primitive, polymorphic data types as well as some standard program synthesis benchmarks.

Cross-lists for Tue, 11 Aug 20

[3]  arXiv:2008.03714 (cross-list from cs.LO) [pdf, ps, other]
Title: The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
Comments: Paper presented at the 36th International Conference on Logic Programming (ICLP 2019), University Of Calabria, Rende (CS), Italy, September 2020, 16 pages
Journal-ref: Theory and Practice of Logic Programming, 2020
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less studied in coinductive extensions of sequent calculi. In this paper, we use coinductive Horn clause theories to show that cut is not eliminable in a coinductive extension of LJ, a system we call CLJ. We derive two further practical results from this study. We show that CoLP by Gupta et al. gives rise to cut-free proofs in CLJ with fixpoint terms, and we formulate and implement a novel method of coinductive theory exploration that provides several heuristics for discovery of cut formulae in CLJ.

[4]  arXiv:2008.03719 (cross-list from cs.DB) [pdf, other]
Title: A Rule-based Language for Application Integration
Comments: 14 pages, work from 2013/14
Subjects: Databases (cs.DB); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

Although message-based (business) application integration is based on orchestrated message flows, current modeling languages exclusively cover (parts of) the control flow, while under-specifying the data flow. Especially for more data-intensive integration scenarios, this fact adds to the inherent data processing weakness in conventional integration systems.
We argue that with a more data-centric integration language and a relational logic based implementation of integration semantics, optimizations from the data management domain(e.g., data partitioning, parallelization) can be combined with common integration processing (e.g., scatter/gather, splitter/gather). With the Logic Integration Language (LiLa) we redefine integration logic tailored for data-intensive processing and propose a novel approach to data-centric integration modeling, from which we derive the control-and data flow and apply them to a conventional integration system.

[5]  arXiv:2008.04133 (cross-list from cs.AI) [pdf, other]
Title: Robot Action Selection Learning via Layered Dimension Informed Program Synthesis
Subjects: Artificial Intelligence (cs.AI); Programming Languages (cs.PL); Robotics (cs.RO)

Action selection policies (ASPs), used to compose low-level robot skills into complex high-level tasks are commonly represented as neural networks (NNs) in the state of the art. Such a paradigm, while very effective, suffers from a few key problems: 1) NNs are opaque to the user and hence not amenable to verification, 2) they require significant amounts of training data, and 3) they are hard to repair when the domain changes. We present two key insights about ASPs for robotics. First, ASPs need to reason about physically meaningful quantities derived from the state of the world, and second, there exists a layered structure for composing these policies. Leveraging these insights, we introduce layered dimension-informed program synthesis (LDIPS) - by reasoning about the physical dimensions of state variables, and dimensional constraints on operators, LDIPS directly synthesizes ASPs in a human-interpretable domain-specific language that is amenable to program repair. We present empirical results to demonstrate that LDIPS 1) can synthesize effective ASPs for robot soccer and autonomous driving domains, 2) requires two orders of magnitude fewer training examples than a comparable NN representation, and 3) can repair the synthesized ASPs with only a small number of corrections when transferring from simulation to real robots.

[6]  arXiv:2008.04165 (cross-list from cs.LO) [pdf, ps, other]
Title: Proof-Carrying Plans: a Resource Logic for AI Planning
Comments: PPDP 2020, 13 pages, 9 figures
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Programming Languages (cs.PL)

Recent trends in AI verification and Explainable AI have raised the question of whether AI planning techniques can be verified. In this paper, we present a novel resource logic, the Proof Carrying Plans (PCP) logic that can be used to verify plans produced by AI planners. The PCP logic takes inspiration from existing resource logics (such as Linear logic and Separation logic) as well as Hoare logic when it comes to modelling states and resource-aware plan execution. It also capitalises on the Curry-Howard approach to logics, in its treatment of plans as functions and plan pre- and post-conditions as types. This paper presents two main results. From the theoretical perspective, we show that the PCP logic is sound relative to the standard possible world semantics used in AI planning. From the practical perspective, we present a complete Agda formalisation of the PCP logic and of its soundness proof. Moreover, we showcase the Curry-Howard, or functional, value of this implementation by supplementing it with the library that parses AI plans into Agda's proofs automatically. We provide evaluation of this library and the resulting Agda functions.

Replacements for Tue, 11 Aug 20

[7]  arXiv:1901.06540 (replaced) [pdf, other]
Title: A Pre-Expectation Calculus for Probabilistic Sensitivity
Comments: Major revision
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
[ total of 7 entries: 1-7 ]
[ showing up to 2000 entries per page: fewer | more ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, recent, 2008, contact, help  (Access key information)