| 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)
|
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)