An Expressive Trace Logic for Recursive Programs

• URL: http://arxiv.org/abs/2411.13125v1
• Date: Wed, 20 Nov 2024 08:35:29 GMT
• Title: An Expressive Trace Logic for Recursive Programs
• Authors: Dilian Gurov, Reiner Hähnle,
• Abstract summary: We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics. Our results shed light on the correspondence between programming constructs and logical connectives.
• Score: 0.36832029288386137
• License:
• Abstract: We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives.

Related papers

• Origami: (un)folding the abstraction of recursion schemes for program synthesis [0.0]
  Genetic Programming searches for a correct program that satisfies the input specification. One particular challenge is how to handle loops and recursion avoiding programs that never terminate. Recursion Schemes generalize the combination of data production and consumption.
  arXiv  Detail & Related papers  (2024-02-21T14:17:45Z)
• Hierarchical Programmatic Reinforcement Learning via Learning to Compose Programs [58.94569213396991]
  We propose a hierarchical programmatic reinforcement learning framework to produce program policies. By learning to compose programs, our proposed framework can produce program policies that describe out-of-distributionally complex behaviors. The experimental results in the Karel domain show that our proposed framework outperforms baselines.
  arXiv  Detail & Related papers  (2023-01-30T14:50:46Z)
• A Divide-Align-Conquer Strategy for Program Synthesis [8.595181704811889]
  We show that compositional segmentation can be applied in the programming by examples setting to divide the search for large programs across multiple smaller program synthesis problems. A structural alignment of the constituent parts in the input and output leads to pairwise correspondences used to guide the program search.
  arXiv  Detail & Related papers  (2023-01-08T19:10:55Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  Two programs are equivalent if there exists a sequence of application of rewrite rules that leads to rewriting one program into the other. We propose a neural network architecture based on a transformer model to generate proofs of equivalence between program pairs. Our system, S4Eq, achieves 97% proof success on a curated dataset of 10,000 pairs of equivalent programs.
  arXiv  Detail & Related papers  (2021-09-22T01:37:08Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  We explore the use of consistency between the output programs for related inputs to reduce the impact of spurious programs. We find that a more consistent formalism leads to improved model performance even without consistency-based training.
  arXiv  Detail & Related papers  (2021-07-13T03:48:04Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  We take the first step to synthesize C programs from input-output examples. In particular, we propose La Synth, which learns the latent representation to approximate the execution of partially generated programs. We show that training on these synthesized programs further improves the prediction performance for both Karel and C program synthesis.
  arXiv  Detail & Related papers  (2021-06-29T02:21:32Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• Sequential composition of propositional logic programs [0.0]
  We show that acyclic programs can be decomposed into single-rule programs and provide a general decomposition result for arbitrary programs. We show that the immediate consequence operator of a program can be represented via composition which allows us to compute its least model without any explicit reference to operators.
  arXiv  Detail & Related papers  (2020-09-12T11:57:30Z)
• Process Discovery for Structured Program Synthesis [70.29027202357385]
  A core task in process mining is process discovery which aims to learn an accurate process model from event log data. In this paper, we propose to use (block-) structured programs directly as target process models. We develop a novel bottom-up agglomerative approach to the discovery of such structured program process models.
  arXiv  Detail & Related papers  (2020-08-13T10:33:10Z)
• LogicalFactChecker: Leveraging Logical Operations for Fact Checking with Graph Module Network [111.24773949467567]
  We propose LogicalFactChecker, a neural network approach capable of leveraging logical operations for fact checking. It achieves the state-of-the-art performance on TABFACT, a large-scale, benchmark dataset.
  arXiv  Detail & Related papers  (2020-04-28T17:04:19Z)
• Equivalence of Dataflow Graphs via Rewrite Rules Using a Graph-to-Sequence Neural Model [0.0]
  We formalize the problem of equivalence between two programs as finding a set of semantics-preserving rewrite rules from one into the other. We then develop the first graph-to-sequence neural network system for program equivalence.
  arXiv  Detail & Related papers  (2020-02-17T06:43:00Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.