* . *
  • About
  • Advertise
  • Privacy & Policy
  • Contact
Sunday, July 27, 2025
Earth-News
  • Home
  • Business
  • Entertainment
    Top 5 entertainment news: Sandeep Reddy Vanga regrets trimming Animal’s runtime by 7-8 minutes, Akshay Ku – Times of India

    Top 5 Entertainment Highlights: Sandeep Reddy Vanga Reveals Why He Trimmed Animal’s Runtime by 7-8 Minutes, Plus Akshay Ku Updates

    Cote de Pablo reveals how Michael Weatherly used his soap opera roots to put her at ease in “NCIS” love scene – yahoo.com

    Cote de Pablo Reveals How Michael Weatherly’s Soap Opera Background Made Their “NCIS” Love Scene Easier

    City of Pelham announces entertainment district plans for former Oak Mountain Amphitheatre site – WVTM

    Pelham Unveils Exciting New Entertainment District Plans for Former Oak Mountain Amphitheatre Site

    Black Box Players presents ‘The Three Musketeers’ – CBS 19 News

    Experience the Adventure: Black Box Players Bring ‘The Three Musketeers’ to Life!

    AP Entertainment SummaryBrief at 1:51 p.m. EDT – Channel 3000

    Entertainment Highlights: Key Updates You Can’t Miss

    ‘Devil Wears Prada 2’ casts Anne Hathaway’s love interest replacing Adrian Grenier’s Nate – Entertainment Weekly

    Devil Wears Prada 2′ Casts New Love Interest for Anne Hathaway, Replacing Adrian Grenier’s Nate

  • General
  • Health
  • News

    Cracking the Code: Why China’s Economic Challenges Aren’t Shaking Markets, Unlike America’s” – Bloomberg

    Trump’s Narrow Window to Spread the Truth About Harris

    Trump’s Narrow Window to Spread the Truth About Harris

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Trending Tags

    • Trump Inauguration
    • United Stated
    • White House
    • Market Stories
    • Election Results
  • Science
  • Sports
  • Technology
    AI’s race in the dark with China – Axios

    The High-Stakes AI Race: Innovation and Competition in the Shadows

    Eagle Unveils Revolutionary X-Ray Technology at Pack Expo

    Validea’s Top Information Technology Stocks Based On Peter Lynch – 7/25/2025 – Nasdaq

    Validea’s Top Information Technology Stocks Based On Peter Lynch – 7/25/2025 – Nasdaq

    WhoFi: New surveillance technology can track people by how they disrupt Wi-Fi signals – Tech Xplore

    WhoFi: New surveillance technology can track people by how they disrupt Wi-Fi signals – Tech Xplore

    Google Cloud Announced as a Key Technology Partner for Odoo Connect 2025 in San Francisco – GlobeNewswire

    Google Cloud Announced as a Key Technology Partner for Odoo Connect 2025 in San Francisco – GlobeNewswire

    Behind the Screens: The Impact of Technology on Real Estate – TRREB

    Behind the Screens: How Technology is Transforming the Future of Real Estate

    Trending Tags

    • Nintendo Switch
    • CES 2017
    • Playstation 4 Pro
    • Mark Zuckerberg
No Result
View All Result
  • Home
  • Business
  • Entertainment
    Top 5 entertainment news: Sandeep Reddy Vanga regrets trimming Animal’s runtime by 7-8 minutes, Akshay Ku – Times of India

    Top 5 Entertainment Highlights: Sandeep Reddy Vanga Reveals Why He Trimmed Animal’s Runtime by 7-8 Minutes, Plus Akshay Ku Updates

    Cote de Pablo reveals how Michael Weatherly used his soap opera roots to put her at ease in “NCIS” love scene – yahoo.com

    Cote de Pablo Reveals How Michael Weatherly’s Soap Opera Background Made Their “NCIS” Love Scene Easier

    City of Pelham announces entertainment district plans for former Oak Mountain Amphitheatre site – WVTM

    Pelham Unveils Exciting New Entertainment District Plans for Former Oak Mountain Amphitheatre Site

    Black Box Players presents ‘The Three Musketeers’ – CBS 19 News

    Experience the Adventure: Black Box Players Bring ‘The Three Musketeers’ to Life!

    AP Entertainment SummaryBrief at 1:51 p.m. EDT – Channel 3000

    Entertainment Highlights: Key Updates You Can’t Miss

    ‘Devil Wears Prada 2’ casts Anne Hathaway’s love interest replacing Adrian Grenier’s Nate – Entertainment Weekly

    Devil Wears Prada 2′ Casts New Love Interest for Anne Hathaway, Replacing Adrian Grenier’s Nate

  • General
  • Health
  • News

    Cracking the Code: Why China’s Economic Challenges Aren’t Shaking Markets, Unlike America’s” – Bloomberg

    Trump’s Narrow Window to Spread the Truth About Harris

    Trump’s Narrow Window to Spread the Truth About Harris

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    Israel-Gaza war live updates: Hamas leader Ismail Haniyeh assassinated in Iran, group says

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    PAP Boss to Niger Delta Youths, Stay Away from the Protest

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Court Restricts Protests In Lagos To Freedom, Peace Park

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Fans React to Jazz Jennings’ Inspiring Weight Loss Journey

    Trending Tags

    • Trump Inauguration
    • United Stated
    • White House
    • Market Stories
    • Election Results
  • Science
  • Sports
  • Technology
    AI’s race in the dark with China – Axios

    The High-Stakes AI Race: Innovation and Competition in the Shadows

    Eagle Unveils Revolutionary X-Ray Technology at Pack Expo

    Validea’s Top Information Technology Stocks Based On Peter Lynch – 7/25/2025 – Nasdaq

    Validea’s Top Information Technology Stocks Based On Peter Lynch – 7/25/2025 – Nasdaq

    WhoFi: New surveillance technology can track people by how they disrupt Wi-Fi signals – Tech Xplore

    WhoFi: New surveillance technology can track people by how they disrupt Wi-Fi signals – Tech Xplore

    Google Cloud Announced as a Key Technology Partner for Odoo Connect 2025 in San Francisco – GlobeNewswire

    Google Cloud Announced as a Key Technology Partner for Odoo Connect 2025 in San Francisco – GlobeNewswire

    Behind the Screens: The Impact of Technology on Real Estate – TRREB

    Behind the Screens: How Technology is Transforming the Future of Real Estate

    Trending Tags

    • Nintendo Switch
    • CES 2017
    • Playstation 4 Pro
    • Mark Zuckerberg
No Result
View All Result
Earth-News
No Result
View All Result
Home Science

The Deep Link Equating Math Proofs and Computer Programs

October 12, 2023
in Science
The Deep Link Equating Math Proofs and Computer Programs
Share on FacebookShare on Twitter

Some scientific discoveries matter because they reveal something new — the double helical structure of DNA, for example, or the existence of black holes. However, some revelations are profound because they show that two old concepts, once thought distinct, are in fact the same. Take James Clerk Maxwell’s equations showing that electricity and magnetism are two aspects of a single phenomenon, or general relativity’s linking of gravity with a curved space-time.

The Curry-Howard correspondence does the same but on a larger scale, linking not just separate concepts within one field, but entire disciplines: computer science and mathematical logic. Also known as the Curry-Howard isomorphism (a term meaning there exists some kind of one-to-one correspondence between two things), it establishes a link between mathematical proofs and computer programs.

Simply stated, the Curry-Howard correspondence posits that two concepts from computer science (types and programs) are equivalent, respectively, to propositions and proofs — concepts from logic.

One ramification of this correspondence is that programming — often seen as a personal craft — is elevated to the idealized level of mathematics. Writing a program is not just “coding,” it becomes an act of proving a theorem. This formalizes the act of programming and provides ways to reason mathematically about the correctness of programs.

The correspondence is named for the two researchers who independently discovered it. In 1934, the mathematician and logician Haskell Curry noticed a similarity between functions in mathematics and the implication relationship in logic, which takes the form of “if-then” statements between two propositions.

Inspired by Curry’s observation, the mathematical logician William Alvin Howard discovered a deeper link between computation and logic in 1969, showing that running a computer program is a lot like simplifying a logical proof. When a computer program runs, each line is “evaluated” to yield a single output. Similarly, in a proof, you start with complex statements that you can simplify (by eliminating redundant steps, for example, or substituting complex expressions with simpler ones) until you arrive at a conclusion — a more condensed and succinct statement derived from many interim statements.

While this description conveys a general sense of the correspondence, to fully understand it we need to learn a bit more about what computer scientists call “type theory.”

Let’s start with a famous paradox: In a village there lives a barber who shaves all the men who do not shave themselves, and only them. Does the barber shave himself? If the answer is yes, then he must not shave himself (because he only shaves men who don’t shave themselves). If the answer is no, then he must shave himself (because he shaves all the men who don’t shave themselves). This is an informal version of a paradox Bertrand Russell discovered while trying to establish the foundations of mathematics using a concept called sets. That is, it’s impossible to define a set that contains all sets that do not contain themselves without encountering contradictions.

To avoid this paradox, Russell showed, we can use “types.” Roughly speaking, these are categories whose specific values are called objects. For example, if there’s a type called “Nat,” meaning natural numbers, its objects are 1, 2, 3, and so on. Researchers typically use a colon to denote the type of an object. The number 7, of integer type, can be written as “7: Integer.” You can have a function that takes an object of type A and spits out an object of type B, or one that combines a pair of objects that were type A and type B into a new type, called “A × B.”

One way to resolve the paradox, therefore, is to put these types into a hierarchy, so they can only contain elements of a “lower level” than themselves. Then a type can’t contain itself, which avoids the self-referentiality that creates the paradox.

In the world of type theory, proving that a statement is true can look different from what we’re used to. If we want to prove that the integer 8 is even, then it’s a matter of showing that 8 is indeed an object of a specific type called “Even,” where the rule for membership is being divisible by 2. After verifying that 8 is divisible by 2, we can conclude that 8 is indeed an “inhabitant” of the type Even.

Curry and Howard showed that types are fundamentally equivalent to logical propositions. When a function “inhabits” a type — that is, when you can successfully define a function that is an object of that type — you’re effectively showing that the corresponding proposition is true. So functions that take an input of type A and give an output of type B, denoted as type A → B, must correspond to an implication: “If A, then B.” For example, take the proposition “If it’s raining, then the ground is wet.” In type theory, this proposition would be modeled by a function with the type “Raining → GroundIsWet.” The different-looking formulations are in fact mathematically the same.

As abstract as that linkage may sound, it has not only changed how practitioners of math and computer science think about their work, but also led to several practical applications in both fields. For computer science, it provides a theoretical foundation for software verification, the process of ensuring the correctness of software. By framing desired behaviors in terms of logical propositions, programmers can mathematically prove that a program behaves as expected. It also provides a strong theoretical foundation for designing more powerful functional programming languages.

And for mathematics, the correspondence has led to the birth of proof assistants, also called interactive theorem provers. These are software tools that aid in constructing formal proofs, such as Coq and Lean. In Coq, each step of the proof is essentially a program, and the proof’s validity is checked with type-checking algorithms. Mathematicians have also been using proof assistants — notably, the Lean theorem prover — to formalize mathematics, which involves representing mathematical concepts, theorems and proofs in a rigorous, computer-verifiable format. That allows the sometimes informal language of mathematics to be checked by computers.

Researchers are still exploring the consequences of this link between math and programming. The original Curry-Howard correspondence fuses programming with a kind of logic called intuitionistic logic, but it turns out that more types of logic could be amenable to such unifications as well.

“What has happened in the century since Curry’s insight is that we keep discovering more and more instances where ‘logical system X corresponds to computational system Y,’” said Michael Clarkson, a computer scientist at Cornell University. Researchers have already connected programming to other types of logic like linear logic, which includes the concept of “resources,” and modal logic, which deals with concepts of possibility and necessity.

And while this correspondence bears Curry’s and Howard’s names, they are by no means the only ones who have discovered it. This attests to the foundational nature of the correspondence: People keep noticing it again and again. “It seems to be no accident that there’s a deep link between computation and logic,” Clarkson said.

>>> Read full article>>>
Copyright for syndicated content belongs to the linked Source : Quanta Magazine – https://www.quantamagazine.org/the-deep-link-equating-math-proofs-and-computer-programs-20231011/

Tags: EquatingProofsscience
Previous Post

Minister, Turkey harps on intelligence sharing

Next Post

Potential Hub for Extraterrestrial Life: Webb Observations of CO2 on Jupiter’s Moon Europa

AI’s race in the dark with China – Axios

The High-Stakes AI Race: Innovation and Competition in the Shadows

July 27, 2025
LeBron James’ future with Lakers beyond 2025-26 certain to generate speculation leading up to training camp – Yahoo Sports

LeBron James’ Lakers Future Beyond 2025-26 Sparks Intense Speculation Ahead of Training Camp

July 27, 2025
Energy landscapes direct the movement preferences of elephants – besjournals

Energy landscapes direct the movement preferences of elephants – besjournals

July 27, 2025
At United Nations Summer Program, Computer Science Student Examines AI Ethics – Georgetown University

At United Nations Summer Program, Computer Science Student Examines AI Ethics – Georgetown University

July 27, 2025
Return of wolves to Yellowstone has led to a surge in aspen trees unseen for 80 years – Live Science

Wolves’ Return to Yellowstone Sparks Unprecedented Aspen Tree Boom After 80 Years

July 27, 2025
‘Bluey’ Is Growing Up: BBC Plots All-Ages Expansion For The Franchise As A Full-Fledged Lifestyle Brand – Cartoon Brew

‘Bluey’ Is Growing Up: BBC Plots All-Ages Expansion For The Franchise As A Full-Fledged Lifestyle Brand – Cartoon Brew

July 27, 2025
Katie Ledecky, Summer McIntosh and a race for the ages at World Swimming Championships – NBC Sports

Katie Ledecky and Summer McIntosh Ignite an Epic Showdown at the World Swimming Championships

July 27, 2025
5 ways Trump has shaped the economy in 6 months – The Hill

5 Game-Changing Ways Trump Transformed the Economy in Just 6 Months

July 27, 2025
Flutter Entertainment Announces Pricing Of $1.272 Bln Of Additional Senior Secured Notes Due 2031 – Nasdaq

Flutter Entertainment Raises $1.27 Billion in Major Senior Secured Notes Offering Due 2031

July 27, 2025
KFF Health Tracking Poll: Public Views on Recent Tax and Budget Legislation – KFF

How the Public Really Feels About the Latest Tax and Budget Changes

July 27, 2025

Categories

Archives

July 2025
MTWTFSS
 123456
78910111213
14151617181920
21222324252627
28293031 
« Jun    
Earth-News.info

The Earth News is an independent English-language daily published Website from all around the World News

Browse by Category

  • Business (20,132)
  • Ecology (741)
  • Economy (765)
  • Entertainment (21,645)
  • General (16,135)
  • Health (9,803)
  • Lifestyle (773)
  • News (22,149)
  • People (767)
  • Politics (774)
  • Science (15,980)
  • Sports (21,263)
  • Technology (15,747)
  • World (748)

Recent News

AI’s race in the dark with China – Axios

The High-Stakes AI Race: Innovation and Competition in the Shadows

July 27, 2025
LeBron James’ future with Lakers beyond 2025-26 certain to generate speculation leading up to training camp – Yahoo Sports

LeBron James’ Lakers Future Beyond 2025-26 Sparks Intense Speculation Ahead of Training Camp

July 27, 2025
  • About
  • Advertise
  • Privacy & Policy
  • Contact

© 2023 earth-news.info

No Result
View All Result

© 2023 earth-news.info

No Result
View All Result

© 2023 earth-news.info

Go to mobile version