Three computational models and its equivalence

• URL: http://arxiv.org/abs/2010.15600v1
• Date: Mon, 26 Oct 2020 05:55:19 GMT
• Title: Three computational models and its equivalence
• Authors: Ciro Ivan Garcia Lopez
• Abstract summary: The study of computability has its origin in Hilbert's conference of 1900, where an adjacent question, is to give a precise description of the notion of algorithm. We intend to fill this gap presenting the proof in a modern way, without forgetting the mathematical details.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: The study of computability has its origin in Hilbert's conference of 1900, where an adjacent question, to the ones he asked, is to give a precise description of the notion of algorithm. In the search for a good definition arose three independent theories: Turing and the Turing machines, G\"odel and the recursive functions, Church and the Lambda Calculus. Later there were established by Kleene that the classic models of computation are equivalent. This fact is widely accepted by many textbooks and the proof is omitted since the proof is tedious and unreadable. We intend to fill this gap presenting the proof in a modern way, without forgetting the mathematical details.

Related papers

• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  Minimo is an agent that learns to pose problems for itself (conjecturing) and solve them (theorem proving) We combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our agent targets generating hard but provable conjectures - a moving target, since its own theorem proving ability also improves as it trains.
  arXiv  Detail & Related papers  (2024-06-30T13:34:54Z)
• 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)
• Connecting classical finite exchangeability to quantum theory [69.62715388742298]
  Exchangeability is a fundamental concept in probability theory and statistics. We show how a de Finetti-like representation theorem for finitely exchangeable sequences requires a mathematical representation which is formally equivalent to quantum theory.
  arXiv  Detail & Related papers  (2023-06-06T17:15:19Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3. We report baseline results on statement autoformalization via in-context learning.
  arXiv  Detail & Related papers  (2023-02-24T03:28:46Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  We explore the abilities of a large language model (Codex) to help with formalisation in the Lean theorem prover. Codex is able to formalise short mathematical statements at undergrad level with nearly 75% accuracy for $120$ theorem statements. We show that with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof.
  arXiv  Detail & Related papers  (2022-11-14T16:52:32Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  Theorem proving in natural mathematical language plays a central role in mathematical advances and education. We develop NaturalProver, a language model that generates proofs by conditioning on background references. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
  arXiv  Detail & Related papers  (2022-05-25T17:01:18Z)
• Proofs of network quantum nonlocality aided by machine learning [68.8204255655161]
  We show that the family of quantum triangle distributions of [DOI40103/PhysRevLett.123.140] did not admit triangle-local models in a larger range than the original proof. We produce a large collection of network Bell inequalities for the triangle scenario with binary outcomes, which are of independent interest.
  arXiv  Detail & Related papers  (2022-03-30T18:00:00Z)
• 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)
• Gull's theorem revisited [0.0]
  Gull's philosophy is that Bell's theorem can be seen as a no-go theorem for a project in distributed computing. We present his argument, correcting misprints and filling gaps.
  arXiv  Detail & Related papers  (2020-12-01T18:29:13Z)
• 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.