An Entity of Type: person, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.

Property Value
dbo:abstract
  • La correspondència Curry-Howard (també coneguda com a isomorfisme Curry-Howard o equivalència Curry-Howard o proposicions Curry-Howard) està ubicada en el camp de la teoria del llenguatge de programació i , i estableix una relació directa entre els programes d'ordinador i les proves. Es tracta d'una generalització d'una sintàctica entre els sistemes de la lògica formal i els càlculs de còmput. Va ser descoberta pel matemàtic nord-americà Haskell Curry i el lògic . (ca)
  • Curryho–Howardův isomorfismus je v logice a teorii typů rovnocennost mezi typy a formulemi, resp. jejich důkazy.Logickým objektům (konektivům a konstantám) odpovídají typy takto: Kvantifikátory v logice prvního řádu odpovídají závislostním typům: Pro rovnost se používá zvláštní typ , jehož jedinou hodnotou je Refl. Konkrétní hodnoty jednotlivých typů přímo odpovídají důkazům formulí. (cs)
  • In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs. It is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the American mathematician Haskell Curry and the logician William Alvin Howard. It is the link between logic and computation that is usually attributed to Curry and Howard, although the idea is related to the operational interpretation of intuitionistic logic given in various formulations by L. E. J. Brouwer, Arend Heyting and Andrey Kolmogorov (see Brouwer–Heyting–Kolmogorov interpretation) and Stephen Kleene (see Realizability). The relationship has been extended to include category theory as the three-way Curry–Howard–Lambek correspondence. (en)
  • Als Curry-Howard-Isomorphismus (auch Curry-Howard-Korrespondenz) bezeichnet man die Interpretation von Typen als logische Aussagen und von Termen eines bestimmten Typs als Beweise der zum Typ gehörenden Aussage; und umgekehrt. Benannt ist er nach den Mathematikern Haskell Brooks Curry und William Alvin Howard. (de)
  • En teoría de la demostración y teoría de lenguajes de programación, la correspondencia de Curry-Howard (también llamada isomorfismo de Curry-Howard) es la relación directa que guardan las demostraciones matemáticas con los programas de ordenador. Es una generalización de una analogía sintáctica entre varios sistemas de la lógica formal y varios cálculos computacionales que fue descubierta por primera vez por Haskell Curry y . ​ (es)
  • La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité. Ils établissent des relations entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, lorsque Haskell Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969, quand William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul typé. La correspondance de Curry-Howard a joué un rôle important en logique, car elle a établi un pont entre théorie de la démonstration et informatique théorique. On la retrouve utilisée sous une forme ou une autre dans de très nombreux travaux allant des années 1960 à nos jours : sémantique dénotationnelle, logique linéaire, réalisabilité, démonstration automatique, etc. (fr)
  • カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry–Howard correspondence)とは、と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種()と関係している。 (ja)
  • 논리학에서 커리-하워드 대응(Curry-Howard correspondence) 또는 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 하스켈 커리와 (William Alvin Howard)에 의해 소개된 개념이다. 정확히 말하면 커리-하워드 대응은 논리의 (proof calculus)과 컴퓨터의 형 체계(type system)가 대응된다는 진술이다. 예를 들어 (Hilbert system)와 (combinatory logic)가, 자연 연역과 람다 계산이 대응된다. 본래 컴퓨터는 구성적인 과정만을 수행가능하기 때문에 증명이 온전히 구성적인 직관 논리에 있어서만 성립하는 것으로서 여겨졌으나 최근에 들어서는 고전 논리에서만 성립하는 비구성적인 개념들은 continuation과 대응됨이 알려졌다. (ko)
  • O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e provas matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência provas-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard. (pt)
  • Izomorfizm Curry’ego-Howarda – określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych opartych na logice intuicjonistycznej, takich, jak np. . (pl)
  • Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями. Хаскелл Карри и заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория Клини (1945). Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами. В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные: Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип в простом типизированном лямбда-исчислении соответствует высказыванию логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: , и это значит, что тавтология доказана. Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как Coq, Agda и . (ru)
  • Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями. Хаскелл Каррі і Вільям Говард помітили, що конструктивне доведення (тобто, доведення в інтуїціоністській логіці) схожа на програму, яка обчислює висновок, а саме висловлювання конструктивної логіки за своєю структурою схожі з типами виразів лямбда-числення — програм для обчислювальної машини. Відповідність Каррі — Говарда не обмежується якоюсь однією логікою або системою типів. Наприклад, інтуїционістське числення висловлювань відповідає простому типізованому λ-численню, логіка висловлювань другого порядку — поліморфному λ-численню, числення предикатів — λ-численню з залежними типами. У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні: Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим -обчисленням і фрагментом інтуїціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип в простому типізованому лямбда-численні відповідає вислову логіки висловлювань. Для доказу цього висловлювання необхідно сконструювати терм зазначеного типу (якщо це вдається зробити, то про тип кажуть, що він населений), в даному випадку можна пред'явити потрібний терм:, і це означає, що тавтологія доведена. Використання ізоморфізму Каррі — Говарда дозволило створити цілий клас функціональних мов програмування, середовище виконання яких одночасно є системою автоматичного доказу, таких як Coq, Agda і Epigram (англ.). (uk)
  • 柯里-霍華德对应(英語:Curry-Howard correspondence)是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算(computational calculus)之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德(William Alvin Howard)独立发现的。 (zh)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 254299 (xsd:integer)
dbo:wikiPageLength
  • 56632 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1113758743 (xsd:integer)
dbo:wikiPageWikiLink
dbp:belowstyle
  • text-align: left (en)
dbp:bot
  • InternetArchiveBot (en)
dbp:content
  • A proof of commutativity of addition on natural numbers in the proof assistant Coq. stands for mathematical induction, for substitution of equals, and for taking the same function on both sides of the equality. Earlier theorems are referenced showing and . (en)
  • plus_comm = fun n m : nat => nat_ind n : forall n m : nat, n + m = m + n (en)
dbp:contentstyle
  • text-align: left; (en)
dbp:date
  • October 2022 (en)
dbp:fixAttempted
  • yes (en)
dbp:style
  • width:30em; (en)
dbp:title
  • A proof written as a functional program (en)
dbp:wikiPageUsesTemplate
dcterms:subject
gold:hypernym
rdf:type
rdfs:comment
  • La correspondència Curry-Howard (també coneguda com a isomorfisme Curry-Howard o equivalència Curry-Howard o proposicions Curry-Howard) està ubicada en el camp de la teoria del llenguatge de programació i , i estableix una relació directa entre els programes d'ordinador i les proves. Es tracta d'una generalització d'una sintàctica entre els sistemes de la lògica formal i els càlculs de còmput. Va ser descoberta pel matemàtic nord-americà Haskell Curry i el lògic . (ca)
  • Curryho–Howardův isomorfismus je v logice a teorii typů rovnocennost mezi typy a formulemi, resp. jejich důkazy.Logickým objektům (konektivům a konstantám) odpovídají typy takto: Kvantifikátory v logice prvního řádu odpovídají závislostním typům: Pro rovnost se používá zvláštní typ , jehož jedinou hodnotou je Refl. Konkrétní hodnoty jednotlivých typů přímo odpovídají důkazům formulí. (cs)
  • Als Curry-Howard-Isomorphismus (auch Curry-Howard-Korrespondenz) bezeichnet man die Interpretation von Typen als logische Aussagen und von Termen eines bestimmten Typs als Beweise der zum Typ gehörenden Aussage; und umgekehrt. Benannt ist er nach den Mathematikern Haskell Brooks Curry und William Alvin Howard. (de)
  • En teoría de la demostración y teoría de lenguajes de programación, la correspondencia de Curry-Howard (también llamada isomorfismo de Curry-Howard) es la relación directa que guardan las demostraciones matemáticas con los programas de ordenador. Es una generalización de una analogía sintáctica entre varios sistemas de la lógica formal y varios cálculos computacionales que fue descubierta por primera vez por Haskell Curry y . ​ (es)
  • カリー=ハワード同型対応(カリー=ハワードどうけいたいおう、英語: Curry–Howard correspondence)とは、と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム=証明」(proofs-as-programs)・「型=命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種()と関係している。 (ja)
  • 논리학에서 커리-하워드 대응(Curry-Howard correspondence) 또는 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 하스켈 커리와 (William Alvin Howard)에 의해 소개된 개념이다. 정확히 말하면 커리-하워드 대응은 논리의 (proof calculus)과 컴퓨터의 형 체계(type system)가 대응된다는 진술이다. 예를 들어 (Hilbert system)와 (combinatory logic)가, 자연 연역과 람다 계산이 대응된다. 본래 컴퓨터는 구성적인 과정만을 수행가능하기 때문에 증명이 온전히 구성적인 직관 논리에 있어서만 성립하는 것으로서 여겨졌으나 최근에 들어서는 고전 논리에서만 성립하는 비구성적인 개념들은 continuation과 대응됨이 알려졌다. (ko)
  • O isomorfismo de Curry–Howard é uma relação direta entre programas de computador e provas matemáticas. Também conhecido como correspondência de Curry–Howard, correspondência provas-como-programas, e correspondência fórmulas-como-tipos, ele se refere à generalização de uma analogia sintática entre sistemas de lógica formal e cálculos computacionais que foi descoberto pela primeira vez pelo matemático americano Haskell Curry e o lógico William Alvin Howard. (pt)
  • Izomorfizm Curry’ego-Howarda – określenie odpowiedniości pomiędzy termami rachunku lambda z typami a dowodami logiki intuicjonistycznej. Odpowiedniość ta pozwala na wyrażanie dowodów twierdzeń jako funkcji, co stało się podstawą dla licznych opartych na logice intuicjonistycznej, takich, jak np. . (pl)
  • 柯里-霍華德对应(英語:Curry-Howard correspondence)是在计算机程序和数学证明之间的紧密联系;这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算(computational calculus)之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德(William Alvin Howard)独立发现的。 (zh)
  • In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs. (en)
  • La correspondance de Curry-Howard, appelée également isomorphisme de Curry-de Bruijn-Howard, correspondance preuve/programme ou correspondance formule/type, est une série de résultats à la frontière entre la logique mathématique, l'informatique théorique et la théorie de la calculabilité. Ils établissent des relations entre les démonstrations formelles d'un système logique et les programmes d'un modèle de calcul. Les premiers exemples de correspondance de Curry-Howard remontent à 1958, lorsque Haskell Curry remarqua l'analogie formelle entre les démonstrations des systèmes à la Hilbert et la logique combinatoire, puis à 1969, quand William Alvin Howard remarqua que les démonstrations en déduction naturelle intuitionniste pouvaient formellement se voir comme des termes du lambda-calcul typé (fr)
  • Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями. Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами. (ru)
  • Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями. У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні: (uk)
rdfs:label
  • Correspondència Curry-Howard (ca)
  • Curryho–Howardův isomorfismus (cs)
  • Curry-Howard-Isomorphismus (de)
  • Correspondencia de Curry-Howard (es)
  • Curry–Howard correspondence (en)
  • Correspondance de Curry-Howard (fr)
  • カリー=ハワード同型対応 (ja)
  • 커리-하워드 대응 (ko)
  • Izomorfizm Curry’ego-Howarda (pl)
  • Isomorfismo de Curry-Howard (pt)
  • Соответствие Карри — Ховарда (ru)
  • Відповідність Каррі — Говарда (uk)
  • 柯里-霍华德同构 (zh)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License