This HTML5 document contains 255 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbthttp://dbpedia.org/resource/Template:
n14http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/
wikipedia-enhttp://en.wikipedia.org/wiki/
n25http://jigpal.oxfordjournals.org/cgi/content/abstract/9/5/
dbrhttp://dbpedia.org/resource/
n40https://web.archive.org/web/20080418044121/http:/www.monad.me.uk/stable/
dbpedia-frhttp://fr.dbpedia.org/resource/
n31https://academic.oup.com/jigpal/article-abstract/3/2-3/243/
dctermshttp://purl.org/dc/terms/
n21http://alexandria.tue.nl/repository/freearticles/
rdfshttp://www.w3.org/2000/01/rdf-schema#
dbpedia-cshttp://cs.dbpedia.org/resource/
n11http://www3.interscience.wiley.com/journal/119262585/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n29http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/
dbphttp://dbpedia.org/property/
n41https://web.archive.org/web/20080819185521/http:/www.thenewsh.com/~newsham/formal/curryhoward/
xsdhhttp://www.w3.org/2001/XMLSchema#
n23https://www.cs.cmu.edu/~crary/819-f09/
dbpedia-ukhttp://uk.dbpedia.org/resource/
dbohttp://dbpedia.org/ontology/
n44https://www.amazon.com/PROGRAM-PROOF-Samuel-Mimram/dp/
n22https://books.google.com/
dbpedia-pthttp://pt.dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/
dbchttp://dbpedia.org/resource/Category:
n39http://www.haskell.org/wikiupload/1/14/
dbpedia-dehttp://de.dbpedia.org/resource/
dbpedia-plhttp://pl.dbpedia.org/resource/
dbpedia-ruhttp://ru.dbpedia.org/resource/
wikidatahttp://www.wikidata.org/entity/
n7http://www.site.uottawa.ca/~afelty/dist/
goldhttp://purl.org/linguistics/gold/
n18https://global.dbpedia.org/id/
n27http://wadler.blogspot.com/2014/08/
dbpedia-cahttp://ca.dbpedia.org/resource/
n30http://www.monad.me.uk/stable/
provhttp://www.w3.org/ns/prov#
foafhttp://xmlns.com/foaf/0.1/
n4https://www.springer.com/philosophy/logic/book/
dbpedia-zhhttp://zh.dbpedia.org/resource/
dbpedia-kohttp://ko.dbpedia.org/resource/
dbpedia-eshttp://es.dbpedia.org/resource/
freebasehttp://rdf.freebase.com/ns/
owlhttp://www.w3.org/2002/07/owl#

Statements

Subject Item
dbr:Curry–Howard_correspondence
rdf:type
dbo:Person owl:Thing
rdfs:label
커리-하워드 대응 Correspondance de Curry-Howard Соответствие Карри — Ховарда Isomorfismo de Curry-Howard Відповідність Каррі — Говарда Curry-Howard-Isomorphismus Correspondencia de Curry-Howard Izomorfizm Curry’ego-Howarda Curryho–Howardův isomorfismus 柯里-霍华德同构 Curry–Howard correspondence Correspondència Curry-Howard カリー＝ハワード同型対応
rdfs:comment
Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями. У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні: Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями. Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами. 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. . 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. 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é 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 . ​ 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. 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 . 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í. カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（）と関係している。 柯里-霍華德对应（英語：Curry-Howard correspondence）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德（William Alvin Howard）独立发现的。 논리학에서 커리-하워드 대응(Curry-Howard correspondence) 또는 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 하스켈 커리와 (William Alvin Howard)에 의해 소개된 개념이다. 정확히 말하면 커리-하워드 대응은 논리의 (proof calculus)과 컴퓨터의 형 체계(type system)가 대응된다는 진술이다. 예를 들어 (Hilbert system)와 (combinatory logic)가, 자연 연역과 람다 계산이 대응된다. 본래 컴퓨터는 구성적인 과정만을 수행가능하기 때문에 증명이 온전히 구성적인 직관 논리에 있어서만 성립하는 것으로서 여겨졌으나 최근에 들어서는 고전 논리에서만 성립하는 비구성적인 개념들은 continuation과 대응됨이 알려졌다. 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.
dcterms:subject
dbc:Proof_theory dbc:Type_theory dbc:1934_in_computing dbc:1958_in_computing dbc:Dependently_typed_programming dbc:Philosophy_of_computer_science dbc:1969_in_computing dbc:Logic_in_computer_science
dbo:wikiPageID
254299
dbo:wikiPageRevisionID
1113758743
dbo:wikiPageWikiLink
dbr:Linear_type_system dbr:Typed_lambda_calculus dbr:Dag_Prawitz dbr:Deduction_theorem dbr:INRIA dbr:Axiom-scheme dbr:Springer_Science+Business_Media dbr:Type_systems dbc:Proof_theory dbr:Relevant_logic dbr:Elsevier_Science dbr:Double-negation_translation dbr:Apply dbr:Product_type dbr:Proof_theory dbr:Natural_deduction dbr:Turing_machine dbr:Automath dbr:Dialectica_interpretation dbr:Identity_type dbr:Georg_Kreisel dbr:Haskell_Curry dbr:Abstract_machine dbr:Lambda_calculus dbr:Kurt_Gödel dbr:Call-by-value dbr:Combinatory_logic dbr:Logician dbr:Kolmogorov dbr:Modal_logic dbr:Arend_Heyting dbr:Continuation dbr:Type_inhabitation_problem dbr:Simply_typed_lambda_calculus dbr:Model_of_computation dbr:Continuation-passing_style dbr:Program_correctness dbr:Implication_introduction dbr:Tautology_(logic) dbc:Type_theory dbr:Return_type dbr:L._E._J._Brouwer dbr:Stephen_Kleene dbr:Currying dbc:1934_in_computing dbr:Sum_type dbr:Realizability dbr:Formula_(mathematical_logic) dbr:Grothendieck_topology dbr:Hilbert-style_deduction_system dbr:Higher-order_logic dbr:Turing_completeness dbr:Programming_language dbr:BHK_interpretation dbr:Intuitionism dbr:Intuitionistic_logic dbr:Intuitionistic_type_theory dbr:Homotopy dbr:Univalence_axiom dbr:Typed_assembly_language dbr:Sequent_calculus dbr:Existential_quantification dbr:Category_theory dbr:Set_theory dbr:Monad_(functional_programming) dbr:Models_of_computation dbr:Proof_calculus dbr:Peirce's_law dbr:Evaluation_strategy dbr:William_Alvin_Howard dbr:Type_theory dbr:Unit_type dbr:Nicolaas_Govert_de_Bruijn dbr:Mathematician dbr:Classical_logic dbr:Internal_language dbc:1958_in_computing dbr:Dependent_type dbr:Mathematical_induction dbr:Corecursion dbr:Joachim_Lambek dbr:Recursion_(computer_science) dbr:Programming_language_theory dbr:Algebraic_data_type dbr:Logical_conjunction dbr:Logical_implication dbr:Logical_disjunction dbr:Martin-Löf dbr:Closed_monoidal_category dbr:Computer_program dbr:Oxford_University_Press dbr:Call-with-current-continuation dbr:Coq dbr:Stephen_Cole_Kleene dbr:Gentzen dbr:System_F dbr:Cobordism dbr:Functional_programming_language dbr:Total_functional_programming dbr:String_theory dbr:Thierry_Coquand dbr:Normalization_property_(lambda-calculus) dbc:Dependently_typed_programming dbr:Data_type dbr:Calculus_of_structures dbr:Categorical_logic dbr:Elsevier dbr:Implication_elimination dbr:Analogy dbr:Call-by-name dbr:Bottom_type dbr:Function_type dbr:Formal_system dbr:Axiom_scheme dbr:Proof_net dbr:Mathematical_proof dbc:Philosophy_of_computer_science dbr:Universal_quantification dbr:Cartesian_closed_categories dbr:Springer-Verlag dbc:1969_in_computing dbr:Axiom_of_choice dbr:Andrey_Kolmogorov dbr:Typing_rule dbr:Hypotheses dbr:Linear_logic dbr:Genetic_programming dbr:Sequent dbr:Terminal_object dbr:Principal_type dbr:Unifying_theories_in_mathematics dbr:Modus_ponens dbr:Calculus_of_Constructions dbc:Logic_in_computer_science dbr:Lambda-mu_calculus dbr:Intuitionistic dbr:Turing-complete dbr:Logic_programming dbr:Brouwer–Heyting–Kolmogorov_interpretation dbr:Academic_Press dbr:Inference_rules dbr:Homotopy_type_theory dbr:Proof-carrying_code
dbo:wikiPageExternalLink
n4:978-0-7923-5687-5 n7:gecco08.pdf n11:abstract%3FCRETRY=1&SRETRY=0 n14:propositions-as-types.pdf%7C n21:597627.pdf n22:books%3Fid=TLHfQPHNs0QC n23:Howard80.pdf n25:693 n27:howard-on-curry-howard.html n29: n30:Proofs+Types.html n31:2897783 n22:books%3Fid=aFO6CgAAQBAJ n39:TMR-Issue6.pdf n40:Proofs+Types.html n41: n44:B08C97TD9G
owl:sameAs
dbpedia-fr:Correspondance_de_Curry-Howard dbpedia-cs:Curryho–Howardův_isomorfismus dbpedia-zh:柯里-霍华德同构 n18:577HP dbpedia-ko:커리-하워드_대응 dbpedia-es:Correspondencia_de_Curry-Howard dbpedia-uk:Відповідність_Каррі_—_Говарда dbpedia-ja:カリー＝ハワード同型対応 dbpedia-ru:Соответствие_Карри_—_Ховарда dbpedia-pt:Isomorfismo_de_Curry-Howard dbpedia-ca:Correspondència_Curry-Howard dbpedia-pl:Izomorfizm_Curry’ego-Howarda freebase:m.01lqbf wikidata:Q975734 dbpedia-de:Curry-Howard-Isomorphismus
dbp:wikiPageUsesTemplate
dbt:Sidebar dbt:Short_description dbt:Wikibooks dbt:Citation dbt:As_of dbt:Mvar dbt:Math dbt:Code dbt:More_footnotes dbt:Harvnb dbt:Reflist dbt:Dead_link dbt:Cite_book dbt:Cite_journal dbt:Authority_control dbt:Sfn
dbp:bot
InternetArchiveBot
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 . plus_comm = fun n m : nat => nat_ind n : forall n m : nat, n + m = m + n
dbp:date
October 2022
dbp:fixAttempted
yes
dbp:style
width:30em;
dbp:title
A proof written as a functional program
dbp:contentstyle
text-align: left;
dbo:abstract
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. 柯里-霍華德对应（英語：Curry-Howard correspondence）是在计算机程序和数学证明之间的紧密联系；这种对应也叫做柯里-霍華德同构、公式为类型对应或命题为类型对应。这是对形式逻辑系统和公式计算（computational calculus）之间符号的相似性的推广。它被认为是由美国数学家哈斯凯尔·柯里和逻辑学家威廉·阿尔文·霍瓦德（William Alvin Howard）独立发现的。 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 . ​ カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（）と関係している。 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í. 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. 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. Соответствие Карри — Ховарда (изоморфизм Карри — Ховарда, англ. formulæ-as-types interpretation) — наблюдаемая структурная эквивалентность между математическими доказательствами и программами, которая может быть формализована в виде изоморфизма между логическими системами и типизированными исчислениями. Хаскелл Карри и заметили, что построение конструктивного доказательства похоже на описание вычислений, а высказывания конструктивной логики по своей структуре схожи с типами вычисляемых выражений — программ для вычислительной машины. Ранние проявления этой связи — (1925), задающая семантику интуиционистской логики через вычисления доказательств, и теория Клини (1945). Соответствие Карри — Ховарда в современном представлении не ограничивается какой-то одной логикой или системой типов. Например, логика высказываний соответствует простому типизированному λ-исчислению, — полиморфному λ-исчислению, исчисление предикатов — λ-исчислению с зависимыми типами. В рамках изоморфизма Карри — Ховарда следующие структурные элементы рассматриваются как эквивалентные: Простейшим примером соответствия Карри — Ховарда может служить изоморфизм между простым типизированным λ-исчислением и фрагментом интуиционистской логики высказываний, включающим только импликацию. Например, тип в простом типизированном лямбда-исчислении соответствует высказыванию логики высказываний. Для доказательства этого высказывания необходимо сконструировать терм указанного типа (если это удаётся сделать, то про тип говорят, что он обитаем или населён), в данном случае можно предъявить нужный терм: , и это значит, что тавтология доказана. Использование изоморфизма Карри — Ховарда позволило создать целый класс функциональных языков программирования, среда выполнения которых одновременно является системой автоматического доказательства, таких как Coq, Agda и . 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. 논리학에서 커리-하워드 대응(Curry-Howard correspondence) 또는 커리-하워드 동형(Curry-Howard isomorphism)은 컴퓨터 프로그램과 논리적 증명을 직접적으로 연관시키는 대응 관계이다. 하스켈 커리와 (William Alvin Howard)에 의해 소개된 개념이다. 정확히 말하면 커리-하워드 대응은 논리의 (proof calculus)과 컴퓨터의 형 체계(type system)가 대응된다는 진술이다. 예를 들어 (Hilbert system)와 (combinatory logic)가, 자연 연역과 람다 계산이 대응된다. 본래 컴퓨터는 구성적인 과정만을 수행가능하기 때문에 증명이 온전히 구성적인 직관 논리에 있어서만 성립하는 것으로서 여겨졌으나 최근에 들어서는 고전 논리에서만 성립하는 비구성적인 개념들은 continuation과 대응됨이 알려졌다. Відповідність Каррі — Говарда (ізоморфізм Каррі — Говарда, англ. Curry-Howard Isomorphism) — теорема, або точніше ряд теорем, що показують структурну еквівалентність між математичними доведеннями та програмами, або обчисленнями англ. computations. Ця еквівалентність може бути формалізована у вигляді ізоморфізму між логічними системами і типізованими лямбда-численнями. Хаскелл Каррі і Вільям Говард помітили, що конструктивне доведення (тобто, доведення в інтуїціоністській логіці) схожа на програму, яка обчислює висновок, а саме висловлювання конструктивної логіки за своєю структурою схожі з типами виразів лямбда-числення — програм для обчислювальної машини. Відповідність Каррі — Говарда не обмежується якоюсь однією логікою або системою типів. Наприклад, інтуїционістське числення висловлювань відповідає простому типізованому λ-численню, логіка висловлювань другого порядку — поліморфному λ-численню, числення предикатів — λ-численню з залежними типами. У рамках ізоморфізму Каррі — Говарда наступні структурні елементи розглядаються як еквівалентні: Найпростішим прикладом відповідності Каррі — Говарда може служити ізоморфізм між простим типізованим -обчисленням і фрагментом інтуїціоністської логіки висловлювань, що включає тільки імплікації. Наприклад, тип в простому типізованому лямбда-численні відповідає вислову логіки висловлювань. Для доказу цього висловлювання необхідно сконструювати терм зазначеного типу (якщо це вдається зробити, то про тип кажуть, що він населений), в даному випадку можна пред'явити потрібний терм:, і це означає, що тавтологія доведена. Використання ізоморфізму Каррі — Говарда дозволило створити цілий клас функціональних мов програмування, середовище виконання яких одночасно є системою автоматичного доказу, таких як Coq, Agda і Epigram (англ.). 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 . 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. .
dbp:belowstyle
text-align: left
gold:hypernym
dbr:Relationship
prov:wasDerivedFrom
wikipedia-en:Curry–Howard_correspondence?oldid=1113758743&ns=0
dbo:wikiPageLength
56632
foaf:isPrimaryTopicOf
wikipedia-en:Curry–Howard_correspondence