Related papers: The nature of loops in programming

The nature of loops in programming

URL: http://arxiv.org/abs/2504.08126v1
Date: Thu, 10 Apr 2025 20:58:55 GMT
Title: The nature of loops in programming
Authors: Bertrand Meyer,
Abstract summary: In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments.<n>A single and simple definition is possible, removing this split.<n>To prove the loop correct there is no need to devise an invariant and a variant.<n>It suffices to identify the relation, yielding both partial correctness and termination.
Score: 37.48416208168878
License: http://creativecommons.org/licenses/by/4.0/
Abstract: In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ignoring termination); and a variant, for termination (ignoring functional properties). A single and simple definition is possible, removing this split. A loop is just the limit (a variant of the reflexive transitive closure) of a Noetherian (well-founded) relation. To prove the loop correct there is no need to devise an invariant and a variant; it suffices to identify the relation, yielding both partial correctness and termination. The present note develops the (small) theory and applies it to standard loop examples and proofs of their correctness.

Related papers

Reasoning about concurrent loops and recursion with rely-guarantee rules [0.0]
We present general, mechanically verified, refinement for reasoning about programs and loops.<n>We make use of the lattice-guarantee approach to that facilitates reasoning about interference from concurrent threads.
arXiv Detail & Related papers (2025-12-06T01:57:42Z)
Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
Modern language models (LMs) exhibit strong deductive reasoning capabilities, yet standard evaluations emphasize correctness while overlooking a key aspect of human-like reasoning: efficiency.<n>We propose a framework for assessing LM reasoning efficiency through the lens of logic programming.
arXiv Detail & Related papers (2025-10-29T15:30:31Z)
On systematic construction of correct logic programs [0.0]
This paper presents an approach to systematically construct provably correct and semi-complete logic programs.<n>The proposed method is simple, and can be used (maybe informally) in actual everyday programming.
arXiv Detail & Related papers (2025-08-22T20:27:21Z)
Search-Based Correction of Reasoning Chains for Language Models [72.61861891295302]
Chain-of-Thought (CoT) reasoning has advanced the capabilities and transparency of language models (LMs)<n>We introduce a new self-correction framework that augments each reasoning step in a CoT with a latent variable indicating its veracity.<n>We also introduce Search Corrector, a discrete search algorithm over-valued veracity assignments.
arXiv Detail & Related papers (2025-05-17T04:16:36Z)
Chain-of-Probe: Examining the Necessity and Accuracy of CoT Step-by-Step [81.50681925980135]
We propose a method to probe changes in the mind during the model's reasoning. By analyzing patterns in mind change, we examine the correctness of the model's reasoning. Our validation reveals that many responses, although correct in their final answer, contain errors in their reasoning process.
arXiv Detail & Related papers (2024-06-23T15:50:22Z)
Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
Two lines of approaches are adopted for complex reasoning with LLMs.<n>One line of work prompts LLMs with various reasoning structures, while the structural outputs can be naturally regarded as intermediate reasoning steps.<n>The other line of work adopt LLM-free declarative solvers to do the reasoning task, rendering higher reasoning accuracy but lacking interpretability due to the black-box nature of the solvers.<n>We present a simple extension to the latter line of work. Specifically, we showcase that the intermediate search logs generated by Prolog interpreters can be accessed and interpreted into human-readable reasoning.
arXiv Detail & Related papers (2023-11-16T11:26:21Z)
Invariant Relations: A Bridge from Programs to Equations [1.3342735568824553]
We propose a method to derive the function of a C-like program, including programs that have loops nested to an arbitrary level. To capture the semantics of loops, we use the concept of invariant relation.
arXiv Detail & Related papers (2023-10-07T04:11:23Z)
On Loop Formulas with Variables [2.1955512452222696]
Recently Ferraris, Lee and Lifschitz proposed a new definition of stable models that does not refer to grounding. We show its relation to the idea of loop formulas with variables by Chen, Lin, Wang and Zhang. We extend the syntax of logic programs to allow explicit quantifiers, and define its semantics as a subclass of the new language of stable models.
arXiv Detail & Related papers (2023-07-15T06:20:43Z)
A Circuit Complexity Formulation of Algorithmic Information Theory [1.5483078145498086]
Inspired by Solomonoffs theory of inductive inference, we propose a prior based on circuit complexity. We argue that an inductive bias towards simple explanations as measured by circuit complexity is appropriate for this problem.
arXiv Detail & Related papers (2023-06-25T01:30:37Z)
Will Bilevel Optimizers Benefit from Loops [63.22466953441521]
Two current popular bilevelimats AID-BiO and ITD-BiO naturally involve solving one or two sub-problems. We first establish unified convergence analysis for both AID-BiO and ITD-BiO that are applicable to all implementation choices of loops.
arXiv Detail & Related papers (2022-05-27T20:28:52Z)
Complexity assessments for decidable fragments of Set Theory. III: A quadratic reduction of constraints over nested sets to Boolean formulae [0.0]
A translation is proposed of conjunctions of literals of the forms $x=ysetminus z$, $x neq ysetminus z$, and $z =x$. The formulae in the target language involve variables ranging over a Boolean ring of sets, along with a difference operator and relators designating equality, non-disjointness and inclusion. The proposed translation has quadratic algorithmic time-complexity, and bridges two languages both of which are known to have an NP-complete satisfiability problem.
arXiv Detail & Related papers (2021-12-09T09:36:39Z)
multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
arXiv Detail & Related papers (2021-06-02T17:58:35Z)
GroupifyVAE: from Group-based Definition to VAE-based Unsupervised Representation Disentanglement [91.9003001845855]
VAE-based unsupervised disentanglement can not be achieved without introducing other inductive bias. We address VAE-based unsupervised disentanglement by leveraging the constraints derived from the Group Theory based definition as the non-probabilistic inductive bias. We train 1800 models covering the most prominent VAE-based models on five datasets to verify the effectiveness of our method.
arXiv Detail & Related papers (2021-02-20T09:49:51Z)
Recursive Rules with Aggregation: A Simple Unified Semantics [0.6662800021628273]
This paper describes a unified semantics for recursion with aggregation. We present a formal definition of the semantics, prove important properties of the semantics, and compare with prior semantics. We show that our semantics is simple and matches the desired results in all cases.
arXiv Detail & Related papers (2020-07-26T04:42:44Z)

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