Réalisabilité

La réalisabilité est une branche de la logique mathématique, et plus précisément de la théorie de la démonstration, qui définit une relation logique entre les formules d'un système logique et les programmes d'un modèle de calcul. Elle a été introduite dans les années 40 par Kleene comme une interprétation des formules de l'arithmétique de Heyting par des ensembles (d'indices) de fonctions récursives. Elle a depuis été étendue à toute sorte d'autres systèmes logiques, et aujourd'hui est vue comme une généralisation de la correspondance de Curry-Howard.

Étant donnés une formule et un programme on note la propriété «  réalise  » ; cette notation est réminiscente du forcing de Cohen avec lequel la réalisabilité présente des analogies formelles. La réalisabilité conduit à une interprétation des formules comme des spécifications de programme : par exemple la tautologie est réalisée par les programmes qui étant donné une entrée de type rendent un résultat de type .

Bibliographie

  • (en) S. C. Kleene, « On the interpretation of intuitionistic number theory », Journal of Symbolic Logic,‎
  • (en) Anne Troelstra, « Realizability », dans S. R. Buss, Handbook of proof theory, North Holland, (lire en ligne)
  • (en) Jaap van Oosten, « Realizability: an historical essay », Mathematical Structures in Computer Science,‎ (lire en ligne)

Read other articles:

SN 2006gy dan inti galaksi NGC 1260 SN 2006gy adalah sebuah supernova yang meledak sangat hebat, ditemukan pada 18 September 2006. Supernova SN 2006gy terjadi pada sebuah galaksi jauh (NGC 1260) berjarak sekitar 238 juta tahun cahaya. Indikasi awal menunjukkan bahwa dia adalah supernova berenergi tinggi yang tidak biasa dan berasal dari sebuah bintang bermassa 150 kali Matahari, kemungkinan sebuah tipe yang dirujuk sebagai supernova ketidakstabilan pasangan.[1] Sebuah supernova ketida...

 

Jagoan SilatGenre Drama Roman Fantasi Laga PembuatMD EntertainmentTerinspirasi olehKung Fu Pandaoleh Mark Osborne & John StevensonDitulis olehDono IndartoSkenarioDono IndartoSutradaraAi ManafPemeran Tommy Kaganangan Thoriq Hafidz Nana Mirdad Niken Anjani Lian Firman Bemby Putuanda Barry Prima George Rudy Ria Irawan Adi Pawitra Marsha Aruan Bintang Elian Nona Laboni Daniel Shivael Abthal Adams Timothy Fidealdo Argo Jimmy Oma Kucrut Amanda Rawles Bella Shania Samantha Dressler Ricky Martin...

 

  رواندا (بالإيطالية: Ruanda)‏  روانداعلم رواندا  روانداشعار رواندا    الشعار الوطني(بالروندية: Ubumwe, Umurimo, Gukunda Igihugu)‏  النشيد: الأرض والسكان إحداثيات 2°S 30°E / 2°S 30°E / -2; 30   [1] أعلى قمة جبل كاريسيمبي  [لغات أخرى]‏  أخفض نقطة نهر روزيزي (950 ...

Sega Game GearPembuatSegaJenisHandheld game consoleGenerasiFourth generationKetersediaan eceranHarga perkenalanUS$150Dihentikan1997Terjual11 million[1]MediaCartridgeCPUZilog Z80 clocked at 3.58MHzMemori8KB RAM, 16KB VRAMTampilan160x144 pixel resolution, 32 on-screen colours out of a palette of 4096Dimensi209 x 111 x 37 mmBerat~400gPenerusSega Nomad Sega Game Gear (ゲームギアcode: ja is deprecated , Gēmu Gia) merupakan konsol Game portabel pertama dari Sega, konsol ini merupakan ...

 

Overview of the presence, role and impact of Hinduism in Australia Australian HindusHindu Temple in Melbourne.Total population 684,002 (2021) 2.7% of the Australian population[1]Regions with significant populationsSydneyCanberraMelbourneAdelaidePerthBrisbaneLanguagesEnglish, Tamil, Fiji Hindi, Nepali,Mauritian Creole, Indian languagesRelated ethnic groupsIndian Australians Historical populationYearPop.±% p.a.1911 414—    1933 212−3.00%1986 21,500+9.11%1991 43,...

 

イスラームにおける結婚(イスラームにおけるけっこん)とは、二者の間で行われる法的な契約である。新郎新婦は自身の自由な意思で結婚に同意する。口頭または紙面での規則に従った拘束的な契約は、イスラームの結婚で不可欠だと考えられており、新郎と新婦の権利と責任の概要を示している[1]。イスラームにおける離婚は様々な形をとることができ、個�...

Russian footballer In this name that follows Eastern Slavic naming customs, the patronymic is Inalbekovich and the family name is Mamtov. Khasan Mamtov Mamtov with Tyumen in 2016Personal informationFull name Khasan Inalbekovich MamtovDate of birth (1984-04-28) 28 April 1984 (age 40)Place of birth Besleney, Russian SFSRHeight 1.81 m (5 ft 11 in)Position(s) ForwardSenior career*Years Team Apps (Gls)2002–2003 FC Nart Cherkessk 65 (5)2004–2005 FC Dynamo Stavropol 23 (1...

 

此条目序言章节没有充分总结全文内容要点。 (2019年3月21日)请考虑扩充序言,清晰概述条目所有重點。请在条目的讨论页讨论此问题。 哈萨克斯坦總統哈薩克總統旗現任Қасым-Жомарт Кемелұлы Тоқаев卡瑟姆若马尔特·托卡耶夫自2019年3月20日在任任期7年首任努尔苏丹·纳扎尔巴耶夫设立1990年4月24日(哈薩克蘇維埃社會主義共和國總統) 哈萨克斯坦 哈萨克斯坦政府...

 

Polish actress and model (born 1976) Agata BuzekAgata Buzek, 2018BornAgata Bronisława Buzek (1976-09-20) 20 September 1976 (age 47)Pyskowice, PolandOccupation(s)Actress, modelYears active1998–presentSpouse Adam Mazan ​(m. 2006)​Parent(s)Jerzy BuzekLudgarda Buzek Agata Bronisława Buzek (born 20 September 1976) is a Polish actress and model. Agata, the daughter of Polish politician, former Prime Minister of Poland and President of the European Parliame...

Area of land where little precipitation occurs Not to be confused with dessert. This article is about dry terrain. For arid climate, see desert climate. For the act of abandoning or withdrawing support, see desertion. For other uses, see Desert (disambiguation). Sand and dunes of the Libyan Desert Valle de la Luna (Moon Valley) in the Atacama Desert of Chile, the world's driest non-polar desert A desert is a landscape where little precipitation occurs and, consequently, living conditions crea...

 

Negara bagian Assam dalam peta India. Banjir Assam 2016 merupakan banjir yang disebabkan oleh hujan lebat di negarabagian India, Assam, selama Juli 2016. Banjir tersebut berdampak kepada 1,8 juta penduduk dan membanjiri Taman Nasional Kaziranga.[1] Sejak 1 Agustus 2016, 28 orang tewas dalam bencana tersebut menurut sebuah laporan dari Otoritas Manajemen Bencana Negara Bagian.[2] Asal banjir Negara bagian utara India mengalami hujan lebat sejak bulan Juli 2016. Assam memperoleh...

 

Halaman artikel ini diterjemahkan, sebagian atau seluruhnya, dari halaman di (Tolong cantumkan kode bahasa Wiki sumber terjemahan) yang berjudul (Tolong cantumkan nama artikel sumber terjemahan). Lihat pula [{{localurle:{{{1}}}:|oldid=&action=history}} sejarah suntingan halaman aslinya] untuk melihat daftar penulisnya. Yang Berhormat DatukArmizan Mohd AliPGDK ADK JP, APارميزان محمد علي Menteri di Sekretariat Perdana Menteri (Bid. Sabah dan Sarawak)PetahanaMulai menjabat ...

This article is about the former Australian rules football club. For the present-day VAFA club, see Brunswick Football Club (1963). For the association football (soccer) clubs, see Brunswick SC. For the 19th-century Scottish association football club, see Brunswick F.C. Former Australian rules football club Australian rules football club BrunswickNamesFull nameBrunswick Football Club Brunswick-Broadmeadows Football Club (1989–91)Nickname(s)Pottery Workers, Brickfielders, Magpies, Wicks, Wic...

 

Disambiguation link for various Greek mythological figures Not to be confused with Menoeceus. For the moon, see 617 Patroclus. Greek deitiesseries Primordial deities Titans Olympians Water deities Chthonic deities Personified concepts Titans The Twelve Titans Oceanus and Tethys, Hyperion and Theia, Coeus and Phoebe, Cronus and Rhea, Mnemosyne and Themis, Crius and Iapetus Children of Cronus Zeus, Hera, Poseidon, Hades, Hestia, Demeter, Chiron Children of Oceanus Oceanids, Potamoi Children of ...

 

Incontro con RamaTitolo originaleRendezvous with Rama AutoreArthur C. Clarke 1ª ed. originale1973 1ª ed. italiana1973 Genereromanzo Sottogenerefantascienza hard Lingua originaleinglese SerieSerie di Rama Seguito daRama II Modifica dati su Wikidata · Manuale Incontro con Rama (titolo originale Rendezvous with Rama) è un romanzo di fantascienza scritto da Arthur C. Clarke, pubblicato nel 1972. L'opera è considerata uno tra i migliori esempi di fantascienza hard grazie alla cura maniac...

Australian politician William Timothy Cape was an early school master in Sydney, Australia William Timothy Cape (25 October 1806 – 4 June 1863) was an early school master in Sydney, Australia; several of the Premiers of New South Wales attended his school. Cape was born at Walworth, Surrey, England, the son of William Cape, a London bank manager who emigrated to Australia with his family in 1821. Cape senior became master of a private school, the Sydney Academy, at the end of 1822 and died ...

 

大衛·歐提茲David Ortiz2007年的歐提茲指定打擊/一壘手出生: (1975-11-18) 1975年11月18日(48歲) 多米尼加國家特區聖多明哥 打擊:左 投球:左 美國職棒大聯盟首秀1997年9月2日,代表明尼蘇達雙城最終美國職棒大聯盟出场2016年10月2日,代表波士頓紅襪美國職棒大聯盟成績打擊率.286安打2472全壘打541打點1768 球队 明尼蘇達雙城(1997年–2002年) 波士頓紅襪(2003年–2016年) 生�...

 

Electoral district for the House of Representatives of the Philippines Congressional districts of the Philippines By district By provinceCategoryElectoral districtLocationPhilippinesNumber253 (as of 2020)Populations18,831–1,207,509Areas4.08–7,725.90 km2 (1.58–2,982.99 sq mi)GovernmentCongress of the Philippines Congressional districts of the Philippines (Filipino: distritong pangkapulungan) refers to the electoral districts or constituencies in which the country is divide...

Основная статья: Экономика Республики Беларусь Основные отрасли промышленности Белоруссии — машиностроение, электроэнергетика и металлообработка, добыча калийной соли, химическая и нефтехимическая промышленность, лесная и деревообрабатывающая, лёгкая и пищевая п...

 

Gunta StölzlBorn(1897-03-05)5 March 1897Munich, German EmpireDied22 April 1983(1983-04-22) (aged 86)Zurich, SwitzerlandNationalitySwissKnown forWeavingSpouse(s)1929-36 Arieh Sharon (1900-84)1942-83 Willy Stadler (1901–90)ChildrenYael Aloni (with Sharon)Monika Stadler (with Stadler) Gunta Stölzl (5 March 1897 – 22 April 1983) was a German textile artist who played a fundamental role in the development of the Bauhaus school's weaving workshop, where she created enormous chan...