Curry–Howard-izomorfizmus

	Rmilan907/próbalap
	Sablon; Wikidata; Segítség;

A programozási nyelvek és a bizonyítások elméletében a Curry–Howard-izomorfizmus, -ekvivalencia vagy -korreszpondencia direkt összefüggést ír le számítógépes programok és matematikai bizonyítások között.

Haskell Brooks Curry és William Alvin Howard munkája szintaktikus analógiát fedezett fel formális logikai rendszerek és számítási kalkulusok között, a korreszpondenciát először pedig Howard egy 1980-ban megjelent kutatásában fejtette ki.^[1]^[2] Habár az izomorfizmust erről a két kutatóról nevezték el, a mögöttes elv kapcsolódik az intuicionista logika operatív értelmezéséhez, amelyet Luitzen Egbertus Jan Brouwer, Arend Heyting és Andrej Nyikolajevics Kolmogorov, (ezt általánosan Brouwer–Heyting–Kolmogorov-interpretációnak nevezzük) továbbá Stephen Kleene dolgozott ki különböző formákban.^[3] A korreszpondenciát később kiterjesztették, hogy tartalmazza a kategóriaelméletet, ezt a hármas összefüggést Curry–Howard–Lambek-izomorfizmusnak hívjuk.^[4]^[5]^[6]

Eredete, hatálya és következményei

A Curry–Howard-izomorfizmus létrejötte számos, 1934 és 1969 közötti észrevételen alapszik. 1934-ben Curry megfigyelte, hogy a kombinátorok típusai az intuicionista implikációs logikában axiómatikus felépítésekként értelmezhetőek.^[7]

Jegyzetek

↑ Gert Smolka, Jan Schwinghammer: Lecture Notes in Semandics. Saarland University
↑ Howard, William A..szerk.: Seldin, Jonathan P.; Hindley, J. Roger: The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 479–490. o. (1980. szeptember 1.). ISBN 978-0-12-349050-6
↑ Kennedy, Juliette; Kossak, Roman. Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies, 161. o. (2011). ISBN 978-1-107-00804-5
↑ Casadio, Claudia; Scott, Philip J.. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer, 184. o. (2021). ISBN 978-3-030-66545-6
↑ Coecke, Bob; Kissinger, Aleks. Picturing Quantum Processes. Cambridge University Press, 82. o. (2017). ISBN 978-1-107-10422-8
↑ Computational trilogy. nLab . (Hozzáférés: 2023. október 29.)
↑ Curry, H B (1934. szeptember 20.). „Functionality in Combinatory Logic”. Proceedings of the National Academy of Sciences of the United States of America 20 (11), 584–90. o. DOI:10.1073/pnas.20.11.584. ISSN 0027-8424. PMID 16577644. PMC 1076489.

Fordítás

Ez a szócikk részben vagy egészben a Curry–Howard correspondence című angol Wikipédia-szócikk fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

Informatikaportál
Matematikaportál

Az átváltozás

Az átváltozás (Die Verwandlung) Franz Kafka egyik legismertebb novellája. 1912-ben keletkezett, azonban csak 1915-ben jelent meg.

A mű nyomtatásban körülbelül 70 oldal, így Kafka életében megjelent leghosszabb olyan műve, amit az író teljesnek tekintett. Először a német Die Weißen Blätter havilapban jelent meg 1915 októberében, könyvként pedig először 1915 decemberében került kiadásra a Der jüngste Tag sorozat részeként, Kurt Wolff szerkesztésében.^[1]

Jegyzetek

↑ Nitschke, Claudia (2008. január 1.). „Peter-André Alt, Franz Kafka. Der ewige Sohn. 2005”. Arbitrium 26 (1). DOI:10.1515/arbi.2008.032. ISSN 0723-2977.

Források

További információk

Kapcsolódó szócikkek

Irodalomportál • összefoglaló, színes tartalomajánló lap

TO DO

Sokaságok
- konstrukciók kibővítése
- klasszifikáció
- általánosítás
Ising-modell start
- Történet befejezése (Onsager, Landau,...)
- Egy dimenziós eredmények
- Két dimenziós eredmények
Heisenberg-modell

Magamnak - fordítások

manifold with a boundary = peremes sokaság
chart = térkép
differentiable structure = sima/differenciálható struktúra
immersion, submersion = immerzió, szubmerzió
tangent space at point m = m-beli érintőtér/tangenstér; tangent vector = érintővektor/tangensvektor;
tangent bundle, vector bundle = tangensnyaláb, vektornyaláb
unit disk = egységkörlap

Jegyzetek

[1] Gert Smolka, Jan Schwinghammer: Lecture Notes in Semandics. Saarland University

[2] Howard, William A..szerk.: Seldin, Jonathan P.; Hindley, J. Roger: The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 479–490. o. (1980. szeptember 1.). ISBN 978-0-12-349050-6

[3] Kennedy, Juliette; Kossak, Roman. Set Theory, Arithmetic, and Foundations of Mathematics: Theorems, Philosophies, 161. o. (2011). ISBN 978-1-107-00804-5

[4] Casadio, Claudia; Scott, Philip J.. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Springer, 184. o. (2021). ISBN 978-3-030-66545-6

[Coecke_Kissinger_2017_p._82-5] Coecke, Bob; Kissinger, Aleks. Picturing Quantum Processes. Cambridge University Press, 82. o. (2017). ISBN 978-1-107-10422-8

[6] Computational trilogy. nLab . (Hozzáférés: 2023. október 29.)

[7] Curry, H B (1934. szeptember 20.). „Functionality in Combinatory Logic”. Proceedings of the National Academy of Sciences of the United States of America 20 (11), 584–90. o. DOI:10.1073/pnas.20.11.584. ISSN 0027-8424. PMID 16577644. PMC 1076489.

[8] Nitschke, Claudia (2008. január 1.). „Peter-André Alt, Franz Kafka. Der ewige Sohn. 2005”. Arbitrium 26 (1). DOI:10.1515/arbi.2008.032. ISSN 0723-2977.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[1]

Rmilan907/próbalap
Sablon Wikidata Segítség