Programming Really Is Simple Mathematics

• URL: http://arxiv.org/abs/2502.17149v3
• Date: Thu, 27 Feb 2025 17:44:11 GMT
• Title: Programming Really Is Simple Mathematics
• Authors: Bertrand Meyer, Reto Weber,
• Abstract summary: This paper is a re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory.<n>It deduces dozens of theorems characterizing important properties of programs and programming.
• Score: 33.351872273350885
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory. Highlights: $\bullet$ Zero axioms. No properties are assumed, all are proved (from standard set theory). $\bullet$ A single concept covers specifications and programs. $\bullet$ Its definition only involves one relation and one set. $\bullet$ Everything proceeds from three operations: choice, composition and restriction. $\bullet$ These techniques suffice to derive the axioms of classic papers on the "laws of programming" as consequences and prove them mechanically. $\bullet$ The ordinary subset operator suffices to define both the notion of program correctness and the concepts of specialization and refinement. $\bullet$ From this basis, the theory deduces dozens of theorems characterizing important properties of programs and programming. $\bullet$ All these theorems have been mechanically verified (using Isabelle/HOL); the proofs are available in a public repository. This paper is a considerable extension and rewrite of an earlier contribution [arXiv:1507.00723]

Related papers

• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  The current state-of-the-art in artificial intelligence is impressive, especially in terms of mastery of language, but not so much in terms of mathematical reasoning. This essay builds on the idea that current deep learning mostly succeeds at system 1 abilities. It takes an information-theoretical posture to ask questions about what constitutes an interesting mathematical statement.
  arXiv  Detail & Related papers  (2024-03-07T15:12:06Z)
• Generalised Kochen-Specker Theorem for Finite Non-Deterministic Outcome Assignments [0.0]
  We show that the Kochen-Specker (KS) theorem rules out hidden variable theories with outcome assignments in the set $0, p, 1-p, 1$ for $p in [0,1/d) cup (1/d, 1/2]$.
  arXiv  Detail & Related papers  (2024-02-14T14:02:37Z)
• Tempered Calculus for ML: Application to Hyperbolic Model Embedding [70.61101116794549]
  Most mathematical distortions used in ML are fundamentally integral in nature. In this paper, we unveil a grounded theory and tools which can help improve these distortions to better cope with ML requirements. We show how to apply it to a problem that has recently gained traction in ML: hyperbolic embeddings with a "cheap" and accurate encoding along the hyperbolic vsean scale.
  arXiv  Detail & Related papers  (2024-02-06T17:21:06Z)
• Hierarchies for Semidefinite Optimization in $\mathcal{C}^\star$-Algebras [0.0]
  This paper presents a way for finite-dimensional relaxations of general cone programs on $mathcalCstar$-algebras. We show that well-known hierarchies for generalized problems like NPA but also Lasserre's hierarchy and to some extend symmetry reductions of generic SDPs.
  arXiv  Detail & Related papers  (2023-09-25T09:01:30Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4's capabilities to solve these problems are unparalleled, achieving an accuracy of 51% with Program-of-Thoughts Prompting. TheoremQA is curated by domain experts containing 800 high-quality questions covering 350 theorems.
  arXiv  Detail & Related papers  (2023-05-21T17:51:35Z)
• Finite mathematics as the most general (fundamental) mathematics [0.0]
  Quantum theory based on a finite ring of characteristic $p$ is more general than standard quantum theory because the latter is a degenerate case of the former in the formal limit $ptoinfty$.
  arXiv  Detail & Related papers  (2022-03-09T18:46:57Z)
• Quantum double aspects of surface code models [77.34726150561087]
  We revisit the Kitaev model for fault tolerant quantum computing on a square lattice with underlying quantum double $D(G)$ symmetry. We show how our constructions generalise to $D(H)$ models based on a finite-dimensional Hopf algebra $H$.
  arXiv  Detail & Related papers  (2021-06-25T17:03:38Z)
• Sequential composition of answer set programs [0.0]
  This paper contributes to the mathematical foundations of logic programming by introducing and studying the sequential composition of answer set programs. In a broader sense, this paper is a first step towards an algebra of answer set programs and in the future we plan to lift the methods of this paper to wider classes of programs.
  arXiv  Detail & Related papers  (2021-04-25T13:27:22Z)
• Discrete Math with Programming: A Principled Approach [0.0]
  It has long been argued that discrete math is better taught with programming. This paper introduces an approach that supports all central concepts of discrete math. Math and logical statements can be expressed precisely at a high level and be executed on a computer.
  arXiv  Detail & Related papers  (2020-11-28T03:41:27Z)
• A Finitist's Manifesto: Do we need to Reformulate the Foundations of Mathematics? [1.384477926572109]
  This essay is a call for practicing mathematicians who have been sleep-walking in their infinitary paradise take heed. Much of mathematics relies upon (i) the "existence" of objects that contain an infinite number of elements, (ii) our ability, "in theory", to compute with an arbitrary level of precision, or (iii) our ability, "in theory", to compute for an arbitrarily large number of time steps.
  arXiv  Detail & Related papers  (2020-09-14T14:44:08Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

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.